update labels_computeLib with improved approach

leaving the code_labels_ok assumption on the proved theorem to be
discharged by someone else later: it should come from compile_dec(s)_thm.