theorem :: TREES_1:50

for n, m being Nat
for s being FinSequence st n <> m holds
not <*n*> is_a_prefix_of <*m*> ^ s