RESQ_MATCH_MP : (thm -> thm -> thm)
STRUCTURE
res_quanTools
SYNOPSIS
Eliminating a restricted universal quantification with automatic matching.
DESCRIPTION
When applied to theorems A1 |- !x::P. Q[x] and A2 |- P x', the derived inference rule RESQ_MATCH_MP matches x' to x by instantiating free or universally quantified variables in the first theorem (only), and returns a theorem A1 u A2 |- Q[x'/x]. Polymorphic types are also instantiated if necessary. 

    A1 |- !x::P.Q[x]   A2 |- P x'
   --------------------------------------  RESQ_MATCH_MP
          A1 u A2 |- Q[x'/x]
FAILURE
Fails unless the first theorem is a (possibly repeatedly) restricted universal quantification whose quantified variable can be instantiated to match the conclusion of the second theorem, without instantiating any variables which are free in A1, the first theorem’s assumption list.
SEEALSO
MATCH_MP, RESQ_HALF_SPEC
HOL  Kananaskis-10