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.