have satX := (MG.prop.1 X).left
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
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
satX : saturated ↑X
⊢ φ ∈ ↑Y