case zero =>
  simp_all only [instBot, insTop, List.cons_append, List.zip_cons_cons, Subtype.forall,
    List.length_cons, Nat.succ_eq_add_one, Fin.val_zero, List.drop_zero, List.get_cons_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)
no goals