Add tactics `destruct select <pat>` and `destruct select <pat> as <intro_pat>`.

These tactics are consistent with existing tactics like revert select and rename select.

mentioned in merge request iris!757 (merged)

added 1 commit

• 589bf0af - CHANGELOG.

Compare with previous version

added 5 commits

• 589bf0af...d9e55d3d - 2 commits from branch master
• a1272450 - Add tactics `destruct select`.
• 723ad25f - Add test for `destruct select`.
• 924782c8 - CHANGELOG.

Compare with previous version

LGTM.

merged

mentioned in commit cf7c2c41