rcases i X with ⟨X_saturated, _, _⟩
case right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
notnotQ_in_X : (~~Q) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝¹ : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
left✝ : ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y
right✝ : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
⊢ evaluate (↑⟨M, ⋯⟩) X Q
case right.intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q : Formula
notnotQ_in_X : (~~Q) ∈ ↑X
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
left✝¹ : ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y
right✝¹ : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
X_saturated : saturated ↑X
left✝ : ⊥ ∉ ↑X
right✝ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
⊢ evaluate (↑⟨M, ⋯⟩) X Q