no goals
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x (bit1 p) = bit1 (eval₂ f x p)
rw [bit1, eval₂_add, eval₂_bit0, eval₂_one, bit1]