cases α
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X Y : { x // x ∈ Worlds }
⊢ Q (↑MG).Rel α X Y → relate (↑MG) α X Y
case atom_prog
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
a✝ : ℕ
⊢ Q (↑MG).Rel (·a✝) X Y → relate (↑MG) (·a✝) X Y

case sequence
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
a✝¹ a✝ : Program
⊢ Q (↑MG).Rel (a✝¹;'a✝) X Y → relate (↑MG) (a✝¹;'a✝) X Y

case union
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
a✝¹ a✝ : Program
⊢ Q (↑MG).Rel (a✝¹⋓a✝) X Y → relate (↑MG) (a✝¹⋓a✝) X Y

case star
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
a✝ : Program
⊢ Q (↑MG).Rel (∗a✝) X Y → relate (↑MG) (∗a✝) X Y

case test
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
a✝ : Formula
⊢ Q (↑MG).Rel (?'a✝) X Y → relate (↑MG) (?'a✝) X Y