strip_forall : term -> term list * term
STRUCTURE
boolSyntax
SYNOPSIS
Iteratively breaks apart universal quantifications.
DESCRIPTION
If M has the form !x1 ... xn. t then strip_forall M returns ([x1,...,xn],t). Note that 
   strip_forall(list_mk_forall([x1,...,xn],t,))
will not return ([x1,...,xn],t) if t is a universal quantification.
FAILURE
Never fails.
SEEALSO
list_mk_forall, dest_forall
HOL  Kananaskis-14