for Z1, Z2 being Tree
for p being FinSequence of NAT st p in Z1 holds
for v being Element of Z1 with-replacement (p,Z2)
for w being Element of Z1 st v = w & not p,w are_c=-comparable holds
succ v = succ w