Various fixes

impl_proofs builds now, but much of replCorrect is commented out,
because all of compilerProofs is commented out.

Updated the inference soundness proofs for tuples, and proved that
the initial_program defined in repl_funScript evaluates to the right
initial environment.