dest_cons : term -> term * term

SYNOPSIS: Breaks apart a `CONS pair' into head and tail.
DESCRIPTION: dest_cons is a term destructor for `CONS pairs'. When applied to a term representing a nonempty list `[t;t1;...;tn]` (which is equivalent to `CONS t [t1;...;tn]`), it returns the pair of terms (`t`,`[t1;...;tn]`).
FAILURE CONDITIONS: Fails with dest_cons if the term is not a non-empty list.
SEE ALSO: dest_list, is_cons, is_list, mk_cons, mk_list.