{X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {motive : C(X, Y) → Sort u} →
          (t : C(X, Y)) →
            ((toFun : X → Y) →
                (continuous_toFun : Continuous toFun) →
                  motive { toFun := toFun, continuous_toFun := continuous_toFun }) →
              motive t