intro acc
case succ
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
j' : ℕ
ih :
  ∀ (i : ℕ) (hj : i + j' = n) (acc : α), foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
i : ℕ
hj : i + (j' + 1) = n
⊢ ∀ (acc : α), foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
case succ
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
j' : ℕ
ih :
  ∀ (i : ℕ) (hj : i + j' = n) (acc : α), foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
i : ℕ
hj : i + (j' + 1) = n
acc : α
⊢ foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc