Proper-consp
Recognizer for proper (nil-terminated) non-empty lists
Proper-consp is the function that checks whether its argument
is a non-empty list that ends in nil. Also see true-listp.
Function: proper-consp
(defun proper-consp (x)
(declare (xargs :guard t))
(and (consp x) (true-listp x)))