Theorem: BVExpr.eval_signExtend (LeanSAT/Reflect/BVExpr/Basic.lean)

State before:
assign : Assignment
v a✝ : Nat
expr : BVExpr a✝
⊢ eval assign (signExtend v expr) = BitVec.signExtend v (eval assign expr)
Tactic:
rfl
State after:
no goals