subst e
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
f✝ p q : Formula α
e : □(□p ⟶ q) ⋎ □(□q ⟶ p) = f✝
V : Valuation F.World α
x : { Frame := F, Valuation := V }.World
⊢ Satisfies { Frame := F, Valuation := V } x f✝
α : 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))