----------------------------------------------------------------------
dest_abs                                                        (Term)
----------------------------------------------------------------------
dest_abs : term -> term * term

SYNOPSIS
Breaks apart an abstraction into abstracted variable and body.

DESCRIBE
{dest_abs} is a term destructor for abstractions: if {M} is a term of
the form {\v.t}, then {dest_abs M} returns {(v,t)}.

FAILURE
Fails if it is not given a lambda abstraction.

SEEALSO
Term.mk_abs, Term.is_abs, Term.dest_var, Term.dest_const,
Term.dest_comb, boolSyntax.strip_abs.

----------------------------------------------------------------------