intro init i j h
α : Type u_1
n : ℕ
f : α → Fin n → α
init : α
⊢ ∀ (init : α) (i j : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ init : α
i j : ℕ
h : i + j = n
⊢ foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))