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