∀ {G : Type u_1} [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] {a : α}
  (motive : ↥(AddAction.stabilizer G a) → Prop) (x : ↥(AddAction.stabilizer G a)),
  (∀ (k : G) (hk : k ∈ AddAction.stabilizer G a), motive ⟨k, hk⟩) → motive x