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

State before:
w : Nat
⊢ not.eval = fun x => ~~~x
Tactic:
rfl
State after:
no goals