----------------------------------------------------------------------
dest_pexists                                              (pairSyntax)
----------------------------------------------------------------------
dest_pexists : term -> term * term

LIBRARY
pair

SYNOPSIS
Breaks apart paired existential quantifiers into the bound pair and the body.

DESCRIBE
{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.

SEEALSO
boolSyntax.dest_exists, pairSyntax.is_pexists,
pairSyntax.strip_pexists.

----------------------------------------------------------------------