∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} (x_1 : ↑(GenLoop N X x))
  (motive : (x_2 : ↑(GenLoop N X x)) → (fun f => ⇑↑f) x_2 = (fun f => ⇑↑f) x_1 → Prop) (x_2 : ↑(GenLoop N X x))
  (x_3 : (fun f => ⇑↑f) x_2 = (fun f => ⇑↑f) x_1),
  (∀ (f : (N → ↑unitInterval) → X) (continuous_toFun : Continuous f)
      (property : { toFun := f, continuous_toFun := continuous_toFun } ∈ GenLoop N X x)
      (x_4 : (fun f => ⇑↑f) ⟨{ toFun := f, continuous_toFun := continuous_toFun }, property⟩ = (fun f => ⇑↑f) x_1),
      motive ⟨{ toFun := f, continuous_toFun := continuous_toFun }, property⟩ x_4) →
    motive x_2 x_3