{M : Type u_2} →
  {α : Type u_1} →
    [inst : AddGroup M] →
      [inst_1 : AddAction M α] →
        {t : Set α} →
          (motive : ↥(SubAddAction.ofFixingAddSubgroup M t) → Sort u_3) →
            (x : ↥(SubAddAction.ofFixingAddSubgroup M t)) →
              ((x : α) → (hx : x ∈ SubAddAction.ofFixingAddSubgroup M t) → motive ⟨x, hx⟩) → motive x