symbol-alistp

(in-package "ACL2")

(defsection std/typed-alists/symbol-alistp
  :parents (std/typed-alists)
  :short "Theorems about the built-in @(tsee symbol-alistp)."
  (defthm symbol-alistp-of-append
    (equal (symbol-alistp (append x y))
      (and (symbol-alistp (true-list-fix x)) (symbol-alistp y))))
  (defthmd alistp-when-symbol-alistp
    (implies (symbol-alistp x) (alistp x)))
  (defthmd symbol-listp-of-strip-cars-when-symbol-alistp
    (implies (symbol-alistp alist)
      (symbol-listp (strip-cars alist)))))