Got a top level repl theorem in the basis env

There is 1 cheat in replCorrect dealing with bytecode termination. There
are 2 cheats in initialProgram, 1 dealing with bytecode termination, and
1 because we can no longer CBV_CONV the primitive program's bytecode
program, but we need that concretely to establish the primitive
program's invariant.