is_pexists : (term -> bool)
STRUCTURE
pairSyntax
LIBRARY
pair
SYNOPSIS
Tests a term to see if it as a paired existential quantification.
DESCRIPTION
is_pexists "?pair. t"
returns
true
. If the term is not a paired existential quantification the result is
false
.
FAILURE
Never fails.
SEEALSO
is_exists
,
dest_pexists
HOL
Kananaskis-14