. simp only [hl, not_true, false_and, iff_false]
  exact List.Nodup.not_mem_erase c.nodup
case pos
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : l' = l
⊢ l' ∈ c.clause.erase l ↔ ¬l' = l ∧ l' ∈ c.clause

case neg
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : ¬l' = l
⊢ l' ∈ c.clause.erase l ↔ ¬l' = l ∧ l' ∈ c.clause
case neg
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : ¬l' = l
⊢ l' ∈ c.clause.erase l ↔ ¬l' = l ∧ l' ∈ c.clause