Start a medium-sized refactoring of the semantics

Instead of a custom env type in the lib.lem, use finite maps where
possible and alists and ALOOKUP where not.
Fix semantics/proofs

Except for 2 lemmas about bootstrapping in evalPropsScript
Some more progress.

Mostly un-finite mapping things. A surprising amount depends on being
able to access various shadowed bindings.
Slow progress fixing the type soundness proof
Progress on type soundness repairs.
Metatheory repaired
Mostly fix translator

Commented out

DeclAssumCons_SNOC_Dtype
DeclAssumCons_cons_lookup

because of the change of type of the constructor environments from lists
to finite maps. Correspondingly, DeclAssumCons lost an ALL_DISTINCT
assumption. I don't know why it was there, unless it was an artifact
from the past when duplicate constructors causes the evaluation to type
error.
Started on the type inference refactoring.
More inferencer repairs
Repaired inference proof
Progress of the compiler proofs
More compiler proof repairs
Work on fixing conLangProofs
More progress. Stop printing constructors definitions.

now that the constructor environment is an fmap instead of a list,
printing constructor definitions is not so simple. However, it's also a
rather pointless thing to do...
uncomment two theorems in evalPropsScript.sml

the statements changed slightly, so wherever these theorems are used
will probably need fixing at some point too.
Fix compiler
Fix repl correct
Merge remote-tracking branch 'origin/master' into fmap_refactor
Fix
Fix ml_translatorScript

Fix the two commented out lemmas. But the translator doesn't work.