∀ (S : Type u_1) [inst : CommSemiring S] (s : Set (PrimeSpectrum S))
  (motive : (∃ s_1, sᶜ = PrimeSpectrum.zeroLocus s_1) → Prop) (x : ∃ s_1, sᶜ = PrimeSpectrum.zeroLocus s_1),
  (∀ (F : Set S) (hF : sᶜ = PrimeSpectrum.zeroLocus F), motive ⋯) → motive x