dest_exists1 : term -> term * term
STRUCTURE
boolSyntax
SYNOPSIS
Breaks apart a unique existence term into quantified variable and body.
DESCRIPTION
If
M
has the form
?!x. t
, then
dest_exists1 M
returns
(x,t)
.
FAILURE
Fails if
M
is not a unique existence term.
SEEALSO
mk_exists1
,
is_exists1
HOL
Kananaskis-14