have := Q_then_relate MG α
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
⊢ Q (↑MG).Rel (α;'β) X Y → relate (↑MG) (α;'β) X Y
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
this : ∀ (X Y : { x // x ∈ Worlds }), Q (↑MG).Rel α X Y → relate (↑MG) α X Y
⊢ Q (↑MG).Rel (α;'β) X Y → relate (↑MG) (α;'β) X Y