∀ {R : Type u_1} [inst : AddMonoid R] (S : AddSubmonoid R) [inst_1 : AddOreLocalization.AddOreSet S] (X : Type u_2)
  [inst_2 : AddAction R X], AddOreLocalization S X = Quotient (AddOreLocalization.oreEqv S X)