exact Q_then_relate MG α a b Qab
case h
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α : Program
a b : { x // x ∈ Worlds }
Qab : Q (↑MG).Rel α a b
⊢ relate (↑MG) α a b
no goals