have ⟨σ',hσ'⟩ := τ.exists_preimage ⟨State.withTemps.vMap s.toState, (LawfulState.withTemps s).vMapInj⟩
case h.a.mpr.intro.intro
ν : Type u_1
s : LawfulState ν
n : ℕ
τ : PropAssignment (ν ⊕ Fin n)
σ : PropAssignment IVar
h1 : PropAssignment.map Sum.inl τ = PropAssignment.map s.vMap σ
h2 : σ ⊨ Cnf.toPropFun s.cnf
⊢ ∃ σ, τ = PropAssignment.map (State.withTemps.vMap s.toState) σ ∧ σ ⊨ Cnf.toPropFun s.cnf
case h.a.mpr.intro.intro
ν : Type u_1
s : LawfulState ν
n : ℕ
τ : PropAssignment (ν ⊕ Fin n)
σ : PropAssignment IVar
h1 : PropAssignment.map Sum.inl τ = PropAssignment.map s.vMap σ
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
hσ' : τ = PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ'
⊢ ∃ σ, τ = PropAssignment.map (State.withTemps.vMap s.toState) σ ∧ σ ⊨ Cnf.toPropFun s.cnf