for p, q being FinSequence
for k, l being Nat st len p = k + l & q = p | (Seg k) holds
len q = k