simp [PropAssignment.map] at h2 ⊢
case h.a.mpr.intro.intro.refl
ν : 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 σ
⊢ ∃ σ,
    PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ' =
        PropAssignment.map (State.withTemps.vMap s.toState) σ ∧
      σ ⊨ Cnf.toPropFun s.cnf
case h.a.mpr.intro.intro.refl
ν : 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 σ
⊢ ∃ σ, σ' ∘ State.withTemps.vMap s.toState = σ ∘ State.withTemps.vMap s.toState ∧ σ ⊨ Cnf.toPropFun s.cnf