have ⟨_,⟨_,_,iii,_⟩⟩ := MG
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
a : ℕ
Y : { x // x ∈ Worlds }
boxP_in_X : (⌈·a⌉φ) ∈ ↑X
X_rel_Y : (↑MG).Rel a X Y
⊢ φ ∈ ↑Y
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
a : ℕ
Y : { x // x ∈ Worlds }
boxP_in_X : (⌈·a⌉φ) ∈ ↑X
val✝ : KripkeModel { x // x ∈ Worlds }
left✝¹ : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ val✝.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) val✝
right✝ : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, Q val✝.Rel α X Y ∧ (~P) ∈ ↑Y
X_rel_Y : (↑⟨val✝, ⋯⟩).Rel a X Y
⊢ φ ∈ ↑Y