Tree matching theorem for parse-?%i.
Theorem: tree-match-of-parse-?%i
(defthm tree-match-of-parse-?%i (b* (((mv & tree &) (parse-?%i input))) (implies (equal element (?_ (/_ "%i"))) (tree-match-element-p tree element *grammar*))))