Disambiguation between (i) any of
Theorem:
(defthm fail-digit/star-when-match-element (implies (and (tree-match-element-p tree (element-rulename *element*) *grammar*) (tree-terminatedp tree)) (and (mv-nth 0 (parse-digit (append (tree->string tree) rest-input))) (mv-nth 0 (parse-ichar #\* (append (tree->string tree) rest-input))))))