(cons-listp x) is like alistp but does not require the list to be nil-terminated.
Function: cons-listp
(defun cons-listp (x) (declare (xargs :guard t)) (if (consp x) (and (consp (car x)) (cons-listp (cdr x))) t))