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