Move comparisonTheory to src/enumfset

(from examples/balanced_bst)

Prove a theorem relating most of the definitions in comparisonTheory to
something in totoTheory.

Also, add a new definition for inverting cpns.

Make the overloads on the constructors of cpn permanent in
comparisonTheory.

Turn on totoTheory's "BigSig" to get more useful exports.

This is work towards integration, but the approach has been towards
plurality, i.e. keeping multiple definitions around and proving
relationships between them. More integration could be possible. Also,
the dependency between toto and comparison could be flipped (I wanted to
write new proofs in the nicer environment of comparison so did not do
that.) It has become apparent that totoTheory is in various minor ways
not self-consistent (esp. with regard to its naming schemes).