When applied to a theorem of the form
PMATCH_MP_TAC produces a tactic that reduces a goal whose
conclusion t' is a substitution and/or type instance of t to the
corresponding instance of s. Any variables free in s but not in t will
be existentially quantified in the resulting subgoal:
A' |- !p1...pn. s ==> !q1...qm. t
where w1, ..., wp are (type instances of) those pairs among
p1, ..., pn having variables that do not occur free in t.
Note that this is not a valid tactic unless A' is a subset of A.
A ?- !u1...ui. t'
====================== PMATCH_MP_TAC (A' |- !p1...pn. s ==> !q1...qm. t)
A ?- ?w1...wp. s'