unfold Fin.foldAll
α : Type u
n : Nat
f : Fin (Nat.succ n) → α → α
init : α
⊢ foldAll f init = foldAll (f ∘ succ) (f 0 init)
α : Type u
n : Nat
f : Fin (Nat.succ n) → α → α
init : α
⊢ Id.run (foldAllM f init) = Id.run (foldAllM (f ∘ succ) (f 0 init))