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

State before:
n w : Nat
x x' : BitVec w
h : x = x'
⊢ x'.sshiftRight n = x.sshiftRight n
Tactic:
simp[*]
State after:
no goals