rewrite labels_computeLib to make use of patricia trees

code_labels_conv now employs the strategy outlined in the previous
commit: create a patricia tree in ML, use the inst_labels_fn_intro
theorem to reduce the goal to a version of inst_labels working on a
patricia tree, prove the two hypotheses of that theorem by evaluation
(this is how we show the ptree is a good replacement for the finite
map), then evaluate.

not sure whether it's faster yet.
tweak timing/info printing output