Disambiguation between
Theorem:
(defthm fail-hexdig-when-match-hex-val-rest (implies (and (tree-match-element-p tree (?_ (/_ (1*_ (!_ (/_ "." (1*_ *hexdig*))))) (/_ (!_ (/_ "-" (1*_ *hexdig*))))) *grammar*) (mv-nth 0 (parse-hexdig rest-input))) (mv-nth 0 (parse-hexdig (append (tree->string tree) rest-input)))))