Add NoDup_bind, vec_enum, vec_finite (new version with proper branch)

Follow up of !451 (closed), but with a branch where I can push.

mentioned in merge request !451 (closed)

changed the description

added 9 commits

• 68d3ec4a...504d165a - 2 commits from branch master
• 44909b3e - Add NoDup_bind, vec_enum, vec_finite.
• c5e00341 - Remove unused names.
• 34812f05 - Tweak proofs.
• 984ee08e - Add `vec_card`.
• 20ad7f5a - Tweak proof of `prod_finite` based on idea from !451 (closed).
• 8470893a - Tweak proof of `list_finite`.
• 28143e23 - CHANGELOG.

Compare with previous version

added 19 commits

• 28143e23...a1765eda - 12 commits from branch master
• f7db3225 - Add NoDup_bind, vec_enum, vec_finite.
• 2c49aef9 - Remove unused names.
• 8334a418 - Tweak proofs.
• e01705cf - Add `vec_card`.
• 919087b3 - Tweak proof of `prod_finite` based on idea from !451 (closed).
• a91ccac4 - Tweak proof of `list_finite`.
• 3c228d84 - CHANGELOG.

Compare with previous version

enabled an automatic merge when the pipeline for 3c228d84 succeeds

Going to merge.

merged

mentioned in commit cccb447d