simp only [maxLiteral, List.maximum?_eq_none_iff] at h
c : CNF Nat
h : c.maxLiteral = none
lit : Nat
hlit : mem lit c
⊢ False
c : CNF Nat
lit : Nat
hlit : mem lit c
h : List.filterMap Clause.maxLiteral c = []
⊢ False