move x64 repl_step correctness out as a separate theory

and prove one of the cheats in it - by changing the statement to include
a REVERSE around bootstrap_lcode