simp only [contains, List.contains]
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ c.contains l = true ↔ l ∈ c.toList
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ List.elem l c.clause = true ↔ l ∈ c.toList