prove basis_repl_fun correct

this is the one that should be implemented by the machine-code.
we now have a theorem connecting it to repl (the semantics relation).
delete repl_fun_alt_proofScript.sml