for p1, p2 being FinSequence st ( {} is_a_proper_prefix_of p2 or {} <> p2 ) holds
p1 is_a_proper_prefix_of p1 ^ p2