Some tweaks.

The plan is to have a series of initial programs. The first just defines
primitive types and exceptions that the compiler needs to know about,
the second will be the rest of the supported basis library, and
subsequent ones (if any) will include any other definitions that should
be in place before the user's program. For example, to support a REPL
with the HOL light kernel already loaded.

Each of the type inference, type soundness, and compiler correctness
proofs rely on an invariant about the various environments and other
inputs that they consume. We can construct these environments by EVALing
the inferencer and compiler on the first initial program, and then
manually proving that the result satisfies the invariant (the completely
empty environments that we will pass to the inferencer/compiler in the
EVAL won't satisfy the invariant). The subsequent initial programs can
be EVALed in the same way (starting from the previously built
initial env), but we can use the inferencer/compiler correctness proofs
to know that the new additions still satisfy the invariants.