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]
α✝ : Type
output a : α✝
assign : α✝ → Bool
⊢ CNF.eval assign (atomToCNF output a) = (assign output == assign a)
α✝ : Type
output a : α✝
assign : α✝ → Bool
⊢ ((assign output || !assign a) && (!assign output || assign a)) = (assign output == assign a)