Need doc fix
"ordered list of pairs" means (probably) "ordered by natural order of keys"
It should be:
"Bi-directional mapping between Dict and the pair (Tag, Pairs), where Pairs is an ordered list of pairs **if Pairs is ouput**"
The predicate doesn't care about ordering when Pairs is input. Duplicate keys, however, lead to an exception.
When verifying Pairs against Dict, the order matters. Duplicates in Pairs lead to failure.