strip_imp_only : term -> term list * term
STRUCTURE
boolSyntax
SYNOPSIS
Iteratively breaks apart implications.
DESCRIPTION
If M is of the form t1 ==> (... (tn ==> t) ...), then strip_imp_only M returns ([t1,...,tn],t). Note that 
   strip_imp_only(list_mk_imp([t1,...,tn],t))
will not return ([t1,...,tn],t) if t is an implication.
FAILURE
Never fails.
EXAMPLE
- strip_imp_only (Term `(T ==> F) ==> (T ==> F)`);
> val it = ([`T ==> F`, `T`], `F`) : term list * term

- strip_imp_only (Term `t1 ==> t2 ==> t3 ==> ~t`);
> val it = ([`t1`, `t2`, `t3`], `~t`) : term list * term

SEEALSO
list_mk_imp, dest_imp
HOL  Kananaskis-13