∀ {R : Type u_1} {M : Type u_2} {x y : M} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (p : Submodule R M), Submodule.Quotient.mk x + Submodule.Quotient.mk y = Submodule.Quotient.mk (x + y)