∀ {X : Type u_2} [tX : TopologicalSpace X] (x : CompHaus) (motive : C(↑x.toTop, X) → Prop) (x_1 : C(↑x.toTop, X)),
  (∀ (g : ↑x.toTop → X) (hg : Continuous g), motive { toFun := g, continuous_toFun := hg }) → motive x_1