induction n
α : Type u
f : Nat → α → α
init : α
n : Nat
⊢ fold f n init = foldM f init n
case zero
α : Type u
f : Nat → α → α
init : α
⊢ fold f zero init = foldM f init zero

case succ
α : Type u
f : Nat → α → α
init : α
n✝ : Nat
n_ih✝ : fold f n✝ init = foldM f init n✝
⊢ fold f (succ n✝) init = foldM f init (succ n✝)