refactor: termination arguments as Expr, not Syntax

[nomeata]

Before, the termination argument as inferred by GuessLex was passed further
on as Syntax, to be elaborated later in WF.Rel.

This didn’t feel quite right anymore. In particular if we want to teach
GuessLex about guessing more complex termination arguments like xs.size - i, using Expr here is more natural.

So this introduces TerminationArgument based on an Expr to be used here.

A side-effect of how the termination arguments are elaborated is that the unused
variables linter will now look at termination_by variables, and that parameters
past the colon are not even invisibly in scope, so ‹_› will not find them
See https://github.com/leanprover-community/mathlib4/pull/11370/files for examples
of fixing these changes.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1388f6bc83b5ea085fe14faa1db213e745c3e398 --onto 32dcc6eb895b58df3d3241a2521963e64995b621. (2024-03-12 14:43:12)
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 995726f75fd7eed223c2189a54f6df3293185327 --onto 317adf42e92a4dbe07295bc1f0429b61bb8079fe. (2024-03-14 14:08:25)
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 795e332fb37729f013c9a66b211fd45e5c90a1f9 --onto 317adf42e92a4dbe07295bc1f0429b61bb8079fe. (2024-03-14 17:01:16)