Rules whose terminal value notations all denote values in a set, generate terminal strings consisting of terminals in the set.
This is disabled by default because its conclusion is fairly general, not specific to terminal sets.
Theorem:
(defthm terminal-strings-in-termset-when-rules-in-termset (implies (and (terminal-string-for-rules-p nats rules) (rulelist-in-termset-p rules termset)) (list-in nats termset)))