An interesting issue arose in verifying the ghc_sort benchmark, in that I needed to establish the output array was a permutation of the input array. This can be done in Dafny using a multiset. I'm wondering what we can do here. Perhaps adding ArrayMultiSet or similar.