It is doing much more than just dealing with ∈, it solves all kinds
of goals involving set operations (including ≡ and ⊆).