prove a divergence-related subgoal of repl_correct_lem

(modulo requiring proofs about well-typed things being closed and not
containing "" constructors etc.)

In particular, this is the proof of the case when the bytecode diverges.
There is another divergence-related goal that I haven't touched yet:
when the bytecode doesn't diverge, I need to show that the semantics
doesn't diverge either.