Skip to content

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

Merge request reports