licenses: convert license tags to SPDX

lib/FastMap: add FIXME for conv_at hack

lib: move FastMap lemma to LemmaBucket

lib/FastMap: fix primrec style

lib/FastMap: refactor convs; renaming; juggle function arguments

Complex conversions have been refactored to the new utility conv_at,
which is easier to use and has better error detection.

Name changes: “*_to_map” naming scheme changed to more descriptive
“*_to_lookup_list”.

Key transformer argument is now the first argument to tree_lookup and
friends, which matches functional programming conventions.

lib/FastMap: use simple locale instead of unnecessary qualify

lib: add FastMap tool

Many issues remain (see TODO list), but it's now mature enough to be
used for proof automation and has a comprehensive test suite.