existsi z
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
⊢ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}.Nonempty
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
⊢ z ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}