Theorem: BVLogicalExpr.sat_and (LeanSAT/Reflect/BVExpr/Basic.lean)

State before:
x y : BVLogicalExpr
assign : BVExpr.Assignment
hx : x.sat assign
hy : y.sat assign
⊢ sat (BoolExpr.gate Gate.and x y) assign
Tactic:
simp only [sat] at *
State after:
x y : BVLogicalExpr
assign : BVExpr.Assignment
hx : eval assign x = true
hy : eval assign y = true
⊢ eval assign (BoolExpr.gate Gate.and x y) = true

State before:
x y : BVLogicalExpr
assign : BVExpr.Assignment
hx : eval assign x = true
hy : eval assign y = true
⊢ eval assign (BoolExpr.gate Gate.and x y) = true
Tactic:
simp [hx, hy, Gate.eval]
State after:
no goals