apply plus_Y
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⟩
plus_Y : P ∈ ↑⟨Y, Y_in⟩ → evaluate ↑MG ⟨Y, Y_in⟩ P
right✝ : (~P) ∈ ↑⟨Y, Y_in⟩ → ¬evaluate ↑MG ⟨Y, Y_in⟩ P
oh_a : ∀ (φ : Formula), (⌈a⌉φ) ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), relate (↑MG) a X Y → φ ∈ ↑Y
⊢ evaluate ↑MG ⟨Y, Y_in⟩ 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⟩
plus_Y : P ∈ ↑⟨Y, Y_in⟩ → evaluate ↑MG ⟨Y, Y_in⟩ P
right✝ : (~P) ∈ ↑⟨Y, Y_in⟩ → ¬evaluate ↑MG ⟨Y, Y_in⟩ P
oh_a : ∀ (φ : Formula), (⌈a⌉φ) ∈ ↑X → ∀ (Y : { x // x ∈ Worlds }), relate (↑MG) a X Y → φ ∈ ↑Y
⊢ P ∈ ↑⟨Y, Y_in⟩