unfold foldlM.aux
case zero.refl
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
macc : m β
⊢ (do
      let acc ← macc
      foldlM.aux n f n acc) =
    if h : n < n then
      foldl.loop n
        (fun macc i => do
          let acc ← macc
          f i acc)
        (do
          let acc ← macc
          f ⟨n, h⟩ acc)
        (n + 1)
    else macc
case zero.refl
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
macc : m β
⊢ (do
      let acc ← macc
      if h' : n < n then do
          let acc ← f ⟨n, h'⟩ acc
          foldlM.aux n f (n + 1) acc
        else pure acc) =
    if h : n < n then
      foldl.loop n
        (fun macc i => do
          let acc ← macc
          f i acc)
        (do
          let acc ← macc
          f ⟨n, h⟩ acc)
        (n + 1)
    else macc