simp_all only [insTop, List.zip_cons_cons, List.length_cons, List.length_zip,
  List.length_append, List.length_singleton, min_self, Nat.succ_eq_add_one,
  add_tsub_cancel_right, instBot, List.get_cons_succ, List.get_zip, Subtype.forall,
  List.append_eq, Fin.castSucc_mk]
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
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'
help1 : (l.append [Y]).length = δ.length
val : ℕ
hyp : val < (l.append [Y]).length
IH : (⌈⌈List.drop (↑⟨val, hyp⟩.castSucc) δ⌉⌉φ) ∈ ↑((X :: (l ++ [Y])).get ⟨val, hyp⟩.castSucc)
⊢ ↑⟨val, hyp⟩ < (((?'⊤) :: δ).zip (X :: (l ++ [Y]))).length - 1
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