cases h
case h.a
ν : Type u_1
n : ℕ
av : Array (Literal ν)
s : LawfulState (ν ⊕ Fin n)
vMap : ν → IVar
vMapLt : ∀ (v : ν), vMap v < s.nextVar
vMapInj : Function.Injective vMap
h : vMap = s.vMap ∘ Sum.inl
τ : PropAssignment ν
⊢ interp (withoutTemps s vMap 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)
⊢ interp (withoutTemps s (s.vMap ∘ Sum.inl) vMapLt vMapInj av) τ ↔ ∃ σ, τ = PropAssignment.map Sum.inl σ ∧ interp s σ