∀ (k : Type u_1) [inst : Field k] (z : AlgebraicClosure k)
  (motive : (∃ a, (Ideal.Quotient.mk (AlgebraicClosure.maxIdeal k)) a = z) → Prop)
  (x : ∃ a, (Ideal.Quotient.mk (AlgebraicClosure.maxIdeal k)) a = z),
  (∀ (p : MvPolynomial (AlgebraicClosure.Vars k) k) (hp : (Ideal.Quotient.mk (AlgebraicClosure.maxIdeal k)) p = z),
      motive ⋯) →
    motive x