Theorems about assoc-equal in the std/alists library.
Theorem: consp-of-assoc-equal
(defthm consp-of-assoc-equal (implies (alistp alist) (iff (consp (assoc-equal key alist)) (assoc-equal key alist))))
