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.