test: restore semantic template list-map conversion coverage

[oxura]

Fixes #1490.

The existing list-map conversion regression currently passes by expecting a legacy parser error. Its own comment says Bend spells equations ==, but the theorem still has =/{=}, old template application syntax and a missing erased argument. Its main returns an unrelated literal, so mapped values are not exercised.

This is a regression-coverage repair, not a claim of a new compiler fix.

Change

• Replace the diagnostic-wording expectation with a runnable semantic result.
• Use current equality/reflexivity, ~ application, explicit erased type argument and annotated operators.
• Use checked Nat arithmetic rather than native U32 models, so the genuine kernel proves both mapped-list length and values ([2n, 3n]).
• Run the same closed callback through an actual mapped-value sum in main (5n), rather than a disconnected literal or a length-only consumer.
• Note the repaired coverage in the existing changelog. No GUIDE edit.

Actual verification

• Untouched main 2343aec: the fixture's --verdict exits 1 at = before elaboration.
• This branch: source interpreter prints 5n, exit 0.
• Real BendTT kernel (same unmodified Lean source as main): --verdict prints ALL PROOFS CHECK, exit 0, including both equality obligations.
• Actual emitted standalone Bun JS, Node JS and native C executable each print 5n, exit 0.
• Repository gate 54/54; checker, kernel, compiler, gates, allow list and caps unchanged.

Mini-cluster/GPU gates were not run. The old error sentence and location are deliberately not re-pinned.

[Lorenzobattistela]

Thanks @oxura! I dropped the CHANGELOG entry: please don't edit CHANGELOG.md in PRs.

[oxura]

Understood, thank you. I will leave CHANGELOG.md to maintainers in future PRs, just as GUIDE.md is hand-written. I am also removing my entry from the already-open IO.exit follow-up (#1492).