no goals
σ : Type u_4
τ : Type u_2
R : Type u_3
S : Type ?u.360595
T : Type ?u.360598
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f✝ : σ → MvPolynomial τ R
υ : Type u_1
f : σ → MvPolynomial τ R
g : τ → MvPolynomial υ R
φ : MvPolynomial σ R
⊢ ↑(bind₁ g) (↑(bind₁ f) φ) = ↑(bind₁ fun i => ↑(bind₁ g) (f i)) φ
simp [bind₁, ← comp_aeval]