minor wibble
got rid of mk_equiv_rule

it was actually useless now that formulas are term: rewrite rules can
act as cheap equiv rules.
WF: no lvar should appear in a matching position

added checks that lvars do not appear in goals in sequent schemas, and
"to" patterns in rewrite schemas
better smt_implies
new default rule: lvar_instantiate_rule

lvar_instantiate_rule takes equalities of the form _x = e on the RHS
(where _x doesn't appear on the LHS) and adds them to the LHS.

This seems to adequately (for now) replace abduce_instance_rule,
although more rules such as a proper match_subformula_rule would be
useful for completeness.