Recognizer for association lists with symbols as keys
(Symbol-alistp x) is true if and only if x is a list of pairs of the form (cons key val) where key is a symbolp.
Function: symbol-alistp
(defun symbol-alistp (x) (declare (xargs :guard t)) (cond ((atom x) (eq x nil)) (t (and (consp (car x)) (symbolp (car (car x))) (symbol-alistp (cdr x))))))