prove compile_special_thm

weaken the statement to talk about the intLang version of the code not
having any labels, rather than trying to push no_functions at the source
level all the way down. hopefully this will be easy to evaluate for our
usage anyway.