Check if all the terminal value notations in an element denote values in a set.
Function:
(defun element-in-termset-p (element termset) (declare (xargs :guard (and (elementp element) (nat-setp termset)))) (element-case element :rulename t :group (alternation-in-termset-p element.get termset) :option (alternation-in-termset-p element.get termset) :char-val (char-val-in-termset-p element.get termset) :num-val (num-val-in-termset-p element.get termset) :prose-val (prose-val-in-termset-p element.get termset)))