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