simp [LawfulState.interp]
case mk.intro.intro
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
a : α
ls' : LawfulState ν
h3 : ∀ (τ : PropAssignment ν), LawfulState.interp ls' τ ↔ P τ
⊢ (∃ τ, LawfulState.interp ls' τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.cnf
case mk.intro.intro
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
a : α
ls' : LawfulState ν
h3 : ∀ (τ : PropAssignment ν), LawfulState.interp ls' τ ↔ P τ
⊢ (∃ τ σ, τ = PropAssignment.map ls'.vMap σ ∧ σ ⊨ Cnf.toPropFun ls'.cnf) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.cnf