Theorem: LRAT.Literal.sat_iff (LeanSAT/LRAT/CNF.lean)

State before:
α : Type u_1
p : α → Bool
a : α
b : Bool
⊢ p ⊨ (a, b) ↔ p a = b
Tactic:
simp only [HSat.eval]
State after:
no goals