Theorem: BVDecide.ReifiedBVLogical.not_congr (LeanSAT/Reflect/Tactics/BVDecide.lean)

State before:
x x' : Bool
h : x' = x
⊢ (!x') = !x
Tactic:
simp[*]
State after:
no goals