clear ih
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
init : α
i : ℕ
h : i + (j + 1) = n
this✝ : i < n
init' : α
this : i + 1 + j = n
ih : foldl.loop n f init' (i + 1) = List.foldl f init' (List.ofFn fun x => cast this (natAdd (i + 1) x))
⊢ List.foldl f init' (List.ofFn fun x => cast this (natAdd (i + 1) x)) =
    List.foldl f init' (List.ofFn fun i_1 => ⟨i + (↑i_1 + 1), ⋯⟩)
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
init : α
i : ℕ
h : i + (j + 1) = n
this✝ : i < n
init' : α
this : i + 1 + j = n
⊢ List.foldl f init' (List.ofFn fun x => cast this (natAdd (i + 1) x)) =
    List.foldl f init' (List.ofFn fun i_1 => ⟨i + (↑i_1 + 1), ⋯⟩)