for p being FinSequence of NAT
for T, T1 being Tree st p in T holds
T1 = (T with-replacement (p,T1)) | p