simp only [maxLiteral, List.maximum?_eq_some_iff', List.mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] at h
maxLit : Nat
c : Clause Nat
h : c.maxLiteral = some maxLit
lit : Nat
hlit : mem lit c
⊢ lit ≤ maxLit
maxLit : Nat
c : Clause Nat
lit : Nat
hlit : mem lit c
h : (∃ a, a ∈ c ∧ a.fst = maxLit) ∧ ∀ (a : Nat × Bool), a ∈ c → a.fst ≤ maxLit
⊢ lit ≤ maxLit