rw [Nat.fold_eq_foldM, foldAllM_comp_val]
n : Nat
α : Type u
f : Nat → α → α
init : α
⊢ Id.run (foldAllM (f ∘ val) init) = Nat.fold f n init
n : Nat
α : Type u
f : Nat → α → α
init : α
⊢ Id.run (Nat.foldM f init n) = Nat.foldM f init n