refactor: ArgsPacker

[nomeata]

This introduces the ArgsPacker module and abstraction, to replace the exising PackDomain/PackMutual code. The motivation was that we now have more uses besides Fix.lean (GuessLex and FunInd), and the code was spread in various places.

The goals are

• consistent function naming withing the the PSigma handling, the PSum handling, and the combined interface
• avoid taking a type apart just based on the PSigma/PSum nesting, to be robust in case the user happens to be using PSigma/PSum somewhere. Therefore, always pass an arity or numFuncs or varNames around.
• keep all the PSigma/PSum encoding logic contained within one module (ArgsPacker), and keep that module independent of its users (so no EqnInfos visible here).
• pick good variable names when matching on a packed argument
• the unary function now is either called fun1._unary or fun1._mutual, never fun1._unary._mutual.

This file has less heavy dependencies than PackMutual had, so build parallelism is improved as well.

[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 f0a762ea4d2a78b1f0e484ffa9154c5f495d4c39 --onto ae492265fec103aa834d897bf9f68c94d10f0785. (2024-03-06 15:17:36)
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0072d13bd40aef791090d1e3e964413f1176162e --onto ae492265fec103aa834d897bf9f68c94d10f0785. (2024-03-06 17:23:41)
• ❗ Std CI can not be attempted yet, as the nightly-testing-2024-03-07 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Std CI should run now. (2024-03-07 08:56:58)
• 💥 Mathlib branch lean-pr-testing-3621 build failed against this PR. (2024-03-10 09:58:33) View Log
• 💥 Mathlib branch lean-pr-testing-3621 build failed against this PR. (2024-03-10 10:46:45) View Log
• ✅ Mathlib branch lean-pr-testing-3621 has successfully built against this PR. (2024-03-10 21:16:48) View Log
• ❗ Std CI can not be attempted yet, as the nightly-testing-2024-03-10 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Std CI should run now. (2024-03-10 22:34:50)
• ❗ Std CI can not be attempted yet, as the nightly-testing-2024-03-11 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Std CI should run now. (2024-03-11 12:17:14)
• 💥 Mathlib branch lean-pr-testing-3621 build failed against this PR. (2024-03-13 14:06:09) View Log
• 💥 Mathlib branch lean-pr-testing-3621 build failed against this PR. (2024-03-13 15:09:25) View Log
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0959bc45d2a50b1dbae8c4cf0b867a03b8fd4ffe --onto 317adf42e92a4dbe07295bc1f0429b61bb8079fe. (2024-03-14 15:01:48)

[nomeata]

This is done, I think. Nice improvements to the variable names shown by termination_by?.
I’ll wait for the next nightly-with-mathlib for some extra testing though. done