simp_all only [instBot, insTop, List.zip_cons_cons, Subtype.forall, List.append_eq,
  Fin.castSucc_mk, boxes, Fin.cast_mk]
case 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
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'
help1 : (l.append [Y]).length = δ.length
val✝ : ℕ
isLt✝ : val✝ < (l.append [Y]).length
IH : (⌈⌈List.drop (↑⟨val✝, isLt✝⟩.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get ⟨val✝, isLt✝⟩.castSucc)
this : List.drop (↑⟨val✝, isLt✝⟩) δ = δ.get ⟨↑⟨val✝, isLt✝⟩, ⋯⟩ :: List.drop (↑⟨val✝, isLt✝⟩ + 1) δ
⊢ (⌈⌈δ.get (Fin.cast help1 ⟨val✝, isLt✝⟩) :: List.drop (↑⟨val✝, isLt✝⟩ + 1) δ⌉⌉φ) =
    ⌈⌈δ.get ⟨↑⟨val✝, isLt✝⟩, ⋯⟩ :: List.drop (↑⟨val✝, isLt✝⟩ + 1) δ⌉⌉φ
no goals