Re-enable check for non-unique taclet names and remove two taclet duplicates

[unp1]

Intended Change

Taclet names must be unique (per rule option). The corresponding check was commented out. This PR reenables the check and removes to duplicate taclets (identical taclets with equal names)

Type of pull request

• [x] Bug fix (non-breaking change which fixes an issue)
• [x] There are changes to the (Java) code
• [x] There are changes to the taclet rule base

Ensuring quality

• [x] I made sure that introduced/changed code is well documented (javadoc and inline comments).
• [x] I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
• [X] I have tested the feature as follows: Load several problems to check whether an exception is thrown due to non-unique names

Additional information and contact(s)

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

[codecov[bot]]

Codecov Report

Attention: 2 lines in your changes are missing coverage. Please review.

Comparison is base (d5b0917) 37.94% compared to head (174ae11) 37.93%.

Files	Patch %	Lines
.../uka/ilkd/key/proof/mgt/RuleJustificationInfo.java	33.33%	2 Missing :warning:

Additional details and impacted files

```diff @@ Coverage Diff @@ ## main #3359 +/- ## ============================================ - Coverage 37.94% 37.93% -0.01% + Complexity 17001 16997 -4 ============================================ Files 2059 2059 Lines 125973 125972 -1 Branches 21273 21273 ============================================ - Hits 47798 47791 -7 - Misses 72293 72298 +5 - Partials 5882 5883 +1 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.