EXISTS_AND_REORDER_CONV : conv
STRUCTURE
Conv
SYNOPSIS
Moves an existential quantification inwards through a conjunction, sorting the body.
DESCRIPTION
When applied to a term of the form ?x. c1 /\ c2 /\ .. /\ cn, where x is not free in at least one of the conjuncts ci, then EXISTS_AND_REORDER_CONV returns a theorem of the form 
   |- (?x. ...) = (ci /\ cj /\ ck /\ ...) /\ (?x. cm /\ cn /\ cp /\ ...)
where the conjuncts ci, cj and ck do not have the bound variable x free, and where the conjuncts cm, cn and cp do.
FAILURE
EXISTS_AND_REORDER_CONV fails if it is applied to a term that is not an existential. It raises UNCHANGED if the existential’s body is not a conjunction, or if the body does not have any conjuncts where the bound variable does not occur, or if none of the body’s conjuncts have free occurrences of the bound variable.
COMMENTS
The conjuncts in the resulting term are kept in the same relative order as in the input term, but will all be right-associated in the two groups (because they are re-assembled with list_mk_conj), possibly destroying structure that existed in the original.
SEEALSO
EXISTS_AND_CONV
HOL  Kananaskis-13