simp [mem, List.mem_append]
α : Type
a : α
x y : CNF α
⊢ mem a (x ++ y) ↔ mem a x ∨ mem a y
α : Type
a : α
x y : CNF α
⊢ (∃ c, (c ∈ x ∨ c ∈ y) ∧ Clause.mem a c) ↔ (∃ c, c ∈ x ∧ Clause.mem a c) ∨ ∃ c, c ∈ y ∧ Clause.mem a c