intro v h
ν : Type u_1
s : LawfulState ν
⊢ ∀ v ∈ PropFun.semVars (Cnf.toPropFun s.cnf), v < s.nextVar
ν : Type u_1
s : LawfulState ν
v : IVar
h : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
⊢ v < s.nextVar