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 & w is_a_proper_prefix_of p holds
succ v = succ w