∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] {σ : Type u_3}
  {A B : Set (σ → K)}, A ≤ B → MvPolynomial.vanishingIdeal k B ≤ MvPolynomial.vanishingIdeal k A