induction i using Fin.inductionOn
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
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
i : Fin (X :: l ++ [Y]).length
⊢ (⌈⌈List.drop (↑i) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i)
case zero
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
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
⊢ (⌈⌈List.drop (↑0) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get 0)

case succ
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
lchain : List.Chain' (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
i✝ : Fin (l.append [Y]).length
a✝ : (⌈⌈List.drop (↑i✝.castSucc) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i✝.castSucc)
⊢ (⌈⌈List.drop (↑i✝.succ) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i✝.succ)