intro
| ⟨x, inl hs, h⟩ => left; refine ⟨x, hs, h⟩
| ⟨x, inr ht, h⟩ => right; refine ⟨x, ht, h⟩
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.19374
f : α → Set β
s t : Set α
y : β
⊢ y ∈ (s.union t).bind f → y ∈ (s.bind f).union (t.bind f)
no goals