Recognizer for a true list of characters
The predicate character-listp tests whether its argument is a true list of characters.
Function: character-listp
(defun character-listp (l) (declare (xargs :guard t)) (cond ((atom l) (equal l nil)) (t (and (characterp (car l)) (character-listp (cdr l))))))