Fix to examples/countable in light of 92317114

move countableLib to examples/countable

Packaged it up to be more like a library plus accompanying theories. Not
ready for src/, perhaps, because the choice of names (all those "_aux"s)
and interface is perhaps a bit wacky. Also due to some errors coming
from deep in TFL I've resorted to using more genvars, so the definitions
and inductions of counting constants look uglier. (And it might be nice
to support records and to deforest the algorithm.)

The only use of countableLib is now in
examples/miniML/compiler/count_expScript.sml, where it proves that
various miniML syntax types are countable.