more work on invariant preservation

have reduced some of the closed_context stuff to goals that might be
provable from the type_soundness_invariants assumption.