simp_all [ValidOnModel]
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
⊢ M ⊧ p ⟶ q ⟶ p
α : Type u_1
inst✝ : Inhabited α
M : Model α
p q r : Formula α
⊢ ∀ (w : M.World) {w' : M.Frame.World},
    w ≺ w' → Satisfies M w' p → ∀ {w'_1 : M.Frame.World}, w' ≺ w'_1 → Satisfies M w'_1 q → Satisfies M w'_1 p