Moves an existential quantification outwards through a conjunction.
DESCRIPTION
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.