intro lit hlit
maxLit : Nat
c : CNF Nat
h : c.maxLiteral = some maxLit
⊢ ∀ (lit : Nat), mem lit c → lit ≤ maxLit
maxLit : Nat
c : CNF Nat
h : c.maxLiteral = some maxLit
lit : Nat
hlit : mem lit c
⊢ lit ≤ maxLit