simp [h]
case h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h : σ ⊨ Cnf.toPropFun s.cnf
⊢ PropAssignment.map Sum.inl (PropAssignment.map (State.withTemps.vMap s.toState) σ) = PropAssignment.map s.vMap σ ∧
    σ ⊨ Cnf.toPropFun s.cnf
case h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h : σ ⊨ Cnf.toPropFun s.cnf
⊢ PropAssignment.map Sum.inl (PropAssignment.map (State.withTemps.vMap s.toState) σ) = PropAssignment.map s.vMap σ