rework treatment of initial bytecode state

make empty_bc_state actually empty, and use labelled_repl_step to make
the transition between empty_bc_state and initial_bc_state (which
contains VfromListCode).

also, realise that repl is non-deterministic because of the type error
mask, so we can't get the nice repl theorem in the "proof aim", and will
have to settle for one direction of the bi-implication until
type-inferencer completeness is proved.