new theorem for code_labels

plan is to both check the ptree and check the result in a single pass
down the code. (both can be computed outside the logic.) the theorem
proved justifies the sufficiency of doing the check.

labels_computeLib not updated.