rework repl_fun again, and push the proofs further

The problem was that the initial bytecode should not be run, it should
just be there. So, now we don't start the REPL with empty_bc_state but
rather with (strip_labels initial_bc_state). (This is better than the
alternative of having the main loop check whether it's in the initial
case every time before deciding whether to run the code.)

Also, fixed some mistakes in the definition of main_loop after the
unrolled stage, and prove the unrolled version correct. The statement
mentions the output from running the basis program - somewhere we will
have to prove that that is empty...