more work on repl_funProofTheory

fix error in definition of unlabelled_repl_fun (had an extra REVERSE).
move various bytecode-related theorems into bytecode (though some still
remain to be moved). work towards proving correctness of the
unlabelled_repl_fun (down to 1 fairly big cheat).