let β' : Nat → Type v := fun i => i ≤ n → β
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
⊢ dfold (fun i x hi => g₂ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => f init) (_ : Nat.le n n) =
    f (dfold (fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n))
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
⊢ dfold (fun i x hi => g₂ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => f init) (_ : Nat.le n n) =
    f (dfold (fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n))