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

State before:
α : Type
h : unsat []
⊢ False
Tactic:
simp [unsat] at h
State after:
no goals

State before:
α : Type
⊢ False → unsat []
Tactic:
simp
State after:
no goals