∀ (B : Type u_1) (G : Type u_2) [inst : CommRing B] [inst_1 : Group G] [inst_2 : MulSemiringAction G B] (Q R : Ideal B)
  (motive : R ∈ MulAction.orbit G Q → Prop) (x : R ∈ MulAction.orbit G Q),
  (∀ (g : G) (hg : (fun m => m • Q) g = R), motive ⋯) → motive x