- ownI_proper for inv
- later_contractive for later_ne
anymore. Instead we use (contractive_proper _) and (contractive_ne _).

Instead we can use (contractive)