∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S}
  (motive : IsAlgebraic R x → Prop) (hx : IsAlgebraic R x),
  (∀ (w : Polynomial R) (p_ne_zero : w ≠ 0) (hp : (Polynomial.aeval x) w = 0), motive ⋯) → motive hx