First see ../../README. In this directory, BinaryTries.hs illustrates properties quantified over functions and requiring the unique existence of a data-structure. Two different trie representations are defined for sets of bitstrings. The properties state that each set has a unique representation as a trie -- true for the second representation, but not for the first. The properties are specified using functions with boolean results as a pure representation of sets, independent of any data structure. Compile or interpret BinaryTries.main for the self-introducing tests.