Check if all the terminal value notations in a rule denote values in a set.
Function:
(defun rule-in-termset-p (rule termset) (declare (xargs :guard (and (rulep rule) (nat-setp termset)))) (alternation-in-termset-p (rule->definiens rule) termset))
Theorem:
(defthm booleanp-of-rule-in-termset-p (b* ((yes/no (rule-in-termset-p rule termset))) (booleanp yes/no)) :rule-classes :rewrite)