WIP: Remove `contractive_ne` and `contractive_proper` as instances.
This is a follow up of !454 (merged). It closes #321.
It removes contractive_ne
and contractive_proper
as instances, to be consistent with ne_proper
. For all functions that are contractive, we already defined the corresponding NonExpansive
and 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 contractive_ne
and contractive_proper
as Hint Immediate
so they are only used at the leaves of type class search. I have done a similar thing for proper_ne
and proper_ne_2
.