have : f = g := funext fun i => funext fun a =>
  hf i i a rfl
case refl
α : Type u
m : Nat
f : Fin m → α → α
init : α
g : Fin m → α → α
hf : ∀ (i j : Fin m) (a : α), i.val = j.val → f i a = g j a
⊢ fold' m f init = fold' m g init
case refl
α : Type u
m : Nat
f : Fin m → α → α
init : α
g : Fin m → α → α
hf : ∀ (i j : Fin m) (a : α), i.val = j.val → f i a = g j a
this : f = g
⊢ fold' m f init = fold' m g init