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