yet another approach to code_labels_conv

don't precompute FLOOKUP theorems for the finite map, but use
flookup_fupdate_conv to compute each particular application of FLOOKUP
during the inst_labels on the fly. this is unlikely to be faster unless
the Labs are very sparse in the code (e.g. much fewer than the total
number of labels). I would think in fact there are many _more_ Labs,
unfortunately.
use Net.index instead of Net.match

only trying to find a single thing in the net with an exact match, so
this should be ok, maybe faster
make code_labels_conv delete the internal constants it defines

they are used to hide the tail of the list as it is being recursed on;
but the final theorem produced doesn't retain the hiding constants, so
they don't need to be saved.