theorem :: VALUED_1:50

for i being Nat
for p1 being FinSequence
for p2 being FinSubsequence st i >= len p1 holds
p1 misses Shift (p2,i)