∀ {R : Type u_3} {N : Type u_6} [inst : Ring R] [inst_1 : AddCommGroup N] [inst_2 : Module R N] [IsDomain R]
  [Module.IsTorsionFree R N] {ι : Type u_7} (p : ι → Submodule R N),
  iSupIndep p → ∀ {v : ι → N}, (∀ (i : ι), v i ∈ p i) → (∀ (i : ι), v i ≠ 0) → LinearIndependent R v