(M : Type u_1) →
  {α : Type u_2} →
    [inst : AddGroup M] →
      [inst_1 : AddAction M α] →
        (a : α) →
          (motive : ↥(fixingAddSubgroup M {a}) → Sort u_3) →
            (x : ↥(fixingAddSubgroup M {a})) →
              ((m : M) → (hm : m ∈ fixingAddSubgroup M {a}) → motive ⟨m, hm⟩) → motive x