intro clause hclause1 hclause2
maxLit localMax : Nat
c : CNF Nat
h : c.maxLiteral = some maxLit
⊢ ∀ (clause : Clause Nat), clause ∈ c → clause.maxLiteral = some localMax → localMax ≤ maxLit
maxLit localMax : Nat
c : CNF Nat
h : c.maxLiteral = some maxLit
clause : Clause Nat
hclause1 : clause ∈ c
hclause2 : clause.maxLiteral = some localMax
⊢ localMax ≤ maxLit