Theorem: List.isEmpty_false_iff_exists_mem (LeanSAT/Reflect/CNF/Basic.lean)

State before:
α : Type u_1
xs : List α
⊢ xs.isEmpty = false ↔ ∃ x, x ∈ xs
Tactic:
cases xs <;> simp
State after:
no goals