When applied to a theorem of the form
MATCH_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' |- !x1...xn. s ==> !y1...ym. t
where z1, ..., zp are (type instances of) those variables among
x1, ..., xn that do not occur free in t. Note that this is not a
valid tactic unless A' is a subset of A.
A ?- !v1...vi. t'
====================== MATCH_MP_TAC (A' |- !x1...xn. s ==> !y1...ym. t)
A ?- ?z1...zp. s'