intro h
case pos.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 : F.World
a✝ : hX₁.some ≺ x
hxs : x ∈ X
y : F.World
hy₁ : y ∈ X
hy₂ : F.Rel x y
⊢ (∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w' (atom default)) →
    Satisfies { Frame := F, Valuation := fun w x => w ∉ X } x (atom default)
case pos.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 : F.World
a✝ : hX₁.some ≺ x
hxs : x ∈ X
y : F.World
hy₁ : y ∈ X
hy₂ : F.Rel x y
h : ∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w x => w ∉ X } w' (atom default)
⊢ Satisfies { Frame := F, Valuation := fun w x => w ∉ X } x (atom default)