simp only [List.any_eq_true, Bool.not_eq_true', not_exists, not_and, Bool.not_eq_false]
α✝ : Type
g : CNF α✝
⊢ ¬(List.any g fun c => !List.isEmpty c) = true ↔ ∃ n, g = List.replicate n []
α✝ : Type
g : CNF α✝
⊢ (∀ (x : Clause α✝), x ∈ g → List.isEmpty x = true) ↔ ∃ n, g = List.replicate n []