Create set type
Having to add the non-duplicate constraint to lists is too low-level. I would like to have these two types of list, where the second one is known to contain no duplicates.
Variable l1: seq nat. Variable l2: set nat.
It would require using a record and defining the equality predicate for ssreflect. But if we keep it in a separate file in util/ it shouldn't affect readability.