case atom_prog =>
  simp only [instBot, Q, relate, imp_self]
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
a✝ : ℕ
⊢ Q (↑MG).Rel (·a✝) X Y → relate (↑MG) (·a✝) X Y
no goals