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