subst X_def Y_def
case intro.zero.intro.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (Nat.succ 0)
X_def : X = YS.last
Y_def : Y = YS.last
right✝ : ∀ (i : Fin 0), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
this : YS.head = YS.last
⊢ φ ∈ ↑Y
case intro.zero.intro.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
φ : Formula
YS : Vector { x // x ∈ Worlds } (Nat.succ 0)
right✝ : ∀ (i : Fin 0), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
this : YS.head = YS.last
boxP_in_X : (⌈∗β⌉φ) ∈ ↑YS.last
⊢ φ ∈ ↑YS.last