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.