Recognizer for association lists with standard strings as keys
Function:
(defun standard-string-alistp (x) (declare (xargs :guard t)) (cond ((atom x) (eq x nil)) (t (and (consp (car x)) (stringp (car (car x))) (standard-string-p (car (car x))) (standard-string-alistp (cdr x))))))