simp only [toList, negateLiteral]
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ ¬l ∈ c.toList ∨ ¬l.negateLiteral ∈ c.toList
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause