dest_exists1 : term -> term * term
STRUCTURE
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
HOL  Kananaskis-13