[ refactor ] Infrastructure for Data.Tree.AVL.Indexed.*

[jamesmckinna]

This PR arises from my review of #2961 and introduces some additional typedefs and lemmas which help streamline the analysis of insert, delete and their various helper join* functions. Specifically, the analysis of base cases for such helpers when one sub-tree is a leaf relies on two new lemmas about instances of the balance relation at height 0.

Systematically uses variable declarations to aid readability; as ever, this technically might be considered breaking, because any given type signature might have subtle differences wrt their prenex implicit forms when fully elaborated, but I think we should regard such things as 'bug fixes' at best (worst?).

Intended to be minimally invasive, but in the course of doing this, I observe:

• the same satisfied/satisfiable clash arising in Rename lemma satisfied to any⇒satisfiable in *.Relation.Unary.Any #2865 / [ refactor ] fix #2865 for v2.4 #2954, for Data.Tree.AVL.Indexed.Relation.Unary.Any
• the import structure is pretty unwieldy, and lower level imports from StrictTotalOrder and their extensions by min/max elements I think really should be folded into the exports from Data.Tree.AVL.Indexed.Key?
• miscellaneous implicit/explicit distinctions might well be improved by careful refactoring, but these would definitely be breaking so not considered here (eg Data.Tree.AVL.Indexed.Key.trans⁺ makes its first argument explicit, rather than typing this as Transitive _<⁺_... but why?)

NB/TODO:

• the functions defined are not consistent wrt compare k′ k (lookup, delete, etc.) else compare k k′ (insert, insertWith) and this discrepancy should be fixed! But doing so might hold up Add properties that characterize Data.Tree.AVL.Indexed.delete. #2961 so I'd be happy to take responsibility to follow up on this downstream
• doing so would tackle the inconsistency between the existing proofs in Properties and the new ones added in Add properties that characterize Data.Tree.AVL.Indexed.delete. #2961 wrt an as-yet undefined property

  keyNotAt : Key → Any P t → Set ℓ₁
  keyNotAt k p = k ≉ lookupKey p

  which in this form, or its symmetric version, are used throughout. DRY says: standardise this via a definition!again: downstream?)