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