AND_EXISTS_CONV : conv

- STRUCTURE
- SYNOPSIS
- 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.
- SEEALSO

HOL Kananaskis-14