fix: missing simproc for BitVec equality

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean

@@ -227,6 +227,9 @@ builtin_dsimproc [simp, seval] reduceOfNat (BitVec.ofNat _ _) := fun e => do
   if bv.toNat == v then return .continue -- already normalized
   return .done <| toExpr (BitVec.ofNat n v)
 
+builtin_simproc [simp, seval] reduceEq  (( _ : BitVec _) = _)  := reduceBinPred ``Eq 3 (. = .)
+builtin_simproc [simp, seval] reduceNe  (( _ : BitVec _) ≠ _)  := reduceBinPred ``Ne 3 (. ≠ .)
+
 /-- Simplification procedure for `<` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceLT (( _ : BitVec _) < _)  := reduceBinPred ``LT.lt 4 (· < ·)
 /-- Simplification procedure for `≤` on `BitVec`s. -/

tests/lean/run/bitvec_simproc.lean

@@ -137,3 +137,7 @@ example (a : BitVec 32) (h : a >>> 3 = b) : (a >>> 1) >>> 2 = b := by
   simp; guard_target =ₛ a >>> 3 = b; assumption
 example (a : BitVec 32) (h : a >>> 3 = b) : (a >>> 1#32) >>> 2 = b := by
   simp; guard_target =ₛ a >>> 3 = b; assumption
+example (h : False) : 1#2 = 2#2 := by
+  simp; guard_target =ₛ False; exact h
+example : 1#2 ≠ 2#2 := by
+  simp