simp only [Satisfies.or_def, or_iff_not_imp_left]
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
p q : Formula α
V : Valuation F.World α
x : { Frame := F, Valuation := V }.World
⊢ Satisfies { Frame := F, Valuation := V } x (□(□p ⟶ q) ⋎ □(□q ⟶ p))
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
p q : Formula α
V : Valuation F.World α
x : { Frame := F, Valuation := V }.World
⊢ ¬Satisfies { Frame := F, Valuation := V } x (□(□p ⟶ q)) → Satisfies { Frame := F, Valuation := V } x (□(□q ⟶ p))