case refl
α : Sort u_1
γ : Sort u_2
f : α → γ
x : α
g : α → γ
h₁ : HEq f g
⊢ f x = g x
α β : Sort u_1
γ : Sort u_2
f : α → γ
g : β → γ
x : α
y : β
h₁ : HEq f g
h₂ : HEq x y
⊢ f x = g y
cases h₂
case refl.refl
α : Sort u_1
γ : Sort u_2
f : α → γ
x : α
⊢ f x = f x
case refl
α : Sort u_1
γ : Sort u_2
f : α → γ
x : α
g : α → γ
h₁ : HEq f g
⊢ f x = g x
cases h₁
no goals
case refl.refl
α : Sort u_1
γ : Sort u_2
f : α → γ
x : α
⊢ f x = f x
rfl