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

State before:
assign : Assignment
op : BVUnOp
a✝ : Nat
operand : BVExpr a✝
⊢ eval assign (un op operand) = op.eval (eval assign operand)
Tactic:
rfl
State after:
no goals