`match` strategy working with axioms and arbitrary formulas

[h0nzZik]

I propose that

1. a variant of match would take an AxiomOrClaimName for the pattern that is used as LHS;
2. match would work on arbitrary patterns (in the spirit of syntacticMatch). That should not break correctness (since, e.g., phi(1)/\psi(2) --> \exists x. psi(x) /\ phi(1)), but the strategy would be more general. Moreover, it would allow us to remove the fail cases where a checks isPredicatePattern and isSpatialPattern are used, since a spatial pattern together with predicate pattern would not match. (I belive that removal of one case of isSpatialPattern is a good thing, since it is SL-specific.)

---

Also, filterPredicates is defined but never used, so we may remove it.