∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {W : Subspace K V}
  (v : V) (motive : (∃ φ, φ (Submodule.Quotient.mk v) ≠ 0) → Prop) (x : ∃ φ, φ (Submodule.Quotient.mk v) ≠ 0),
  (∀ (φ : Module.Dual K (V ⧸ W)) (hφ : φ (Submodule.Quotient.mk v) ≠ 0), motive ⋯) → motive x