∀ {σ : Type u_1} (R : Type u_2) [inst : CommRing R] [Nontrivial R] {i : σ} {s : Set σ} {f : Polynomial R},
  Transcendental (↥(MvPolynomial.supported R s)) ((Polynomial.aeval (MvPolynomial.X i)) f) ↔ i ∉ s ∧ Transcendental R f