use δ
case refl.a.h
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ a✝ : Formula
Y : { x // x ∈ Worlds }
δ : List Program
boxP_in_X : (⌈?'a✝⌉φ) ∈ ↑Y
X_rel_Y : X = Y ∧ evaluate (↑MG) X a✝
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑Y → P ∈ ↑Y) ∧
      (P⋀Q ∈ ↑Y → P ∈ ↑Y ∧ Q ∈ ↑Y) ∧
        ((~P⋀Q) ∈ ↑Y → (~P) ∈ ↑Y ∨ (~Q) ∈ ↑Y) ∧
          ((⌈α⌉P) ∈ ↑Y → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑Y) ∧
            ((~⌈α⌉P) ∈ ↑Y → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑Y)
X_δ_Y : relateSeq (↑MG) δ Y Y
ℓ : TP (?'a✝)
Xset_sub_X : ∀ (x : Formula), (x ∈ F (?'a✝) ℓ ∨ ∃ a ∈ P (?'a✝) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑Y
X_F : ∀ τ ∈ F (?'a✝) (⋯ ▸ ℓ), evaluate (↑MG) Y τ
δ_in_P : δ ∈ P (?'a✝) (⋯ ▸ ℓ)
⊢ ∃ a ∈ P (?'a✝) ℓ, (⌈⌈a⌉⌉φ) = ⌈⌈δ⌉⌉φ
no goals