Theorem: tree-list-list-match-alternation-p-when-atom-alternation
(defthm tree-list-list-match-alternation-p-when-atom-alternation (implies (atom alternation) (not (tree-list-list-match-alternation-p treess alternation rules))))