A λ rebuilt as a match keeps its annotations on its own binders, so --verdict checks what bend2 checks (#1669)

[aaaxn]

Fixes #1669. Depends on #1666, whose subst(t, d) the fix uses. Until #1666 merges, this PR's diff also shows its two commits. Only the last commit, 45716b3, is new here.

Cause

use(-f: P -> Nat) takes f erased, so bend2 lets the λ passed for it use its variable twice. rebuild in safe.ts turns that λ into a λ-match on the variable and calls the λ's body on each constructor, under a binder per field. bend2's annotations name a variable by the level bend2 checked it at, so they still name the variable's old level. With fields, that level now belongs to the first field, and the kernel rejects the term (expected: P). With no fields, no variable in scope has that level, and --verdict reports a free variable.

Fix

rebuild passes the λ through subst(x, s.d) before it calls the body, as #1666 does in eta. In the lowered form, an annotation names the body's binders as the body's own uses do, so the annotations move with the binders.

Checks

On #1666's head (fce97a9), Linux x86_64, kernel built from main's bendtt.lean with Lean 4.34.0:

• tests/check/rebuild_levels.bend covers an annotation that names the variable, for a type with two constructors (pair) and for one with no fields (unit), and one that names the binder of a λ inside the body (inner). Each one fails --verdict on A term η-expanded under a new λ keeps its annotations on its own binders, so --verdict checks what bend2 checks (#1665) #1666 when it is on its own. pair and inner fail in the kernel, and unit fails as out of scope. A law pins main at 6n. The file prints 6n when run and from the JS and C builds, and --checkup exits 0.
• Mutations: the old line, or subst at s.d + 1 or s.d - 1, fails all three.
• On the other 1,734 test, demo, and bench files, --verdict gives the same exit code and output as A term η-expanded under a new λ keeps its annotations on its own binders, so --verdict checks what bend2 checks (#1665) #1666, and -o is byte-identical. Both files in --verdict mismatch: a λ rebuilt as a match keeps its variable's old level in its annotations (Nat where P is expected) #1669 check, and the -o of its twice.bend is byte-identical to the hand-written version's.
• bun gates/repo.ts with ttok==0.3: 54 / 54. safe.ts goes from 23,987 to 23,997 ttok. tsc: 11 errors, the same as main.
• I didn't run the cluster gates.

Merge order

With #1657 as well, all three PRs apply cleanly and the tests above check, but safe.ts comes to 24,006 ttok, over its 24,000 cap. Whichever of #1657 and this PR lands second has to save 6 tokens.