simp only [List.any_eq_true, Bool.not_eq_true', List.isEmpty_false_iff_exists_mem, mem,
  Clause.mem]
α : Type
g : CNF α
⊢ (List.any g fun c => !List.isEmpty c) = true ↔ ∃ a, mem a g
α : Type
g : CNF α
⊢ (∃ x, x ∈ g ∧ ∃ x_1, x_1 ∈ x) ↔ ∃ a c, c ∈ g ∧ ((a, false) ∈ c ∨ (a, true) ∈ c)