Theorem: BVDecide.ReifiedBVExpr.extract_congr (LeanSAT/Reflect/Tactics/BVDecide.lean)

State before:
hi lo w : Nat
x x' : BitVec w
h1 : x = x'
⊢ BitVec.extractLsb hi lo x' = BitVec.extractLsb hi lo x
Tactic:
simp[*]
State after:
no goals