Disambiguation between
Theorem:
(defthm fail-digit-when-match-a/b/c/d/e/f (implies (and (tree-match-element-p tree element *grammar*) (elementp element) (equal (element-kind element) :char-val) (equal (char-val-kind (element-char-val->get element)) :insensitive) (equal (char-val-insensitive->iprefix (element-char-val->get element)) nil) (member-equal (char-val-insensitive->get (element-char-val->get element)) '("A" "B" "C" "D" "E" "F"))) (mv-nth 0 (parse-digit (append (tree->string tree) rest-input)))))