Theorem: LeanSAT.Encode.VEncCNF.toICnf_equisatisfiable (LeanSAT/Encode/VEncCNF.lean)

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