∀ {A : Type u_1} (S : Type u_2) [inst : CommRing S] [inst_1 : CommRing A] [inst_2 : Algebra S A] (St : Subalgebra S A)
  (motive : ↥St → Prop) (x : ↥St), (∀ (y : A) (hy : y ∈ St), motive ⟨y, hy⟩) → motive x