∀ {R : Type u_2} {A : Type u_1} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  (x : ↥(integralClosure R A)) (motive : ↑x ∈ integralClosure R A → Prop) (x_1 : ↑x ∈ integralClosure R A),
  (∀ (p : Polynomial R) (hpm : p.Monic) (hpx : Polynomial.eval₂ (algebraMap R A) (↑x) p = 0), motive ⋯) → motive x_1