only pattern vars can be matched in [find_pattern_matches]
Debug.prof_fun5 and Debug.prof_fun6

this might be getting out of hands... oh, well, let's worry when we get
to prof_fun1000.
added Syntax.symbol_equal

strangely missing from Z3 bindings
{hash,}{set,map} facilities for sorts in Syntax

as we already have for expressions.
allow polymorphic sorts in patterns

Some user rules are naturally written for several sorts at a time. For
instance, the following simplification rule ought to be common:

rewrite not_equal:
  not ('a ?x = 'a ?y) -> 'a ?x != 'a ?y
;

(this changes (not (eq ?x ?y)) into (distinct ?x ?y) for, eg,
normalisation purposes)

One solution is to write one such pattern for each possible sort, but
that's not very efficient, as one quickly gets many rules instead of a
few. Another solution, implemented here, is to make coreStar aware of
polymorphic sorts in patterns.