add replDecsProofsScript.sml

and prove the first instantiated compiler correctness theorem.