refactor: deriving DecidableEq to use termination_by structural

[nomeata]

now that we support structural mutual recursion, I expect that every
DecidableEq instance be implemented using structural recursion, so
let's be explicit about it.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 93fa9c8837e071a866b62e2ca73c22a362ccb988 --onto 5938dbbd14145c9b78f7645c4777f62a3fc8212c. (2024-07-25 10:18:58)
• ✅ Mathlib branch lean-pr-testing-4826 has successfully built against this PR. (2024-07-29 15:24:55) View Log

[nomeata]

@arthur-adjedj, what do you think about this change?

[arthur-adjedj]

I think ensuring good reduction on decide is desirable, so I'm all for this. Some other derive handlers such as BEq and Hashable might also benefit from having them forcibly be structural, but I'm not so certain it would be useful enough to impose it.

[nomeata]

I guess I’ll wait until we have a nighty-with-mathlib and see if it survives testing against mathlib :-)