[JoAdo07]

Fixes #58.

visitedExprs was keyed by Expr using its default BEq instance, which is alpha-equivalence and ignores binder names and binder info. An expression could therefore reuse the index of an alpha-equivalent expression exported earlier. This made the exported binder names and binder info depend on which declarations had already been exported.

This change introduces a small ExprKey wrapper whose BEq is Expr.equal (structural equality), and uses it for the expression cache. Expr.hash is still used for hashing; structural equality implies alpha-equivalence, so the existing hash remains compatible.

The regression test exports two lambda expressions that differ only in binder name and binder info. On the old code the second expression reuses the first index and is not emitted; with this change both expressions are emitted with their own indices.

This can slightly increase export size because alpha-equivalent copies are no longer deduplicated, but it makes each declaration's export independent of export order.

Validation:

• lake build passes.
• lake test passes on leanprover/lean4:v4.36.0-rc1.
• The pre-existing functionWithLet linter warning is unchanged.