intro Y Y_in X_rel_Y
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
boxP_in_X : (⌈a⌉P) ∈ ↑X
⊢ ∀ (a_1 : Finset Formula) (b : a_1 ∈ Worlds), relate (↑MG) a X ⟨a_1, b⟩ → evaluate ↑MG ⟨a_1, b⟩ P
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
boxP_in_X : (⌈a⌉P) ∈ ↑X
Y : Finset Formula
Y_in : Y ∈ Worlds
X_rel_Y : relate (↑MG) a X ⟨Y, Y_in⟩
⊢ evaluate ↑MG ⟨Y, Y_in⟩ P