∀ {ι : Type u_1} {K : Type u_3} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {v : ι → V} {s t : Set ι} (hs : LinearIndepOn K v s) (hst : s ⊆ t)
  (motive :
    Classical.choose ⋯ ⊆ t ∧
        s ⊆ Classical.choose ⋯ ∧
          v '' t ⊆ ↑(Submodule.span K (v '' Classical.choose ⋯)) ∧ LinearIndepOn K v (Classical.choose ⋯) →
      Prop)
  (x :
    Classical.choose ⋯ ⊆ t ∧
      s ⊆ Classical.choose ⋯ ∧
        v '' t ⊆ ↑(Submodule.span K (v '' Classical.choose ⋯)) ∧ LinearIndepOn K v (Classical.choose ⋯)),
  (∀ (_hbt : Classical.choose ⋯ ⊆ t) (_hsb : s ⊆ Classical.choose ⋯)
      (htb : v '' t ⊆ ↑(Submodule.span K (v '' Classical.choose ⋯))) (_hli : LinearIndepOn K v (Classical.choose ⋯)),
      motive ⋯) →
    motive x