Work on updating replCorrect, and trying to prove things.

The proof for a subgoal about type inferencer invariant preservation
stopped working.

Some of the remaining cheats look pretty scary, especially involving
divergence. But this could be because I haven't yet thought about how
all that is going to fit together.