Theorem: vDashSingleton_iff_vDash_formula (Pdl/Semantics.lean)

State before:
W : Type
M : KripkeModel W
w : W
⊢ ∀ (φ : Formula), (M, w)⊨[φ] ↔ evaluate M w φ
Tactic:
intro phi
State after:
W : Type
M : KripkeModel W
w : W
phi : Formula
⊢ (M, w)⊨[phi] ↔ evaluate M w phi

State before:
W : Type
M : KripkeModel W
w : W
phi : Formula
⊢ (M, w)⊨[phi] ↔ evaluate M w phi
Tactic:
simp [modelCanSemImplyList]
State after:
no goals