string-stringlist-alistp

(in-package "ACL2")

(defalist string-stringlist-alistp
  (x)
  :parents (std/typed-alists)
  :short "Recognize alists from strings to true lists of strings."
  :key (stringp x)
  :val (string-listp x)
  :true-listp t
  :keyp-of-nil nil
  :valp-of-nil t
  ///
  (defthm string-listp-of-cdr-of-assoc-equal-when-string-string/s-alistp
    (implies (string-stringlist-alistp x)
      (string-listp (cdr (assoc-equal k x))))))