WIP: Remove `contractive_ne` and `contractive_proper` as instances.
contractive_proper as instances, to be consistent with
ne_proper. For all functions that are contractive, we already defined the corresponding
Proper instances, so these instances just caused type class search to try useless paths.
These instances are sometimes useful when considering a lemma or section with a
Contractive f parameter. Hence I added
Hint Immediate so they are only used at the leaves of type class search. I have done a similar thing for