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 sigT_equiv_eq_alt.