Theorem:
(defthm tree-list-match-repetition-p-of-1-repetition (implies (equal (repetition->range repetition) (repeat-range 1 (nati-finite 1))) (equal (tree-list-match-repetition-p trees repetition rules) (and (consp trees) (not (consp (cdr trees))) (tree-match-element-p (car trees) (repetition->element repetition) rules)))))