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