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