Spec Example 2.25. Unordered Sets