Mark projections for sigTO as NonExpansive and Proper

Merged Paolo G. Giarrusso requested to merge Blaisorblade/iris:sigTO_proper_projs into master

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.

Edited by Paolo G. Giarrusso

Merge request reports