rfl
case refl.refl.zero
α : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
a : α 0
g : (n : Nat) → α n → α (n + 1)
hfg : ∀ (n : Nat) (a b : α n), a = b → f n a = g n b
⊢ dfold f zero a = dfold g zero a
no goals