theorem :: TREES_3:76

tree ((elementary_tree 0),(elementary_tree 0)) = elementary_tree 2