Recognizer for true (proper) lists of true lists
True-list-listp is the function that checks whether its argument is a list that ends in, or equals, nil, and furthermore, all of its elements have that property. Also see true-listp.
Function: true-list-listp
(defun true-list-listp (x) (declare (xargs :guard t)) (cond ((atom x) (eq x nil)) (t (and (true-listp (car x)) (true-list-listp (cdr x))))))