for p, q being FinSequence st p c= q holds
len p <= len q