Theorem: CNF.unsat_nil_cons (LeanSAT/Reflect/CNF/Basic.lean)

State before:
α✝ : Type
g : List (Clause α✝)
⊢ unsat ([] :: g) ↔ True
Tactic:
simp [unsat]
State after:
no goals