dsimp
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldM f init (n + 1) = foldM f init n >>= f n
f : Nat → α → m α
init : α
⊢ (f 0 init >>= fun x => foldM (f ∘ succ) x n >>= (f ∘ succ) n) =
    (do
        let x ← f 0 init
        foldM (f ∘ succ) x n) >>=
      f (n + 1)
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldM f init (n + 1) = foldM f init n >>= f n
f : Nat → α → m α
init : α
⊢ (f 0 init >>= fun x => foldM (f ∘ succ) x n >>= f (succ n)) =
    (do
        let x ← f 0 init
        foldM (f ∘ succ) x n) >>=
      f (n + 1)