simp only [toList, delete, ne_eq]
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
⊢ l' ∈ (c.delete l).toList ↔ l' ≠ l ∧ l' ∈ c.toList
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
⊢ l' ∈ c.clause.erase l ↔ ¬l' = l ∧ l' ∈ c.clause