dest_pexists : term -> term * term
STRUCTURE
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
HOL  Trindemossen-1