have := ((MG.2.1 (YS.last)).1 φ φ (∗β)).right.right.right.left boxP_in_X
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
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
this : ∃ l, ((Xset (∗β) l φ).all fun y => decide (y ∈ ↑YS.last)) = true
⊢ φ ∈ ↑YS.last