∀ {K : Type u_1} [inst : Field K] [inst_1 : FirstOrder.Ring.CompatibleRing K] (n : ℕ),
  K ⊨ FirstOrder.Field.genericMonicPolyHasRoot n =
    ∀ (p : { p // p.Monic ∧ p.natDegree = n }), ∃ x, Polynomial.eval x ↑p = 0