simp [interp, withTemps, State.withTemps]
case h.a
ν : Type u_1
s : LawfulState ν
n : ℕ
τ : PropAssignment (ν ⊕ Fin n)
⊢ interp (withTemps s) τ ↔ interp s (PropAssignment.map Sum.inl τ)
case h.a
ν : Type u_1
s : LawfulState ν
n : ℕ
τ : PropAssignment (ν ⊕ Fin n)
⊢ (∃ σ, τ = PropAssignment.map (State.withTemps.vMap s.toState) σ ∧ σ ⊨ Cnf.toPropFun s.cnf) ↔
    ∃ σ, PropAssignment.map Sum.inl τ = PropAssignment.map s.vMap σ ∧ σ ⊨ Cnf.toPropFun s.cnf