∀ (F : Type u) {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (q : ℕ) [ExpChar F q]
  [IsPurelyInseparable F E] (x : E), ∃ n y, minpoly F x = Polynomial.X ^ q ^ n - Polynomial.C y