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