rcases h with ⟨l,hl,rfl⟩
case intro.intro
ν : Type u_1
s : LawfulState ν
v : IVar
C : Clause ILit
hC : C ∈ s.cnf
h : ∃ l ∈ C, LitVar.toVar l = v
⊢ v < s.nextVar
case intro.intro.intro.intro
ν : Type u_1
s : LawfulState ν
C : Clause ILit
hC : C ∈ s.cnf
l : ILit
hl : l ∈ C
⊢ LitVar.toVar l < s.nextVar