IMP_RES_FORALL_CONV
res_quanLib.IMP_RES_FORALL_CONV : conv
Converts an implication to a restricted universal quantification.
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.