for w, s, t being FinSequence st w ^ t is_a_proper_prefix_of w ^ s holds
t is_a_proper_prefix_of s