Theorem: singletonSat_iff_sat (Bml/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