intro X φ boxP_in_X
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
⊢ ∀ (X : { x // x ∈ Worlds }) (φ : Formula), (⌈α⌉φ) ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), relate (↑MG) α X Y → φ ∈ ↑Y
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
⊢ ∀ (Y : { x // x ∈ Worlds }), relate (↑MG) α X Y → φ ∈ ↑Y