. simp only [hl, not_false_eq_true, true_and]
  exact List.mem_erase_of_ne hl
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
no goals