let Z := YS.get 1
case intro.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
⊢ φ ∈ ↑Y
case intro.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
m : ℕ
innerIH :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin m), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
YS : Vector { x // x ∈ Worlds } (m + 1).succ
X_def : X = YS.head
Y_def : Y = YS.last
relSteps : ∀ (i : Fin (m + 1)), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
Z : { x // x ∈ Worlds } := YS.get 1
⊢ φ ∈ ↑Y