∀ (R : Type u_1) [inst : CommSemiring R],
  Polynomial.Bivariate.equivMvPolynomial R =
    AlgEquiv.ofAlgHom (Polynomial.aevalAeval (MvPolynomial.X 0) (MvPolynomial.X 1))
      (MvPolynomial.aeval ![Polynomial.C Polynomial.X, Polynomial.X]) ⋯ ⋯