have : (f ∘ Fin.val (n:=n+1)) ∘ Fin.succ = (f ∘ Nat.succ) ∘ Fin.val :=
  funext fun x => rfl
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 : α
⊢ f 0 init >>= foldAllM ((f ∘ val) ∘ succ) = Nat.foldM f init (Nat.succ n)
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 : α
this : (f ∘ val) ∘ succ = (f ∘ Nat.succ) ∘ val
⊢ f 0 init >>= foldAllM ((f ∘ val) ∘ succ) = Nat.foldM f init (Nat.succ n)