α✝ : Sort u
β : Sort v
γ : Sort w
α : Sort u_1
a b : α
⊢ ↑(Equiv.cast (_ : α = α)) a = b ↔ HEq a b
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α β : Sort u_1
h : α = β
a : α
b : β
⊢ ↑(Equiv.cast h) a = b ↔ HEq a b
subst h
no goals
α✝ : Sort u
β : Sort v
γ : Sort w
α : Sort u_1
a b : α
⊢ ↑(Equiv.cast (_ : α = α)) a = b ↔ HEq a b
simp [coe_refl]