good-pseudo-term-listp

(in-package "ACL2")

(deflist good-pseudo-term-listp
  (x)
  :guard (pseudo-term-listp x)
  :short "Check if all the terms in a list are good,
          i.e. their values do not contain any bad atoms."
  (good-pseudo-termp x))