Theorem: Decl.constToCNF_eval (LeanSAT/AIG/CNF.lean)

State before:
α✝ : Type
output : α✝
b : Bool
assign : α✝ → Bool
⊢ CNF.eval assign (constToCNF output b) = (assign output == b)
Tactic:
simp [constToCNF, CNF.eval, CNF.Clause.eval]
State after:
no goals