simp only [mem] at hlit
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
maxLit : Nat
c : Clause Nat
lit : Nat
hlit : (lit, false) ∈ c ∨ (lit, true) ∈ c
h : (∃ a, a ∈ c ∧ a.fst = maxLit) ∧ ∀ (a : Nat × Bool), a ∈ c → a.fst ≤ maxLit
⊢ lit ≤ maxLit