prove some theorems about uses_label and code_labels_ok

characterise uses_label in terms of a new constant inst_uses_label.
prove theorems for introducing code_labels_ok when consing or appending
onto code.
add code_labels_ok proof to various compiler functions

however, it will be impossible to prove this for compile_append_out,
since closure compilation may introduce references to labels that aren't
in the generated code - an additional hypotheses is needed to guarantee
that the labels are there, and they may be in previously generated code.
so may have to add the code_labels_ok conclusion to the main compiler
theorem instead... or add more hypotheses to compile_append_out...