simp only [sat] at *
α : Type
x y : BoolExpr α
f : α → Bool
hx : x.sat f
hy : y.sat f
⊢ (gate Gate.and x y).sat f
α : Type
x y : BoolExpr α
f : α → Bool
hx : eval f x = true
hy : eval f y = true
⊢ eval f (gate Gate.and x y) = true