dsimp [mem] at hlit
c : CNF Nat
lit : Nat
hlit : mem lit c
h : List.filterMap Clause.maxLiteral c = []
⊢ False
c : CNF Nat
lit : Nat
hlit : ∃ c_1, c_1 ∈ c ∧ Clause.mem lit c_1
h : List.filterMap Clause.maxLiteral c = []
⊢ False