Tree matching theorem for parse-hex-val-rest.
Theorem:
(defthm tree-match-of-parse-hex-val-rest (b* (((mv & tree &) (parse-hex-val-rest input))) (implies (equal element (?_ (/_ (1*_ (!_ (/_ "." (1*_ *hexdig*))))) (/_ (!_ (/_ "-" (1*_ *hexdig*)))))) (tree-match-element-p tree element *grammar*))))