rw [← length_def]
case h.e'_3.h.e'_3.h.e'_2.h.e'_1
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain✝ :
  ∀ (i : ℕ) (h : i < (((?'⊤) :: δ).zip (X :: (l ++ [Y]))).length - 1),
    pairRel (↑MG) ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i, ⋯⟩)
      ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i + 1, ⋯⟩)
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
lchain : relate (↑MG) (δ.get ⟨↑i, ⋯⟩) (((?'(~bottom), X) :: δ.zip (l ++ [Y])).get ⟨↑i, ⋯⟩).2 ((l ++ [Y]).get ⟨↑i, ⋯⟩)
⊢ δ.length = (l ++ [Y]).length
case h.e'_3.h.e'_3.h.e'_2.h.e'_1
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
δ : List Program
φ : Formula
l : List { x // x ∈ Worlds }
length_def : l.length + 1 = δ.length
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
i : Fin (l.append [Y]).length
lchain✝ :
  ∀ (i : ℕ) (h : i < (((?'⊤) :: δ).zip (X :: (l ++ [Y]))).length - 1),
    pairRel (↑MG) ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i, ⋯⟩)
      ((((?'⊤) :: δ).zip (X :: (l ++ [Y]))).get ⟨i + 1, ⋯⟩)
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
IH : (⌈⌈List.drop (↑i.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get i.castSucc)
help1 : (l.append [Y]).length = δ.length
lchain : relate (↑MG) (δ.get ⟨↑i, ⋯⟩) (((?'(~bottom), X) :: δ.zip (l ++ [Y])).get ⟨↑i, ⋯⟩).2 ((l ++ [Y]).get ⟨↑i, ⋯⟩)
⊢ l.length + 1 = (l ++ [Y]).length