fix: implement capture-avoiding substitution for De Bruijn indices

[yyhrnk]

Replaced the ad-hoc substitution with the standard De Bruijn algorithm using shift/subst. This prevents variable capture under lambdas and ensures correct beta-reduction. The new step applies beta as shift(-1, 0, subst(0, shift(1, 0, arg), body)), following the canonical formulation. Existing simple assertions continue to pass while complex terms now reduce correctly.

[github-actions]

All contributors have signed the CLA ✍️ ✅
_{Posted by the CLA Assistant Lite bot.}

[yyhrnk]

I have read the CLA Document and I hereby sign the CLA

[sjudson]

Thanks for the PR. I'm going to pass: this is just some toy demo code, and I don't want it to fall out of consistency with the docs.