Fix termination issues

[eyihluyc]

This PR fixes all decreasing_by sorry's.

Most fixes were achieved by introducing two mutually dependent functions, one of which was built with the structural induction on Term, and another one – with induction on Bindings.

Another kind of issue was caused by consBindingsRedMany, which is defined by induction on (obj l1) ⇝* (obj l2). For some reason, structural recursion was not applied directly because (obj l1) and (obj l2) do not happen to be variables. This thread on Zulip was about a similar issue and helped to find the solution. However it was still not enough because "code generator does not support recursor 'ReflTransGen.rec' yet, consider using 'match ... with' and/or structural recursion". Structural recursion could not be used because of non-variable arguments, so now we rely on Mathlib.Util.CompileInductive to generate ReflTransGen.rec.

Also, this PR updates lean-toolchain and contains code refactoring which was caused by the update.

---

PR-Codex overview

The focus of this PR is to introduce new dependencies and update existing ones.

Detailed summary

• Added new dependencies quote4, aesop, proofwidgets, and importGraph
• Updated dependencies std, doc-gen4, and mathlib4
• Modified functions incLocatorsFrom, substitute, substituteLst, subst_inc_cancel, subst_inc_cancel_Lst, lookup, and insert_φ

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}