dest_exists
boolSyntax.dest_exists : term -> term * term
Breaks apart an existentially quantified term into quantified variable and body.
If M has the form ?x. t, then dest_exists M returns (x,t).
Failure
Fails if M is not an existential quantification.
See also
boolSyntax.mk_exists,
boolSyntax.is_exists,
boolSyntax.strip_exists