Character value notations that denote terminals in a set can be matched only by trees whose terminal leaves are in the set.
Theorem:
(defthm leaves-in-termset-when-match-char-val-in-termset (implies (and (tree-match-char-val-p tree char-val) (char-val-in-termset-p char-val termset)) (string-in-termset-p (tree->string tree) termset)))