dest_abs : term -> term * term
STRUCTURE
SYNOPSIS
Breaks apart an abstraction into abstracted variable and body.
DESCRIPTION
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
HOL  Kananaskis-13