simp
case h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : ↑v < ↑s.nextVar
v' : Fin n
⊢ ¬↑{ val := ↑s.nextVar + ↑v', property := ⋯ } = ↑v
case h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : ↑v < ↑s.nextVar
v' : Fin n
⊢ ¬↑s.nextVar + ↑v' = ↑v