simp [foldl, foldl']
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
⊢ foldl n f init = foldl' n init fun i h acc => f acc ⟨i, h⟩
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
⊢ foldl.loop n f init 0 = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) 0 ⋯ init