prove theorem about RTC bc_next after compile_labels

probably in a very roundabout way - this took surprisingly long to prove.
start looking at the compiler part of the value case of repl_correct

amongst other things, looks like RTC_bc_next_compile_labels is the wrong
way around; could avoid proving it the other way by instead showing that
bc_eval is deterministic...