∀ {σ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  (f : R →+* MvPolynomial σ S) (d : σ →₀ ℕ) (r : R),
  (MvPolynomial.bind₂ f) ((MvPolynomial.monomial d) r) = f r * (MvPolynomial.monomial d) 1