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

State before:
α✝ : Type
output a : α✝
assign : α✝ → Bool
⊢ CNF.eval assign (atomToCNF output a) = (assign output == assign a)
Tactic:
simp only [atomToCNF, CNF.eval_succ, CNF.Clause.eval_succ, Bool.beq_true, Bool.beq_false,
  CNF.Clause.eval_nil, Bool.or_false, CNF.eval_nil, Bool.and_true]
State after:
α✝ : Type
output a : α✝
assign : α✝ → Bool
⊢ ((assign output || !assign a) && (!assign output || assign a)) = (assign output == assign a)

State before:
α✝ : Type
output a : α✝
assign : α✝ → Bool
⊢ ((assign output || !assign a) && (!assign output || assign a)) = (assign output == assign a)
Tactic:
cases assign output <;> cases assign a <;> decide
State after:
no goals