intro i
case intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
⊢ ∀ (i : Fin (X :: l ++ [Y]).length), (⌈⌈List.drop (↑i) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i)
case intro.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
δ_notEmpty : ¬δ = []
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
i : Fin (X :: l ++ [Y]).length
⊢ (⌈⌈List.drop (↑i) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i)