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