simp[← Option.ne_none_iff_exists', h1, h2, maxLiteral]
case inr
l : Nat
c : Clause Nat
h : (l, true) ∈ c
h1 : c ≠ []
h2 : ¬(List.map (fun x => x.fst) c).maximum? = none ↔ ¬List.map (fun x => x.fst) c = []
⊢ ∃ maxLit, c.maxLiteral = some maxLit
no goals