constructor
case h
p q r : Prop
s t u : Set ℕ
x : ℕ
⊢ x ∈ (s ∪ t) ∩ u ↔ x ∈ s ∩ u ∪ t ∩ u
case h.mp
p q r : Prop
s t u : Set ℕ
x : ℕ
⊢ x ∈ (s ∪ t) ∩ u → x ∈ s ∩ u ∪ t ∩ u

case h.mpr
p q r : Prop
s t u : Set ℕ
x : ℕ
⊢ x ∈ s ∩ u ∪ t ∩ u → x ∈ (s ∪ t) ∩ u