suffices ∀ init i j (h : i + j = n),
  foldl.loop n f init i =
    List.foldl f init (List.ofFn (n := j) (fun x => Fin.natAdd i x |>.cast h))
  by
    have := this init 0 n (by simp)
    simp at this; rw [this]; rfl
α : Type u_1
n : ℕ
f : α → Fin n → α
init : α
⊢ foldl.loop n f init 0 = List.foldl f init (List.ofFn id)
α : 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))