feat: allow decidable equality for empty lists and empty arrays

[robsimmons]

This PR adds support for decidable equality of empty lists and empty arrays. Decidable equality for lists and arrays is suitably modified so that all diamonds are definitionally equal.

Following #9302, the strong condition of definitionally equal under with_reducible_and_instances is tested. This also moves some of the comments added in #9302 out of docstrings.

[robsimmons]

!bench

[leanprover-radar]

Benchmark results for a90f7a6 against 5a4226f are in! @robsimmons

Major changes (2)

• Init.Prelude async//instructions changed by +1.0% (🟥).
• stdlib//instructions changed by +7.3% (🟥).

Minor changes (1)

• parser//instructions changed by +0.8% (🟥).

[kim-em]

(Let's make sure to test against Mathlib before merging this one.)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-11-18 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-11-19 23:08:15)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 5c8ebd886873c3c476a4a6729bb850d5f571b8d7 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-20 03:25:38)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 51b67385cc0cd2613764ee4607957fef1f06128b --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-20 20:19:24)

[robsimmons]

@kim-em in addition to waiting for mathlib, I won't merge this one until I either figure out how to make the array instances defeq or just remove the array coercion

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-11269 has successfully built against this PR. (2025-11-20 00:17:57) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5c8ebd886873c3c476a4a6729bb850d5f571b8d7 --onto 5a4226f2bdcc6299df76285b1d30f238546c09fe. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-20 03:25:37)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 51b67385cc0cd2613764ee4607957fef1f06128b --onto a106ea053fec080a50204b0ad6dadc69bc3f0937. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-20 20:19:23)