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

State before:
assign : Assignment
a✝ : Nat
lhs : BVExpr a✝
op : BVBinOp
rhs : BVExpr a✝
⊢ eval assign (lhs.bin op rhs) = op.eval (eval assign lhs) (eval assign rhs)
Tactic:
rfl
State after:
no goals