conv =>
  dsimp [foldM, foldM.loop]
  change f 0 init >>= pure = pure init >>= f 0
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
f : Nat → α → m α
init : α
⊢ foldM f init (zero + 1) = foldM f init zero >>= f zero
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
f : Nat → α → m α
init : α
⊢ f 0 init >>= pure = pure init >>= f 0