∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set M}
  {p : (x : M) → x ∈ Submodule.span R s → Prop},
  p 0 ⋯ →
    (∀ (x y : M) (hx : x ∈ Submodule.span R s) (hy : y ∈ Submodule.span R s), p x hx → p y hy → p (x + y) ⋯) →
      (∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯) → ∀ {x : M} (hx : x ∈ Submodule.span R s), p x hx