theorem :: TREES_3:64
for T1, T2 being Tree st ^ T1 = ^ T2 holds
T1 = T2