∀ {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M}
  (p q : Submodule R M) (h : p = q) (x x_1 : ↥p),
  (Equiv.setCongr ⋯).toFun (x + x_1) = (Equiv.setCongr ⋯).toFun (x + x_1)