for W, W1 being Tree
for p, q being FinSequence of NAT st p in W & q in W & not p is_a_prefix_of q holds
q in W with-replacement (p,W1)