IMP_RES_FORALL_CONV : conv
STRUCTURE
res_quanLib
SYNOPSIS
Converts an implication to a restricted universal quantification.
DESCRIPTION
When applied to a term of the form !x. x IN P ==> Q, the conversion IMP_RES_FORALL_CONV returns the theorem: 
   |- (!x. x IN P ==> Q) = !x::P. Q
FAILURE
Fails if applied to a term not of the form !x. x IN P ==> Q.
SEEALSO
RES_FORALL_CONV
HOL  Trindemossen-1