strip_exists : term -> term list * term

SYNOPSIS
Iteratively breaks apart existential quantifications.

DESCRIPTION
strip_exists `?x1 ... xn. t` returns ([`x1`;...;`xn`],`t`). Note that
   strip_exists(list_mk_exists([`x1`;...;`xn`],`t`))
will not return ([`x1`;...;`xn`],`t`) if t is an existential quantification.

FAILURE CONDITIONS
Never fails.

SEE ALSO
dest_exists, list_mk_exists.