for t being finite-branching Tree
for p being Element of t
for n being Nat holds
( p ^ <*n*> in succ p iff n < card (succ p) )