∀ {α : Type u_1} [inst : CommSemiring α] (s : Set α) (motive : (∃ T, ↑T ⊆ s ∧ 1 ∈ Submodule.span α ↑T) → Prop)
  (x : ∃ T, ↑T ⊆ s ∧ 1 ∈ Submodule.span α ↑T),
  (∀ (t : Finset α) (hts : ↑t ⊆ s) (mem : 1 ∈ Submodule.span α ↑t), motive ⋯) → motive x