Refactor

[eyihluyc]

Addresses #16

This is an attempt to clean up the code. So far, the following was done:

• deleted (unused) definitions of InsertAll and InsertMany,
• renamed AttrList to Bindings,
• deleted Reduce namespace and closed PReduce namespace.

We further need to add explanations to the documentation, and maybe we want to split the formalization into separate more focused files.

---

PR-Codex overview

This PR focuses on refactoring the code by replacing AttrList with Bindings and making related changes.

Detailed summary

• Replaced AttrList with Bindings throughout the codebase.
• Updated function signatures to use Bindings instead of AttrList.
• Updated mapBindings function to work with Bindings instead of AttrList.
• Added mapBindings_compose function to compose multiple mapBindings calls.
• Added min_free_loc function to calculate the minimal free locator in a term.
• Added min_free_loc_inc function to increment the minimal free locator in a term.
• Added subst_inc_cancel function to cancel the effect of substitute and incLocatorsFrom on free locators.
• Updated lookup function to work with Bindings instead of AttrList.

The following files were skipped due to too many changes: Minimal/Calculus.lean

✨ Ask PR-Codex anything about this PR by commenting with /codex {your question}