. intro x _;
  by_cases hxs : x ∈ X
  . obtain ⟨y, hy₁, hy₂⟩ := hX₂ x hxs;
    intro h;
    exact h x (by simp_all only [Satisfies]);
  . aesop;
case intro.intro.left
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)

case intro.intro.right
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, hX₁.some ≺ x ∧ ¬Satisfies { Frame := F, Valuation := fun w x => w ∉ X } x (atom default)
case intro.intro.right
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, hX₁.some ≺ x ∧ ¬Satisfies { Frame := F, Valuation := fun w x => w ∉ X } x (atom default)