case a.h
X : Type u_1
Y : Type ?u.114429
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.114444
γ : Path x y
a : X
x✝ : ↑I
⊢ ↑(symm (refl a)) x✝ = ↑(refl a) x✝
X : Type u_1
Y : Type ?u.114429
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.114444
γ : Path x y
a : X
⊢ symm (refl a) = refl a
ext
no goals
case a.h
X : Type u_1
Y : Type ?u.114429
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.114444
γ : Path x y
a : X
x✝ : ↑I
⊢ ↑(symm (refl a)) x✝ = ↑(refl a) x✝
rfl