This also needs changes in type and continuation context inclusion. It allows us to prove that the empty sum is equal to the empty type. I also took the opportunity to rename TCtx_holds to TCtx_hasty, which at least says what is "holding".
