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