for p, q being FinSequence holds
( p in ProperPrefixes q iff p is_a_proper_prefix_of q )