intro hpq v hv
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✝
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✝
hpq : ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p✝ ∨ Satisfies M w' q✝
v : M.Frame.World
hv : w' ≺ v
⊢ ¬Satisfies M v p✝ ∨ Satisfies M v q✝