simp only at this ⊢
case mk
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
a : α
ls' : LawfulState ν
hls' : ↑e ls = (a, ls')
this :
  let s' := (a, ls').2;
  s'.vMap = ls.vMap ∧
    s'.assumeVars = ls.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp s' τ ↔ LawfulState.interp ls τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun ls.assumeVars)ᶜ ⇨ P
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun (a, ls').2.cnf
case mk
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
ls : LawfulState ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
a : α
ls' : LawfulState ν
hls' : ↑e ls = (a, ls')
this :
  ls'.vMap = ls.vMap ∧
    ls'.assumeVars = ls.assumeVars ∧
      ∀ (τ : PropAssignment ν),
        LawfulState.interp ls' τ ↔ LawfulState.interp ls τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun ls.assumeVars)ᶜ ⇨ P
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.cnf