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