Dedup: share the alpha-renaming binder __eq__ body (refs #813)

[jsiek]

What

Deduplicate the alpha-renaming binder __eq__ methods. FunctionType,
Lambda, All, Some, and TLet (all in abstract_syntax/terms.py) each
carried the same three-line body:

def __eq__(self, other):
    if not isinstance(other, <Cls>):
        return False
    return <_alpha_equiv_helper>(self, other, {}, {})

The only things that vary are the operand class and the per-node
alpha-equivalence helper. This PR extracts the shared body into
abstract_syntax/ops.binder_eq(self, other, cls, alpha) so the five methods
become one-liners, and the subtle "these deliberately bypass the
_alpha_equiv empty-env fast path, which calls == and would recurse back
here" rationale is documented in exactly one place instead of being implicit
in five.

Why this is safe

binder_eq(self, other, Cls, alpha) is exactly
isinstance(other, Cls) and alpha(self, other, {}, {}), which short-circuits
to False on a type mismatch just like the original guard. No semantic
change.

Verification

Local (this container has no ruff/mypy/pytest; those run in CI):

• python3 test-deduce.py --passable — pass
• python3 test-deduce.py --lib — pass
• python3 test-deduce.py --equiv — pass (grammar + should-error corpus +
  round-trip; canonical-AST comparison exercises these __eq__ methods)
• python3 test-deduce.py --errors --warns — pass
• Direct alpha-equivalence spot check: all x. x=x == all y. y=y (True),
  vs all y. y=zero (False), analogous cases for some/fun/term-let, and
  All != Lambda / All != 5 (False) all behave as before.

Scope / coordination

Touches only abstract_syntax/terms.py and abstract_syntax/ops.py, disjoint
from the other in-flight #813 slices (#1153 error.py, #1151 declarations.py,
#1147 proofs.py, #1148 uniquify binder, #1149 checker view-law).

Refs #813 (this is one slice of the standing dedup umbrella, which stays open).

Resume this session on ginger: ~/deduce-runner/resume.sh 2a46bc68-a6b2-4e22-82b2-a48cd10d0ef8 routine/20260728-080201

🤖 Generated with Claude Code