dsimp [fold', dfold]
α : Type u
motive : Nat → α → Prop
n : Nat
f : Fin n → α → α
init : α
zero : motive 0 init
succ : ∀ (i : Nat) (hi : i < n) (a : α), motive i a → motive (i + 1) (f { val := i, isLt := hi } a)
⊢ motive n (fold' n f init)
α : Type u
motive : Nat → α → Prop
n : Nat
f : Fin n → α → α
init : α
zero : motive 0 init
succ : ∀ (i : Nat) (hi : i < n) (a : α), motive i a → motive (i + 1) (f { val := i, isLt := hi } a)
⊢ motive n (dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n))