tell lem to suppress renaming in compiler and metatheory

the rename of count to count0 was breaking some proofs. probably we
don't ever want lem to do renaming.
delete some broken proofs that got re-introduced during a merge

they were commented out in 60245dac; the commented out copy remains.
comment out more code_labels_ok stuff

hoping these theorems never become necessary
fix proof of compile_initial_prog_thm

it needed to be updated for the new part of the invariant saying the
code always contains the VfromList code.