simp_all [Satisfies]
case hor
α : 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 hor
α : 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✝ ∨ Satisfies M w q✝ → Satisfies M w' p✝ ∨ Satisfies M w' q✝