α : Sort u
a b : α
h₂ : Eq.rec a (_ : α = α) = b
⊢ HEq a b
α β : Sort u
a : α
b : β
h₁ : α = β
h₂ : Eq.rec a h₁ = b
⊢ HEq a b
subst h₁
case h
α : Sort u
a b : α
h₂ : Eq.rec a (_ : α = α) = b
⊢ a = b
α : Sort u
a b : α
h₂ : Eq.rec a (_ : α = α) = b
⊢ HEq a b
apply heq_of_eq
no goals
case h
α : Sort u
a b : α
h₂ : Eq.rec a (_ : α = α) = b
⊢ a = b
exact h₂