Recognizer for a true list of strings
The predicate string-listp tests whether its argument is a true-listp of strings.
Function: string-listp
(defun string-listp (x) (declare (xargs :guard t)) (cond ((atom x) (eq x nil)) (t (and (stringp (car x)) (string-listp (cdr x))))))