assoc

(in-package "ACL2")

(defsection std/alists/assoc-equal
  :parents (std/alists assoc)
  :short "Theorems about @(tsee assoc-equal)
          in the @(see std/alists) library."
  (defthm consp-of-assoc-equal
    (implies (alistp alist)
      (iff (consp (assoc-equal key alist))
        (assoc-equal key alist)))))