Prover.abduce_instance_rule throws rule_not_applicable more often
minor optimisation

it's better to use Syntax.mk_big_star instead of Prover.mk_big_star when
there is nothing to "optimise" in the expression.
non-exponential pattern matching

It comes at a price (which could be mitigated by re-implementing some of
what I've removed). Please yell if this stuff was necessary:

- patterns and concrete expressions have to not start with disjunctions
  (so only * or straight to "atoms")
- patterns are allowed at most one occurrence of a ?f formula variable