for p, q being XFinSequence st p c= q holds
p ^ (q /^ (len p)) = q