∀ {ι : Type u'} (R : Type u_2) {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (v : ι → M), ∃ s, LinearIndepOn R v s ∧ ∀ i ∉ s, ∃ a, a ≠ 0 ∧ a • v i ∈ Submodule.span R (v '' s)