open Or in intro
| inl (inl hs) => exact inl hs
| inl (inr ht) => exact inr (inl ht)
| inr hu => exact inr (inr hu)
case a.mp
α : 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