strip_abs : term -> term list * term
STRUCTURE
boolSyntax
SYNOPSIS
Iteratively breaks apart abstractions.
DESCRIPTION
If M has the form \x1 ... xn.t then strip_abs M returns ([x1,...,xn],t). Note that 
   strip_abs(list_mk_abs([x1,...,xn],t))
will not return ([x1,...,xn],t) if t is an abstraction.
FAILURE
Never fails.
SEEALSO
list_mk_abs, dest_abs
HOL  Kananaskis-13