Theorem: BVUnOp.eval_arithShiftRightConst (LeanSAT/Reflect/BVExpr/Basic.lean)

State before:
n w : Nat
⊢ (arithShiftRightConst n).eval = fun x => x.sshiftRight n
Tactic:
rfl
State after:
no goals