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

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