Improve the arity error message for destructuring let

[MavenRain]

Fixes / closes #7833

Explanation

The arity error for a destructuring let used to be a bare user_err in the
pretyper:

Destructing let on this type expects 2 variables.

It now names the destructured term and its type, and reports the number of
variables actually given:

Destructing let on term "p" of type "point2d"
expects 2 variables, but 3 were given.

As requested in the review of the earlier attempt #7943, no Printer call is
made inside pretyping: the error is a new Pretype_errors.pretype_error
constructor (LetTupleArity, carrying the judgment of the destructured term
plus the expected and given variable counts) raised through a new
error_lettuple_arity helper and rendered in Himsg, mirroring the
neighboring CaseNotInductive / NumberBranches plumbing.

API note: Pretype_errors.pretype_error gains the LetTupleArity
constructor, so external plugin code matching exhaustively on
pretype_error needs a new arm. In-tree code needed no change besides
Himsg.

The new output test covers both plural renderings in each position
("expects 1 variable" / "expects 2 variables", "1 was given" / "3 were
given").

• Added / updated test-suite (test-suite/output/bug_7833.v).
• Added changelog.

_{Drafted with AI assistance; the change and its verification (full build,
output test-suite, mutation check on the new test) were reviewed and run
locally by me.}

[SkySkimmer]

I'm not sure we want to print the full term and type. They can be arbitrarily large. Also we have the error location pointing at the term so printing it seems redundant.
Maybe just print the name of the inductive? eg

Destructing let on term of type "prod"
expects 2 variables, but 3 were given.

(where the full type would be prod nat nat printed nat * nat)

(but I have a strong bias towards brevity, so maybe the average user would benefit from the full term & type? IDK)