∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {β : LocalizedModule S M → Prop}, (∀ (m : M) (s : ↥S), β (LocalizedModule.mk m s)) → ∀ (x : LocalizedModule S M), β x