for t, t1 being Tree
for xi, nu being Element of t st not xi c= nu & not nu c= xi holds
(t with-replacement (xi,t1)) | nu = t | nu