Theorem:
(defthm tree-list-list-match-concatenation-p-of-cons-concatenation (equal (tree-list-list-match-concatenation-p treess (cons repetition concatenation) rules) (and (consp treess) (tree-list-match-repetition-p (car treess) repetition rules) (tree-list-list-match-concatenation-p (cdr treess) concatenation rules))))