dest_list : term -> term list * hol_type
STRUCTURE
SYNOPSIS
Iteratively breaks apart a list term.
DESCRIPTION
dest_list is a term destructor for lists: dest_list ``[t1;...;tn]:ty list`` returns ([t1,...,tn], ty).
FAILURE
Fails if the term is not a list.
SEEALSO
HOL  Trindemossen-1