∀ {σ : Type u_1} {τ : Type u_2} {α : Type u_3} (R : Type u_4) [inst : CommSemiring R] (e : σ ≃ τ) (f : τ ≃ α),
  (MvPolynomial.renameEquiv R e).trans (MvPolynomial.renameEquiv R f) = MvPolynomial.renameEquiv R (e.trans f)