dest_exists : term -> term * term

SYNOPSIS: Breaks apart an existentially quantified term into quantified variable and body.
DESCRIPTION: dest_exists is a term destructor for existential quantification: dest_exists `?var. t` returns (`var`,`t`).
FAILURE CONDITIONS: Fails with dest_exists if term is not an existential quantification.
SEE ALSO: is_exists, mk_exists, strip_exists.