This is in preparation for coq/coq#9274.

Two reasons:

- The equality makes it very hard to use the lemma with `rewrite`.
- The version for lists `insert_zip_with` does not have the equality either.

Adding a hint without a database now triggers a deprecation warning in
Coq master (https://github.com/coq/coq/pull/8987).

- Interaction with delete
- Make name about map interacting with insert consistent.

This makes some proress on #21. Still, the question remains if a more
generic solution exists.

Works around Coq bug #7731