intro x
case a
α : Sort u_1
β : ?m.18244
γ : ?m.18247
s t u : Set α
⊢ ∀ (x : α), x ∈ (s.union t).union u ↔ x ∈ s.union (t.union u)
case a
α : Sort u_1
β : ?m.18244
γ : ?m.18247
s t u : Set α
x : α
⊢ x ∈ (s.union t).union u ↔ x ∈ s.union (t.union u)