∀ {R : Type u} [inst : CommSemiring R] {S : Type u_2} {T : Type u_3} [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : CommSemiring T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] {σ : Type u_4}
  {τ : Type u_5} (p : MvPolynomial (σ ⊕ τ) R) (f : τ → S) (g : σ → T),
  (MvPolynomial.aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) p =
    (MvPolynomial.aeval g) ((MvPolynomial.aeval (Sum.elim MvPolynomial.X (⇑MvPolynomial.C ∘ f))) p)