Theorem:
(defthm tree-list-match-repetition-p-of-0+-reps-when-1+-reps (implies (tree-list-match-repetition-p trees (repetition (repeat-range 1 (nati-infinity)) element) rules) (tree-list-match-repetition-p trees (repetition (repeat-range 0 (nati-infinity)) element) rules)) :rule-classes nil)