rcases X_rel_Y with ⟨n, claim⟩
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
β : Program
Y : { x // x ∈ Worlds }
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
X_rel_Y : ∃ n ys, X = ys.head ∧ Y = ys.last ∧ ∀ (i : Fin n), relate (↑MG) β (ys.get i.castSucc) (ys.get i.succ)
⊢ φ ∈ ↑Y
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