dsimp [fold', dfold]
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
⊢ fold' (n + 1) f init = f (Fin.last n) (fold' n (f ∘ Fin.castSucc) init)
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
⊢ f { val := n, isLt := (_ : Nat.le (n + 1) (n + 1)) }
      (dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) n (fun x => init) (_ : n ≤ n + 1)) =
    f (Fin.last n)
      (dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) n (fun x => init)
        (_ : Nat.le n n))