A prose value notation is unconstrained, so it cannot be guaranteed to denote values in a set.
(prose-val-in-termset-p prose-val termset) → yes/no
Function:
(defun prose-val-in-termset-p (prose-val termset) (declare (xargs :guard (and (prose-val-p prose-val) (nat-setp termset)))) nil)
Theorem:
(defthm booleanp-of-prose-val-in-termset-p (b* ((yes/no (prose-val-in-termset-p prose-val termset))) (booleanp yes/no)) :rule-classes :rewrite)