unfold foldl
α : Type u_1
n : ℕ
f : α → Fin n → α
init : α
⊢ foldl n f init = List.foldl f init (List.ofFn id)
α : Type u_1
n : ℕ
f : α → Fin n → α
init : α
⊢ foldl.loop n f init 0 = List.foldl f init (List.ofFn id)