{R : Type u_1} →
  [inst : TopologicalSpace R] →
    [inst_1 : NonUnitalNonAssocRing R] →
      {motive : IsTopologicalRing R → Sort u} →
        (t : IsTopologicalRing R) →
          ([toIsTopologicalSemiring : IsTopologicalSemiring R] → [toContinuousNeg : ContinuousNeg R] → motive ⋯) →
            motive t