have := Vector.exists_eq_cons YS
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.head
Y_def : Y = YS.last
right✝ : ∀ (i : Fin 0), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
⊢ YS.head = YS.last
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.head
Y_def : Y = YS.last
right✝ : ∀ (i : Fin 0), relate (↑MG) β (YS.get i.castSucc) (YS.get i.succ)
this : ∃ a as, YS = a ::ᵥ as
⊢ YS.head = YS.last