(G : Type u_1) →
  [inst : AddGroup G] →
    {X : Type u_2} →
      [inst_1 : AddAction G X] →
        (a : X) →
          (motive : ↑(Set.Ici (AddAction.stabilizer G a)) → Sort u_3) →
            (x : ↑(Set.Ici (AddAction.stabilizer G a))) →
              ((H : AddSubgroup G) → (hH : H ∈ Set.Ici (AddAction.stabilizer G a)) → motive ⟨H, hH⟩) → motive x