strip_exists : term -> term list * term
STRUCTURE
boolSyntax
SYNOPSIS
Iteratively breaks apart existential quantifications.
DESCRIPTION
If M has the structure ?x1 ... xn. t then strip_exists M 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
Never fails.
SEEALSO
list_mk_exists, dest_exists
HOL  Kananaskis-13