dest_exists1
boolSyntax.dest_exists1 : term -> term * term
Breaks apart a unique existence term into quantified variable and body.
If M has the form ?!x. t, then dest_exists1 M returns (x,t).
Failure
Fails if M is not a unique existence term.