Функция multiset в Dafny

Еще одна недокументированная возможность Dafny - функция multiset. Она принимает один аргумент - seq - и возвращает "мультимножество", в котором есть ровно те же элементы, что и в seq'е, но без какого-либо порядка. Ее можно использовать для спецификации свойств перестановок элементов seq'а.