Coefficient evaluation agrees with univariate evaluation under $\mathrm{XCoeffEquiv}$

Let $x \in \mathbb{R}$ be a real number and $r$ an element of the coefficient ring $\mathrm{XCoeff} = \mathrm{MvPolynomial}(\mathrm{Fin}\,1, \mathbb{R})$. Then evaluating the transported univariate polynomial at $x$ agrees with the coefficient evaluation homomorphism:

Here XCoeffEquiv is the ring isomorphism between $\mathrm{XCoeff}$ and $\mathrm{Polynomial}(\mathbb{R})$. This bridge lemma lets proofs move freely between the multivariate-coefficient view (needed for currying/specialization) and the ordinary univariate-polynomial view (needed for root and degree bounds).