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