. obtain ⟨w', hw'₁, hw'₂⟩ := hX₂ hX₁.some (by apply Set.Nonempty.some_mem);
  existsi w';
  constructor;
  . simpa using hw'₂;
  . simpa [Satisfies];
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)
no goals