Recognize a list of true-lists
;; See also true-list-listp, but that one requires the final cdr to be nil. (defund all-true-listp (x) (declare (xargs :guard t)) (if (atom x) t (and (true-listp (first x)) (all-true-listp (rest x)))))