simpa using hw'₂
case intro.intro.right.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
hw'₁ : w' ∈ X
hw'₂ : F.Rel hX₁.some w'
⊢ hX₁.some ≺ w'
no goals