case union α β =>
  have := Q_then_relate MG α
  have := Q_then_relate MG β
  simp only [instBot, Subtype.forall, Q, relate] at *
  tauto
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
⊢ Q (↑MG).Rel (α⋓β) X Y → relate (↑MG) (α⋓β) X Y
no goals