rcases hlit with ⟨clause, ⟨hclause1, hclause2⟩⟩
c : CNF Nat
lit : Nat
hlit : ∃ c_1, c_1 ∈ c ∧ Clause.mem lit c_1
h : List.filterMap Clause.maxLiteral c = []
⊢ False
case intro.intro
c : CNF Nat
lit : Nat
h : List.filterMap Clause.maxLiteral c = []
clause : Clause Nat
hclause1 : clause ∈ c
hclause2 : Clause.mem lit clause
⊢ False