case succ n h_ind =>
  rw [foldAllM_succ]; dsimp
  have : (f ∘ Fin.val (n:=n+1)) ∘ Fin.succ = (f ∘ Nat.succ) ∘ Fin.val :=
    funext fun x => rfl
  conv => lhs; rhs; rw [this]; ext x; rw [h_ind]
  conv => rhs; rw [Nat.foldM_succ]
m : Type u → Type v
inst✝ : Monad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldAllM (f ∘ val) init = Nat.foldM f init n
f : Nat → α → m α
init : α
⊢ foldAllM (f ∘ val) init = Nat.foldM f init (Nat.succ n)
no goals