simp [withTemps, State.withTemps, State.withTemps.vMap]
case h.left.h.inl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
⊢ σ (s.vMap v) =
    PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ'
      (State.withTemps.vMap s.toState (Sum.inl v))
case h.left.h.inl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
⊢ σ (s.vMap v) =
    PropAssignment.setMany σ (Finset.image (fun x => { val := ↑s.nextVar + ↑x, property := ⋯ }) Finset.univ) σ'
      (s.vMap v)