rework replCorrect to talk about primed repl_fun; introduced cheats

the cheats are mainly about proving code_labels_ok and code_executes_ok.

the hardest one is showing that diverging code produces no output. i
don't know how to go about proving this; it would probably require
reworking the current correctness theorems quite a bit... maybe to add
this condition to all the timeout-related conclusions...

another one looks like a lot of tedious proof refactoring of
replCorrect_lem, to do all the invariant preservation in one place and
then use both of the conclusions of the inductive hypothesis at once.

the rest look not-too-bad.