specialize i X
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P_in_X : bottom ∈ ↑X
val✝ : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝¹ : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) val✝
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) val✝
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) val✝
⊢ bottom ∉ ↑X
case left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
P_in_X : bottom ∈ ↑X
val✝ : KripkeModel { x // x ∈ Worlds }
left✝¹ : (fun M => ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p) val✝
left✝ : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) val✝
right✝ :
  (fun M => ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q M.Rel α X Y ∧ (~P) ∈ ↑Y) val✝
i : saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
⊢ bottom ∉ ↑X