(character-list-listp x) recognizes lists where every element satisfies character-listp.
(character-list-listp x) → std::bool
This is an ordinary deflist. It is
"loose" in that it does not care whether
(defun character-list-listp (x) (declare (xargs :guard t)) (let ((__function__ 'character-list-listp)) (declare (ignorable __function__)) (if (consp x) (and (character-listp (car x)) (character-list-listp (cdr x))) t)))