Theorem: singletonSat_iff_sat (Pdl/Semantics.lean)

State before:
⊢ ∀ (φ : Formula), satisfiable {φ} ↔ satisfiable φ
Tactic:
intro phi
State after:
phi : Formula
⊢ satisfiable {phi} ↔ satisfiable phi

State before:
phi : Formula
⊢ satisfiable {phi} ↔ satisfiable phi
Tactic:
simp
State after:
no goals