theorem :: TREES_3:67

^ (elementary_tree 0) = elementary_tree 1