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

State before:
α : Type u_1
xs : List α
⊢ xs.isEmpty = true ↔ xs = []
Tactic:
cases xs <;> simp
State after:
no goals