existsi (atom default), (λ w _ => w ∉ X), hX₁.some
case intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
⊢ ∃ x x_1 x_2,
    (∀ (w' : F.World),
        x_2 ≺ w' →
          (∀ (w'_1 : F.World), w' ≺ w'_1 → Satisfies { Frame := F, Valuation := x_1 } w'_1 x) →
            Satisfies { Frame := F, Valuation := x_1 } w' x) ∧
      ∃ x_3, x_2 ≺ x_3 ∧ ¬Satisfies { Frame := F, Valuation := x_1 } x_3 x
case intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hCF : ¬ConverseWellFounded F.Rel
X : Set F.World
hX₁ : X.Nonempty
hX₂ : ∀ x ∈ X, ∃ x_1 ∈ X, F.Rel x x_1
⊢ (∀ (w' : F.World),
      hX₁.some ≺ w' →
        (∀ (w'_1 : F.World), w' ≺ w'_1 → Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w'_1 (atom default)) →
          Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w' (atom default)) ∧
    ∃ x, hX₁.some ≺ x ∧ ¬Satisfies { Frame := F, Valuation := fun w x => w ∉ X } x (atom default)