Introduce `set_bind` and associated lemmas + set_bind theory: revise setoid rewriting

This is @dfrumin's !383 (closed) (with authorship preserved) + some tweaks to setoid rewriting:

• strengthen set_bind_subset to have the same arity
• add missing Params instance to prevent slow failures in setoid rewriting
• Proper instances can be proven before set_bind_ext via set_solver.
• set_bind_ext is then provable by set_solver directly.

I originally sent dfrumin/coq-stdpp!1 (closed) to be added into !383 (closed), but maybe it's easier with this MR? @robbertkrebbers up to you.

Modulo minor nits this looks good to me.

Could you add Dan and your name to the CHANGELOG so you get credit for this effort?

resolved all threads

added 1 commit

• 22569164 - Formatting review

Compare with previous version

added 42 commits

• 22569164...f844da54 - 35 commits from branch iris:master
• f4072243 - Introduce `set_bind` and associated lemmas.
• 13c3510c - Update the CHANGELOG
• bcc9161a - Apply some sugguestions from Robbert and Paolo
• feb655ce - set_bind theory: revise setoid rewriting
• 693458bb - set_bind_subset -> set_bind_mono
• db5e0008 - Formatting review
• 38a93520 - Add names to CHANGELOG

Compare with previous version

All done!

resolved all threads

Merging. And closing !383 (closed) in favor of this one.

enabled an automatic merge when the pipeline for 38a93520 succeeds

mentioned in merge request !383 (closed)

merged

mentioned in commit 42af9985