Disambiguation between
Theorem:
(defthm fail-dot-when-match-dash-etc (implies (and (tree-match-element-p tree element *grammar*) (equal (element-kind element) :group) (consp (element-group->get element)) (not (consp (cdr (element-group->get element)))) (consp (car (element-group->get element))) (equal (car (car (element-group->get element))) (repetition (repeat-range 1 (nati-finite 1)) (element-char-val (char-val-insensitive nil "-"))))) (mv-nth 0 (parse-ichar #\. (append (tree->string tree) rest-input)))))