case succ n h_ind =>
  simp only [Nat.succ_eq_add_one]
  conv => lhs; rw [foldM_succ]; rhs; ext; rw [h_ind]
  conv => rhs; rw [foldM_succ]
  dsimp; rw [bind_assoc]
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 : α
⊢ foldM f init (succ n + 1) = foldM f init (succ n) >>= f (succ n)
no goals