for T1, T2 being Tree holds
( (tree (T1,T2)) | <*0*> = T1 & (tree (T1,T2)) | <*1*> = T2 )