Develop theory of finite sets, using developing transfer library

Use our existing quotient library to create new type, but then
transfer theorems using new technology.

New entry-points in transferLib are mostly there to make debugging
easier.

Polish some fmspTheory results

More results about the finite-map/sptree connection

I haven't forced it be a bijection (i.e, finite maps are allowed to be
related to non-wellformed sptrees), in the hope that I will still to
be able to figure out a good way of translating recursive
definitions.

Also put src/transfer into build sequence

Remove flagged Unicode from previous commit

Start theories necessary to do "transfer" between fmaps and sptrees

This being "transfer" in the style of the Isabelle package (Huffman
and Kunčar).