α : Sort u_1
a : α
β : Sort u_2
C : α → Sort u_2
x : C a
y : β
⊢ HEq ((_ : a = a) ▸ x) y ↔ HEq x y
α : Sort u_1
a : α
β : Sort u_2
b : α
C : α → Sort u_2
x : C a
y : β
e : a = b
⊢ HEq (e ▸ x) y ↔ HEq x y
subst e
no goals
α : Sort u_1
a : α
β : Sort u_2
C : α → Sort u_2
x : C a
y : β
⊢ HEq ((_ : a = a) ▸ x) y ↔ HEq x y
rfl