strip_forall : term -> term list * term

SYNOPSIS

Iteratively breaks apart universal quantifications.

DESCRIPTION

strip_forall `!x1 ... xn. t` 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 CONDITIONS

Never fails.

SEE ALSO

dest_forall, list_mk_forall.