\DOC AND_EXISTS_CONV

\TYPE {AND_EXISTS_CONV : conv}

\SYNOPSIS
Moves an existential quantification outwards through a conjunction.

\KEYWORDS
conversion, quantifier.

\DESCRIBE
When applied to a term of the form {(?x.P) /\ (?x.Q)}, where {x} is free
in neither {P} nor {Q}, {AND_EXISTS_CONV} returns the theorem:
{
   |- (?x. P) /\ (?x. Q) = (?x. P /\ Q)
}


\FAILURE
{AND_EXISTS_CONV} fails if it is applied to a term not of the form
{(?x.P) /\ (?x.Q)}, or if it is applied to a term {(?x.P) /\ (?x.Q)}
in which the variable {x} is free in either {P} or {Q}.

\COMMENTS
It may be easier to use higher order rewriting with some of
{BOTH_EXISTS_AND_THM}, {LEFT_EXISTS_AND_THM}, and
{RIGHT_EXISTS_AND_THM}.



\SEEALSO
Conv.EXISTS_AND_CONV, Conv.LEFT_AND_EXISTS_CONV, Conv.RIGHT_AND_EXISTS_CONV.

\ENDDOC