subst α_def
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a : ℕ
α_def : α = ·a
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (·a) X Y
⊢ φ ∈ ↑Y
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
a : ℕ
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (·a) X Y
boxP_in_X : (⌈·a⌉φ) ∈ ↑X
⊢ φ ∈ ↑Y