----------------------------------------------------------------------
RES_FORALL_AND_CONV                                    (res_quanTools)
----------------------------------------------------------------------
RES_FORALL_AND_CONV : conv

SYNOPSIS
Splits a restricted universal quantification across a conjunction.

KEYWORDS
conversion, restricted quantifier, universal.

DESCRIBE
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}.

----------------------------------------------------------------------