for S, T being Polish-language
for u being FinSequence st S c= T & u is S -headed holds
( S -head u = T -head u & S -tail u = T -tail u )