PEXISTS_AND_CONV : conv
STRUCTURE
LIBRARY
pair
SYNOPSIS
Moves a paired existential quantification inwards through a conjunction.
DESCRIPTION
When applied to a term of the form ?p. t /\ u, where variables in p are not free in both t and u, PEXISTS_AND_CONV returns a theorem of one of three forms, depending on occurrences of variables from p in t and u. If p contains variables free in t but none in u, then the theorem:
   |- (?p. t /\ u) = (?p. t) /\ u
is returned. If p contains variables free in u but none in t, then the result is:
   |- (?p. t /\ u) = t /\ (?x. u)
And if p does not contain any variable free in either t nor u, then the result is:
   |- (?p. t /\ u) = (?x. t) /\ (?x. u)

FAILURE
PEXISTS_AND_CONV fails if it is applied to a term not of the form ?p. t /\ u, or if it is applied to a term ?p. t /\ u in which variables in p are free in both t and u.
SEEALSO
HOL  Kananaskis-10