Mark projections for sigTO as NonExpansive and Proper
Not urgent (can wait till after POPL).
These changes are logically part of the recent addition of sigTO. I'm using
projT1_ne, but I added the other ones for completeness. One of these lemmas (
projT2_proper) depends on UIP, since it's almost a rephrasing of