case a.h
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
⊢ ↑(delayReflRight 1 γ) t = ↑γ t
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ delayReflRight 1 γ = γ
ext t
no goals
case a.h
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
⊢ ↑(delayReflRight 1 γ) t = ↑γ t
exact congr_arg γ (qRight_one_right t)