RES_FORALL_AND_CONV : conv
STRUCTURE
res_quanLib
SYNOPSIS
Splits a restricted universal quantification across a conjunction.
DESCRIPTION
When applied to a term of the form !x::P. Q /\ R, the conversion RES_FORALL_AND_CONV returns the theorem: 
   |- (!x::P. Q /\ R) = ((!x::P. Q) /\ (!x::P. R))
FAILURE
Fails if applied to a term not of the form !x::P. Q /\ R.
HOL  Kananaskis-14