induction n generalizing X φ
case intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
β : Program
Y : { x // x ∈ Worlds }
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
n : ℕ
claim : ∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin n), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)
⊢ φ ∈ ↑Y
case intro.zero
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
claim : ∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin 0), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)
⊢ φ ∈ ↑Y

case intro.succ
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
β : Program
Y : { x // x ∈ Worlds }
n✝ : ℕ
a✝ :
  ∀ (X : { x // x ∈ Worlds }) (φ : Formula),
    (⌈∗β⌉φ) ∈ ↑X →
      (∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin n✝), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)) → φ ∈ ↑Y
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
claim : ∃ ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin (n✝ + 1)), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)
⊢ φ ∈ ↑Y