simp only [instBot, Subtype.forall, Q, relate] at *
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
this : ∀ (X Y : { x // x ∈ Worlds }), Q (↑MG).Rel β X Y → relate (↑MG) β X Y
⊢ Q (↑MG).Rel (α⋓β) X Y → relate (↑MG) (α⋓β) X Y
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X Y : { x // x ∈ Worlds }
α β : Program
this✝ :
  ∀ (a : Finset Formula) (b : a ∈ Worlds) (a_1 : Finset Formula) (b_1 : a_1 ∈ Worlds),
    Q (↑MG).Rel α ⟨a, b⟩ ⟨a_1, b_1⟩ → relate (↑MG) α ⟨a, b⟩ ⟨a_1, b_1⟩
this :
  ∀ (a : Finset Formula) (b : a ∈ Worlds) (a_1 : Finset Formula) (b_1 : a_1 ∈ Worlds),
    Q (↑MG).Rel β ⟨a, b⟩ ⟨a_1, b_1⟩ → relate (↑MG) β ⟨a, b⟩ ⟨a_1, b_1⟩
⊢ Q (↑MG).Rel α X Y ∨ Q (↑MG).Rel β X Y → relate (↑MG) α X Y ∨ relate (↑MG) β X Y