case star α =>
  simp only [instBot, Q, relate]
  apply Relation.ReflTransGen.lift
  intro a b Qab
  exact Q_then_relate MG α a b Qab
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α : Program
⊢ Q (↑MG).Rel (∗α) X Y → relate (↑MG) (∗α) X Y
no goals