have h1 := List.ne_nil_of_mem h
case inr
l : Nat
c : Clause Nat
h : (l, true) ∈ c
⊢ ∃ maxLit, c.maxLiteral = some maxLit
case inr
l : Nat
c : Clause Nat
h : (l, true) ∈ c
h1 : c ≠ []
⊢ ∃ maxLit, c.maxLiteral = some maxLit