case atom_prog a =>
  subst α_def
  simp only [instBot, relate] at X_rel_Y
  have ⟨_,⟨_,_,iii,_⟩⟩ := MG
  exact iii X Y _ _ X_rel_Y boxP_in_X
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a : ℕ
α_def : α = ·a
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (·a) X Y
⊢ φ ∈ ↑Y
no goals