no goals
σ : Type u_1
τ : Type ?u.200346
R : Type u_2
S : Type ?u.200352
T : Type ?u.200355
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : σ → MvPolynomial τ R
⊢ bind₂ C = RingHom.id (MvPolynomial σ R)
ext : 2 <;> simp