simp_all [Satisfies]
case himp
α : Type u_1
inst✝ : Inhabited α
M : Model α
w w' : M.Frame.World
hw : w ≺ w'
p✝ q✝ : Formula α
a✝¹ : Satisfies M w p✝ → Satisfies M w' p✝
a✝ : Satisfies M w q✝ → Satisfies M w' q✝
⊢ Satisfies M w (p✝ ⟶ q✝) → Satisfies M w' (p✝ ⟶ q✝)
case himp
α : Type u_1
inst✝ : Inhabited α
M : Model α
w w' : M.Frame.World
hw : w ≺ w'
p✝ q✝ : Formula α
a✝¹ : Satisfies M w p✝ → Satisfies M w' p✝
a✝ : Satisfies M w q✝ → Satisfies M w' q✝
⊢ (∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p✝ ∨ Satisfies M w' q✝) →
    ∀ {w'_1 : M.Frame.World}, w' ≺ w'_1 → ¬Satisfies M w'_1 p✝ ∨ Satisfies M w'_1 q✝