∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommSemiring R] (f : σ → MvPolynomial τ R)
  (p : MvPolynomial σ R), (MvPolynomial.aeval id) ((MvPolynomial.rename f) p) = (MvPolynomial.aeval f) p