cases g with
| nil => simp
| cons c g =>
  simp only [not_mem_cons] at h
  obtain ⟨n, h⟩ := h
  cases n with
  | zero => simp at h
  | succ n =>
    simp_all
case isFalse
g : CNF Nat
h : ¬∃ a, mem a g
⊢ unsat (List.replicate (List.length g) []) ↔ g.unsat
no goals