Theorem: BVDecide.Normalize.BitVec.ne_to_beq (LeanSAT/Reflect/Tactics/Normalize/Canonicalize.lean)

State before:
w : Nat
a b : BitVec w
⊢ (a ≠ b) = ((!a == b) = true)
Tactic:
simp
State after:
no goals