This module contains the equality simplifying part of the bv_normalize simp set.

theorem Std.Tactic.BVDecide.Frontend.Normalize.Bool.not_beq_not (a b : Bool) : ((!a) == !b) = (a == b)

theorem Std.Tactic.BVDecide.Frontend.Normalize.BitVec.not_beq_not {w : Nat} (a b : BitVec w) : (~~~a == ~~~b) = (a == b)