∀ {R : Type u_2} {S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (Q : Ideal S) (t : S)
  (Q' : Ideal S) (motive : Q' ∈ (Ideal.under (↥(Algebra.adjoin R {t})) Q).primesOver S → Prop)
  (x : Q' ∈ (Ideal.under (↥(Algebra.adjoin R {t})) Q).primesOver S),
  (∀ (left : Q'.IsPrime) (right : Q'.LiesOver (Ideal.under (↥(Algebra.adjoin R {t})) Q)), motive ⋯) → motive x