suffices ∀ i j (hj : i + j = n) acc,
  foldl.loop n f acc i =
    foldl'.aux (n := n) (β := fun _ _ => α)
      init (fun i h acc => f acc ⟨i, h⟩)
      i (hj ▸ Nat.le_add_right i j) acc
  from this 0 n (by simp) init
α : 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
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
⊢ ∀ (i j : ℕ) (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