Theorem: BoolExprNat.sat_and (LeanSAT/Reflect/BoolExpr/Nat.lean)

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

State before:
x y : BoolExprNat
f : List Bool
hx : eval f x = true
hy : eval f y = true
⊢ eval f (gate Gate.and x y) = true
Tactic:
simp [hx, hy, Gate.eval]
State after:
no goals