simp only [List.not_mem_nil, List.isEmpty_true_iff, false_implies, forall_const, true_iff]
case nil
α✝ : Type
⊢ (∀ (x : Clause α✝), x ∈ [] → List.isEmpty x = true) ↔ ∃ n, [] = List.replicate n []
case nil
α✝ : Type
⊢ ∃ n, [] = List.replicate n []