for w, s, t being FinSequence of NAT st w ^ t is_a_proper_prefix_of w ^ s holds
t is_a_proper_prefix_of s by TREES_1:49;