open Or in intro
| inl hs => left; left; exact hs
| inr (inl ht) => left; right; exact ht
| inr (inr hu) => right; exact hu
case a.mpr
α : Sort u_1
β : ?m.18244
γ : ?m.18247
s t u : Set α
x : α
⊢ x ∈ s.union (t.union u) → x ∈ (s.union t).union u
no goals