no goals
X : Type u
inst✝ : TopologicalSpace X
n : ℕ
x : X
f g : GenLoop 1 x
⊢ Path.Homotopic (↑genLoopOneEquivPathSelf f) (↑genLoopOneEquivPathSelf g) ↔ GenLoop.Homotopic f g
rw [← genLoopOneEquivPathSelf_symm_homotopic_iff, Equiv.symm_apply_apply, Equiv.symm_apply_apply]