Theorem: nat-listp-of-tree->string-when-match-element-num/char-val
(defthm nat-listp-of-tree->string-when-match-element-num/char-val (implies (and (tree-match-element-p tree element rules) (member-equal (element-kind element) '(:num-val :char-val))) (nat-listp (tree->string tree))))