for t, t1 being Tree
for xi being Element of t holds (t with-replacement (xi,t1)) | xi = t1