dest_pexists
pairSyntax.dest_pexists : term -> term * term
Breaks apart paired existential quantifiers into the bound pair and the body.
dest_pexists is a term destructor for paired existential
quantification. The application of dest_pexists to ?pair. t returns
(pair,t).
Failure
Fails with dest_pexists if term is not a paired existential
quantification.
See also
boolSyntax.dest_exists,
pairSyntax.is_pexists,
pairSyntax.strip_pexists