induction n with
| zero => rfl
| succ n IH => dsimp [dfold]; exact hfg n _ _ IH
case refl.refl
α : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
n : Nat
a : α 0
g : (n : Nat) → α n → α (n + 1)
hfg : ∀ (n : Nat) (a b : α n), a = b → f n a = g n b
⊢ dfold f n a = dfold g n a
no goals