simp[maxLiteral, List.maximum?_eq_some_iff'] at h
maxLit localMax : Nat
c : CNF Nat
h : c.maxLiteral = some maxLit
clause : Clause Nat
hclause1 : clause ∈ c
hclause2 : clause.maxLiteral = some localMax
⊢ localMax ≤ maxLit
maxLit localMax : Nat
c : CNF Nat
clause : Clause Nat
hclause1 : clause ∈ c
hclause2 : clause.maxLiteral = some localMax
h : (∃ a, a ∈ c ∧ a.maxLiteral = some maxLit) ∧ ∀ (b : Nat) (x : Clause Nat), x ∈ c → x.maxLiteral = some b → b ≤ maxLit
⊢ localMax ≤ maxLit