simp only [instBot, relate] at X_rel_Y
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
a : ℕ
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (·a) X Y
boxP_in_X : (⌈·a⌉φ) ∈ ↑X
⊢ φ ∈ ↑Y
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ : Formula
a : ℕ
Y : { x // x ∈ Worlds }
boxP_in_X : (⌈·a⌉φ) ∈ ↑X
X_rel_Y : (↑MG).Rel a X Y
⊢ φ ∈ ↑Y