apply Set.ext
α : Sort u_2
β : Sort u_1
γ : ?m.19374
f : α → Set β
s t : Set α
⊢ (s.union t).bind f = (s.bind f).union (t.bind f)
case a
α : Sort u_2
β : Sort u_1
γ : ?m.19374
f : α → Set β
s t : Set α
⊢ ∀ (x : β), x ∈ (s.union t).bind f ↔ x ∈ (s.bind f).union (t.bind f)