This module provides predicates for implementing dictionaries. Such dictionaries are currently implemented as ordered binary trees of key-value pairs.
D is a dictionary.
The dictionary node D has key K, value V, left child L, and right child R.
D contains value V at key K. If it was not already in D it is added.
D contains value V at key K. Fails if it is not already in D.
D and D1 are identical except for the element at key K, which in D1 contains value V, whatever has (or whether it is) in D.
D is a non-empty dictionary.