Check if a pseudo-term only contains good values, i.e. no bad atoms.
(good-pseudo-termp term) → yes/no
That is, check if every value of every quoted constant in the term satisfies good-valuep.
(defthm return-type-of-good-pseudo-termp.yes/no (b* ((?yes/no (good-pseudo-termp term))) (booleanp yes/no)) :rule-classes :rewrite)
(defthm return-type-of-good-pseudo-term-listp.yes/no (b* ((?yes/no (good-pseudo-term-listp terms))) (booleanp yes/no)) :rule-classes :rewrite)