simp [LawfulState.withoutTemps, State.withoutTemps, interp]
case h.a.refl
ν : Type u_1
n : ℕ
av : Array (Literal ν)
s : LawfulState (ν ⊕ Fin n)
τ : PropAssignment ν
vMapLt : ∀ (v : ν), (s.vMap ∘ Sum.inl) v < s.nextVar
vMapInj : Function.Injective (s.vMap ∘ Sum.inl)
⊢ interp (withoutTemps s (s.vMap ∘ Sum.inl) vMapLt vMapInj av) τ ↔ ∃ σ, τ = PropAssignment.map Sum.inl σ ∧ interp s σ
case h.a.refl
ν : Type u_1
n : ℕ
av : Array (Literal ν)
s : LawfulState (ν ⊕ Fin n)
τ : PropAssignment ν
vMapLt : ∀ (v : ν), (s.vMap ∘ Sum.inl) v < s.nextVar
vMapInj : Function.Injective (s.vMap ∘ Sum.inl)
⊢ (∃ σ, τ = PropAssignment.map (s.vMap ∘ Sum.inl) σ ∧ σ ⊨ Cnf.toPropFun s.cnf) ↔
    ∃ σ, τ = PropAssignment.map Sum.inl σ ∧ ∃ σ_1, σ = PropAssignment.map s.vMap σ_1 ∧ σ_1 ⊨ Cnf.toPropFun s.cnf