cases α_def : α <;> intro Y X_rel_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
case atom_prog
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

case sequence
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝¹ a✝ : Program
α_def : α = (a✝¹;'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (a✝¹;'a✝) X Y
⊢ φ ∈ ↑Y

case union
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝¹ a✝ : Program
α_def : α = (a✝¹⋓a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (a✝¹⋓a✝) X Y
⊢ φ ∈ ↑Y

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

case test
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
⊢ φ ∈ ↑Y