Lemma to prove leaves-in-termset-when-match-char-val-in-termset.
This is disabled by default because its conclusion is fairly general, not specific to terminal sets.
Theorem:
(defthm nats-in-termset-when-match-sensitive-chars-in-termset (implies (and (nat-listp nats) (nats-match-sensitive-chars-p nats chars) (chars-sensitive-in-termset-p chars termset)) (list-in nats termset)))