fix: improve proof search in IndPredBelow

[nomeata]

MVarId.apply is clever in the order it returns mvars, by putting those
arising from non-dependent arguments first. If we lean on that behavior,
this fixes #1672.

H'T to @DanielFabian, this was found together in a call.

Also improves tracing.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2024-07-26 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2024-07-26 09:52:04)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f830fc9f4dae8b4d4719b9e886b41a4e2343ddf5 --onto bb9c9bd99f4e81b6199573351a1372482d76541b. (2024-07-28 19:16:12)

[nomeata]

Ok, we now get test failures because the .brecOn construction succeeds now (previously it was failing silently), and then the function definitions compilation fails in a way that #4827 is likely to fix. So I’ll wait here for that (or its variant #4839).

[nomeata]

This change broke some other tests, until I added the reverse here; now the existing tests succeed. 🤷

Note to my future self:

I wonder if this just means that for any order of mvars we’ll have examples where it fails, or if there is really a reason why this order is good™. I’ll have to come back to this and think about it some more.

Maybe I’ll also investigate if we avoid proof search here and build the necessary terms direct, relying on the structure of the .ibelow construction.