{E : Type u_8} →
  [inst : TopologicalSpace E] →
    {motive : ContinuousENorm E → Sort u} →
      (t : ContinuousENorm E) →
        ([toENorm : ENorm E] →
            (continuous_enorm : Continuous enorm) →
              motive { toENorm := toENorm, continuous_enorm := continuous_enorm }) →
          motive t