Theorem: equiv_iff_TPequiv (Pdl/Unfold.lean)

State before:
φ ψ : Formula
α : Program
⊢ φ≡ψ ↔ ∀ (ℓ : TP α), φ⋀signature α ℓ≡ψ⋀signature α ℓ
Tactic:
sorry
State after:
no goals