When given a theorem A' |- t and a goal A ?- t' where t can be matched
to t' by instantiating variables which are either free or
universally quantified at the outer level, including appropriate type
instantiation, MATCH_ACCEPT_TAC completely solves the goal.
Unless A' is a subset of A, this is an invalid tactic.
A ?- t'
========= MATCH_ACCEPT_TAC (A' |- t)