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

State before:
lhs rhs lhs' rhs' : Bool
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ (lhs' == rhs') = (lhs == rhs)
Tactic:
simp[*]
State after:
no goals