induction n with
| zero => rfl
| succ n IH => dsimp [dfold]; rw [IH, H]
α : Nat → Sort u
β : Nat → Sort v
f : (n : Nat) → α n → β n
g₁ : (n : Nat) → α n → α (n + 1)
g₂ : (n : Nat) → β n → β (n + 1)
n : Nat
init : α 0
H : ∀ (n : Nat) (a : α n), g₂ n (f n a) = f (n + 1) (g₁ n a)
⊢ dfold g₂ n (f 0 init) = f n (dfold g₁ n init)
no goals