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