dest_pexists : term -> term * term
STRUCTURE
pairSyntax
LIBRARY
pair
SYNOPSIS
Breaks apart paired existential quantifiers into the bound pair and the body.
DESCRIPTION
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
dest_exists
,
is_pexists
,
strip_pexists
HOL
Kananaskis-14