case succ n h_ind =>
  rw [foldM_succ_eq_foldM_bind, ←h_ind]; rfl
α : Type u
f : Nat → α → α
init : α
n : Nat
h_ind : fold f n init = foldM f init n
⊢ fold f (succ n) init = foldM f init (succ n)
no goals