Ah, I thought this wasn't necessarily the case (e.g. adjoining an item to a set that already has the item), but if we allow the returned object to be passed to mutating procedures, this guarantee is indeed necessary.