case h
R : Type u_1
ι : Type ?u.1918
inst✝¹ : Semiring R
inst✝ : CharP R 2
x✝ : R
⊢ bit0 x✝ = OfNat.ofNat 0 x✝
R : Type u_1
ι : Type ?u.1918
inst✝¹ : Semiring R
inst✝ : CharP R 2
⊢ bit0 = 0
funext
no goals
case h
R : Type u_1
ι : Type ?u.1918
inst✝¹ : Semiring R
inst✝ : CharP R 2
x✝ : R
⊢ bit0 x✝ = OfNat.ofNat 0 x✝
exact add_self_eq_zero _