fix: abstract_eq is false in two independent ways

[vasnesterov]

The bug

Lean.Expr.abstract_eq equates Expr.abstract with a model, and the two differ
for two independent reasons:

1. Capture. The C abstract does not shift loose bvars, so abstracting a
   term that already contains them under a binder captures.
2. Duplicates. C resolves a repeated free variable last-wins; the model
   takes the first.

Both have #eval counterexamples. Not Lean-inconsistent — the upstream side is
opaque — but wrong about what runs.

The fix

(he : e.looseBVarRange' = 0) (hx : xs.Nodup)

What this exposed — the caller was relying on the false form, heavily

LocalContext.mkBinding_eq was stated with no hypotheses at all, for an
arbitrary lctx, b and xs. So it asserted precisely what the two
counterexamples refute.

It now takes three conditions, and the third is new rather than transplanted:

• hb — the body is closed;
• hnd — the variable list is duplicate-free;
• hlc — every declaration type and let-value reachable from lctx.find? is
  loose-bvar-free. mkBinding abstracts those too, which the old statement
  silently assumed.

The proof is restructured rather than patched: a local Nat.foldRev_congr_fun
lets the fold body be converted to mkBindingList1 pointwise, instead of by a
blind simp only [abstract_eq] that was quietly using the unconditional form
everywhere.

hlc does not propagate: TrLCtx.closed_of_find? (new, in the same file)
supplies it from local-context well-formedness alone — no env.WF needed — so
it is discharged where it arises.

MLCtx.WF.mkForall_partial, mkForall_eq and mkLambda_eq gain the closed-body
condition; the two mkForall_eq sites discharge it with
(m.noBV ▸ h2'.closed).looseBVarRange_zero.

4 files, +101/−11. lake build Lean4Lean.Verify green.

Note on the freeze

Verify/Axioms.lean is frozen per CLAUDE.md; this is a proposal for sign-off.
The axiom's name is unchanged.

🤖 Generated with Claude Code