{G : Type u} →
  [inst : TopologicalSpace G] →
    [inst_1 : Neg G] →
      {motive : ContinuousNeg G → Sort u_1} →
        ((continuous_neg : Continuous fun a => -a) → motive ⋯) → (t : ContinuousNeg G) → motive t