all_goals simp
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ (⌈a⌉P) ∈ ↑X → evaluate (↑MG) X (⌈a⌉P)

case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ (~⌈a⌉P) ∈ ↑X → ¬evaluate (↑MG) X (⌈a⌉P)
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ (⌈a⌉P) ∈ ↑X → ∀ (a_2 : Finset Formula) (b : a_2 ∈ Worlds), relate (↑MG) a X ⟨a_2, b⟩ → evaluate ↑MG ⟨a_2, b⟩ P

case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
a : Program
P : Formula
⊢ (~⌈a⌉P) ∈ ↑X → ∃ x, ∃ (h : x ∈ Worlds), relate (↑MG) a X ⟨x, ⋯⟩ ∧ ¬evaluate ↑MG ⟨x, ⋯⟩ P