install code for Cons
fix broken proof
updated repl_step and made repl_fun use real_inst_length

I had to cheat a proof in replCorrect because I
can't start an interactive session for replCorrectScript.sml
to fix the issue.