intro w
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
⊢ ∀ (w : M.World), Satisfies M w p ∨ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
hExt : Extensive M.Rel
w : M.World
⊢ Satisfies M w p ∨ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p