{S : Type u_3} →
  {G : Type u_4} →
    [inst : SubNegMonoid G] →
      [inst_1 : SetLike S G] →
        {motive : AddSubgroupClass S G → Sort u} →
          ([toAddSubmonoidClass : AddSubmonoidClass S G] → [toNegMemClass : NegMemClass S G] → motive ⋯) →
            (t : AddSubgroupClass S G) → motive t