theorem :: TREES_3:64

for T1, T2 being Tree st ^ T1 = ^ T2 holds
T1 = T2