rw [v.val.encodesProp_equisatisfiable _ v.property]
ν α : Type u_1
P : PropPred ν
inst✝¹ : IndexType ν
inst✝ : LawfulIndexType ν
v : VEncCNF ν α P
⊢ (∃ τ, τ ⊨ Cnf.toPropFun (toICnf ↑v)) ↔ ∃ τ, τ ⊨ P
no goals