simp only [sat] at *
x y : BVLogicalExpr
assign : BVExpr.Assignment
hx : x.sat assign
hy : y.sat assign
⊢ sat (BoolExpr.gate Gate.and x y) assign
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