∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R]
  {s t u : Set M}, LinearIndependent R Subtype.val → s ⊆ u → t ⊆ u → (Submodule.span R s ≤ Submodule.span R t ↔ s ⊆ t)