simp [ValidOnFrame, ValidOnModel, Axioms.Dot3]
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : Connected F.Rel
⊢ F ⊧* .𝟯
α : 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