a✝ b✝ c d : Prop
α : Sort u
h₁ : Subsingleton α
a b : α
⊢ HEq a b
a✝ b✝ c d : Prop
α β : Sort u
h₁ : Subsingleton α
h₂ : α = β
a : α
b : β
⊢ HEq a b
subst h₂
case h
a✝ b✝ c d : Prop
α : Sort u
h₁ : Subsingleton α
a b : α
⊢ a = b
a✝ b✝ c d : Prop
α : Sort u
h₁ : Subsingleton α
a b : α
⊢ HEq a b
apply heq_of_eq
no goals
case h
a✝ b✝ c d : Prop
α : Sort u
h₁ : Subsingleton α
a b : α
⊢ a = b
apply Subsingleton.elim