unfold foldl'.aux
case zero.refl
α : Sort u_1
n : ℕ
f : α → Fin n → α
init acc : α
hj : n + 0 = n
⊢ (if h : n < n then foldl.loop n f (f acc ⟨n, h⟩) (n + 1) else acc) =
    foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) n ⋯ acc
case zero.refl
α : Sort u_1
n : ℕ
f : α → Fin n → α
init acc : α
hj : n + 0 = n
⊢ (if h : n < n then foldl.loop n f (f acc ⟨n, h⟩) (n + 1) else acc) =
    if h' : n < n then foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) (n + 1) h' (f acc ⟨n, h'⟩)
    else
      let_fun this := ⋯;
      Eq.ndrec (motive := fun n_1 =>
        {β : (i : ℕ) → i ≤ n_1 → Sort u_1} →
          β 0 ⋯ → ((i : ℕ) → (h : i < n_1) → β i ⋯ → β (i + 1) h) → (h : n ≤ n_1) → β n h → ¬n < n_1 → β n_1 ⋯)
        (fun {β} init f h acc h' => acc) this init (fun i h acc => f acc ⟨i, h⟩) ⋯ acc h'