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