for p, q being FinSequence st p is_a_prefix_of q holds
ProperPrefixes p c= ProperPrefixes q