generalize hls : LawfulState.new' _ _ = ls
ν α : Type u_1
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
e : EncCNF ν α
P : PropPred ν
h : encodesProp e P
⊢ (∃ τ, P τ) ↔
    ∃ τ, τ ⊨ Cnf.toPropFun (↑e (LawfulState.new' (IndexType.card ν) (Equiv.toEmbedding IndexType.toEquiv))).2.cnf
ν α : 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
⊢ (∃ τ, P τ) ↔ ∃ τ, τ ⊨ Cnf.toPropFun (↑e ls).2.cnf