∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f₀ f₁ : C(X, Y)} {g₀ g₁ : C(X, Z)} (motive : f₀.Homotopic f₁ → g₀.Homotopic g₁ → Prop)
  (x : f₀.Homotopic f₁) (x_1 : g₀.Homotopic g₁),
  (∀ (F : f₀.Homotopy f₁) (G : g₀.Homotopy g₁), motive ⋯ ⋯) → motive x x_1