rewrite [<- H]
α : Type ?u.95188
xs : List α
ix bound : ℕ
H : ix + length xs = bound
deltaIx : ℕ
GETIX : deltaIx < length xs
⊢ ix + deltaIx < bound
α : Type ?u.95188
xs : List α
ix bound : ℕ
H : ix + length xs = bound
deltaIx : ℕ
GETIX : deltaIx < length xs
⊢ ix + deltaIx < ix + length xs