cases hab
case 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), HEq a b → HEq (f n a) (g n b)
b : α 0
hab : HEq a b
⊢ HEq (dfold f n a) (dfold g n b)
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), HEq a b → HEq (f n a) (g n b)
⊢ HEq (dfold f n a) (dfold g n a)