simp at X_rel_Y
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
β : Program
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (∗β) X Y
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
⊢ φ ∈ ↑Y
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
β : Program
Y : { x // x ∈ Worlds }
boxP_in_X : (⌈∗β⌉φ) ∈ ↑X
X_rel_Y : Relation.ReflTransGen (relate (↑MG) β) X Y
⊢ φ ∈ ↑Y