rw [←hls] at h3
case mk.intro.intro
ν α : 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')
h3 :
  ∀ (τ : PropAssignment ν),
    LawfulState.interp ls' τ ↔ LawfulState.interp ls τ ∧ τ ⊨ (fun τ => τ ⊨ Clause.toPropFun ls.assumeVars)ᶜ ⇨ P
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ 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 ν
hls : LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv) = ls
a : α
ls' : LawfulState ν
hls' : ↑e ls = (a, ls')
h3 :
  ∀ (τ : PropAssignment ν),
    LawfulState.interp ls' τ ↔
      LawfulState.interp (LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv)) τ ∧
        τ ⊨
          (fun τ =>
                τ ⊨
                  Clause.toPropFun
                    (LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv)).assumeVars)ᶜ ⇨
            P
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun ls'.cnf