intro x
case a
α : Sort u_1
β : ?m.20207
γ : ?m.20210
s t : Set α
⊢ ∀ (x : α), x ∈ s.inter t ↔ x ∈ t.inter s
case a
α : Sort u_1
β : ?m.20207
γ : ?m.20210
s t : Set α
x : α
⊢ x ∈ s.inter t ↔ x ∈ t.inter s