no goals
X : Type u
inst✝ : TopologicalSpace X
n : ℕ
x : X
f g : GenLoop 0 x
⊢ Joined (↑genLoopZeroEquiv f) (↑genLoopZeroEquiv g) ↔ GenLoop.Homotopic f g
rw [← homotopic_genLoopZeroEquiv_symm_iff, Equiv.symm_apply_apply, Equiv.symm_apply_apply]