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