dest_exists : term -> term * term
STRUCTURE
boolSyntax
SYNOPSIS
Breaks apart an existentially quantified term into quantified variable and body.
DESCRIPTION
If
M
has the form
?x. t
, then
dest_exists M
returns
(x,t)
.
FAILURE
Fails if
M
is not an existential quantification.
SEEALSO
mk_exists
,
is_exists
,
strip_exists
HOL
Kananaskis-13