intro x hx h
case intro.intro.intro.intro.intro.left
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₂ : F.World
r₁₂ : F.Rel w₁ w₂
w₃ : F.World
r₂₃ : F.Rel w₂ w₃
nr₁₃ : ¬F.Rel w₁ w₃
⊢ ∀ (w' : F.World),
    w₁ ≺ w' →
      (∀ (w'_1 : F.World),
          w' ≺ w'_1 → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w'_1 (atom default)) →
        Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)
case intro.intro.intro.intro.intro.left
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₂ : F.World
r₁₂ : F.Rel w₁ w₂
w₃ : F.World
r₂₃ : F.Rel w₂ w₃
nr₁₃ : ¬F.Rel w₁ w₃
x : F.World
hx : w₁ ≺ x
h : ∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } w' (atom default)
⊢ Satisfies { Frame := F, Valuation := fun w' x => w' ≠ w₂ ∧ w' ≠ w₃ } x (atom default)