∀ {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {p : Submodule R M}
  (motive : ↥p → Prop) (x : ↥p), (∀ (y : M) (hy : y ∈ p), motive ⟨y, hy⟩) → motive x