Work on the translator.

Proved the theorems in ml_translateScript.sml up until they start
obviously dealing with the cenv. I guess these are likely to change
significantly, or be obsolete, now.