Theorem:
(defthm tree-list-list-match-alternation-p-of-cons-alternation (equal (tree-list-list-match-alternation-p treess (cons concatenation alternation) rules) (or (tree-list-list-match-concatenation-p treess concatenation rules) (tree-list-list-match-alternation-p treess alternation rules))))