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 sigT_equiv_eq_alt
.
Edited by Paolo G. Giarrusso