rw [← length_def]
case a.mk
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
val : ℕ
hyp : val < (l.append [Y]).length
lchain : ∀ i < δ.length, True
IHδ :
  ∀ d ∈ δ,
    ∀ (a : Finset Formula) (b : a ∈ Worlds) (a_1 : Finset Formula) (b_1 : a_1 ∈ Worlds) (φ' : Formula),
      (⌈d⌉φ') ∈ a → relate (↑MG) d ⟨a, b⟩ ⟨a_1, b_1⟩ → φ' ∈ a_1
help1 : l.length + ([].length + 1) = δ.length
IH : (⌈⌈List.drop val δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get ⟨val, ⋯⟩)
⊢ val < δ.length
case a.mk
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
val : ℕ
hyp : val < (l.append [Y]).length
lchain : ∀ i < δ.length, True
IHδ :
  ∀ d ∈ δ,
    ∀ (a : Finset Formula) (b : a ∈ Worlds) (a_1 : Finset Formula) (b_1 : a_1 ∈ Worlds) (φ' : Formula),
      (⌈d⌉φ') ∈ a → relate (↑MG) d ⟨a, b⟩ ⟨a_1, b_1⟩ → φ' ∈ a_1
help1 : l.length + ([].length + 1) = δ.length
IH : (⌈⌈List.drop val δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get ⟨val, ⋯⟩)
⊢ val < l.length + 1