∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] {s : Set ι} {i : ι},
  LinearIndepOn R v s → (∀ (r : R), r • v i ∈ Submodule.span R (v '' s) → r = 0) → LinearIndepOn R v (insert i s)