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