Work on repl correct

1) reverted recent change to bytecode compset, since we don't actually
need to evaluate bytecode.

2) got rid of repl_fun, and replaced with repl_fun_alt

3) added simple_repl_fun, which corresponds to the old repl_fun'

4) renamed the old repl_fun_alt' to repl_fun'

All of the repl_funs now are parameterised over the initial state.

Thus repl_fun runs a bytecode problem from an empty state before
executing the user's program. repl_fun' is the same, but with some kind
of invariant tracking baked in. simple_repl_fun starts from an initial
bytecode state that already has the initial bytecod program evaluated.

Proved that if the initial envs are good, then the simple_repl_fun
implements the repl. Unfortunately the theorem relating simple_repl_fun
to repl_fun' is of the form simple_repl_fun ==> repl_fun', whereas I
wanted the implication in the other direction so that I could use the
existing replCorrect_lem, which is in terms of simple_repl_fun, and know
that repl_fun' (and hence repl_fun) implements the repl semantics. I
think these two should be equal.

Also added some lemmas about how the invariant from initialProgram
relates to the invariant from replCorrect.