for T1, T2 being Tree holds elementary_tree 2 c= tree (T1,T2)