From 61a568696914129aa203a03797be081fd542fcfd Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 20 Mar 2026 08:19:18 +0000
Subject: [PATCH 01/35] add : lemmas about balance factors at height 0

---
 src/Data/Tree/AVL/Height.agda | 24 +++++++++++++++++++-----
 1 file changed, 19 insertions(+), 5 deletions(-)

diff --git a/src/Data/Tree/AVL/Height.agda b/src/Data/Tree/AVL/Height.agda
index fa50705952..4e03ee0307 100644
--- a/src/Data/Tree/AVL/Height.agda
+++ b/src/Data/Tree/AVL/Height.agda
@@ -11,6 +11,12 @@ module Data.Tree.AVL.Height where
 
 open import Data.Nat.Base
 open import Data.Fin.Base using (Fin; zero; suc)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
+
+private
+  variable
+    i j m n : ℕ
+
 
 ℕ₂ = Fin 2
 pattern 0# = zero
@@ -39,18 +45,26 @@ infix 4 _∼_⊔_
 -- absolute value of the balance factor is never more than 1.
 
 data _∼_⊔_ : ℕ → ℕ → ℕ → Set where
-  ∼+ : ∀ {n} →     n ∼ 1 + n ⊔ 1 + n
-  ∼0 : ∀ {n} →     n ∼ n     ⊔ n
-  ∼- : ∀ {n} → 1 + n ∼ n     ⊔ 1 + n
+  ∼+ :     n ∼ 1 + n ⊔ 1 + n
+  ∼0 :     n ∼ n     ⊔ n
+  ∼- : 1 + n ∼ n     ⊔ 1 + n
 
 -- Some lemmas.
 
-max∼ : ∀ {i j m} → i ∼ j ⊔ m → m ∼ i ⊔ m
+max∼ : i ∼ j ⊔ m → m ∼ i ⊔ m
 max∼ ∼+ = ∼-
 max∼ ∼0 = ∼0
 max∼ ∼- = ∼0
 
-∼max : ∀ {i j m} → i ∼ j ⊔ m → j ∼ m ⊔ m
+∼max : i ∼ j ⊔ m → j ∼ m ⊔ m
 ∼max ∼+ = ∼0
 ∼max ∼0 = ∼0
 ∼max ∼- = ∼+
+
+0∼⊔ : 0 ∼ j ⊔ m → j ≡ m
+0∼⊔ ∼+ = refl
+0∼⊔ ∼0 = refl
+
+∼0⊔ : i ∼ 0 ⊔ m → i ≡ m
+∼0⊔ ∼- = refl
+∼0⊔ ∼0 = refl

From 669d9bc0983aaa1570489081465b0a389adeeea5 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 20 Mar 2026 08:24:56 +0000
Subject: [PATCH 02/35] add: `variable`s; tighten `import`s

---
 src/Data/Tree/AVL/Value.agda | 32 ++++++++++++++++++++------------
 1 file changed, 20 insertions(+), 12 deletions(-)

diff --git a/src/Data/Tree/AVL/Value.agda b/src/Data/Tree/AVL/Value.agda
index 6305bd5c2c..91b05ee857 100644
--- a/src/Data/Tree/AVL/Value.agda
+++ b/src/Data/Tree/AVL/Value.agda
@@ -8,14 +8,20 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Relation.Binary.Bundles using (Setoid)
-open import Relation.Binary.Definitions using (_Respects_)
 
 module Data.Tree.AVL.Value {a ℓ} (S : Setoid a ℓ) where
 
 open import Data.Product.Base using (Σ; _,_)
-open import Level using (suc; _⊔_)
-import Function.Base as F
-open Setoid S renaming (Carrier to Key)
+open import Level using (Level; suc; _⊔_)
+import Function.Base as Function
+open import Relation.Binary.Definitions using (_Respects_)
+
+open Setoid S using (_≈_) renaming (Carrier to Key)
+
+private
+  variable
+    v : Level
+
 
 ------------------------------------------------------------------------
 -- A Value
@@ -26,23 +32,25 @@ record Value v : Set (a ⊔ ℓ ⊔ suc v) where
     family   : Key → Set v
     respects : family Respects _≈_
 
+open Value using (family)
+
 ------------------------------------------------------------------------
 -- A Key together with its value
 
-record K&_ {v} (V : Value v) : Set (a ⊔ v) where
+record K&_ (V : Value v) : Set (a ⊔ v) where
   constructor _,_
   field
     key   : Key
-    value : Value.family V key
+    value : family V key
 infixr 4 _,_
 open K&_ public
 
-module _ {v} {V : Value v} where
+module _ {V : Value v} where
 
-  toPair : K& V → Σ Key (Value.family V)
+  toPair : K& V → Σ Key (family V)
   toPair (k , v) = k , v
 
-  fromPair : Σ Key (Value.family V) → K& V
+  fromPair : Σ Key (family V) → K& V
   fromPair (k , v) = k , v
 
 ------------------------------------------------------------------------
@@ -50,6 +58,6 @@ module _ {v} {V : Value v} where
 
 -- The function `const` is defined using copatterns to prevent eager
 -- unfolding of the function in goal types.
-const : ∀ {v} → Set v → Value v
-Value.family   (const V) = F.const V
-Value.respects (const V) = F.const F.id
+const : Set v → Value v
+Value.family   (const V) = Function.const V
+Value.respects (const V) = Function.const F.id

From 8a4efef57bf5eb861164bc8f7d6a14e61eda1cd9 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 20 Mar 2026 08:26:17 +0000
Subject: [PATCH 03/35] fix: qualified module name `Function`

---
 src/Data/Tree/AVL/Value.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Tree/AVL/Value.agda b/src/Data/Tree/AVL/Value.agda
index 91b05ee857..f6662512d3 100644
--- a/src/Data/Tree/AVL/Value.agda
+++ b/src/Data/Tree/AVL/Value.agda
@@ -60,4 +60,4 @@ module _ {V : Value v} where
 -- unfolding of the function in goal types.
 const : Set v → Value v
 Value.family   (const V) = Function.const V
-Value.respects (const V) = Function.const F.id
+Value.respects (const V) = Function.const Function.id

From bab782252595163f2b379c6187b6828e22c37bec Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 20 Mar 2026 09:23:00 +0000
Subject: [PATCH 04/35] refactor: introduce typedefs, remove parentheses,
 streamline functions definitions

---
 src/Data/Tree/AVL/Indexed.agda | 286 +++++++++++++++++----------------
 1 file changed, 147 insertions(+), 139 deletions(-)

diff --git a/src/Data/Tree/AVL/Indexed.agda b/src/Data/Tree/AVL/Indexed.agda
index 94d1b0782b..c6ac393cf8 100644
--- a/src/Data/Tree/AVL/Indexed.agda
+++ b/src/Data/Tree/AVL/Indexed.agda
@@ -16,17 +16,12 @@ open import Data.Nat.Base using (ℕ; zero; suc; _+_)
 open import Data.Product.Base using (Σ; ∃; _×_; _,_; proj₁)
 open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Data.List.Base as List using (List)
-open import Data.DifferenceList using (DiffList; []; _∷_; _++_)
-open import Function.Base as F hiding (const)
+open import Data.DifferenceList as DiffList using (DiffList; []; _∷_; _++_)
+open import Function.Base as Function hiding (const)
 open import Relation.Unary
 open import Relation.Binary.Definitions using (_Respects_; Tri; tri<; tri≈; tri>)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
-private
-  variable
-    l v : Level
-    A : Set l
-
 open StrictTotalOrder strictTotalOrder renaming (Carrier to Key)
 
 ------------------------------------------------------------------------
@@ -37,7 +32,19 @@ open import Data.Tree.AVL.Value Eq.setoid public
 open import Data.Tree.AVL.Height public
 
 ------------------------------------------------------------------------
--- Definitions of the tree
+-- Now we have vocabulary in which to state things more cleanly
+
+private
+  variable
+    ℓ v w : Level
+    A : Set ℓ
+    k : Key
+    l m u : Key⁺
+    hˡ hʳ h : ℕ
+
+
+------------------------------------------------------------------------
+-- Definitions of the tree types
 
 -- The trees have three parameters/indices: a lower bound on the
 -- keys, an upper bound, and a height.
@@ -53,15 +60,45 @@ data Tree {v} (V : Value v) (l u : Key⁺) : ℕ → Set (a ⊔ v ⊔ ℓ₂) wh
          (bal : hˡ ∼ hʳ ⊔ h) →
          Tree V l u (suc h)
 
-module _ {v} {V : Value v} where
+-- Auxiliary type definitions for the types of insert, delete etc.
+
+module _ (V : Value v) (l u : Key⁺) where
+
+  Tree⁺ Tree⁻ : (h : ℕ) → Set (a ⊔ v ⊔ ℓ₂)
+  Tree⁺ h = ∃ λ i → Tree V l u (i ⊕ h)
+  Tree⁻ h = ∃ λ i → Tree V l u pred[ i ⊕ h ]
+
+  pattern leaf⁻ l<u = _ , leaf l<u  -- empty trees when passed as Tree⁻ V l u 0
+
+------------------------------------------------------------------------
+-- Functorial map over all values in the tree.
+
+module _ {V : Value v} {W : Value w}
+         (open Value using (family))
+         (f : family V ⊆ family W) where
+
+  map : Tree V l u h → Tree W l u h
+  map (leaf l<u)             = leaf l<u
+  map (node (k , v) l r bal) = node (k , f v) (map l) (map r) bal
+
+------------------------------------------------------------------------
+-- Properties relative to a fixed Value type family
+
+module _ {V : Value v} (open Value V using (respects) renaming (family to Val)) where
 
   ordered : ∀ {l u n} → Tree V l u n → l <⁺ u
   ordered (leaf l<u)          = l<u
   ordered (node kv lk ku bal) = trans⁺ _ (ordered lk) (ordered ku)
 
   private
-    Val = Value.family V
-    V≈  = Value.respects V
+  
+  -- This lemma justifies the use of `leaf⁻` pattern matches in code below
+
+    tree⁻0 : (t⁻ : Tree⁻ V l u 0) →
+             ∃ λ i → ∃ λ t → t⁻ ≡ (i , t) × t ≡ leaf (ordered t)
+    tree⁻0 t⁻@(leaf⁻ _) = _ , _ , refl , refl
+
+  -- Injectivity of constructors
 
   leaf-injective : ∀ {l u} {p q : l <⁺ u} → (Tree V l u 0 ∋ leaf p) ≡ leaf q → p ≡ q
   leaf-injective refl = refl
@@ -77,6 +114,19 @@ module _ {v} {V : Value v} where
   -- See also node-injectiveˡ, node-injectiveʳ, and node-injective-bal
   -- in Data.Tree.AVL.Indexed.WithK.
 
+------------------------------------------------------------------------
+-- Constructions on trees
+
+  -- An empty tree.
+
+  empty : l <⁺ u → Tree V l u 0
+  empty = leaf
+
+  -- A singleton tree.
+
+  singleton : ∀ (k : Key) → Val k → l < k < u → Tree V l u 1
+  singleton k v (l<k , k<u) = node (k , v) (leaf l<k) (leaf k<u) ∼0
+
   -- Cast operations. Logarithmic in the size of the tree, if we don't
   -- count the time needed to construct the new proofs in the leaf
   -- cases. (The same kind of caveat applies to other operations
@@ -87,170 +137,139 @@ module _ {v} {V : Value v} where
   -- proof manipulation). However, note that this would not change the
   -- worst-case time complexity of the operations below (up to Θ).
 
-  castˡ : ∀ {l m u h} → l <⁺ m → Tree V m u h → Tree V l u h
-  castˡ {l} l<m (leaf m<u)         = leaf (trans⁺ l l<m m<u)
-  castˡ     l<m (node k mk ku bal) = node k (castˡ l<m mk) ku bal
+  castˡ : l <⁺ m → Tree V m u h → Tree V l u h
+  castˡ l<m (leaf m<u)         = leaf (trans⁺ _ l<m m<u)
+  castˡ l<m (node k mk ku bal) = node k (castˡ l<m mk) ku bal
 
-  castʳ : ∀ {l m u h} → Tree V l m h → m <⁺ u → Tree V l u h
-  castʳ {l} (leaf l<m)         m<u = leaf (trans⁺ l l<m m<u)
-  castʳ     (node k lk km bal) m<u = node k lk (castʳ km m<u) bal
+  castʳ : Tree V l m h → m <⁺ u → Tree V l u h
+  castʳ (leaf l<m)         m<u = leaf (trans⁺ _ l<m m<u)
+  castʳ (node k lk km bal) m<u = node k lk (castʳ km m<u) bal
 
   -- Various constant-time functions which construct trees out of
   -- smaller pieces, sometimes using rotation.
 
+  pattern node⁰ʳ k₁ t₁ k₂ t₂ t₃ = node k₁ t₁ (node k₂ t₂ t₃ ∼0) ∼0
+  pattern node⁰ˡ k₁ k₂ t₁ t₂ t₃ = node k₁ (node k₂ t₁ t₂ ∼0) t₃ ∼0
+
   pattern node⁺ k₁ t₁ k₂ t₂ t₃ bal = node k₁ t₁ (node k₂ t₂ t₃ bal) ∼+
 
-  joinˡ⁺ : ∀ {l u hˡ hʳ h} →
-           (k : K& V) →
-           (∃ λ i → Tree V l [ k .key ] (i ⊕ hˡ)) →
-           Tree V [ k .key ] u hʳ →
-           (bal : hˡ ∼ hʳ ⊔ h) →
-           ∃ λ i → Tree V l u (i ⊕ (1 + h))
-  joinˡ⁺ k₂ (0# , t₁)                t₃ bal = (0# , node k₂ t₁ t₃ bal)
-  joinˡ⁺ k₂ (1# , t₁)                t₃ ∼0  = (1# , node k₂ t₁ t₃ ∼-)
-  joinˡ⁺ k₂ (1# , t₁)                t₃ ∼+  = (0# , node k₂ t₁ t₃ ∼0)
-  joinˡ⁺ k₄ (1# , node  k₂ t₁ t₃ ∼-) t₅ ∼-  = (0# , node k₂ t₁ (node k₄ t₃ t₅ ∼0) ∼0)
-  joinˡ⁺ k₄ (1# , node  k₂ t₁ t₃ ∼0) t₅ ∼-  = (1# , node k₂ t₁ (node k₄ t₃ t₅ ∼-) ∼+)
+  joinˡ⁺ : ∀ kv → let k = [ kv . key ] in
+           Tree⁺ V l k hˡ → Tree V k u hʳ → hˡ ∼ hʳ ⊔ h →
+           Tree⁺ V l u (suc h)
+  joinˡ⁺ k₂ (0# , t₁)                t₃ bal = 0# , node k₂ t₁ t₃ bal
+  joinˡ⁺ k₂ (1# , t₁)                t₃ ∼0  = 1# , node k₂ t₁ t₃ ∼-
+  joinˡ⁺ k₂ (1# , t₁)                t₃ ∼+  = 0# , node k₂ t₁ t₃ ∼0
+  joinˡ⁺ k₄ (1# , node  k₂ t₁ t₃ ∼-) t₅ ∼-  = 0# , node⁰ʳ k₂ t₁ k₄ t₃ t₅
+  joinˡ⁺ k₄ (1# , node  k₂ t₁ t₃ ∼0) t₅ ∼-  = 1# , node⁺ k₂ t₁ k₄ t₃ t₅ ∼-
   joinˡ⁺ k₆ (1# , node⁺ k₂ t₁ k₄ t₃ t₅ bal) t₇ ∼-
-    = (0# , node k₄ (node k₂ t₁ t₃ (max∼ bal))
-                    (node k₆ t₅ t₇ (∼max bal))
-                    ∼0)
+    = 0# , node k₄ (node k₂ t₁ t₃ (max∼ bal)) (node k₆ t₅ t₇ (∼max bal)) ∼0
 
   pattern node⁻ k₁ k₂ t₁ t₂ bal t₃ = node k₁ (node k₂ t₁ t₂ bal) t₃ ∼-
 
-  joinʳ⁺ : ∀ {l u hˡ hʳ h} →
-           (k : K& V) →
-           Tree V l [ k .key ] hˡ →
-           (∃ λ i → Tree V [ k .key ] u (i ⊕ hʳ)) →
-           (bal : hˡ ∼ hʳ ⊔ h) →
-           ∃ λ i → Tree V l u (i ⊕ (1 + h))
-  joinʳ⁺ k₂ t₁ (0# , t₃)               bal = (0# , node k₂ t₁ t₃ bal)
-  joinʳ⁺ k₂ t₁ (1# , t₃)               ∼0  = (1# , node k₂ t₁ t₃ ∼+)
-  joinʳ⁺ k₂ t₁ (1# , t₃)               ∼-  = (0# , node k₂ t₁ t₃ ∼0)
-  joinʳ⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼+) ∼+  = (0# , node k₄ (node k₂ t₁ t₃ ∼0) t₅ ∼0)
-  joinʳ⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼0) ∼+  = (1# , node k₄ (node k₂ t₁ t₃ ∼+) t₅ ∼-)
+  joinʳ⁺ : ∀ kv → let k = [ kv . key ] in
+           Tree V l k hˡ → Tree⁺ V k u hʳ → hˡ ∼ hʳ ⊔ h →
+           Tree⁺ V l u (suc h)
+  joinʳ⁺ k₂ t₁ (0# , t₃)               bal = 0# , node k₂ t₁ t₃ bal
+  joinʳ⁺ k₂ t₁ (1# , t₃)               ∼0  = 1# , node k₂ t₁ t₃ ∼+
+  joinʳ⁺ k₂ t₁ (1# , t₃)               ∼-  = 0# , node k₂ t₁ t₃ ∼0
+  joinʳ⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼+) ∼+  = 0# , node⁰ˡ k₄ k₂ t₁ t₃ t₅
+  joinʳ⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼0) ∼+  = 1# , node⁻ k₄ k₂ t₁ t₃ ∼+ t₅
   joinʳ⁺ k₂ t₁ (1# , node⁻ k₆ k₄ t₃ t₅ bal t₇) ∼+
-    = (0# , node k₄ (node k₂ t₁ t₃ (max∼ bal))
-                    (node k₆ t₅ t₇ (∼max bal))
-                    ∼0)
-
-  joinˡ⁻ : ∀ {l u} hˡ {hʳ h} →
-           (k : K& V) →
-           (∃ λ i → Tree V l [ k .key ] pred[ i ⊕ hˡ ]) →
-           Tree V [ k .key ] u hʳ →
-           (bal : hˡ ∼ hʳ ⊔ h) →
-           ∃ λ i → Tree V l u (i ⊕ h)
-  joinˡ⁻ zero    k₂ (0# , t₁) t₃ bal = (1# , node k₂ t₁ t₃ bal)
-  joinˡ⁻ zero    k₂ (1# , t₁) t₃ bal = (1# , node k₂ t₁ t₃ bal)
-  joinˡ⁻ (suc _) k₂ (0# , t₁) t₃ ∼+  = joinʳ⁺ k₂ t₁ (1# , t₃) ∼+
-  joinˡ⁻ (suc _) k₂ (0# , t₁) t₃ ∼0  = (1# , node k₂ t₁ t₃ ∼+)
-  joinˡ⁻ (suc _) k₂ (0# , t₁) t₃ ∼-  = (0# , node k₂ t₁ t₃ ∼0)
-  joinˡ⁻ (suc _) k₂ (1# , t₁) t₃ bal = (1# , node k₂ t₁ t₃ bal)
-
-  joinʳ⁻ : ∀ {l u hˡ} hʳ {h} →
-           (k : K& V) →
-           Tree V l [ k .key ] hˡ →
-           (∃ λ i → Tree V [ k .key ] u pred[ i ⊕ hʳ ]) →
-           (bal : hˡ ∼ hʳ ⊔ h) →
-           ∃ λ i → Tree V l u (i ⊕ h)
-  joinʳ⁻ zero    k₂ t₁ (0# , t₃) bal = (1# , node k₂ t₁ t₃ bal)
-  joinʳ⁻ zero    k₂ t₁ (1# , t₃) bal = (1# , node k₂ t₁ t₃ bal)
-  joinʳ⁻ (suc _) k₂ t₁ (0# , t₃) ∼-  = joinˡ⁺ k₂ (1# , t₁) t₃ ∼-
-  joinʳ⁻ (suc _) k₂ t₁ (0# , t₃) ∼0  = (1# , node k₂ t₁ t₃ ∼-)
-  joinʳ⁻ (suc _) k₂ t₁ (0# , t₃) ∼+  = (0# , node k₂ t₁ t₃ ∼0)
-  joinʳ⁻ (suc _) k₂ t₁ (1# , t₃) bal = (1# , node k₂ t₁ t₃ bal)
+    = 0# , node k₄ (node k₂ t₁ t₃ (max∼ bal)) (node k₆ t₅ t₇ (∼max bal)) ∼0
+
+  joinˡ⁻ : ∀ hˡ (kv : K& V) → let k = [ kv . key ] in
+           Tree⁻ V l k hˡ → Tree V k u hʳ → hˡ ∼ hʳ ⊔ h →
+           Tree⁺ V l u h
+  joinˡ⁻ zero    k₂ (leaf⁻ l<k) t₃ bal = 1# , node k₂ (leaf l<k) t₃ bal
+  joinˡ⁻ (suc _) k₂ (0# , t₁)   t₃ ∼+  = joinʳ⁺ k₂ t₁ (1# , t₃) ∼+
+  joinˡ⁻ (suc _) k₂ (0# , t₁)   t₃ ∼0  = 1# , node k₂ t₁ t₃ ∼+
+  joinˡ⁻ (suc _) k₂ (0# , t₁)   t₃ ∼-  = 0# , node k₂ t₁ t₃ ∼0
+  joinˡ⁻ (suc _) k₂ (1# , t₁)   t₃ bal = 1# , node k₂ t₁ t₃ bal
+
+  joinʳ⁻ : ∀ hʳ (kv : K& V) → let k = [ kv . key ] in
+           Tree V l k hˡ → Tree⁻ V k u hʳ → hˡ ∼ hʳ ⊔ h →
+           Tree⁺ V l u h
+  joinʳ⁻ zero    k₂ t₁ (leaf⁻ k<u) bal = 1# , node k₂ t₁ (leaf k<u) bal
+  joinʳ⁻ (suc _) k₂ t₁ (0# , t₃)   ∼-  = joinˡ⁺ k₂ (1# , t₁) t₃ ∼-
+  joinʳ⁻ (suc _) k₂ t₁ (0# , t₃)   ∼0  = 1# , node k₂ t₁ t₃ ∼-
+  joinʳ⁻ (suc _) k₂ t₁ (0# , t₃)   ∼+  = 0# , node k₂ t₁ t₃ ∼0
+  joinʳ⁻ (suc _) k₂ t₁ (1# , t₃)   bal = 1# , node k₂ t₁ t₃ bal
 
   -- Extracts the smallest element from the tree, plus the rest.
   -- Logarithmic in the size of the tree.
 
-  headTail : ∀ {l u h} → Tree V l u (1 + h) →
-             ∃ λ (k : K& V) → l <⁺ [ k .key ] ×
-                            ∃ λ i → Tree V [ k .key ] u (i ⊕ h)
-  headTail (node k₁ (leaf l<k₁) t₂ ∼+) = (k₁ , l<k₁ , 0# , t₂)
-  headTail (node k₁ (leaf l<k₁) t₂ ∼0) = (k₁ , l<k₁ , 0# , t₂)
-  headTail (node {hˡ = suc _} k₃ t₁₂ t₄ bal) with headTail t₁₂
-  ... | (k₁ , l<k₁ , t₂) = (k₁ , l<k₁ , joinˡ⁻ _ k₃ t₂ t₄ bal)
+  headTail : Tree V l u (suc h) →
+             ∃ λ kv → let k = [ kv . key ] in l <⁺ k × Tree⁺ V k u h
+  headTail (node k₁ (leaf l<k₁) t₂ bal)
+    with refl ← 0∼⊔ bal                 = k₁ , l<k₁ , 0# , t₂
+  headTail (node k₃ t₁₂@(node _ _ _ _) t₄ bal)
+    using k₁ , l<k₁ , t₂ ← headTail t₁₂ = k₁ , l<k₁ , joinˡ⁻ _ k₃ t₂ t₄ bal
 
   -- Extracts the largest element from the tree, plus the rest.
   -- Logarithmic in the size of the tree.
 
-  initLast : ∀ {l u h} → Tree V l u (1 + h) →
-             ∃ λ (k : K& V) → [ k .key ] <⁺ u ×
-                            ∃ λ i → Tree V l [ k .key ] (i ⊕ h)
-  initLast (node k₂ t₁ (leaf k₂<u) ∼-) = (k₂ , k₂<u , (0# , t₁))
-  initLast (node k₂ t₁ (leaf k₂<u) ∼0) = (k₂ , k₂<u , (0# , t₁))
-  initLast (node {hʳ = suc _} k₂ t₁ t₃₄ bal) with initLast t₃₄
-  ... | (k₄ , k₄<u , t₃) = (k₄ , k₄<u , joinʳ⁻ _ k₂ t₁ t₃ bal)
+  initLast : Tree V l u (suc h) →
+             ∃ λ kv → let k = [ kv . key ] in k <⁺ u × Tree⁺ V l k h
+  initLast (node k₂ t₁ (leaf k₂<u) bal)
+    with refl ← ∼0⊔ bal                 = k₂ , k₂<u , 0# , t₁
+  initLast (node k₂ t₁ t₃₄@(node _ _ _ _) bal)
+    using k₄ , k₄<u , t₃ ← initLast t₃₄ = k₄ , k₄<u , joinʳ⁻ _ k₂ t₁ t₃ bal
 
   -- Another joining function. Logarithmic in the size of either of
   -- the input trees (which need to have almost equal heights).
 
-  join : ∀ {l m u hˡ hʳ h} →
-         Tree V l m hˡ → Tree V m u hʳ → (bal : hˡ ∼ hʳ ⊔ h) →
-         ∃ λ i → Tree V l u (i ⊕ h)
-  join t₁ (leaf m<u) ∼0 = (0# , castʳ t₁ m<u)
-  join t₁ (leaf m<u) ∼- = (0# , castʳ t₁ m<u)
-  join {hʳ = suc _} t₁ t₂₃ bal with headTail t₂₃
-  ... | (k₂ , m<k₂ , t₃) = joinʳ⁻ _ k₂ (castʳ t₁ m<k₂) t₃ bal
-
-  -- An empty tree.
-
-  empty : ∀ {l u} → l <⁺ u → Tree V l u 0
-  empty = leaf
-
-  -- A singleton tree.
-
-  singleton : ∀ {l u} (k : Key) → Val k → l < k < u → Tree V l u 1
-  singleton k v (l<k , k<u) = node (k , v) (leaf l<k) (leaf k<u) ∼0
+  join : Tree V l m hˡ → Tree V m u hʳ → hˡ ∼ hʳ ⊔ h → Tree⁺ V l u h
+  join t₁ (leaf m<u) bal
+    with refl ← ∼0⊔ bal                 = 0# , castʳ t₁ m<u
+  join t₁ t₂₃@(node _ _ _ _) bal
+    using k₂ , m<k₂ , t₃ ← headTail t₂₃ = joinʳ⁻ _ k₂ (castʳ t₁ m<k₂) t₃ bal
 
   -- Inserts a key into the tree, using a function to combine any
   -- existing value with the new value. Logarithmic in the size of the
   -- tree (assuming constant-time comparisons and a constant-time
   -- combining function).
 
-  insertWith : ∀ {l u h} (k : Key) → (Maybe (Val k) → Val k) →  -- Maybe old → result.
-               Tree V l u h → l < k < u →
-               ∃ λ i → Tree V l u (i ⊕ h)
-  insertWith k f (leaf l<u) l<k<u = (1# , singleton k (f nothing) l<k<u)
-  insertWith k f (node (k′ , v′) lp pu bal) (l<k , k<u) with compare k k′
-  ... | tri< k<k′ _ _ = joinˡ⁺ (k′ , v′) (insertWith k f lp (l<k , [ k<k′ ]ᴿ)) pu bal
-  ... | tri> _ _ k′<k = joinʳ⁺ (k′ , v′) lp (insertWith k f pu ([ k′<k ]ᴿ , k<u)) bal
-  ... | tri≈ _ k≈k′ _ = (0# , node (k′ , V≈ k≈k′ (f (just (V≈ (Eq.sym k≈k′) v′)))) lp pu bal)
+  insertWith : ∀ (k : Key) → (Maybe (Val k) → Val k) →  -- Maybe old → result.
+               Tree V l u h → l < k < u → Tree⁺ V l u h
+  insertWith k f (leaf l<u) l<k<u = 1# , singleton k (f nothing) l<k<u
+  insertWith k f (node kv@(k′ , v) lk ku bal) (l<k , k<u) with compare k k′
+  ... | tri< k<k′ _ _ = joinˡ⁺ kv (insertWith k f lk (l<k , [ k<k′ ]ᴿ)) ku bal
+  ... | tri> _ _ k′<k = joinʳ⁺ kv lk (insertWith k f ku ([ k′<k ]ᴿ , k<u)) bal
+  ... | tri≈ _ k≈k′ _ = 0# , node (k′ , v′) lk ku bal
+        where v′ = respects k≈k′ (f (just (respects (Eq.sym k≈k′) v)))
 
   -- Inserts a key into the tree. If the key already exists, then it
   -- is replaced. Logarithmic in the size of the tree (assuming
   -- constant-time comparisons).
 
-  insert : ∀ {l u h} → (k : Key) → Val k → Tree V l u h → l < k < u →
-           ∃ λ i → Tree V l u (i ⊕ h)
-  insert k v = insertWith k (F.const v)
+  insert : ∀ k → Val k → Tree V l u h → l < k < u → Tree⁺ V l u h
+  insert k v = insertWith k (Function.const v)
 
   -- Deletes the key/value pair containing the given key, if any.
   -- Logarithmic in the size of the tree (assuming constant-time
   -- comparisons).
 
-  delete : ∀ {l u h} (k : Key) → Tree V l u h → l < k < u →
-           ∃ λ i → Tree V l u pred[ i ⊕ h ]
-  delete k (leaf l<u) l<k<u = (0# , leaf l<u)
-  delete k (node p@(k′ , v) lp pu bal) (l<k , k<u) with compare k′ k
-  ... | tri< k′<k _ _ = joinʳ⁻ _ p lp (delete k pu ([ k′<k ]ᴿ , k<u)) bal
-  ... | tri> _ _ k′>k = joinˡ⁻ _ p (delete k lp (l<k , [ k′>k ]ᴿ)) pu bal
-  ... | tri≈ _ k′≡k _ = join lp pu bal
+  delete : ∀ k → Tree V l u h → l < k < u → Tree⁻ V l u h
+  delete k (leaf l<u) l<k<u = 0# , leaf l<u
+  delete k (node kv@(k′ , v) lk ku bal) (l<k , k<u) with compare k′ k
+  ... | tri< k′<k _ _ = joinʳ⁻ _ kv lk (delete k ku ([ k′<k ]ᴿ , k<u)) bal
+  ... | tri> _ _ k′>k = joinˡ⁻ _ kv (delete k lk (l<k , [ k′>k ]ᴿ)) ku bal
+  ... | tri≈ _ k′≡k _ = join lk ku bal
 
   -- Looks up a key. Logarithmic in the size of the tree (assuming
   -- constant-time comparisons).
 
-  lookup : ∀ {l u h} → Tree V l u h → (k : Key) → l < k < u → Maybe (Val k)
-  lookup (leaf _) k l<k<u = nothing
-  lookup (node (k′ , v) lk′ k′u _) k (l<k , k<u) with compare k′ k
-  ... | tri< k′<k _ _ = lookup k′u k ([ k′<k ]ᴿ , k<u)
-  ... | tri> _ _ k′>k = lookup lk′ k (l<k , [ k′>k ]ᴿ)
-  ... | tri≈ _ k′≡k _ = just (V≈ k′≡k v)
+  lookup : Tree V l u h → ∀ k → l < k < u → Maybe (Val k)
+  lookup (leaf _)                  k l<k<u       = nothing
+  lookup (node (k′ , v) lk ku _) k (l<k , k<u) with compare k′ k
+  ... | tri< k′<k _ _ = lookup ku k ([ k′<k ]ᴿ , k<u)
+  ... | tri> _ _ k′>k = lookup lk k (l<k , [ k′>k ]ᴿ)
+  ... | tri≈ _ k′≡k _ = just (respects k′≡k v)
 
   -- Converts the tree to an ordered list. Linear in the size of the
   -- tree.
 
-  foldr : ∀ {l u h} → (∀ {k} → Val k → A → A) → A → Tree V l u h → A
+  foldr : (∀ {k} → Val k → A → A) → A → Tree V l u h → A
   foldr cons nil (leaf l<u)             = nil
   foldr cons nil (node (_ , v) l r bal) = foldr cons (cons v (foldr cons nil r)) l
 
@@ -259,19 +278,8 @@ module _ {v} {V : Value v} where
   toDiffList (node k l r _) = toDiffList l ++ k ∷ toDiffList r
 
   toList : ∀ {l u h} → Tree V l u h → List (K& V)
-  toList t = toDiffList t List.[]
+  toList = DiffList.toList ∘ toDiffList
 
   size : ∀ {l u h} → Tree V l u h → ℕ
   size = List.length ∘′ toList
 
-module _ {v w} {V : Value v} {W : Value w} where
-
-  private
-    Val = Value.family V
-    Wal = Value.family W
-
-  -- Maps a function over all values in the tree.
-
-  map : ∀[ Val ⇒ Wal ] → ∀ {l u h} → Tree V l u h → Tree W l u h
-  map f (leaf l<u)             = leaf l<u
-  map f (node (k , v) l r bal) = node (k , f v) (map f l) (map f r) bal

From 47008bd0785a2c26d8f7a75c201d841b35f7d661 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 20 Mar 2026 09:32:12 +0000
Subject: [PATCH 05/35] refactor: use of `variable`s; tighten `import`s

---
 .../Tree/AVL/Indexed/Relation/Unary/Any.agda  | 35 ++++++++++---------
 1 file changed, 18 insertions(+), 17 deletions(-)

diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
index c81599da2a..2e7b636f5e 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
@@ -18,9 +18,9 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (_∘′_; _∘_)
 open import Level using (Level; _⊔_)
 open import Relation.Nullary.Decidable.Core using (Dec; no; map′; _⊎?_)
-open import Relation.Unary
+open import Relation.Unary using (Pred; _⊆_; Satisfiable; Decidable)
 
-open StrictTotalOrder strictTotalOrder renaming (Carrier to Key)
+open StrictTotalOrder strictTotalOrder using () renaming (Carrier to Key)
 open import Data.Tree.AVL.Indexed strictTotalOrder
   using (Tree; Value; Key⁺; [_]; _<⁺_; K&_; _,_; key; _∼_⊔_; ∼0; leaf; node)
 
@@ -31,9 +31,12 @@ private
     V : Value v
     P : Pred (K& V) p
     Q : Pred (K& V) q
+    k : Key
     l u : Key⁺
     n : ℕ
-    t : Tree V l u n
+    hˡ hʳ h : ℕ
+    t : Tree V l u h
+
 
 ------------------------------------------------------------------------
 -- Definition
@@ -42,20 +45,20 @@ private
 -- satisfies P. There may be others.
 -- See `Relation.Unary` for an explanation of predicates.
 
-data Any {V : Value v} (P : Pred (K& V) p) {l u}
-     : ∀ {n} → Tree V l u n → Set (p ⊔ a ⊔ v ⊔ ℓ₂) where
-  here  : ∀ {hˡ hʳ h} {kv : K& V} → P kv →
+data Any {V : Value v} (P : Pred (K& V) p)
+     : Tree V l u n → Set (p ⊔ a ⊔ v ⊔ ℓ₂) where
+  here  : ∀ {kv : K& V} → P kv →
           {lk : Tree V l [ kv .key ] hˡ}
           {ku : Tree V [ kv .key ] u hʳ}
           {bal : hˡ ∼ hʳ ⊔ h} →
           Any P (node kv lk ku bal)
-  left  : ∀ {hˡ hʳ h} {kv : K& V}
+  left  : ∀ {kv : K& V}
           {lk : Tree V l [ kv .key ] hˡ} →
           Any P lk →
           {ku : Tree V [ kv .key ] u hʳ}
           {bal : hˡ ∼ hʳ ⊔ h} →
           Any P (node kv lk ku bal)
-  right : ∀ {hˡ hʳ h} {kv : K& V}
+  right : ∀ {kv : K& V}
           {lk : Tree V l [ kv .key ] hˡ}
           {ku : Tree V [ kv .key ] u hʳ} →
           Any P ku →
@@ -80,12 +83,12 @@ lookupKey = key ∘′ lookup
 
 -- If any element satisfies P, then P is satisfied.
 
-satisfied : Any P t → ∃ P
+satisfied : Any P t → Satisfiable P
 satisfied (here  p) = -, p
 satisfied (left  p) = satisfied p
 satisfied (right p) = satisfied p
 
-module _ {hˡ hʳ h} {kv : K& V}
+module _ {kv : K& V}
   {lk : Tree V l [ kv .key ] hˡ}
   {ku : Tree V [ kv .key ] u hʳ}
   {bal : hˡ ∼ hʳ ⊔ h}
@@ -104,13 +107,11 @@ module _ {hˡ hʳ h} {kv : K& V}
 ------------------------------------------------------------------------
 -- Properties of predicates preserved by Any
 
-any? : Decidable P → (t : Tree V l u n) → Dec (Any P t)
-any? P? (leaf _)          = no λ ()
-any? P? (node kv l r bal) = map′ fromSum toSum
-  (P? kv ⊎? any? P? l ⊎? any? P? r)
+any? : Decidable P → Decidable {A = Tree V l u h} (Any P)
+any? P? (leaf _)        = no λ()
+any? P? (node kv l r _) = map′ fromSum toSum (P? kv ⊎? any? P? l ⊎? any? P? r)
 
-satisfiable : ∀ {k l u} → l <⁺ [ k ] → [ k ] <⁺ u →
+satisfiable : l <⁺ [ k ] → [ k ] <⁺ u →
               Satisfiable (P ∘ (k ,_)) →
               Satisfiable {A = Tree V l u 1} (Any P)
-satisfiable {k = k} lb ub sat = node (k , proj₁ sat) (leaf lb) (leaf ub) ∼0
-                              , here (proj₂ sat)
+satisfiable {k = k} lb ub (v , pv) = node (k , v) (leaf lb) (leaf ub) ∼0 , here pv

From 6535cd0b6c8ac51474ee304fe5ae2e6b011a8071 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 20 Mar 2026 10:01:54 +0000
Subject: [PATCH 06/35] tidy up: use of `variable`s; tighten `import`s

---
 src/Data/Tree/AVL/Indexed.agda                | 25 +++++++++----------
 .../Tree/AVL/Indexed/Relation/Unary/Any.agda  |  2 +-
 2 files changed, 13 insertions(+), 14 deletions(-)

diff --git a/src/Data/Tree/AVL/Indexed.agda b/src/Data/Tree/AVL/Indexed.agda
index c6ac393cf8..74bd58669a 100644
--- a/src/Data/Tree/AVL/Indexed.agda
+++ b/src/Data/Tree/AVL/Indexed.agda
@@ -13,7 +13,7 @@ module Data.Tree.AVL.Indexed
 
 open import Level using (Level; _⊔_)
 open import Data.Nat.Base using (ℕ; zero; suc; _+_)
-open import Data.Product.Base using (Σ; ∃; _×_; _,_; proj₁)
+open import Data.Product.Base using (Σ; ∃; _×_; _,_)
 open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Data.List.Base as List using (List)
 open import Data.DifferenceList as DiffList using (DiffList; []; _∷_; _++_)
@@ -22,7 +22,8 @@ open import Relation.Unary
 open import Relation.Binary.Definitions using (_Respects_; Tri; tri<; tri≈; tri>)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
-open StrictTotalOrder strictTotalOrder renaming (Carrier to Key)
+open StrictTotalOrder strictTotalOrder
+  using (module Eq; compare) renaming (Carrier to Key)
 
 ------------------------------------------------------------------------
 -- Re-export core definitions publicly
@@ -38,7 +39,6 @@ private
   variable
     ℓ v w : Level
     A : Set ℓ
-    k : Key
     l m u : Key⁺
     hˡ hʳ h : ℕ
 
@@ -51,10 +51,9 @@ private
 --
 -- (The bal argument is the balance factor.)
 
-data Tree {v} (V : Value v) (l u : Key⁺) : ℕ → Set (a ⊔ v ⊔ ℓ₂) where
+data Tree (V : Value v) (l u : Key⁺) : ℕ → Set (a ⊔ v ⊔ ℓ₂) where
   leaf : (l<u : l <⁺ u) → Tree V l u 0
-  node : ∀ {hˡ hʳ h}
-         (kv : K& V)
+  node : (kv : K& V)
          (lk : Tree V l [ kv .key ] hˡ)
          (ku : Tree V [ kv .key ] u hʳ)
          (bal : hˡ ∼ hʳ ⊔ h) →
@@ -86,7 +85,7 @@ module _ {V : Value v} {W : Value w}
 
 module _ {V : Value v} (open Value V using (respects) renaming (family to Val)) where
 
-  ordered : ∀ {l u n} → Tree V l u n → l <⁺ u
+  ordered : Tree V l u h → l <⁺ u
   ordered (leaf l<u)          = l<u
   ordered (node kv lk ku bal) = trans⁺ _ (ordered lk) (ordered ku)
 
@@ -100,7 +99,7 @@ module _ {V : Value v} (open Value V using (respects) renaming (family to Val))
 
   -- Injectivity of constructors
 
-  leaf-injective : ∀ {l u} {p q : l <⁺ u} → (Tree V l u 0 ∋ leaf p) ≡ leaf q → p ≡ q
+  leaf-injective : ∀ {p q : l <⁺ u} → (Tree V l u 0 ∋ leaf p) ≡ leaf q → p ≡ q
   leaf-injective refl = refl
 
   node-injective-key :
@@ -124,7 +123,7 @@ module _ {V : Value v} (open Value V using (respects) renaming (family to Val))
 
   -- A singleton tree.
 
-  singleton : ∀ (k : Key) → Val k → l < k < u → Tree V l u 1
+  singleton : ∀ k → Val k → l < k < u → Tree V l u 1
   singleton k v (l<k , k<u) = node (k , v) (leaf l<k) (leaf k<u) ∼0
 
   -- Cast operations. Logarithmic in the size of the tree, if we don't
@@ -229,7 +228,7 @@ module _ {V : Value v} (open Value V using (respects) renaming (family to Val))
   -- tree (assuming constant-time comparisons and a constant-time
   -- combining function).
 
-  insertWith : ∀ (k : Key) → (Maybe (Val k) → Val k) →  -- Maybe old → result.
+  insertWith : ∀ k → (Maybe (Val k) → Val k) →  -- Maybe old → result.
                Tree V l u h → l < k < u → Tree⁺ V l u h
   insertWith k f (leaf l<u) l<k<u = 1# , singleton k (f nothing) l<k<u
   insertWith k f (node kv@(k′ , v) lk ku bal) (l<k , k<u) with compare k k′
@@ -273,13 +272,13 @@ module _ {V : Value v} (open Value V using (respects) renaming (family to Val))
   foldr cons nil (leaf l<u)             = nil
   foldr cons nil (node (_ , v) l r bal) = foldr cons (cons v (foldr cons nil r)) l
 
-  toDiffList : ∀ {l u h} → Tree V l u h → DiffList (K& V)
+  toDiffList : Tree V l u h → DiffList (K& V)
   toDiffList (leaf _)       = []
   toDiffList (node k l r _) = toDiffList l ++ k ∷ toDiffList r
 
-  toList : ∀ {l u h} → Tree V l u h → List (K& V)
+  toList : Tree V l u h → List (K& V)
   toList = DiffList.toList ∘ toDiffList
 
-  size : ∀ {l u h} → Tree V l u h → ℕ
+  size : Tree V l u h → ℕ
   size = List.length ∘′ toList
 
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
index 2e7b636f5e..527e0b3788 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
@@ -81,7 +81,7 @@ lookup (right p)          = lookup p
 lookupKey : Any P t → Key
 lookupKey = key ∘′ lookup
 
--- If any element satisfies P, then P is satisfied.
+-- If any element satisfies P, then P is satisfiable.
 
 satisfied : Any P t → Satisfiable P
 satisfied (here  p) = -, p

From 21e69ddc5ea14e32cbd4b6d532b787d79e5aaf05 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 20 Mar 2026 10:05:53 +0000
Subject: [PATCH 07/35] fix: `CHANGELOG`

---
 CHANGELOG.md | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 99dea4e749..6c43eae734 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -397,6 +397,20 @@ Additions to existing modules
   showAtPrecision : ℕ → ℚᵘ → String
   ```
 
+* In `Data.Tree.AVL.Height`:
+  ```agda
+  0∼⊔ : 0 ∼ j ⊔ m → j ≡ m
+  ∼0⊔ : i ∼ 0 ⊔ m → i ≡ m
+  ```
+
+* In `Data.Tree.AVL.Indexed`:
+  ```agda
+  Tree⁺ Tree⁻ : (V : Value v) (l u : Key⁺) (h : ℕ) → Set _
+  pattern leaf⁻ l<u = _ , leaf l<u
+  pattern node⁰ʳ k₁ t₁ k₂ t₂ t₃ = node k₁ t₁ (node k₂ t₂ t₃ ∼0) ∼0
+  pattern node⁰ˡ k₁ k₂ t₁ t₂ t₃ = node k₁ (node k₂ t₁ t₂ ∼0) t₃ ∼0
+  ```
+
 * In `Data.Vec.Properties`:
   ```agda
   map-removeAt : ∀ (f : A → B) (xs : Vec A (suc n)) (i : Fin (suc n)) →

From 10d8877e67c6057600c013b2c9a3d7ff843b3267 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 20 Mar 2026 10:06:47 +0000
Subject: [PATCH 08/35] fix: whitespace

---
 src/Data/Tree/AVL/Indexed.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Tree/AVL/Indexed.agda b/src/Data/Tree/AVL/Indexed.agda
index 74bd58669a..9510b125ae 100644
--- a/src/Data/Tree/AVL/Indexed.agda
+++ b/src/Data/Tree/AVL/Indexed.agda
@@ -90,7 +90,7 @@ module _ {V : Value v} (open Value V using (respects) renaming (family to Val))
   ordered (node kv lk ku bal) = trans⁺ _ (ordered lk) (ordered ku)
 
   private
-  
+
   -- This lemma justifies the use of `leaf⁻` pattern matches in code below
 
     tree⁻0 : (t⁻ : Tree⁻ V l u 0) →

From a1615e7cbc6ecefd487d1cb61a69fd03f1635cf8 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 25 Mar 2026 09:29:38 +0000
Subject: [PATCH 09/35] fix: remove `n` as a name for height `h`

---
 src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
index 527e0b3788..100584948c 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
@@ -33,7 +33,6 @@ private
     Q : Pred (K& V) q
     k : Key
     l u : Key⁺
-    n : ℕ
     hˡ hʳ h : ℕ
     t : Tree V l u h
 
@@ -46,7 +45,7 @@ private
 -- See `Relation.Unary` for an explanation of predicates.
 
 data Any {V : Value v} (P : Pred (K& V) p)
-     : Tree V l u n → Set (p ⊔ a ⊔ v ⊔ ℓ₂) where
+     : Tree V l u h → Set (p ⊔ a ⊔ v ⊔ ℓ₂) where
   here  : ∀ {kv : K& V} → P kv →
           {lk : Tree V l [ kv .key ] hˡ}
           {ku : Tree V [ kv .key ] u hʳ}

From f40e5726913e9cba104be6551b0415b6560f0fe2 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 25 Mar 2026 09:36:19 +0000
Subject: [PATCH 10/35] add: `private` lemma `tree0`

---
 src/Data/Tree/AVL/Indexed.agda | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/Data/Tree/AVL/Indexed.agda b/src/Data/Tree/AVL/Indexed.agda
index 9510b125ae..fac711cbec 100644
--- a/src/Data/Tree/AVL/Indexed.agda
+++ b/src/Data/Tree/AVL/Indexed.agda
@@ -91,7 +91,10 @@ module _ {V : Value v} (open Value V using (respects) renaming (family to Val))
 
   private
 
-  -- This lemma justifies the use of `leaf⁻` pattern matches in code below
+  -- Lemmas justifying the use of `leaf`/`leaf⁻` pattern matches in code below
+
+    tree0 : (t : Tree V l u 0) → t ≡ leaf (ordered t)
+    tree0 t@(leaf _) = refl
 
     tree⁻0 : (t⁻ : Tree⁻ V l u 0) →
              ∃ λ i → ∃ λ t → t⁻ ≡ (i , t) × t ≡ leaf (ordered t)
@@ -281,4 +284,3 @@ module _ {V : Value v} (open Value V using (respects) renaming (family to Val))
 
   size : Tree V l u h → ℕ
   size = List.length ∘′ toList
-

From 75fd7422c67636e2a244ee5a5ab7c4eda8e4db6c Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 25 Mar 2026 09:46:17 +0000
Subject: [PATCH 11/35] refactor: rename and deprecate

---
 CHANGELOG.md                                  |  8 ++
 .../Relation/Unary/Any/Properties.agda        | 77 ++++++++++++++-----
 2 files changed, 64 insertions(+), 21 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6c43eae734..62062b45f6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -104,6 +104,14 @@ Deprecated names
   nonPos*nonPos⇒nonPos  ↦  nonPos*nonPos⇒nonNeg
   ```
 
+* In `Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties`:
+  ```agda
+  Any-insertWith-nothing  ↦  insertWith-nothing
+  Any-insertWith-just     ↦  insertWith-just
+  Any-insert-nothing      ↦  insert-nothing
+  Any-insert-just         ↦  insert-just
+  ```
+
 * In `Data.Vec.Properties`:
   ```agda
   truncate-irrelevant  ↦  Relation.Binary.PropositionalEquality.Core.refl
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
index c2762172b9..322b7daac3 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
@@ -249,31 +249,33 @@ module _ {V : Value v} where
 
     open <-Reasoning AVL.strictPartialOrder
 
-    Any-insertWith-nothing : (t : Tree V l u n) (seg : l < k < u) →
-                             P (k , f nothing) →
-                             ¬ (Any ((k ≈_) ∘′ key) t) → Any P (proj₂ (insertWith k f t seg))
-    Any-insertWith-nothing (leaf l<u)                   seg         pr ¬p = here pr
-    Any-insertWith-nothing (node kv@(k′ , v) lk ku bal) (l<k , k<u) pr ¬p
+    insertWith-nothing : (t : Tree V l u n) (seg : l < k < u) →
+                         P (k , f nothing) →
+                         ¬ (Any ((k ≈_) ∘′ key) t) →
+                         Any P (proj₂ (insertWith k f t seg))
+    insertWith-nothing (leaf l<u)                   seg         pr ¬p = here pr
+    insertWith-nothing (node kv@(k′ , v) lk ku bal) (l<k , k<u) pr ¬p
       with compare k k′
     ... | tri≈ _ k≈k′ _ = contradiction (here k≈k′) ¬p
     ... | tri< k<k′ _ _ = let seg′ = l<k , [ k<k′ ]ᴿ; lk′ = insertWith k f lk seg′
-                              ih = Any-insertWith-nothing lk seg′ pr (λ p → ¬p (left p))
+                              ih = insertWith-nothing lk seg′ pr (λ p → ¬p (left p))
                           in joinˡ⁺-left⁺ kv lk′ ku bal ih
     ... | tri> _ _ k>k′ = let seg′ = [ k>k′ ]ᴿ , k<u; ku′ = insertWith k f ku seg′
-                              ih = Any-insertWith-nothing ku seg′ pr (λ p → ¬p (right p))
+                              ih = insertWith-nothing ku seg′ pr (λ p → ¬p (right p))
                           in joinʳ⁺-right⁺ kv lk ku′ bal ih
 
-    Any-insertWith-just : (t : Tree V l u n) (seg : l < k < u) →
-                          (pr : ∀ k′ v → (eq : k ≈ k′) → P (k′ , Val≈ eq (f (just (Val≈ (sym eq) v))))) →
-                          Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insertWith k f t seg))
-    Any-insertWith-just (node kv@(k′ , v) lk ku bal) (l<k , k<u) pr p
+    insertWith-just : (t : Tree V l u n) (seg : l < k < u) →
+                      (pr : ∀ k′ v → (eq : k ≈ k′) →
+                            P (k′ , Val≈ eq (f (just (Val≈ (sym eq) v))))) →
+                      Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insertWith k f t seg))
+    insertWith-just (node kv@(k′ , v) lk ku bal) (l<k , k<u) pr p
       with p | compare k k′
     -- happy paths
     ... | here _   | tri≈ _ k≈k′ _ = here (pr k′ v k≈k′)
     ... | left lp  | tri< k<k′ _ _ = let seg′ = l<k , [ k<k′ ]ᴿ; lk′ = insertWith k f lk seg′ in
-                                     joinˡ⁺-left⁺ kv lk′ ku bal (Any-insertWith-just lk seg′ pr lp)
+                                     joinˡ⁺-left⁺ kv lk′ ku bal (insertWith-just lk seg′ pr lp)
     ... | right rp | tri> _ _ k>k′ = let seg′ = [ k>k′ ]ᴿ , k<u; ku′ = insertWith k f ku seg′ in
-                                     joinʳ⁺-right⁺ kv lk ku′ bal (Any-insertWith-just ku seg′ pr rp)
+                                     joinʳ⁺-right⁺ kv lk ku′ bal (insertWith-just ku seg′ pr rp)
 
     -- impossible cases
     ... | here eq  | tri< k<k′ _ _ = begin-contradiction
@@ -311,17 +313,18 @@ module _ {V : Value v} where
 
   module _ (k : Key) (v : Val k) (t : Tree V l u n) (seg : l < k < u) where
 
-    Any-insert-nothing : P (k , v) → ¬ (Any ((k ≈_) ∘′ key) t) → Any P (proj₂ (insert k v t seg))
-    Any-insert-nothing = Any-insertWith-nothing k (F.const v) t seg
+    insert-nothing : P (k , v) → ¬ (Any ((k ≈_) ∘′ key) t) →
+                     Any P (proj₂ (insert k v t seg))
+    insert-nothing = insertWith-nothing k (F.const v) t seg
 
-    Any-insert-just : (pr : ∀ k′ → (eq : k ≈ k′) → P (k′ , Val≈ eq v)) →
-                      Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insert k v t seg))
-    Any-insert-just pr = Any-insertWith-just k (F.const v) t seg (λ k′ _ eq → pr k′ eq)
+    insert-just : (pr : ∀ k′ → (eq : k ≈ k′) → P (k′ , Val≈ eq v)) →
+                  Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insert k v t seg))
+    insert-just pr = insertWith-just k (F.const v) t seg (λ k′ _ eq → pr k′ eq)
 
   module _ (k : Key) (f : Maybe (Val k) → Val k) where
 
     insertWith⁺ : (t : Tree V l u n) (seg : l < k < u) →
-                  (p : Any P t) → k ≉ Any.lookupKey p →
+                  (p : Any P t) → k ≉ lookupKey p →
                   Any P (proj₂ (insertWith k f t seg))
     insertWith⁺ (node kv@(k′ , v′) l r bal) (l<k , k<u) (here p) k≉
       with compare k k′
@@ -348,7 +351,7 @@ module _ {V : Value v} where
                           in joinʳ⁺-right⁺ kv l r′ bal ih
 
   insert⁺ : (k : Key) (v : Val k) (t : Tree V l u n) (seg : l < k < u) →
-            (p : Any P t) → k ≉ Any.lookupKey p →
+            (p : Any P t) → k ≉ lookupKey p →
             Any P (proj₂ (insert k v t seg))
   insert⁺ k v = insertWith⁺ k (F.const v)
 
@@ -393,7 +396,7 @@ module _ {V : Value v} where
 
   lookup⁺ : (t : Tree V l u n) (k : Key) (seg : l < k < u) →
             (p : Any P t) →
-            key (Any.lookup p) ≉ k ⊎ ∃[ p≈k ] AVL.lookup t k seg ≡ just (Val≈ p≈k (value (Any.lookup p)))
+            lookupKey p ≉ k ⊎ ∃[ p≈k ] AVL.lookup t k seg ≡ just (Val≈ p≈k (value (Any.lookup p)))
   lookup⁺ (node (k′ , v′) l r bal) k (l<k , k<u) p
       with compare k′ k | p
   ... | tri< k′<k _ _ | right p = lookup⁺ r k ([ k′<k ]ᴿ , k<u) p
@@ -417,3 +420,35 @@ module _ {V : Value v} where
   ... | tri< k′<k _ _ = right (lookup⁻ r k v ([ k′<k ]ᴿ , k<u) eq)
   ... | tri≈ _ k′≈k _ = here (k′≈k , just-injective eq)
   ... | tri> _ _ k<k′ = left (lookup⁻ l k v (l<k , [ k<k′ ]ᴿ) eq)
+
+
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.4
+
+Any-insertWith-nothing = insertWith-nothing
+{-# WARNING_ON_USAGE Any-insertWith-nothing
+"Warning: Any-insertWith-nothing was deprecated in v2.4.
+Please use insertWith-nothing instead."
+#-}
+Any-insertWith-just = insertWith-just
+{-# WARNING_ON_USAGE Any-insertWith-just
+"Warning: Any-insertWith-just was deprecated in v2.4.
+Please use insertWith-just instead."
+#-}
+Any-insert-nothing = insert-nothing
+{-# WARNING_ON_USAGE Any-insert-nothing
+"Warning: Any-insert-nothing was deprecated in v2.4.
+Please use insert-nothing instead."
+#-}
+Any-insert-just = insert-just
+{-# WARNING_ON_USAGE Any-insert-just
+"Warning: Any-insert-just was deprecated in v2.4.
+Please use insert-just instead."
+#-}

From 3795466c46e61629c394065ab1919f0d931f74f1 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 25 Mar 2026 15:02:03 +0000
Subject: [PATCH 12/35] revert: renaming/deprecation

---
 CHANGELOG.md                                  |  8 --
 .../Relation/Unary/Any/Properties.agda        | 76 ++++++-------------
 2 files changed, 23 insertions(+), 61 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 62062b45f6..6c43eae734 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -104,14 +104,6 @@ Deprecated names
   nonPos*nonPos⇒nonPos  ↦  nonPos*nonPos⇒nonNeg
   ```
 
-* In `Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties`:
-  ```agda
-  Any-insertWith-nothing  ↦  insertWith-nothing
-  Any-insertWith-just     ↦  insertWith-just
-  Any-insert-nothing      ↦  insert-nothing
-  Any-insert-just         ↦  insert-just
-  ```
-
 * In `Data.Vec.Properties`:
   ```agda
   truncate-irrelevant  ↦  Relation.Binary.PropositionalEquality.Core.refl
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
index 322b7daac3..013ee3029b 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
@@ -249,33 +249,33 @@ module _ {V : Value v} where
 
     open <-Reasoning AVL.strictPartialOrder
 
-    insertWith-nothing : (t : Tree V l u n) (seg : l < k < u) →
-                         P (k , f nothing) →
-                         ¬ (Any ((k ≈_) ∘′ key) t) →
-                         Any P (proj₂ (insertWith k f t seg))
-    insertWith-nothing (leaf l<u)                   seg         pr ¬p = here pr
-    insertWith-nothing (node kv@(k′ , v) lk ku bal) (l<k , k<u) pr ¬p
+    Any-insertWith-nothing : (t : Tree V l u n) (seg : l < k < u) →
+                             P (k , f nothing) →
+                             ¬ (Any ((k ≈_) ∘′ key) t) →
+                             Any P (proj₂ (insertWith k f t seg))
+    Any-insertWith-nothing (leaf l<u)                   seg         pr ¬p = here pr
+    Any-insertWith-nothing (node kv@(k′ , v) lk ku bal) (l<k , k<u) pr ¬p
       with compare k k′
     ... | tri≈ _ k≈k′ _ = contradiction (here k≈k′) ¬p
     ... | tri< k<k′ _ _ = let seg′ = l<k , [ k<k′ ]ᴿ; lk′ = insertWith k f lk seg′
-                              ih = insertWith-nothing lk seg′ pr (λ p → ¬p (left p))
+                              ih = Any-insertWith-nothing lk seg′ pr (λ p → ¬p (left p))
                           in joinˡ⁺-left⁺ kv lk′ ku bal ih
     ... | tri> _ _ k>k′ = let seg′ = [ k>k′ ]ᴿ , k<u; ku′ = insertWith k f ku seg′
-                              ih = insertWith-nothing ku seg′ pr (λ p → ¬p (right p))
+                              ih = Any-insertWith-nothing ku seg′ pr (λ p → ¬p (right p))
                           in joinʳ⁺-right⁺ kv lk ku′ bal ih
 
-    insertWith-just : (t : Tree V l u n) (seg : l < k < u) →
+    Any-insertWith-just : (t : Tree V l u n) (seg : l < k < u) →
                       (pr : ∀ k′ v → (eq : k ≈ k′) →
                             P (k′ , Val≈ eq (f (just (Val≈ (sym eq) v))))) →
                       Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insertWith k f t seg))
-    insertWith-just (node kv@(k′ , v) lk ku bal) (l<k , k<u) pr p
+    Any-insertWith-just (node kv@(k′ , v) lk ku bal) (l<k , k<u) pr p
       with p | compare k k′
     -- happy paths
     ... | here _   | tri≈ _ k≈k′ _ = here (pr k′ v k≈k′)
     ... | left lp  | tri< k<k′ _ _ = let seg′ = l<k , [ k<k′ ]ᴿ; lk′ = insertWith k f lk seg′ in
-                                     joinˡ⁺-left⁺ kv lk′ ku bal (insertWith-just lk seg′ pr lp)
+                                     joinˡ⁺-left⁺ kv lk′ ku bal (Any-insertWith-just lk seg′ pr lp)
     ... | right rp | tri> _ _ k>k′ = let seg′ = [ k>k′ ]ᴿ , k<u; ku′ = insertWith k f ku seg′ in
-                                     joinʳ⁺-right⁺ kv lk ku′ bal (insertWith-just ku seg′ pr rp)
+                                     joinʳ⁺-right⁺ kv lk ku′ bal (Any-insertWith-just ku seg′ pr rp)
 
     -- impossible cases
     ... | here eq  | tri< k<k′ _ _ = begin-contradiction
@@ -315,45 +315,45 @@ module _ {V : Value v} where
 
     insert-nothing : P (k , v) → ¬ (Any ((k ≈_) ∘′ key) t) →
                      Any P (proj₂ (insert k v t seg))
-    insert-nothing = insertWith-nothing k (F.const v) t seg
+    insert-nothing = Any-insertWith-nothing k (F.const v) t seg
 
     insert-just : (pr : ∀ k′ → (eq : k ≈ k′) → P (k′ , Val≈ eq v)) →
                   Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insert k v t seg))
-    insert-just pr = insertWith-just k (F.const v) t seg (λ k′ _ eq → pr k′ eq)
+    insert-just pr = Any-insertWith-just k (F.const v) t seg (λ k′ _ eq → pr k′ eq)
 
   module _ (k : Key) (f : Maybe (Val k) → Val k) where
 
-    insertWith⁺ : (t : Tree V l u n) (seg : l < k < u) →
-                  (p : Any P t) → k ≉ lookupKey p →
-                  Any P (proj₂ (insertWith k f t seg))
-    insertWith⁺ (node kv@(k′ , v′) l r bal) (l<k , k<u) (here p) k≉
+    Any-insertWith⁺ : (t : Tree V l u n) (seg : l < k < u) →
+                      (p : Any P t) → k ≉ lookupKey p →
+                      Any P (proj₂ (insertWith k f t seg))
+    Any-insertWith⁺ (node kv@(k′ , v′) l r bal) (l<k , k<u) (here p) k≉
       with compare k k′
     ... | tri< k<k′ _ _ = let l′ = insertWith k f l (l<k , [ k<k′ ]ᴿ)
                           in joinˡ⁺-here⁺ kv l′ r bal p
     ... | tri≈ _ k≈k′ _ = contradiction k≈k′ k≉
     ... | tri> _ _ k′<k = let r′ = insertWith k f r ([ k′<k ]ᴿ , k<u)
                           in joinʳ⁺-here⁺ kv l r′ bal p
-    insertWith⁺ (node kv@(k′ , v′) l r bal) (l<k , k<u) (left p) k≉
+    Any-insertWith⁺ (node kv@(k′ , v′) l r bal) (l<k , k<u) (left p) k≉
       with compare k k′
     ... | tri< k<k′ _ _ = let l′ = insertWith k f l (l<k , [ k<k′ ]ᴿ)
-                              ih = insertWith⁺ l (l<k , [ k<k′ ]ᴿ) p k≉
+                              ih = Any-insertWith⁺ l (l<k , [ k<k′ ]ᴿ) p k≉
                           in joinˡ⁺-left⁺ kv l′ r bal ih
     ... | tri≈ _ k≈k′ _ = left p
     ... | tri> _ _ k′<k = let r′ = insertWith k f r ([ k′<k ]ᴿ , k<u)
                           in joinʳ⁺-left⁺ kv l r′ bal p
-    insertWith⁺ (node kv@(k′ , v′) l r bal) (l<k , k<u) (right p) k≉
+    Any-insertWith⁺ (node kv@(k′ , v′) l r bal) (l<k , k<u) (right p) k≉
       with compare k k′
     ... | tri< k<k′ _ _ = let l′ = insertWith k f l (l<k , [ k<k′ ]ᴿ)
                           in joinˡ⁺-right⁺ kv l′ r bal p
     ... | tri≈ _ k≈k′ _ = right p
     ... | tri> _ _ k′<k = let r′ = insertWith k f r ([ k′<k ]ᴿ , k<u)
-                              ih = insertWith⁺ r ([ k′<k ]ᴿ , k<u) p k≉
+                              ih = Any-insertWith⁺ r ([ k′<k ]ᴿ , k<u) p k≉
                           in joinʳ⁺-right⁺ kv l r′ bal ih
 
   insert⁺ : (k : Key) (v : Val k) (t : Tree V l u n) (seg : l < k < u) →
             (p : Any P t) → k ≉ lookupKey p →
             Any P (proj₂ (insert k v t seg))
-  insert⁺ k v = insertWith⁺ k (F.const v)
+  insert⁺ k v = Any-insertWith⁺ k (F.const v)
 
   module _
     {P : Pred (K& V) p}
@@ -422,33 +422,3 @@ module _ {V : Value v} where
   ... | tri> _ _ k<k′ = left (lookup⁻ l k v (l<k , [ k<k′ ]ᴿ) eq)
 
 
-
-
-------------------------------------------------------------------------
--- DEPRECATED NAMES
-------------------------------------------------------------------------
--- Please use the new names as continuing support for the old names is
--- not guaranteed.
-
--- Version 2.4
-
-Any-insertWith-nothing = insertWith-nothing
-{-# WARNING_ON_USAGE Any-insertWith-nothing
-"Warning: Any-insertWith-nothing was deprecated in v2.4.
-Please use insertWith-nothing instead."
-#-}
-Any-insertWith-just = insertWith-just
-{-# WARNING_ON_USAGE Any-insertWith-just
-"Warning: Any-insertWith-just was deprecated in v2.4.
-Please use insertWith-just instead."
-#-}
-Any-insert-nothing = insert-nothing
-{-# WARNING_ON_USAGE Any-insert-nothing
-"Warning: Any-insert-nothing was deprecated in v2.4.
-Please use insert-nothing instead."
-#-}
-Any-insert-just = insert-just
-{-# WARNING_ON_USAGE Any-insert-just
-"Warning: Any-insert-just was deprecated in v2.4.
-Please use insert-just instead."
-#-}

From 23f34985c0ebc3a1271fbd429dc855ab29a090a5 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 25 Mar 2026 15:06:32 +0000
Subject: [PATCH 13/35] fix: more things

---
 .../AVL/Indexed/Relation/Unary/Any/Properties.agda   | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
index 013ee3029b..4039064368 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
@@ -313,13 +313,13 @@ module _ {V : Value v} where
 
   module _ (k : Key) (v : Val k) (t : Tree V l u n) (seg : l < k < u) where
 
-    insert-nothing : P (k , v) → ¬ (Any ((k ≈_) ∘′ key) t) →
-                     Any P (proj₂ (insert k v t seg))
-    insert-nothing = Any-insertWith-nothing k (F.const v) t seg
+    Any-insert-nothing : P (k , v) → ¬ (Any ((k ≈_) ∘′ key) t) →
+                         Any P (proj₂ (insert k v t seg))
+    Any-insert-nothing = Any-insertWith-nothing k (F.const v) t seg
 
-    insert-just : (pr : ∀ k′ → (eq : k ≈ k′) → P (k′ , Val≈ eq v)) →
-                  Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insert k v t seg))
-    insert-just pr = Any-insertWith-just k (F.const v) t seg (λ k′ _ eq → pr k′ eq)
+    Any-insert-just : (pr : ∀ k′ → (eq : k ≈ k′) → P (k′ , Val≈ eq v)) →
+                      Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insert k v t seg))
+    Any-insert-just pr = Any-insertWith-just k (F.const v) t seg (λ k′ _ eq → pr k′ eq)
 
   module _ (k : Key) (f : Maybe (Val k) → Val k) where
 

From 1a1b8abd23e0a19181e4ca95cb9bad5c969a338c Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 25 Mar 2026 15:09:17 +0000
Subject: [PATCH 14/35] fix: more things

---
 .../AVL/Indexed/Relation/Unary/Any/Properties.agda    | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
index 4039064368..5ca1fdd10d 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
@@ -251,8 +251,7 @@ module _ {V : Value v} where
 
     Any-insertWith-nothing : (t : Tree V l u n) (seg : l < k < u) →
                              P (k , f nothing) →
-                             ¬ (Any ((k ≈_) ∘′ key) t) →
-                             Any P (proj₂ (insertWith k f t seg))
+                             ¬ (Any ((k ≈_) ∘′ key) t) → Any P (proj₂ (insertWith k f t seg))
     Any-insertWith-nothing (leaf l<u)                   seg         pr ¬p = here pr
     Any-insertWith-nothing (node kv@(k′ , v) lk ku bal) (l<k , k<u) pr ¬p
       with compare k k′
@@ -265,9 +264,8 @@ module _ {V : Value v} where
                           in joinʳ⁺-right⁺ kv lk ku′ bal ih
 
     Any-insertWith-just : (t : Tree V l u n) (seg : l < k < u) →
-                      (pr : ∀ k′ v → (eq : k ≈ k′) →
-                            P (k′ , Val≈ eq (f (just (Val≈ (sym eq) v))))) →
-                      Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insertWith k f t seg))
+                          (pr : ∀ k′ v → (eq : k ≈ k′) → P (k′ , Val≈ eq (f (just (Val≈ (sym eq) v))))) →
+                          Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insertWith k f t seg))
     Any-insertWith-just (node kv@(k′ , v) lk ku bal) (l<k , k<u) pr p
       with p | compare k k′
     -- happy paths
@@ -313,8 +311,7 @@ module _ {V : Value v} where
 
   module _ (k : Key) (v : Val k) (t : Tree V l u n) (seg : l < k < u) where
 
-    Any-insert-nothing : P (k , v) → ¬ (Any ((k ≈_) ∘′ key) t) →
-                         Any P (proj₂ (insert k v t seg))
+    Any-insert-nothing : P (k , v) → ¬ (Any ((k ≈_) ∘′ key) t) → Any P (proj₂ (insert k v t seg))
     Any-insert-nothing = Any-insertWith-nothing k (F.const v) t seg
 
     Any-insert-just : (pr : ∀ k′ → (eq : k ≈ k′) → P (k′ , Val≈ eq v)) →

From a34eb52e058134bf2357668b5444cec02a2a37bb Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 25 Mar 2026 15:10:35 +0000
Subject: [PATCH 15/35] fix: more things

---
 .../AVL/Indexed/Relation/Unary/Any/Properties.agda | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
index 5ca1fdd10d..acd10032b0 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
@@ -320,37 +320,37 @@ module _ {V : Value v} where
 
   module _ (k : Key) (f : Maybe (Val k) → Val k) where
 
-    Any-insertWith⁺ : (t : Tree V l u n) (seg : l < k < u) →
+    insertWith⁺ : (t : Tree V l u n) (seg : l < k < u) →
                       (p : Any P t) → k ≉ lookupKey p →
                       Any P (proj₂ (insertWith k f t seg))
-    Any-insertWith⁺ (node kv@(k′ , v′) l r bal) (l<k , k<u) (here p) k≉
+    insertWith⁺ (node kv@(k′ , v′) l r bal) (l<k , k<u) (here p) k≉
       with compare k k′
     ... | tri< k<k′ _ _ = let l′ = insertWith k f l (l<k , [ k<k′ ]ᴿ)
                           in joinˡ⁺-here⁺ kv l′ r bal p
     ... | tri≈ _ k≈k′ _ = contradiction k≈k′ k≉
     ... | tri> _ _ k′<k = let r′ = insertWith k f r ([ k′<k ]ᴿ , k<u)
                           in joinʳ⁺-here⁺ kv l r′ bal p
-    Any-insertWith⁺ (node kv@(k′ , v′) l r bal) (l<k , k<u) (left p) k≉
+    insertWith⁺ (node kv@(k′ , v′) l r bal) (l<k , k<u) (left p) k≉
       with compare k k′
     ... | tri< k<k′ _ _ = let l′ = insertWith k f l (l<k , [ k<k′ ]ᴿ)
-                              ih = Any-insertWith⁺ l (l<k , [ k<k′ ]ᴿ) p k≉
+                              ih = insertWith⁺ l (l<k , [ k<k′ ]ᴿ) p k≉
                           in joinˡ⁺-left⁺ kv l′ r bal ih
     ... | tri≈ _ k≈k′ _ = left p
     ... | tri> _ _ k′<k = let r′ = insertWith k f r ([ k′<k ]ᴿ , k<u)
                           in joinʳ⁺-left⁺ kv l r′ bal p
-    Any-insertWith⁺ (node kv@(k′ , v′) l r bal) (l<k , k<u) (right p) k≉
+    insertWith⁺ (node kv@(k′ , v′) l r bal) (l<k , k<u) (right p) k≉
       with compare k k′
     ... | tri< k<k′ _ _ = let l′ = insertWith k f l (l<k , [ k<k′ ]ᴿ)
                           in joinˡ⁺-right⁺ kv l′ r bal p
     ... | tri≈ _ k≈k′ _ = right p
     ... | tri> _ _ k′<k = let r′ = insertWith k f r ([ k′<k ]ᴿ , k<u)
-                              ih = Any-insertWith⁺ r ([ k′<k ]ᴿ , k<u) p k≉
+                              ih = insertWith⁺ r ([ k′<k ]ᴿ , k<u) p k≉
                           in joinʳ⁺-right⁺ kv l r′ bal ih
 
   insert⁺ : (k : Key) (v : Val k) (t : Tree V l u n) (seg : l < k < u) →
             (p : Any P t) → k ≉ lookupKey p →
             Any P (proj₂ (insert k v t seg))
-  insert⁺ k v = Any-insertWith⁺ k (F.const v)
+  insert⁺ k v = insertWith⁺ k (F.const v)
 
   module _
     {P : Pred (K& V) p}

From bfb3e9a3d8b0d69703eb1dfee54aaf2e3f06db16 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 25 Mar 2026 15:13:12 +0000
Subject: [PATCH 16/35] fix: final things?

---
 .../AVL/Indexed/Relation/Unary/Any/Properties.agda     | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
index acd10032b0..c2762172b9 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
@@ -321,8 +321,8 @@ module _ {V : Value v} where
   module _ (k : Key) (f : Maybe (Val k) → Val k) where
 
     insertWith⁺ : (t : Tree V l u n) (seg : l < k < u) →
-                      (p : Any P t) → k ≉ lookupKey p →
-                      Any P (proj₂ (insertWith k f t seg))
+                  (p : Any P t) → k ≉ Any.lookupKey p →
+                  Any P (proj₂ (insertWith k f t seg))
     insertWith⁺ (node kv@(k′ , v′) l r bal) (l<k , k<u) (here p) k≉
       with compare k k′
     ... | tri< k<k′ _ _ = let l′ = insertWith k f l (l<k , [ k<k′ ]ᴿ)
@@ -348,7 +348,7 @@ module _ {V : Value v} where
                           in joinʳ⁺-right⁺ kv l r′ bal ih
 
   insert⁺ : (k : Key) (v : Val k) (t : Tree V l u n) (seg : l < k < u) →
-            (p : Any P t) → k ≉ lookupKey p →
+            (p : Any P t) → k ≉ Any.lookupKey p →
             Any P (proj₂ (insert k v t seg))
   insert⁺ k v = insertWith⁺ k (F.const v)
 
@@ -393,7 +393,7 @@ module _ {V : Value v} where
 
   lookup⁺ : (t : Tree V l u n) (k : Key) (seg : l < k < u) →
             (p : Any P t) →
-            lookupKey p ≉ k ⊎ ∃[ p≈k ] AVL.lookup t k seg ≡ just (Val≈ p≈k (value (Any.lookup p)))
+            key (Any.lookup p) ≉ k ⊎ ∃[ p≈k ] AVL.lookup t k seg ≡ just (Val≈ p≈k (value (Any.lookup p)))
   lookup⁺ (node (k′ , v′) l r bal) k (l<k , k<u) p
       with compare k′ k | p
   ... | tri< k′<k _ _ | right p = lookup⁺ r k ([ k′<k ]ᴿ , k<u) p
@@ -417,5 +417,3 @@ module _ {V : Value v} where
   ... | tri< k′<k _ _ = right (lookup⁻ r k v ([ k′<k ]ᴿ , k<u) eq)
   ... | tri≈ _ k′≈k _ = here (k′≈k , just-injective eq)
   ... | tri> _ _ k<k′ = left (lookup⁻ l k v (l<k , [ k<k′ ]ᴿ) eq)
-
-

From b4a68f15b2a4d6584299c29eafb0893ba0d087e9 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 2 Apr 2026 10:27:01 +0100
Subject: [PATCH 17/35] tidy up: `Properties.Delete`

---
 .../Tree/AVL/Indexed/Relation/Unary/Any/Properties/Delete.agda  | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Delete.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Delete.agda
index 1b48c29b63..4a27c96dfc 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Delete.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Delete.agda
@@ -140,6 +140,6 @@ module _ (k : Key) where
 
   delete-key⁻ : (t : Tree V l u h) (seg : l < k < u) →
                 (p : Any P (proj₂ (delete k t seg))) →
-                Any.lookupKey p ≉ k
+                lookupKey p ≉ k
   delete-key⁻ t seg p kp≈k =
     delete-key-∈⁻ k t seg (lookup-rebuild p Eq.refl) kp≈k

From e508b20fb0c4f372d421884109ee8c32d9c89344 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 2 Apr 2026 12:33:19 +0100
Subject: [PATCH 18/35] tidy up: `Properties.Insert`

---
 CHANGELOG.md                                  |  8 +++
 .../Relation/Unary/Any/Properties/Insert.agda | 69 ++++++++++++++-----
 2 files changed, 58 insertions(+), 19 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d1626d2a92..f47178994b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -109,6 +109,14 @@ Deprecated names
   nonPos*nonPos⇒nonPos  ↦  nonPos*nonPos⇒nonNeg
   ```
 
+* In `Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Insert`:
+  ```agda
+  Any-insertWith-nothing  ↦  insertWith-nothing
+  Any-insertWith-just     ↦  insertWith-just
+  Any-insert-nothing      ↦  insert-nothing
+  Any-insert-just         ↦  insert-just
+  ```
+
 * In `Data.Vec.Properties`:
   ```agda
   truncate-irrelevant  ↦  Relation.Binary.PropositionalEquality.Core.refl
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Insert.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Insert.agda
index 9283c834c3..5a71b3b5d2 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Insert.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Insert.agda
@@ -54,38 +54,39 @@ module _ {V : Value v} where
 
     open <-Reasoning AVL.strictPartialOrder
 
-    Any-insertWith-nothing : (t : Tree V l u n) (seg : l < k < u) →
-                             P (k , f nothing) →
-                             ¬ (Any ((k ≈_) ∘′ key) t) → Any P (proj₂ (insertWith k f t seg))
-    Any-insertWith-nothing (leaf l<u)                   seg         pr ¬p = here pr
-    Any-insertWith-nothing (node kv@(k′ , v) lk ku bal) (l<k , k<u) pr ¬p
+    insertWith-nothing : (t : Tree V l u n) (seg : l < k < u) →
+                         P (k , f nothing) →
+                         ¬ (Any ((k ≈_) ∘′ key) t) →
+                         Any P (proj₂ (insertWith k f t seg))
+    insertWith-nothing (leaf l<u)                   seg         pr ¬p = here pr
+    insertWith-nothing (node kv@(k′ , v) lk ku bal) (l<k , k<u) pr ¬p
       with compare k k′
     ... | tri≈ _ k≈k′ _ = contradiction (here k≈k′) ¬p
     ... | tri< k<k′ _ _ = joinˡ⁺-left⁺ kv lk′ ku bal ih
       where
       seg′ = l<k , [ k<k′ ]ᴿ
       lk′  = insertWith k f lk seg′
-      ih   = Any-insertWith-nothing lk seg′ pr (λ p → ¬p (left p))
+      ih   = insertWith-nothing lk seg′ pr (λ p → ¬p (left p))
     ... | tri> _ _ k>k′ = joinʳ⁺-right⁺ kv lk ku′ bal ih
       where
       seg′ = [ k>k′ ]ᴿ , k<u
       ku′  = insertWith k f ku seg′
-      ih   = Any-insertWith-nothing ku seg′ pr (λ p → ¬p (right p))
+      ih   = insertWith-nothing ku seg′ pr (λ p → ¬p (right p))
 
-    Any-insertWith-just : (t : Tree V l u n) (seg : l < k < u) →
-                          (pr : ∀ k′ v → (eq : k ≈ k′) → P (k′ , Val≈ eq (f (just (Val≈ (sym eq) v))))) →
-                          Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insertWith k f t seg))
-    Any-insertWith-just (node kv@(k′ , v) lk ku bal) (l<k , k<u) pr p
+    insertWith-just : (t : Tree V l u n) (seg : l < k < u) →
+                      (pr : ∀ k′ v → (eq : k ≈ k′) → P (k′ , Val≈ eq (f (just (Val≈ (sym eq) v))))) →
+                      Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insertWith k f t seg))
+    insertWith-just (node kv@(k′ , v) lk ku bal) (l<k , k<u) pr p
       with p | compare k k′
     -- happy paths
     ... | here _   | tri≈ _ k≈k′ _ = here (pr k′ v k≈k′)
     ... | left lp  | tri< k<k′ _ _ =
-      joinˡ⁺-left⁺ kv lk′ ku bal (Any-insertWith-just lk seg′ pr lp)
+      joinˡ⁺-left⁺ kv lk′ ku bal (insertWith-just lk seg′ pr lp)
       where
       seg′ = l<k , [ k<k′ ]ᴿ
       lk′  = insertWith k f lk seg′
     ... | right rp | tri> _ _ k>k′ =
-      joinʳ⁺-right⁺ kv lk ku′ bal (Any-insertWith-just ku seg′ pr rp)
+      joinʳ⁺-right⁺ kv lk ku′ bal (insertWith-just ku seg′ pr rp)
       where
       seg′ = [ k>k′ ]ᴿ , k<u
       ku′  = insertWith k f ku seg′
@@ -126,17 +127,17 @@ module _ {V : Value v} where
 
   module _ (k : Key) (v : Val k) (t : Tree V l u n) (seg : l < k < u) where
 
-    Any-insert-nothing : P (k , v) → ¬ (Any ((k ≈_) ∘′ key) t) → Any P (proj₂ (insert k v t seg))
-    Any-insert-nothing = Any-insertWith-nothing k (F.const v) t seg
+    insert-nothing : P (k , v) → ¬ (Any ((k ≈_) ∘′ key) t) → Any P (proj₂ (insert k v t seg))
+    insert-nothing = insertWith-nothing k (F.const v) t seg
 
-    Any-insert-just : (pr : ∀ k′ → (eq : k ≈ k′) → P (k′ , Val≈ eq v)) →
+    insert-just : (pr : ∀ k′ → (eq : k ≈ k′) → P (k′ , Val≈ eq v)) →
                       Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insert k v t seg))
-    Any-insert-just pr = Any-insertWith-just k (F.const v) t seg (λ k′ _ eq → pr k′ eq)
+    insert-just pr = insertWith-just k (F.const v) t seg (λ k′ _ eq → pr k′ eq)
 
   module _ (k : Key) (f : Maybe (Val k) → Val k) where
 
     insertWith⁺ : (t : Tree V l u n) (seg : l < k < u) →
-                  (p : Any P t) → k ≉ Any.lookupKey p →
+                  (p : Any P t) → k ≉ lookupKey p →
                   Any P (proj₂ (insertWith k f t seg))
     insertWith⁺ (node kv@(k′ , v′) l r bal) (l<k , k<u) (here p) k≉
       with compare k k′
@@ -163,7 +164,7 @@ module _ {V : Value v} where
                           in joinʳ⁺-right⁺ kv l r′ bal ih
 
   insert⁺ : (k : Key) (v : Val k) (t : Tree V l u n) (seg : l < k < u) →
-            (p : Any P t) → k ≉ Any.lookupKey p →
+            (p : Any P t) → k ≉ lookupKey p →
             Any P (proj₂ (insert k v t seg))
   insert⁺ k v = insertWith⁺ k (F.const v)
 
@@ -205,3 +206,33 @@ module _ {V : Value v} where
       where
       k′<p = [<]-injective (proj₁ (lookup-bounded p))
       k≉p  = λ k≈p → irrefl (trans (sym k≈k′) k≈p) k′<p
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.4
+
+Any-insertWith-nothing = insertWith-nothing
+{-# WARNING_ON_USAGE Any-insertWith-nothing
+"Warning: Any-insertWith-nothing was deprecated in v2.4.
+Please use insertWith-nothing instead."
+#-}
+Any-insertWith-just = insertWith-just
+{-# WARNING_ON_USAGE Any-insertWith-just
+"Warning: Any-insertWith-just was deprecated in v2.4.
+Please use insertWith-just instead."
+#-}
+Any-insert-nothing = insert-nothing
+{-# WARNING_ON_USAGE Any-insert-nothing
+"Warning: Any-insert-nothing was deprecated in v2.4.
+Please use insert-nothing instead."
+#-}
+Any-insert-just = insert-just
+{-# WARNING_ON_USAGE Any-insert-just
+"Warning: Any-insert-just was deprecated in v2.4.
+Please use insert-just instead."
+#-}

From b970cd56fa68e6835496e501cc05e9043cda390a Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 2 Apr 2026 12:39:14 +0100
Subject: [PATCH 19/35] tidy up: `Properties.HeadTail`

---
 .../Indexed/Relation/Unary/Any/Properties/Cast.agda   |  8 ++++++--
 .../Relation/Unary/Any/Properties/HeadTail.agda       | 11 +++++++----
 2 files changed, 13 insertions(+), 6 deletions(-)

diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Cast.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Cast.agda
index fc3d3a1ade..7bba3f78a3 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Cast.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Cast.agda
@@ -12,6 +12,7 @@ module Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Cast
   {a ℓ₁ ℓ₂} (sto : StrictTotalOrder a ℓ₁ ℓ₂)
   where
 
+open import Data.Nat.Base using (ℕ)
 open import Level using (Level)
 open import Relation.Unary using (Pred)
 
@@ -23,14 +24,17 @@ private
     v p : Level
     V : Value v
     P : Pred (K& V) p
+    l m u : Key⁺
+    h : ℕ
 
-castʳ⁺ : ∀ {l m u h} {lm : Tree V l m h} {m<u : m <⁺ u} →
+
+castʳ⁺ : ∀ {lm : Tree V l m h} {m<u : m <⁺ u} →
          Any P lm → Any P (castʳ lm m<u)
 castʳ⁺ (here p)  = here p
 castʳ⁺ (left p)  = left p
 castʳ⁺ (right p) = right (castʳ⁺ p)
 
-castʳ⁻ : ∀ {l m u h} {lm : Tree V l m h} {m<u : m <⁺ u} →
+castʳ⁻ : ∀ {lm : Tree V l m h} {m<u : m <⁺ u} →
          Any P (castʳ lm m<u) → Any P lm
 castʳ⁻ {lm = node _ _ _ _} (here p)  = here p
 castʳ⁻ {lm = node _ _ _ _} (left p)  = left p
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/HeadTail.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/HeadTail.agda
index 39d17648ef..4b10b2ed48 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/HeadTail.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/HeadTail.agda
@@ -12,7 +12,7 @@ module Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.HeadTail
   {a ℓ₁ ℓ₂} (sto : StrictTotalOrder a ℓ₁ ℓ₂)
   where
 
-open import Data.Nat.Base using (suc; _+_)
+open import Data.Nat.Base using (ℕ; suc)
 open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Function using (id)
@@ -30,8 +30,11 @@ private
     v p : Level
     V : Value v
     P : Pred (K& V) p
+    l m u : Key⁺
+    h : ℕ
 
-headTail⁺ : ∀ {l u h} (t : Tree V l u (1 + h)) →
+
+headTail⁺ : (t : Tree V l u (suc h)) →
             let kv , _ , _ , t⁻ = headTail t in
             Any P t → P kv ⊎ Any P t⁻
 headTail⁺ (node _ (leaf _) _ ∼+)              (here p)  = inj₁ p
@@ -47,14 +50,14 @@ headTail⁺ (node k₃ t₁₂@(node _ _ _ _) t₄ bal) (right p)
   = let _ , _ , t₂ = headTail t₁₂
     in inj₂ (joinˡ⁻-right⁺ k₃ t₂ t₄ bal p)
 
-headTail-head⁻ : ∀ {l u h} → (t : Tree V l u (suc h)) →
+headTail-head⁻ : (t : Tree V l u (suc h)) →
                  P (proj₁ (headTail t)) → Any P t
 headTail-head⁻ (node _ (leaf _) _ ∼+)          p = here p
 headTail-head⁻ (node _ (leaf _) _ ∼0)          p = here p
 headTail-head⁻ (node _ t₁₂@(node _ _ _ _) _ _) p =
   left (headTail-head⁻ t₁₂ p)
 
-headTail-tail⁻ : ∀ {l u h} (t : Tree V l u (1 + h)) →
+headTail-tail⁻ : (t : Tree V l u (suc h)) →
                  let _ , _ , _ , t⁻ = headTail t in
                  Any P t⁻ → Any P t
 headTail-tail⁻ (node _ (leaf _) _ ∼+)              p = right p

From d86406169c1051c89870c0a66ba0a49d4570dd17 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 2 Apr 2026 12:43:42 +0100
Subject: [PATCH 20/35] tidy up: `Properties.Lookup`

---
 .../Relation/Unary/Any/Properties/Lookup.agda        | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Lookup.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Lookup.agda
index 709681a39c..c3206a7a23 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Lookup.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Lookup.agda
@@ -26,25 +26,27 @@ private
     v p : Level
     V : Value v
     l u : Key⁺
-    n : ℕ
+    h : ℕ
     P Q : Pred (K& V) p
+    t : Tree V l u h
 
-lookup-result : {t : Tree V l u n} (p : Any P t) → P (lookup p)
+
+lookup-result : (p : Any P t) → P (lookup p)
 lookup-result (here p)  = p
 lookup-result (left p)  = lookup-result p
 lookup-result (right p) = lookup-result p
 
-lookup-bounded : {t : Tree V l u n} (p : Any P t) → l < lookup p .key < u
+lookup-bounded : (p : Any P {l = l} {u = u} t) → l < lookupKey p < u
 lookup-bounded {t = node kv lk ku bal} (here p)  = ordered lk , ordered ku
 lookup-bounded {t = node kv lk ku bal} (left p)  =
   Prod.map₂ (flip (trans⁺ _) (ordered ku)) (lookup-bounded p)
 lookup-bounded {t = node kv lk ku bal} (right p) =
   Prod.map₁ (trans⁺ _ (ordered lk)) (lookup-bounded p)
 
-lookup-rebuild : {t : Tree V l u n} (p : Any P t) → Q (lookup p) → Any Q t
+lookup-rebuild : (p : Any P t) → Q (lookup p) → Any Q t
 lookup-rebuild (here _)  q = here q
 lookup-rebuild (left p)  q = left (lookup-rebuild p q)
 lookup-rebuild (right p) q = right (lookup-rebuild p q)
 
-lookup-rebuild-accum : {t : Tree V l u n} (p : Any P t) → Q (lookup p) → Any (Q ∩ P) t
+lookup-rebuild-accum : (p : Any P t) → Q (lookup p) → Any (Q ∩ P) t
 lookup-rebuild-accum p q = lookup-rebuild p (q , lookup-result p)

From be31fc6c146692cf659482814bdd3ca9b361e153 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 2 Apr 2026 12:47:26 +0100
Subject: [PATCH 21/35] tidy up: `Properties.LookupFun`

---
 .../Relation/Unary/Any/Properties/LookupFun.agda  | 15 ++++++---------
 1 file changed, 6 insertions(+), 9 deletions(-)

diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/LookupFun.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/LookupFun.agda
index 38747f6713..2539a18eb1 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/LookupFun.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/LookupFun.agda
@@ -24,6 +24,9 @@ open import Relation.Unary using (Pred)
 
 open import Data.Tree.AVL.Indexed sto as AVL
 open import Data.Tree.AVL.Indexed.Relation.Unary.Any sto as Any
+open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Lookup sto
+  using (lookup-bounded)
+
 open StrictTotalOrder sto renaming (Carrier to Key; trans to <-trans); open Eq using (sym; trans)
 
 open import Relation.Binary.Construct.Add.Extrema.Strict _<_ using ([<]-injective)
@@ -36,20 +39,14 @@ private
     n : ℕ
     P : Pred (K& V) p
 
-open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Lookup sto
-  using (lookup-bounded)
-
-module _ {V : Value v} where
 
-  private
-    Val  = Value.family V
-    Val≈ = Value.respects V
+module _ {V : Value v} (open Value V using (respects) renaming (family to Val)) where
 
   lookup⁺ : (t : Tree V l u n) (k : Key) (seg : l < k < u) →
             (p : Any P t) →
             (key (Any.lookup p) ≉ k)
             ⊎ (∃[ p≈k ] AVL.lookup t k seg
-               ≡ just (Val≈ p≈k (value (Any.lookup p))))
+               ≡ just (respects p≈k (value (Any.lookup p))))
   lookup⁺ (node (k′ , v′) l r bal) k (l<k , k<u) p
       with compare k′ k | p
   ... | tri< k′<k _ _ | right p = lookup⁺ r k ([ k′<k ]ᴿ , k<u) p
@@ -68,7 +65,7 @@ module _ {V : Value v} where
 
   lookup⁻ : (t : Tree V l u n) (k : Key) (v : Val k) (seg : l < k < u) →
             AVL.lookup t k seg ≡ just v →
-            Any (λ{ (k′ , v′) → ∃ λ k′≈k → Val≈ k′≈k v′ ≡ v}) t
+            Any (λ{ (k′ , v′) → ∃ λ k′≈k → respects k′≈k v′ ≡ v}) t
   lookup⁻ (node (k′ , v′) l r bal) k v (l<k , k<u) eq with compare k′ k
   ... | tri< k′<k _ _ = right (lookup⁻ r k v ([ k′<k ]ᴿ , k<u) eq)
   ... | tri≈ _ k′≈k _ = here (k′≈k , just-injective eq)

From 7024c9fdd592ad64b9e39a54f91101c8483addb8 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 2 Apr 2026 12:53:00 +0100
Subject: [PATCH 22/35] tidy up: `Properties.Singleton`

---
 .../Relation/Unary/Any/Properties/Singleton.agda   | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Singleton.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Singleton.agda
index c90c680f67..3fd4182603 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Singleton.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Singleton.agda
@@ -17,19 +17,21 @@ open import Relation.Unary using (Pred)
 
 open import Data.Tree.AVL.Indexed sto
 open import Data.Tree.AVL.Indexed.Relation.Unary.Any sto as Any
-open StrictTotalOrder sto renaming (Carrier to Key)
+
 
 private
   variable
     v p : Level
+    V : Value v
+    P : Pred (K& V) p
     l u : Key⁺
 
-module _ {V : Value v} {P : Pred (K& V) p}
-         (k : Key) (v : Value.family V k) (l<k<u : l < k < u)
-         where
 
-  singleton⁺ : P (k , v) → Any P (singleton k v l<k<u)
+module _ {V : Value v} (open Value V renaming (family to Val))
+         k (v : Val k) (l<k<u : l < k < u) where
+
+  singleton⁺ : P (k , v) → Any {V = V} P (singleton k v l<k<u)
   singleton⁺ Pkv = here Pkv
 
-  singleton⁻ : Any P (singleton k v l<k<u) → P (k , v)
+  singleton⁻ : Any {V = V} P (singleton k v l<k<u) → P (k , v)
   singleton⁻ (here Pkv) = Pkv

From 5499508d78bfc00ad398f01e0d807d5daebe58cf Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 3 Apr 2026 10:37:31 +0100
Subject: [PATCH 23/35] refactor: `Properties.Join` and consolidate as one
 module

---
 CHANGELOG.md                                  |  22 +-
 .../Relation/Unary/Any/Properties/Join.agda   | 314 ++++++++++++++++--
 .../Unary/Any/Properties/JoinConstFuns.agda   | 294 ----------------
 3 files changed, 294 insertions(+), 336 deletions(-)
 delete mode 100644 src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/JoinConstFuns.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index f47178994b..17c42cdcbd 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -68,7 +68,7 @@ Minor improvements
   levels to be used.
 
 * Due to becoming large, `Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties`
-  has been split into small modules
+  has been split into smaller modules
   `Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.*`
   that are reexported by the original `Properties`.
 
@@ -191,9 +191,7 @@ New modules
   Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Delete
   Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.HeadTail
   Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Insert
-  Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.JoinConstFuns
   Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Join
-  Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.LookupFun
   Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Singleton
   ```
 
@@ -472,47 +470,47 @@ Additions to existing modules
                    Any P t⁻ → Any P t
   ```
 
-* In `Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.JoinConstFuns`:
+* In `Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Join`:
   ```
   joinˡ⁻-here⁺ : (kv : K& V) →
-                 (l : ∃ λ i → Tree V l [ kv .key ] pred[ i ⊕ hˡ ]) →
+                 (l : Tree⁻ V l [ kv .key ] hˡ) →
                  (r : Tree V [ kv .key ] u hʳ) →
                  (bal : hˡ ∼ hʳ ⊔ h) →
                  P kv → Any P (proj₂ (joinˡ⁻ hˡ kv l r bal))
   joinˡ⁻-left⁺ : (kv : K& V) →
-                 (l : ∃ λ i → Tree V l [ kv .key ] pred[ i ⊕ hˡ ]) →
+                 (l : Tree⁻ V l [ kv .key ] hˡ) →
                  (r : Tree V [ kv .key ] u hʳ) →
                  (bal : hˡ ∼ hʳ ⊔ h) →
                  Any P (proj₂ l) → Any P (proj₂ (joinˡ⁻ hˡ kv l r bal))
   joinˡ⁻-right⁺ : (kv : K& V) →
-                  (l : ∃ λ i → Tree V l [ kv .key ] pred[ i ⊕ hˡ ]) →
+                  (l : Tree⁻ V l [ kv .key ] hˡ) →
                   (r : Tree V [ kv .key ] u hʳ) →
                   (bal : hˡ ∼ hʳ ⊔ h) →
                   Any P r → Any P (proj₂ (joinˡ⁻ hˡ kv l r bal))
   joinˡ⁻⁻ : (kv : K& V) →
-            (l : ∃ λ i → Tree V l [ kv .key ] pred[ i ⊕ hˡ ]) →
+            (l : Tree⁻ V l [ kv .key ] hˡ) →
             (r : Tree V [ kv .key ] u hʳ) →
             (bal : hˡ ∼ hʳ ⊔ h) →
             Any P (proj₂ (joinˡ⁻ hˡ kv l r bal)) →
             P kv ⊎ Any P (proj₂ l) ⊎ Any P r
   joinʳ⁻-here⁺ : (kv : K& V) →
                  (l : Tree V l [ kv .key ] hˡ) →
-                 (r : ∃ λ i → Tree V [ kv .key ] u pred[ i ⊕ hʳ ]) →
+                 (r : Tree⁻ V [ kv .key ] u hʳ) →
                  (bal : hˡ ∼ hʳ ⊔ h) →
                  P kv → Any P (proj₂ (joinʳ⁻ hʳ kv l r bal))
   joinʳ⁻-left⁺ : (kv : K& V) →
                  (l : Tree V l [ kv .key ] hˡ) →
-                 (r : ∃ λ i → Tree V [ kv .key ] u pred[ i ⊕ hʳ ]) →
+                 (r : Tree⁻ V [ kv .key ] u hʳ) →
                  (bal : hˡ ∼ hʳ ⊔ h) →
                  Any P l → Any P (proj₂ (joinʳ⁻ hʳ kv l r bal))
   joinʳ⁻-right⁺ : (kv : K& V) →
                   (l : Tree V l [ kv .key ] hˡ) →
-                  (r : ∃ λ i → Tree V [ kv .key ] u pred[ i ⊕ hʳ ]) →
+                  (r : Tree⁻ V [ kv .key ] u hʳ) →
                   (bal : hˡ ∼ hʳ ⊔ h) →
                   Any P (proj₂ r) → Any P (proj₂ (joinʳ⁻ hʳ kv l r bal))
   joinʳ⁻⁻ : (kv : K& V) →
             (l : Tree V l [ kv .key ] hˡ) →
-            (r : ∃ λ i → Tree V [ kv .key ] u pred[ i ⊕ hʳ ]) →
+            (r : Tree⁻ V [ kv .key ] u hʳ) →
             (bal : hˡ ∼ hʳ ⊔ h) →
             Any P (proj₂ (joinʳ⁻ hʳ kv l r bal)) →
             P kv ⊎ Any P l ⊎ Any P (proj₂ r)
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Join.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Join.agda
index 04ebd6b45f..152e51d1fc 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Join.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Join.agda
@@ -12,7 +12,7 @@ module Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Join
   {a ℓ₁ ℓ₂} (sto : StrictTotalOrder a ℓ₁ ℓ₂)
   where
 
-open import Data.Nat.Base using (ℕ)
+open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.Product.Base using (_,_; proj₂)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Level using (Level)
@@ -20,12 +20,8 @@ open import Relation.Unary using (Pred)
 
 open import Data.Tree.AVL.Indexed sto
 open import Data.Tree.AVL.Indexed.Relation.Unary.Any sto as Any
-open StrictTotalOrder sto renaming (Carrier to Key)
-
 open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Cast sto
   using (castʳ⁺; castʳ⁻)
-open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.JoinConstFuns sto
-  using (joinʳ⁻-left⁺; joinʳ⁻-here⁺; joinʳ⁻-right⁺; joinʳ⁻⁻)
 open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.HeadTail sto
   using (headTail⁺; headTail-head⁻; headTail-tail⁻)
 
@@ -37,33 +33,291 @@ private
     l m u : Key⁺
     hˡ hʳ h : ℕ
 
-module _ {V : Value v} where
+  [_]ᵏ : K& V → Key⁺
+  [ kv ]ᵏ = [ kv .key ]
+
+
+----------------------------------------------------------------------
+-- joinˡ⁺
+
+joinˡ⁺-here⁺ : (kv : K& V) →
+               (l : Tree⁺ V l [ kv ]ᵏ hˡ) →
+               (r : Tree V [ kv ]ᵏ u hʳ) →
+               (bal : hˡ ∼ hʳ ⊔ h) →
+               P kv → Any P (proj₂ (joinˡ⁺ kv l r bal))
+joinˡ⁺-here⁺ _ (0# , _)                 _ _  p = here p
+joinˡ⁺-here⁺ _ (1# , _)                 _ ∼0 p = here p
+joinˡ⁺-here⁺ _ (1# , _)                 _ ∼+ p = here p
+joinˡ⁺-here⁺ _ (1# , node _ _ _ ∼-)     _ ∼- p = right (here p)
+joinˡ⁺-here⁺ _ (1# , node _ _ _ ∼0)     _ ∼- p = right (here p)
+joinˡ⁺-here⁺ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- p = right (here p)
 
-  join-left⁺ : (t₁ : Tree V l m hˡ) (t₂ : Tree V m u hʳ) →
+joinˡ⁺-left⁺ : (kv : K& V) →
+               (l : Tree⁺ V l [ kv ]ᵏ hˡ) →
+               (r : Tree V [ kv ]ᵏ u hʳ) →
                (bal : hˡ ∼ hʳ ⊔ h) →
-               Any P t₁ → Any P (proj₂ (join t₁ t₂ bal))
-  join-left⁺ _ (leaf _)            ∼-  p = castʳ⁺ p
-  join-left⁺ t₁ t₂₃@(node _ _ _ _) bal p
-    = let k₂ , m<k₂ , t₃ = headTail t₂₃
-      in joinʳ⁻-left⁺ k₂ (castʳ t₁ m<k₂) t₃ bal (castʳ⁺ p)
+               Any P (proj₂ l) → Any P (proj₂ (joinˡ⁺ kv l r bal))
+joinˡ⁺-left⁺ _ (0# , _)                 _ _  p                 = left p
+joinˡ⁺-left⁺ _ (1# , _)                 _ ∼0 p                 = left p
+joinˡ⁺-left⁺ _ (1# , _)                 _ ∼+ p                 = left p
+joinˡ⁺-left⁺ _ (1# , node _ _ _ ∼-)     _ ∼- (here p)          = here p
+joinˡ⁺-left⁺ _ (1# , node _ _ _ ∼-)     _ ∼- (left p)          = left p
+joinˡ⁺-left⁺ _ (1# , node _ _ _ ∼-)     _ ∼- (right p)         = right (left p)
+joinˡ⁺-left⁺ _ (1# , node _ _ _ ∼0)     _ ∼- (here p)          = here p
+joinˡ⁺-left⁺ _ (1# , node _ _ _ ∼0)     _ ∼- (left p)          = left p
+joinˡ⁺-left⁺ _ (1# , node _ _ _ ∼0)     _ ∼- (right p)         = right (left p)
+joinˡ⁺-left⁺ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- (here p)          = left (here p)
+joinˡ⁺-left⁺ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- (left p)          = left (left p)
+joinˡ⁺-left⁺ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- (right (here p))  = here p
+joinˡ⁺-left⁺ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- (right (left p))  = left (right p)
+joinˡ⁺-left⁺ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- (right (right p)) = right (left p)
 
-  join-right⁺ : (t₁ : Tree V l m hˡ) (t₂ : Tree V m u hʳ) →
+joinˡ⁺-right⁺ : (kv : K& V) →
+                (l : Tree⁺ V l [ kv ]ᵏ hˡ) →
+                (r : Tree V [ kv ]ᵏ u hʳ) →
                 (bal : hˡ ∼ hʳ ⊔ h) →
-                Any P t₂ → Any P (proj₂ (join t₁ t₂ bal))
-  join-right⁺ t₁ t₂₃@(node _ _ _ _) bal p
-    = let k₂ , m<k₂ , t₃ = headTail t₂₃
-      in Sum.[ joinʳ⁻-here⁺ k₂ (castʳ t₁ m<k₂) t₃ bal
-             , joinʳ⁻-right⁺ k₂ (castʳ t₁ m<k₂) t₃ bal ]′
-             (headTail⁺ t₂₃ p)
-
-  join⁻ : (t₁ : Tree V l m hˡ) (t₂ : Tree V m u hʳ) →
+                Any P r → Any P (proj₂ (joinˡ⁺ kv l r bal))
+joinˡ⁺-right⁺ _ (0# , _)                 _ _  p = right p
+joinˡ⁺-right⁺ _ (1# , _)                 _ ∼0 p = right p
+joinˡ⁺-right⁺ _ (1# , _)                 _ ∼+ p = right p
+joinˡ⁺-right⁺ _ (1# , node _ _ _ ∼-)     _ ∼- p = right (right p)
+joinˡ⁺-right⁺ _ (1# , node _ _ _ ∼0)     _ ∼- p = right (right p)
+joinˡ⁺-right⁺ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- p = right (right p)
+
+joinˡ⁺⁻ : (kv : K& V) →
+          (l : Tree⁺ V l [ kv ]ᵏ hˡ) →
+          (r : Tree V [ kv ]ᵏ u hʳ) →
           (bal : hˡ ∼ hʳ ⊔ h) →
-          Any P (proj₂ (join t₁ t₂ bal)) →
-          Any P t₁ ⊎ Any P t₂
-  join⁻ _ (leaf _) ∼- p = inj₁ (castʳ⁻ p)
-  join⁻ t₁ t₂₃@(node _ _ _ _) bal p
-    using k₂ , m<k₂ , t₃ ← headTail t₂₃
-    with joinʳ⁻⁻ k₂ (castʳ t₁ m<k₂) t₃ bal p
-  ... | inj₁ pk        = inj₂ (headTail-head⁻ t₂₃ pk)
-  ... | inj₂ (inj₁ pl) = inj₁ (castʳ⁻ pl)
-  ... | inj₂ (inj₂ pr) = inj₂ (headTail-tail⁻ t₂₃ pr)
+          Any P (proj₂ (joinˡ⁺ kv l r bal)) →
+          P kv ⊎ Any P (proj₂ l) ⊎ Any P r
+joinˡ⁺⁻ _ (0# , _)                 _ _  = Any.toSum
+joinˡ⁺⁻ _ (1# , _)                 _ ∼0 = Any.toSum
+joinˡ⁺⁻ _ (1# , _)                 _ ∼+ = Any.toSum
+joinˡ⁺⁻ _ (1# , node _ _ _ ∼-)     _ ∼- = λ where
+  (left p)          → inj₂ (inj₁ (left p))
+  (here p)          → inj₂ (inj₁ (here p))
+  (right (left p))  → inj₂ (inj₁ (right p))
+  (right (here p))  → inj₁ p
+  (right (right p)) → inj₂ (inj₂ p)
+joinˡ⁺⁻ _ (1# , node _ _ _ ∼0)     _ ∼- = λ where
+  (left p)          → inj₂ (inj₁ (left p))
+  (here p)          → inj₂ (inj₁ (here p))
+  (right (left p))  → inj₂ (inj₁ (right p))
+  (right (here p))  → inj₁ p
+  (right (right p)) → inj₂ (inj₂ p)
+joinˡ⁺⁻ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- = λ where
+  (left (left p))   → inj₂ (inj₁ (left p))
+  (left (here p))   → inj₂ (inj₁ (here p))
+  (left (right p))  → inj₂ (inj₁ (right (left p)))
+  (here p)          → inj₂ (inj₁ (right (here p)))
+  (right (left p))  → inj₂ (inj₁ (right (right p)))
+  (right (here p))  → inj₁ p
+  (right (right p)) → inj₂ (inj₂ p)
+
+----------------------------------------------------------------------
+-- joinʳ⁺
+
+joinʳ⁺-here⁺ : (kv : K& V) →
+               (l : Tree V l [ kv ]ᵏ hˡ) →
+               (r : Tree⁺ V [ kv ]ᵏ u hʳ) →
+               (bal : hˡ ∼ hʳ ⊔ h) →
+               P kv → Any P (proj₂ (joinʳ⁺ kv l r bal))
+joinʳ⁺-here⁺ _ _ (0# , _)                 _  p = here p
+joinʳ⁺-here⁺ _ _ (1# , _)                 ∼0 p = here p
+joinʳ⁺-here⁺ _ _ (1# , _)                 ∼- p = here p
+joinʳ⁺-here⁺ _ _ (1# , node _ _ _ ∼+)     ∼+ p = left (here p)
+joinʳ⁺-here⁺ _ _ (1# , node _ _ _ ∼0)     ∼+ p = left (here p)
+joinʳ⁺-here⁺ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ p = left (here p)
+
+joinʳ⁺-left⁺ : (kv : K& V) →
+               (l : Tree V l [ kv ]ᵏ hˡ) →
+               (r : Tree⁺ V [ kv ]ᵏ u hʳ) →
+               (bal : hˡ ∼ hʳ ⊔ h) →
+               Any P l → Any P (proj₂ (joinʳ⁺ kv l r bal))
+joinʳ⁺-left⁺ _ _ (0# , _)                 _  p = left p
+joinʳ⁺-left⁺ _ _ (1# , _)                 ∼0 p = left p
+joinʳ⁺-left⁺ _ _ (1# , _)                 ∼- p = left p
+joinʳ⁺-left⁺ _ _ (1# , node _ _ _ ∼+)     ∼+ p = left (left p)
+joinʳ⁺-left⁺ _ _ (1# , node _ _ _ ∼0)     ∼+ p = left (left p)
+joinʳ⁺-left⁺ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ p = left (left p)
+
+joinʳ⁺-right⁺ : (kv : K& V) →
+                (l : Tree V l [ kv ]ᵏ hˡ) →
+                (r : Tree⁺ V [ kv ]ᵏ u hʳ) →
+                (bal : hˡ ∼ hʳ ⊔ h) →
+                Any P (proj₂ r) → Any P (proj₂ (joinʳ⁺ kv l r bal))
+joinʳ⁺-right⁺ _ _ (0# , _)                 _  p                = right p
+joinʳ⁺-right⁺ _ _ (1# , _)                 ∼0 p                = right p
+joinʳ⁺-right⁺ _ _ (1# , _)                 ∼- p                = right p
+joinʳ⁺-right⁺ _ _ (1# , node _ _ _ ∼+)     ∼+ (here p)         = here p
+joinʳ⁺-right⁺ _ _ (1# , node _ _ _ ∼+)     ∼+ (left p)         = left (right p)
+joinʳ⁺-right⁺ _ _ (1# , node _ _ _ ∼+)     ∼+ (right p)        = right p
+joinʳ⁺-right⁺ _ _ (1# , node _ _ _ ∼0)     ∼+ (here p)         = here p
+joinʳ⁺-right⁺ _ _ (1# , node _ _ _ ∼0)     ∼+ (left p)         = left (right p)
+joinʳ⁺-right⁺ _ _ (1# , node _ _ _ ∼0)     ∼+ (right p)        = right p
+joinʳ⁺-right⁺ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ (here p)         = right (here p)
+joinʳ⁺-right⁺ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ (left (here p))  = here p
+joinʳ⁺-right⁺ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ (left (left p))  = left (right p)
+joinʳ⁺-right⁺ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ (left (right p)) = right (left p)
+joinʳ⁺-right⁺ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ (right p)        = right (right p)
+
+joinʳ⁺⁻ : (kv : K& V) →
+          (l : Tree V l [ kv ]ᵏ hˡ) →
+          (r : Tree⁺ V [ kv ]ᵏ u hʳ) →
+          (bal : hˡ ∼ hʳ ⊔ h) →
+          Any P (proj₂ (joinʳ⁺ kv l r bal)) →
+          P kv ⊎ Any P l ⊎ Any P (proj₂ r)
+joinʳ⁺⁻ _ _ (0# , _)                 _  = Any.toSum
+joinʳ⁺⁻ _ _ (1# , _)                 ∼0 = Any.toSum
+joinʳ⁺⁻ _ _ (1# , _)                 ∼- = Any.toSum
+joinʳ⁺⁻ _ _ (1# , node _ _ _ ∼+)     ∼+ = λ where
+  (left (left p))  → inj₂ (inj₁ p)
+  (left (here p))  → inj₁ p
+  (left (right p)) → inj₂ (inj₂ (left p))
+  (here p)         → inj₂ (inj₂ (here p))
+  (right p)        → inj₂ (inj₂ (right p))
+joinʳ⁺⁻ _ _ (1# , node _ _ _ ∼0)     ∼+ = λ where
+  (left (left p))  → inj₂ (inj₁ p)
+  (left (here p))  → inj₁ p
+  (left (right p)) → inj₂ (inj₂ (left p))
+  (here p)         → inj₂ (inj₂ (here p))
+  (right p)        → inj₂ (inj₂ (right p))
+joinʳ⁺⁻ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ = λ where
+  (left (left p))   → inj₂ (inj₁ p)
+  (left (here p))   → inj₁ p
+  (left (right p))  → inj₂ (inj₂ (left (left p)))
+  (here p)          → inj₂ (inj₂ (left (here p)))
+  (right (left p))  → inj₂ (inj₂ (left (right p)))
+  (right (here p))  → inj₂ (inj₂ (here p))
+  (right (right p)) → inj₂ (inj₂ (right p))
+
+----------------------------------------------------------------------
+-- joinˡ⁻
+
+joinˡ⁻-here⁺ : (kv : K& V) →
+               (l : Tree⁻ V l [ kv ]ᵏ hˡ) →
+               (r : Tree V [ kv ]ᵏ u hʳ) →
+               (bal : hˡ ∼ hʳ ⊔ h) →
+               P kv → Any P (proj₂ (joinˡ⁻ hˡ kv l r bal))
+joinˡ⁻-here⁺ {hˡ = zero}  _ (leaf⁻ _) _  _  p = here p
+joinˡ⁻-here⁺ {hˡ = suc _} _ (0# , t₁) t₃ ∼+ p =
+  joinʳ⁺-here⁺ _ t₁ (1# , t₃) ∼+ p
+joinˡ⁻-here⁺ {hˡ = suc _} _ (0# , _)  _  ∼0 p = here p
+joinˡ⁻-here⁺ {hˡ = suc _} _ (0# , _)  _  ∼- p = here p
+joinˡ⁻-here⁺ {hˡ = suc _} _ (1# , _)  _  _  p = here p
+
+joinˡ⁻-left⁺ : (kv : K& V) →
+               (l : Tree⁻ V l [ kv ]ᵏ hˡ) →
+               (r : Tree V [ kv ]ᵏ u hʳ) →
+               (bal : hˡ ∼ hʳ ⊔ h) →
+               Any P (proj₂ l) → Any P (proj₂ (joinˡ⁻ hˡ kv l r bal))
+joinˡ⁻-left⁺ {hˡ = zero}  _ (leaf⁻ _)  _  _  p = left p
+joinˡ⁻-left⁺ {hˡ = suc _} _ (0# , t₁)  t₃ ∼+ p =
+  joinʳ⁺-left⁺ _ t₁ (1# , t₃) ∼+ p
+joinˡ⁻-left⁺ {hˡ = suc _} _ (0# , _)   _  ∼0 p = left p
+joinˡ⁻-left⁺ {hˡ = suc _} _ (0# , _)   _  ∼- p = left p
+joinˡ⁻-left⁺ {hˡ = suc _} _ (1# , _)   _  _  p = left p
+
+joinˡ⁻-right⁺ : (kv : K& V) →
+                (l : Tree⁻ V l [ kv ]ᵏ hˡ) →
+                (r : Tree V [ kv ]ᵏ u hʳ) →
+                (bal : hˡ ∼ hʳ ⊔ h) →
+                Any P r → Any P (proj₂ (joinˡ⁻ hˡ kv l r bal))
+joinˡ⁻-right⁺ {hˡ = zero}  _ (leaf⁻ _)  _  _  p = right p
+joinˡ⁻-right⁺ {hˡ = suc _} _ (0# , t₁)  t₃ ∼+ p =
+  joinʳ⁺-right⁺ _ t₁ (1# , t₃) ∼+ p
+joinˡ⁻-right⁺ {hˡ = suc _} _ (0# , _)   _  ∼0 p = right p
+joinˡ⁻-right⁺ {hˡ = suc _} _ (0# , _)   _  ∼- p = right p
+joinˡ⁻-right⁺ {hˡ = suc _} _ (1# , _)   _  _  p = right p
+
+joinˡ⁻⁻ : (kv : K& V) →
+          (l : Tree⁻ V l [ kv ]ᵏ hˡ) →
+          (r : Tree V [ kv ]ᵏ u hʳ) →
+          (bal : hˡ ∼ hʳ ⊔ h) →
+          Any P (proj₂ (joinˡ⁻ hˡ kv l r bal)) →
+          P kv ⊎ Any P (proj₂ l) ⊎ Any P r
+joinˡ⁻⁻ {hˡ = zero}  _ (leaf⁻ _) _  _  = Any.toSum
+joinˡ⁻⁻ {hˡ = suc _} _ (0# , t₁) t₃ ∼+ = joinʳ⁺⁻ _ t₁ (1# , t₃) ∼+
+joinˡ⁻⁻ {hˡ = suc _} _ (0# , _)  _  ∼0 = Any.toSum
+joinˡ⁻⁻ {hˡ = suc _} _ (0# , _)  _  ∼- = Any.toSum
+joinˡ⁻⁻ {hˡ = suc _} _ (1# , _)  _  _  = Any.toSum
+
+----------------------------------------------------------------------
+-- joinʳ⁻
+
+joinʳ⁻-here⁺ : (kv : K& V) →
+               (l : Tree V l [ kv ]ᵏ hˡ) →
+               (r : Tree⁻ V [ kv ]ᵏ u hʳ) →
+               (bal : hˡ ∼ hʳ ⊔ h) →
+               P kv → Any P (proj₂ (joinʳ⁻ hʳ kv l r bal))
+joinʳ⁻-here⁺ {hʳ = zero}  _ _  (leaf⁻ _) _  p = here p
+joinʳ⁻-here⁺ {hʳ = suc _} _ t₁ (0# , t₃) ∼- p =
+  joinˡ⁺-here⁺ _ (1# , t₁) t₃ ∼- p
+joinʳ⁻-here⁺ {hʳ = suc _} _ _  (0# , _)  ∼0 p = here p
+joinʳ⁻-here⁺ {hʳ = suc _} _ _  (0# , _)  ∼+ p = here p
+joinʳ⁻-here⁺ {hʳ = suc _} _ _  (1# , _)  _  p = here p
+
+joinʳ⁻-left⁺ : (kv : K& V) →
+               (l : Tree V l [ kv ]ᵏ hˡ) →
+               (r : Tree⁻ V [ kv ]ᵏ u hʳ) →
+               (bal : hˡ ∼ hʳ ⊔ h) →
+               Any P l → Any P (proj₂ (joinʳ⁻ hʳ kv l r bal))
+joinʳ⁻-left⁺ {hʳ = zero}  _ _  (leaf⁻ _) _  p = left p
+joinʳ⁻-left⁺ {hʳ = suc _} _ t₁ (0# , t₃) ∼- p =
+  joinˡ⁺-left⁺ _ (1# , t₁) t₃ ∼- p
+joinʳ⁻-left⁺ {hʳ = suc _} _ _  (0# , _)  ∼0 p = left p
+joinʳ⁻-left⁺ {hʳ = suc _} _ _  (0# , _)  ∼+ p = left p
+joinʳ⁻-left⁺ {hʳ = suc _} _ _  (1# , _)  _  p = left p
+
+joinʳ⁻-right⁺ : (kv : K& V) →
+                (l : Tree V l [ kv ]ᵏ hˡ) →
+                (r : Tree⁻ V [ kv ]ᵏ u hʳ) →
+                (bal : hˡ ∼ hʳ ⊔ h) →
+                Any P (proj₂ r) → Any P (proj₂ (joinʳ⁻ hʳ kv l r bal))
+joinʳ⁻-right⁺ {hʳ = zero}  _ _  (leaf⁻ _) _  p = right p
+joinʳ⁻-right⁺ {hʳ = suc _} _ t₁ (0# , t₃) ∼- p =
+  joinˡ⁺-right⁺ _ (1# , t₁) t₃ ∼- p
+joinʳ⁻-right⁺ {hʳ = suc _} _ _  (0# , _)  ∼0 p = right p
+joinʳ⁻-right⁺ {hʳ = suc _} _ _  (0# , _)  ∼+ p = right p
+joinʳ⁻-right⁺ {hʳ = suc _} _ _  (1# , _)  _  p = right p
+
+joinʳ⁻⁻ : (kv : K& V) →
+          (l : Tree V l [ kv ]ᵏ hˡ) →
+          (r : Tree⁻ V [ kv ]ᵏ u hʳ) →
+          (bal : hˡ ∼ hʳ ⊔ h) →
+          Any P (proj₂ (joinʳ⁻ hʳ kv l r bal)) →
+          P kv ⊎ Any P l ⊎ Any P (proj₂ r)
+joinʳ⁻⁻ {hʳ = zero}  _ _  (leaf⁻ _) _  = Any.toSum
+joinʳ⁻⁻ {hʳ = suc _} _ t₁ (0# , t₃) ∼- = joinˡ⁺⁻ _ (1# , t₁) t₃ ∼-
+joinʳ⁻⁻ {hʳ = suc _} _ _  (0# , _)  ∼0 = Any.toSum
+joinʳ⁻⁻ {hʳ = suc _} _ _  (0# , _)  ∼+ = Any.toSum
+joinʳ⁻⁻ {hʳ = suc _} _ _  (1# , _)  _  = Any.toSum
+
+----------------------------------------------------------------------
+-- join
+
+join-left⁺ : (t₁ : Tree V l m hˡ) (t₂ : Tree V m u hʳ) →
+             (bal : hˡ ∼ hʳ ⊔ h) →
+             Any {V = V} P t₁ → Any P (proj₂ (join t₁ t₂ bal))
+join-left⁺ _ (leaf _)            ∼-  p = castʳ⁺ p
+join-left⁺ t₁ t₂₃@(node _ _ _ _) bal p using k₂ , m<k₂ , t₃ ← headTail t₂₃
+  = joinʳ⁻-left⁺ k₂ (castʳ t₁ m<k₂) t₃ bal (castʳ⁺ p)
+
+join-right⁺ : (t₁ : Tree V l m hˡ) (t₂ : Tree V m u hʳ) →
+              (bal : hˡ ∼ hʳ ⊔ h) →
+              Any {V = V} P t₂ → Any P (proj₂ (join t₁ t₂ bal))
+join-right⁺ t₁ t₂₃@(node _ _ _ _) bal p using k₂ , m<k₂ , t₃ ← headTail t₂₃
+  = Sum.[ joinʳ⁻-here⁺ k₂ (castʳ t₁ m<k₂) t₃ bal
+        , joinʳ⁻-right⁺ k₂ (castʳ t₁ m<k₂) t₃ bal ]′
+        (headTail⁺ t₂₃ p)
+
+join⁻ : (t₁ : Tree V l m hˡ) (t₂ : Tree V m u hʳ) →
+        (bal : hˡ ∼ hʳ ⊔ h) →
+        Any {V = V} P (proj₂ (join t₁ t₂ bal)) →
+        Any P t₁ ⊎ Any P t₂
+join⁻ _ (leaf _) ∼- p = inj₁ (castʳ⁻ p)
+join⁻ t₁ t₂₃@(node _ _ _ _) bal p using k₂ , m<k₂ , t₃ ← headTail t₂₃
+  with joinʳ⁻⁻ k₂ (castʳ t₁ m<k₂) t₃ bal p
+... | inj₁ pk        = inj₂ (headTail-head⁻ t₂₃ pk)
+... | inj₂ (inj₁ pl) = inj₁ (castʳ⁻ pl)
+... | inj₂ (inj₂ pr) = inj₂ (headTail-tail⁻ t₂₃ pr)
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/JoinConstFuns.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/JoinConstFuns.agda
deleted file mode 100644
index 079c16ee0b..0000000000
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/JoinConstFuns.agda
+++ /dev/null
@@ -1,294 +0,0 @@
-------------------------------------------------------------------------
--- The Agda standard library
---
--- Properties constant-time join functions related to Any
-------------------------------------------------------------------------
-
-{-# OPTIONS --cubical-compatible --safe #-}
-
-open import Relation.Binary.Bundles using (StrictTotalOrder)
-
-module Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.JoinConstFuns
-  {a ℓ₁ ℓ₂} (sto : StrictTotalOrder a ℓ₁ ℓ₂)
-  where
-
-open import Data.Nat.Base using (ℕ; zero; suc)
-open import Data.Product.Base using (∃; _,_; proj₂)
-open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
-open import Level using (Level)
-open import Relation.Unary using (Pred)
-
-open import Data.Tree.AVL.Indexed sto
-open import Data.Tree.AVL.Indexed.Relation.Unary.Any sto as Any
-
-private
-  variable
-    v p : Level
-    V : Value v
-    P : Pred (K& V) p
-    l u : Key⁺
-    hˡ hʳ h : ℕ
-
-----------------------------------------------------------------------
--- joinˡ⁺
-
-joinˡ⁺-here⁺ : (kv : K& V) →
-               (l : ∃ λ i → Tree V l [ kv .key ] (i ⊕ hˡ)) →
-               (r : Tree V [ kv .key ] u hʳ) →
-               (bal : hˡ ∼ hʳ ⊔ h) →
-               P kv → Any P (proj₂ (joinˡ⁺ kv l r bal))
-joinˡ⁺-here⁺ _ (0# , _)                 _ _  p = here p
-joinˡ⁺-here⁺ _ (1# , _)                 _ ∼0 p = here p
-joinˡ⁺-here⁺ _ (1# , _)                 _ ∼+ p = here p
-joinˡ⁺-here⁺ _ (1# , node _ _ _ ∼-)     _ ∼- p = right (here p)
-joinˡ⁺-here⁺ _ (1# , node _ _ _ ∼0)     _ ∼- p = right (here p)
-joinˡ⁺-here⁺ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- p = right (here p)
-
-joinˡ⁺-left⁺ : (k : K& V) →
-               (l : ∃ λ i → Tree V l [ k .key ] (i ⊕ hˡ)) →
-               (r : Tree V [ k .key ] u hʳ) →
-               (bal : hˡ ∼ hʳ ⊔ h) →
-               Any P (proj₂ l) → Any P (proj₂ (joinˡ⁺ k l r bal))
-joinˡ⁺-left⁺ _ (0# , _)                 _ _  p                 = left p
-joinˡ⁺-left⁺ _ (1# , _)                 _ ∼0 p                 = left p
-joinˡ⁺-left⁺ _ (1# , _)                 _ ∼+ p                 = left p
-joinˡ⁺-left⁺ _ (1# , node _ _ _ ∼-)     _ ∼- (here p)          = here p
-joinˡ⁺-left⁺ _ (1# , node _ _ _ ∼-)     _ ∼- (left p)          = left p
-joinˡ⁺-left⁺ _ (1# , node _ _ _ ∼-)     _ ∼- (right p)         = right (left p)
-joinˡ⁺-left⁺ _ (1# , node _ _ _ ∼0)     _ ∼- (here p)          = here p
-joinˡ⁺-left⁺ _ (1# , node _ _ _ ∼0)     _ ∼- (left p)          = left p
-joinˡ⁺-left⁺ _ (1# , node _ _ _ ∼0)     _ ∼- (right p)         = right (left p)
-joinˡ⁺-left⁺ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- (here p)          = left (here p)
-joinˡ⁺-left⁺ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- (left p)          = left (left p)
-joinˡ⁺-left⁺ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- (right (here p))  = here p
-joinˡ⁺-left⁺ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- (right (left p))  = left (right p)
-joinˡ⁺-left⁺ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- (right (right p)) = right (left p)
-
-joinˡ⁺-right⁺ : (kv@(k , v) : K& V) →
-                (l : ∃ λ i → Tree V l [ k ] (i ⊕ hˡ)) →
-                (r : Tree V [ k ] u hʳ) →
-                (bal : hˡ ∼ hʳ ⊔ h) →
-                Any P r → Any P (proj₂ (joinˡ⁺ kv l r bal))
-joinˡ⁺-right⁺ _ (0# , _)                 _ _  p = right p
-joinˡ⁺-right⁺ _ (1# , _)                 _ ∼0 p = right p
-joinˡ⁺-right⁺ _ (1# , _)                 _ ∼+ p = right p
-joinˡ⁺-right⁺ _ (1# , node _ _ _ ∼-)     _ ∼- p = right (right p)
-joinˡ⁺-right⁺ _ (1# , node _ _ _ ∼0)     _ ∼- p = right (right p)
-joinˡ⁺-right⁺ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- p = right (right p)
-
-joinˡ⁺⁻ : (kv@(k , v) : K& V) →
-          (l : ∃ λ i → Tree V l [ k ] (i ⊕ hˡ)) →
-          (r : Tree V [ k ] u hʳ) →
-          (bal : hˡ ∼ hʳ ⊔ h) →
-          Any P (proj₂ (joinˡ⁺ kv l r bal)) →
-          P kv ⊎ Any P (proj₂ l) ⊎ Any P r
-joinˡ⁺⁻ _ (0# , _)                 _ _  = Any.toSum
-joinˡ⁺⁻ _ (1# , _)                 _ ∼0 = Any.toSum
-joinˡ⁺⁻ _ (1# , _)                 _ ∼+ = Any.toSum
-joinˡ⁺⁻ _ (1# , node _ _ _ ∼-)     _ ∼- = λ where
-  (left p)          → inj₂ (inj₁ (left p))
-  (here p)          → inj₂ (inj₁ (here p))
-  (right (left p))  → inj₂ (inj₁ (right p))
-  (right (here p))  → inj₁ p
-  (right (right p)) → inj₂ (inj₂ p)
-joinˡ⁺⁻ _ (1# , node _ _ _ ∼0)     _ ∼- = λ where
-  (left p)          → inj₂ (inj₁ (left p))
-  (here p)          → inj₂ (inj₁ (here p))
-  (right (left p))  → inj₂ (inj₁ (right p))
-  (right (here p))  → inj₁ p
-  (right (right p)) → inj₂ (inj₂ p)
-joinˡ⁺⁻ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- = λ where
-  (left (left p))   → inj₂ (inj₁ (left p))
-  (left (here p))   → inj₂ (inj₁ (here p))
-  (left (right p))  → inj₂ (inj₁ (right (left p)))
-  (here p)          → inj₂ (inj₁ (right (here p)))
-  (right (left p))  → inj₂ (inj₁ (right (right p)))
-  (right (here p))  → inj₁ p
-  (right (right p)) → inj₂ (inj₂ p)
-
-----------------------------------------------------------------------
--- joinʳ⁺
-
-joinʳ⁺-here⁺ : (kv : K& V) →
-               (l : Tree V l [ kv .key ] hˡ) →
-               (r : ∃ λ i → Tree V [ kv .key ] u (i ⊕ hʳ)) →
-               (bal : hˡ ∼ hʳ ⊔ h) →
-               P kv → Any P (proj₂ (joinʳ⁺ kv l r bal))
-joinʳ⁺-here⁺ _ _ (0# , _)                 _  p = here p
-joinʳ⁺-here⁺ _ _ (1# , _)                 ∼0 p = here p
-joinʳ⁺-here⁺ _ _ (1# , _)                 ∼- p = here p
-joinʳ⁺-here⁺ _ _ (1# , node _ _ _ ∼+)     ∼+ p = left (here p)
-joinʳ⁺-here⁺ _ _ (1# , node _ _ _ ∼0)     ∼+ p = left (here p)
-joinʳ⁺-here⁺ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ p = left (here p)
-
-joinʳ⁺-left⁺ : (kv : K& V) →
-               (l : Tree V l [ kv .key ] hˡ) →
-               (r : ∃ λ i → Tree V [ kv .key ] u (i ⊕ hʳ)) →
-               (bal : hˡ ∼ hʳ ⊔ h) →
-               Any P l → Any P (proj₂ (joinʳ⁺ kv l r bal))
-joinʳ⁺-left⁺ _ _ (0# , _)                 _  p = left p
-joinʳ⁺-left⁺ _ _ (1# , _)                 ∼0 p = left p
-joinʳ⁺-left⁺ _ _ (1# , _)                 ∼- p = left p
-joinʳ⁺-left⁺ _ _ (1# , node _ _ _ ∼+)     ∼+ p = left (left p)
-joinʳ⁺-left⁺ _ _ (1# , node _ _ _ ∼0)     ∼+ p = left (left p)
-joinʳ⁺-left⁺ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ p = left (left p)
-
-joinʳ⁺-right⁺ : (kv : K& V) →
-                (l : Tree V l [ kv .key ] hˡ) →
-                (r : ∃ λ i → Tree V [ kv .key ] u (i ⊕ hʳ)) →
-                (bal : hˡ ∼ hʳ ⊔ h) →
-                Any P (proj₂ r) → Any P (proj₂ (joinʳ⁺ kv l r bal))
-joinʳ⁺-right⁺ _ _ (0# , _)                 _  p                = right p
-joinʳ⁺-right⁺ _ _ (1# , _)                 ∼0 p                = right p
-joinʳ⁺-right⁺ _ _ (1# , _)                 ∼- p                = right p
-joinʳ⁺-right⁺ _ _ (1# , node _ _ _ ∼+)     ∼+ (here p)         = here p
-joinʳ⁺-right⁺ _ _ (1# , node _ _ _ ∼+)     ∼+ (left p)         = left (right p)
-joinʳ⁺-right⁺ _ _ (1# , node _ _ _ ∼+)     ∼+ (right p)        = right p
-joinʳ⁺-right⁺ _ _ (1# , node _ _ _ ∼0)     ∼+ (here p)         = here p
-joinʳ⁺-right⁺ _ _ (1# , node _ _ _ ∼0)     ∼+ (left p)         = left (right p)
-joinʳ⁺-right⁺ _ _ (1# , node _ _ _ ∼0)     ∼+ (right p)        = right p
-joinʳ⁺-right⁺ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ (here p)         = right (here p)
-joinʳ⁺-right⁺ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ (left (here p))  = here p
-joinʳ⁺-right⁺ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ (left (left p))  = left (right p)
-joinʳ⁺-right⁺ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ (left (right p)) = right (left p)
-joinʳ⁺-right⁺ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ (right p)        = right (right p)
-
-joinʳ⁺⁻ : (kv : K& V) →
-          (l : Tree V l [ kv .key ] hˡ) →
-          (r : ∃ λ i → Tree V [ kv .key ] u (i ⊕ hʳ)) →
-          (bal : hˡ ∼ hʳ ⊔ h) →
-          Any P (proj₂ (joinʳ⁺ kv l r bal)) →
-          P kv ⊎ Any P l ⊎ Any P (proj₂ r)
-joinʳ⁺⁻ _ _ (0# , _)                 _  = Any.toSum
-joinʳ⁺⁻ _ _ (1# , _)                 ∼0 = Any.toSum
-joinʳ⁺⁻ _ _ (1# , _)                 ∼- = Any.toSum
-joinʳ⁺⁻ _ _ (1# , node _ _ _ ∼+)     ∼+ = λ where
-  (left (left p))  → inj₂ (inj₁ p)
-  (left (here p))  → inj₁ p
-  (left (right p)) → inj₂ (inj₂ (left p))
-  (here p)         → inj₂ (inj₂ (here p))
-  (right p)        → inj₂ (inj₂ (right p))
-joinʳ⁺⁻ _ _ (1# , node _ _ _ ∼0)     ∼+ = λ where
-  (left (left p))  → inj₂ (inj₁ p)
-  (left (here p))  → inj₁ p
-  (left (right p)) → inj₂ (inj₂ (left p))
-  (here p)         → inj₂ (inj₂ (here p))
-  (right p)        → inj₂ (inj₂ (right p))
-joinʳ⁺⁻ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ = λ where
-  (left (left p))   → inj₂ (inj₁ p)
-  (left (here p))   → inj₁ p
-  (left (right p))  → inj₂ (inj₂ (left (left p)))
-  (here p)          → inj₂ (inj₂ (left (here p)))
-  (right (left p))  → inj₂ (inj₂ (left (right p)))
-  (right (here p))  → inj₂ (inj₂ (here p))
-  (right (right p)) → inj₂ (inj₂ (right p))
-
-----------------------------------------------------------------------
--- joinˡ⁻
-
-joinˡ⁻-here⁺ : (kv : K& V) →
-               (l : ∃ λ i → Tree V l [ kv .key ] pred[ i ⊕ hˡ ]) →
-               (r : Tree V [ kv .key ] u hʳ) →
-               (bal : hˡ ∼ hʳ ⊔ h) →
-               P kv → Any P (proj₂ (joinˡ⁻ hˡ kv l r bal))
-joinˡ⁻-here⁺ {hˡ = zero}  _ (0# , leaf _) _  _  p = here p
-joinˡ⁻-here⁺ {hˡ = zero}  _ (1# , leaf _) _  _  p = here p
-joinˡ⁻-here⁺ {hˡ = suc _} _ (0# , t₁)     t₃ ∼+ p =
-  joinʳ⁺-here⁺ _ t₁ (1# , t₃) ∼+ p
-joinˡ⁻-here⁺ {hˡ = suc _} _ (0# , _)      _  ∼0 p = here p
-joinˡ⁻-here⁺ {hˡ = suc _} _ (0# , _)      _  ∼- p = here p
-joinˡ⁻-here⁺ {hˡ = suc _} _ (1# , _)      _  _  p = here p
-
-joinˡ⁻-left⁺ : (kv : K& V) →
-               (l : ∃ λ i → Tree V l [ kv .key ] pred[ i ⊕ hˡ ]) →
-               (r : Tree V [ kv .key ] u hʳ) →
-               (bal : hˡ ∼ hʳ ⊔ h) →
-               Any P (proj₂ l) → Any P (proj₂ (joinˡ⁻ hˡ kv l r bal))
-joinˡ⁻-left⁺ {hˡ = zero}  _ (0# , leaf _)  _  _  p = left p
-joinˡ⁻-left⁺ {hˡ = zero}  _ (1# , leaf _)  _  _  p = left p
-joinˡ⁻-left⁺ {hˡ = suc _} _ (0# , t₁)      t₃ ∼+ p =
-  joinʳ⁺-left⁺ _ t₁ (1# , t₃) ∼+ p
-joinˡ⁻-left⁺ {hˡ = suc _} _ (0# , _)       _  ∼0 p = left p
-joinˡ⁻-left⁺ {hˡ = suc _} _ (0# , _)       _  ∼- p = left p
-joinˡ⁻-left⁺ {hˡ = suc _} _ (1# , _)       _  _  p = left p
-
-joinˡ⁻-right⁺ : (kv : K& V) →
-                (l : ∃ λ i → Tree V l [ kv .key ] pred[ i ⊕ hˡ ]) →
-                (r : Tree V [ kv .key ] u hʳ) →
-                (bal : hˡ ∼ hʳ ⊔ h) →
-                Any P r → Any P (proj₂ (joinˡ⁻ hˡ kv l r bal))
-joinˡ⁻-right⁺ {hˡ = zero}  _ (0# , leaf _)  _  _  p = right p
-joinˡ⁻-right⁺ {hˡ = zero}  _ (1# , leaf _)  _  _  p = right p
-joinˡ⁻-right⁺ {hˡ = suc _} _ (0# , t₁)      t₃ ∼+ p =
-  joinʳ⁺-right⁺ _ t₁ (1# , t₃) ∼+ p
-joinˡ⁻-right⁺ {hˡ = suc _} _ (0# , _)       _  ∼0 p = right p
-joinˡ⁻-right⁺ {hˡ = suc _} _ (0# , _)       _  ∼- p = right p
-joinˡ⁻-right⁺ {hˡ = suc _} _ (1# , _)       _  _  p = right p
-
-joinˡ⁻⁻ : (kv : K& V) →
-          (l : ∃ λ i → Tree V l [ kv .key ] pred[ i ⊕ hˡ ]) →
-          (r : Tree V [ kv .key ] u hʳ) →
-          (bal : hˡ ∼ hʳ ⊔ h) →
-          Any P (proj₂ (joinˡ⁻ hˡ kv l r bal)) →
-          P kv ⊎ Any P (proj₂ l) ⊎ Any P r
-joinˡ⁻⁻ {hˡ = zero}  _ (0# , leaf _) _  _  = Any.toSum
-joinˡ⁻⁻ {hˡ = zero}  _ (1# , leaf _) _  _  = Any.toSum
-joinˡ⁻⁻ {hˡ = suc _} _ (0# , t₁)     t₃ ∼+ = joinʳ⁺⁻ _ t₁ (1# , t₃) ∼+
-joinˡ⁻⁻ {hˡ = suc _} _ (0# , _)      _  ∼0 = Any.toSum
-joinˡ⁻⁻ {hˡ = suc _} _ (0# , _)      _  ∼- = Any.toSum
-joinˡ⁻⁻ {hˡ = suc _} _ (1# , _)      _  _  = Any.toSum
-
-----------------------------------------------------------------------
--- joinʳ⁻
-
-joinʳ⁻-here⁺ : (kv : K& V) →
-               (l : Tree V l [ kv .key ] hˡ) →
-               (r : ∃ λ i → Tree V [ kv .key ] u pred[ i ⊕ hʳ ]) →
-               (bal : hˡ ∼ hʳ ⊔ h) →
-               P kv → Any P (proj₂ (joinʳ⁻ hʳ kv l r bal))
-joinʳ⁻-here⁺ {hʳ = zero}  _ _  (0# , leaf _) _  p = here p
-joinʳ⁻-here⁺ {hʳ = zero}  _ _  (1# , leaf _) _  p = here p
-joinʳ⁻-here⁺ {hʳ = suc _} _ t₁ (0# , t₃)     ∼- p =
-  joinˡ⁺-here⁺ _ (1# , t₁) t₃ ∼- p
-joinʳ⁻-here⁺ {hʳ = suc _} _ _  (0# , _)      ∼0 p = here p
-joinʳ⁻-here⁺ {hʳ = suc _} _ _  (0# , _)      ∼+ p = here p
-joinʳ⁻-here⁺ {hʳ = suc _} _ _  (1# , _)      _  p = here p
-
-joinʳ⁻-left⁺ : (kv : K& V) →
-               (l : Tree V l [ kv .key ] hˡ) →
-               (r : ∃ λ i → Tree V [ kv .key ] u pred[ i ⊕ hʳ ]) →
-               (bal : hˡ ∼ hʳ ⊔ h) →
-               Any P l → Any P (proj₂ (joinʳ⁻ hʳ kv l r bal))
-joinʳ⁻-left⁺ {hʳ = zero}  _ _  (0# , leaf _) _  p = left p
-joinʳ⁻-left⁺ {hʳ = zero}  _ _  (1# , leaf _) _  p = left p
-joinʳ⁻-left⁺ {hʳ = suc _} _ t₁ (0# , t₃)     ∼- p =
-  joinˡ⁺-left⁺ _ (1# , t₁) t₃ ∼- p
-joinʳ⁻-left⁺ {hʳ = suc _} _ _  (0# , _)      ∼0 p = left p
-joinʳ⁻-left⁺ {hʳ = suc _} _ _  (0# , _)      ∼+ p = left p
-joinʳ⁻-left⁺ {hʳ = suc _} _ _  (1# , _)      _  p = left p
-
-joinʳ⁻-right⁺ : (kv : K& V) →
-                (l : Tree V l [ kv .key ] hˡ) →
-                (r : ∃ λ i → Tree V [ kv .key ] u pred[ i ⊕ hʳ ]) →
-                (bal : hˡ ∼ hʳ ⊔ h) →
-                Any P (proj₂ r) → Any P (proj₂ (joinʳ⁻ hʳ kv l r bal))
-joinʳ⁻-right⁺ {hʳ = zero}  _ _  (0# , leaf _) _  p = right p
-joinʳ⁻-right⁺ {hʳ = zero}  _ _  (1# , leaf _) _  p = right p
-joinʳ⁻-right⁺ {hʳ = suc _} _ t₁ (0# , t₃)     ∼- p =
-  joinˡ⁺-right⁺ _ (1# , t₁) t₃ ∼- p
-joinʳ⁻-right⁺ {hʳ = suc _} _ _  (0# , _)      ∼0 p = right p
-joinʳ⁻-right⁺ {hʳ = suc _} _ _  (0# , _)      ∼+ p = right p
-joinʳ⁻-right⁺ {hʳ = suc _} _ _  (1# , _)      _  p = right p
-
-joinʳ⁻⁻ : (kv : K& V) →
-          (l : Tree V l [ kv .key ] hˡ) →
-          (r : ∃ λ i → Tree V [ kv .key ] u pred[ i ⊕ hʳ ]) →
-          (bal : hˡ ∼ hʳ ⊔ h) →
-          Any P (proj₂ (joinʳ⁻ hʳ kv l r bal)) →
-          P kv ⊎ Any P l ⊎ Any P (proj₂ r)
-joinʳ⁻⁻ {hʳ = zero}  _ _  (0# , leaf _) _  = Any.toSum
-joinʳ⁻⁻ {hʳ = zero}  _ _  (1# , leaf _) _  = Any.toSum
-joinʳ⁻⁻ {hʳ = suc _} _ t₁ (0# , t₃)     ∼- = joinˡ⁺⁻ _ (1# , t₁) t₃ ∼-
-joinʳ⁻⁻ {hʳ = suc _} _ _  (0# , _)      ∼0 = Any.toSum
-joinʳ⁻⁻ {hʳ = suc _} _ _  (0# , _)      ∼+ = Any.toSum
-joinʳ⁻⁻ {hʳ = suc _} _ _  (1# , _)      _  = Any.toSum

From 4403f64ba99834ab7ce4f84573e18ecd95b7c164 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 3 Apr 2026 11:32:18 +0100
Subject: [PATCH 24/35] add: freshness predicate `_#_`

---
 CHANGELOG.md                                      |  7 +++++++
 src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda | 11 ++++++++++-
 2 files changed, 17 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 17c42cdcbd..626e025e31 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -435,6 +435,13 @@ Additions to existing modules
   pattern node⁰ˡ k₁ k₂ t₁ t₂ t₃ = node k₁ (node k₂ t₁ t₂ ∼0) t₃ ∼0
   ```
 
+* In `Data.Tree.AVL.Indexed.Relation.Unary.Any`:
+  ```agda
+  infix 5 _#[_]_ _#_
+  _#[_]_ : (k : Key) (P : Pred (K& V) p) → Pred (Any P t) ℓ₁
+  _#_ : Key → Pred (Any P t) ℓ₁
+  ```
+
 * In `Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Cast`:
   ```agda
   castʳ⁺ : Any P lm → Any P (castʳ lm m<u)
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
index 100584948c..3a66341576 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
@@ -20,7 +20,7 @@ open import Level using (Level; _⊔_)
 open import Relation.Nullary.Decidable.Core using (Dec; no; map′; _⊎?_)
 open import Relation.Unary using (Pred; _⊆_; Satisfiable; Decidable)
 
-open StrictTotalOrder strictTotalOrder using () renaming (Carrier to Key)
+open StrictTotalOrder strictTotalOrder using (_≉_) renaming (Carrier to Key)
 open import Data.Tree.AVL.Indexed strictTotalOrder
   using (Tree; Value; Key⁺; [_]; _<⁺_; K&_; _,_; key; _∼_⊔_; ∼0; leaf; node)
 
@@ -80,6 +80,15 @@ lookup (right p)          = lookup p
 lookupKey : Any P t → Key
 lookupKey = key ∘′ lookup
 
+-- Freshness of a given k : Key wrt a position p : Any P t
+infix 5 _#[_]_ _#_
+
+_#[_]_ : (k : Key) (P : Pred (K& V) p) → Pred (Any P t) ℓ₁
+k #[ P ] p = lookupKey p ≉ k
+
+_#_ : Key → Pred (Any P t) ℓ₁
+_#_ {P = P} k p = k #[ P ] p
+
 -- If any element satisfies P, then P is satisfiable.
 
 satisfied : Any P t → Satisfiable P

From b2fed916c123936ed439b0ec8ca2678966797c64 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 3 Apr 2026 11:39:57 +0100
Subject: [PATCH 25/35] refactor: consolidate `Lookup`

---
 .../Relation/Unary/Any/Properties/Lookup.agda | 68 +++++++++++++++---
 .../Unary/Any/Properties/LookupFun.agda       | 72 -------------------
 2 files changed, 59 insertions(+), 81 deletions(-)
 delete mode 100644 src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/LookupFun.agda

diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Lookup.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Lookup.agda
index c3206a7a23..65130ece76 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Lookup.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Lookup.agda
@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Properties related to Any.lookup
+-- Properties of lookup related to Any
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
@@ -12,14 +12,26 @@ module Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Lookup
   {a ℓ₁ ℓ₂} (sto : StrictTotalOrder a ℓ₁ ℓ₂)
   where
 
+open import Data.Maybe.Base using (Maybe; just)
+open import Data.Maybe.Properties using (just-injective)
 open import Data.Nat.Base using (ℕ)
-open import Data.Product.Base as Prod using (_,_)
+open import Data.Product.Base as Product using (∃; ∃-syntax; _,_; proj₁; proj₂)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base using (flip)
 open import Level using (Level)
+open import Relation.Binary.Definitions using (tri<; tri≈; tri>)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 open import Relation.Unary using (Pred; _∩_)
 
-open import Data.Tree.AVL.Indexed sto hiding (lookup)
-open import Data.Tree.AVL.Indexed.Relation.Unary.Any sto
+open import Data.Tree.AVL.Indexed sto as AVL hiding (lookup)
+open import Data.Tree.AVL.Indexed.Relation.Unary.Any sto as Any
+
+open StrictTotalOrder sto
+  using (_<_; module Eq; compare; irrefl)
+  renaming (Carrier to Key; trans to <-trans)
+open Eq using (_≉_; sym; trans)
+
+open import Relation.Binary.Construct.Add.Extrema.Strict _<_ using ([<]-injective)
 
 private
   variable
@@ -31,17 +43,21 @@ private
     t : Tree V l u h
 
 
+
+----------------------------------------------------------------------
+-- lookup
+
 lookup-result : (p : Any P t) → P (lookup p)
 lookup-result (here p)  = p
 lookup-result (left p)  = lookup-result p
 lookup-result (right p) = lookup-result p
 
 lookup-bounded : (p : Any P {l = l} {u = u} t) → l < lookupKey p < u
-lookup-bounded {t = node kv lk ku bal} (here p)  = ordered lk , ordered ku
-lookup-bounded {t = node kv lk ku bal} (left p)  =
-  Prod.map₂ (flip (trans⁺ _) (ordered ku)) (lookup-bounded p)
-lookup-bounded {t = node kv lk ku bal} (right p) =
-  Prod.map₁ (trans⁺ _ (ordered lk)) (lookup-bounded p)
+lookup-bounded {t = node _ lk ku _} (here p) = ordered lk , ordered ku
+lookup-bounded {t = node _ _  ku _} (left p) =
+  Product.map₂ (flip (trans⁺ _) (ordered ku)) (lookup-bounded p)
+lookup-bounded {t = node _ lk _ _} (right p) =
+  Product.map₁ (trans⁺ _ (ordered lk)) (lookup-bounded p)
 
 lookup-rebuild : (p : Any P t) → Q (lookup p) → Any Q t
 lookup-rebuild (here _)  q = here q
@@ -50,3 +66,37 @@ lookup-rebuild (right p) q = right (lookup-rebuild p q)
 
 lookup-rebuild-accum : (p : Any P t) → Q (lookup p) → Any (Q ∩ P) t
 lookup-rebuild-accum p q = lookup-rebuild p (q , lookup-result p)
+
+
+----------------------------------------------------------------------
+-- Relating Any.lookup to AVL.lookup
+
+module _ {V : Value v} (open Value V using (respects) renaming (family to Val)) where
+
+  lookup⁺ : (t : Tree V l u h) (k : Key) (seg : l < k < u) →
+            (p : Any P t) →
+            lookupKey p ≉ k
+            ⊎ ∃[ p≈k ] AVL.lookup t k seg ≡ just (respects p≈k (value (lookup p)))
+  lookup⁺ (node (k′ , v′) l r bal) k (l<k , k<u) p
+      with compare k′ k | p
+  ... | tri< k′<k _ _ | right p = lookup⁺ r k ([ k′<k ]ᴿ , k<u) p
+  ... | tri≈ _ k′≈k _ | here p = inj₂ (k′≈k , refl)
+  ... | tri> _ _ k<k′ | left p = lookup⁺ l k (l<k , [ k<k′ ]ᴿ) p
+  ... | tri< k′<k _ _ | left p = inj₁ (λ p≈k → irrefl p≈k (<-trans p<k′ k′<k))
+    where p<k′ = [<]-injective (proj₂ (lookup-bounded p))
+  ... | tri< k′<k _ _ | here p = inj₁ (λ p≈k → irrefl p≈k k′<k)
+  ... | tri≈ _ k′≈k _ | left p = inj₁ (λ p≈k → irrefl (trans p≈k (sym k′≈k)) p<k′)
+    where p<k′ = [<]-injective (proj₂ (lookup-bounded p))
+  ... | tri≈ _ k′≈k _ | right p = inj₁ (λ p≈k → irrefl (trans k′≈k (sym p≈k)) k′<p)
+    where k′<p = [<]-injective (proj₁ (lookup-bounded p))
+  ... | tri> _ _ k<k′ | here p = inj₁ (λ p≈k → irrefl (sym p≈k) k<k′)
+  ... | tri> _ _ k<k′ | right p = inj₁ (λ p≈k → irrefl (sym p≈k) (<-trans k<k′ k′<p))
+    where k′<p = [<]-injective (proj₁ (lookup-bounded p))
+
+  lookup⁻ : (t : Tree V l u h) (k : Key) (v : Val k) (seg : l < k < u) →
+            AVL.lookup t k seg ≡ just v →
+            Any (λ{ (k′ , v′) → ∃ λ k′≈k → respects k′≈k v′ ≡ v}) t
+  lookup⁻ (node (k′ , v′) l r bal) k v (l<k , k<u) eq with compare k′ k
+  ... | tri< k′<k _ _ = right (lookup⁻ r k v ([ k′<k ]ᴿ , k<u) eq)
+  ... | tri≈ _ k′≈k _ = here (k′≈k , just-injective eq)
+  ... | tri> _ _ k<k′ = left (lookup⁻ l k v (l<k , [ k<k′ ]ᴿ) eq)
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/LookupFun.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/LookupFun.agda
deleted file mode 100644
index 2539a18eb1..0000000000
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/LookupFun.agda
+++ /dev/null
@@ -1,72 +0,0 @@
-------------------------------------------------------------------------
--- The Agda standard library
---
--- Properties of lookup related to Any
-------------------------------------------------------------------------
-
-{-# OPTIONS --cubical-compatible --safe #-}
-
-open import Relation.Binary.Bundles using (StrictTotalOrder)
-
-module Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.LookupFun
-  {a ℓ₁ ℓ₂} (sto : StrictTotalOrder a ℓ₁ ℓ₂)
-  where
-
-open import Data.Maybe.Base using (Maybe; just)
-open import Data.Maybe.Properties using (just-injective)
-open import Data.Nat.Base using (ℕ)
-open import Data.Product.Base using (∃; ∃-syntax; _,_; proj₁; proj₂)
-open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
-open import Level using (Level)
-open import Relation.Binary.Definitions using (tri<; tri≈; tri>)
-open import Relation.Binary.PropositionalEquality.Core using (_≡_) renaming (refl to ≡-refl)
-open import Relation.Unary using (Pred)
-
-open import Data.Tree.AVL.Indexed sto as AVL
-open import Data.Tree.AVL.Indexed.Relation.Unary.Any sto as Any
-open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Lookup sto
-  using (lookup-bounded)
-
-open StrictTotalOrder sto renaming (Carrier to Key; trans to <-trans); open Eq using (sym; trans)
-
-open import Relation.Binary.Construct.Add.Extrema.Strict _<_ using ([<]-injective)
-
-private
-  variable
-    v p : Level
-    V : Value v
-    l u : Key⁺
-    n : ℕ
-    P : Pred (K& V) p
-
-
-module _ {V : Value v} (open Value V using (respects) renaming (family to Val)) where
-
-  lookup⁺ : (t : Tree V l u n) (k : Key) (seg : l < k < u) →
-            (p : Any P t) →
-            (key (Any.lookup p) ≉ k)
-            ⊎ (∃[ p≈k ] AVL.lookup t k seg
-               ≡ just (respects p≈k (value (Any.lookup p))))
-  lookup⁺ (node (k′ , v′) l r bal) k (l<k , k<u) p
-      with compare k′ k | p
-  ... | tri< k′<k _ _ | right p = lookup⁺ r k ([ k′<k ]ᴿ , k<u) p
-  ... | tri≈ _ k′≈k _ | here p = inj₂ (k′≈k , ≡-refl)
-  ... | tri> _ _ k<k′ | left p = lookup⁺ l k (l<k , [ k<k′ ]ᴿ) p
-  ... | tri< k′<k _ _ | left p = inj₁ (λ p≈k → irrefl p≈k (<-trans p<k′ k′<k))
-    where p<k′ = [<]-injective (proj₂ (lookup-bounded p))
-  ... | tri< k′<k _ _ | here p = inj₁ (λ p≈k → irrefl p≈k k′<k)
-  ... | tri≈ _ k′≈k _ | left p = inj₁ (λ p≈k → irrefl (trans p≈k (sym k′≈k)) p<k′)
-    where p<k′ = [<]-injective (proj₂ (lookup-bounded p))
-  ... | tri≈ _ k′≈k _ | right p = inj₁ (λ p≈k → irrefl (trans k′≈k (sym p≈k)) k′<p)
-    where k′<p = [<]-injective (proj₁ (lookup-bounded p))
-  ... | tri> _ _ k<k′ | here p = inj₁ (λ p≈k → irrefl (sym p≈k) k<k′)
-  ... | tri> _ _ k<k′ | right p = inj₁ (λ p≈k → irrefl (sym p≈k) (<-trans k<k′ k′<p))
-    where k′<p = [<]-injective (proj₁ (lookup-bounded p))
-
-  lookup⁻ : (t : Tree V l u n) (k : Key) (v : Val k) (seg : l < k < u) →
-            AVL.lookup t k seg ≡ just v →
-            Any (λ{ (k′ , v′) → ∃ λ k′≈k → respects k′≈k v′ ≡ v}) t
-  lookup⁻ (node (k′ , v′) l r bal) k v (l<k , k<u) eq with compare k′ k
-  ... | tri< k′<k _ _ = right (lookup⁻ r k v ([ k′<k ]ᴿ , k<u) eq)
-  ... | tri≈ _ k′≈k _ = here (k′≈k , just-injective eq)
-  ... | tri> _ _ k<k′ = left (lookup⁻ l k v (l<k , [ k<k′ ]ᴿ) eq)

From ed6c17623eb46be6ce8177e5043a4df139608cc0 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 3 Apr 2026 11:40:53 +0100
Subject: [PATCH 26/35] refactor: use freshness predicate

---
 .../AVL/Indexed/Relation/Unary/Any/Properties/Lookup.agda     | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Lookup.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Lookup.agda
index 65130ece76..3added7bb6 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Lookup.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Lookup.agda
@@ -29,7 +29,7 @@ open import Data.Tree.AVL.Indexed.Relation.Unary.Any sto as Any
 open StrictTotalOrder sto
   using (_<_; module Eq; compare; irrefl)
   renaming (Carrier to Key; trans to <-trans)
-open Eq using (_≉_; sym; trans)
+open Eq using (sym; trans)
 
 open import Relation.Binary.Construct.Add.Extrema.Strict _<_ using ([<]-injective)
 
@@ -75,7 +75,7 @@ module _ {V : Value v} (open Value V using (respects) renaming (family to Val))
 
   lookup⁺ : (t : Tree V l u h) (k : Key) (seg : l < k < u) →
             (p : Any P t) →
-            lookupKey p ≉ k
+            k # p
             ⊎ ∃[ p≈k ] AVL.lookup t k seg ≡ just (respects p≈k (value (lookup p)))
   lookup⁺ (node (k′ , v′) l r bal) k (l<k , k<u) p
       with compare k′ k | p

From 2cadab590d0ff24a8bff638181470b6eba0a3eac Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 3 Apr 2026 11:43:51 +0100
Subject: [PATCH 27/35] refactor: standardise bound name for a segment `l < k <
 u`

---
 .../AVL/Indexed/Relation/Unary/Any/Properties/Lookup.agda     | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Lookup.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Lookup.agda
index 3added7bb6..32ca6fede2 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Lookup.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Lookup.agda
@@ -73,10 +73,10 @@ lookup-rebuild-accum p q = lookup-rebuild p (q , lookup-result p)
 
 module _ {V : Value v} (open Value V using (respects) renaming (family to Val)) where
 
-  lookup⁺ : (t : Tree V l u h) (k : Key) (seg : l < k < u) →
+  lookup⁺ : (t : Tree V l u h) (k : Key) (l<k<u : l < k < u) →
             (p : Any P t) →
             k # p
-            ⊎ ∃[ p≈k ] AVL.lookup t k seg ≡ just (respects p≈k (value (lookup p)))
+            ⊎ ∃[ p≈k ] AVL.lookup t k l<k<u ≡ just (respects p≈k (value (lookup p)))
   lookup⁺ (node (k′ , v′) l r bal) k (l<k , k<u) p
       with compare k′ k | p
   ... | tri< k′<k _ _ | right p = lookup⁺ r k ([ k′<k ]ᴿ , k<u) p

From 1e5ae6d6352aa0417212f3f4cd310d772eeb0edf Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 3 Apr 2026 12:29:24 +0100
Subject: [PATCH 28/35] refactor: split up `Join` and `JoinLemmas`

---
 CHANGELOG.md                                  |   5 +-
 .../Relation/Unary/Any/Properties/Join.agda   | 262 +---------------
 .../Unary/Any/Properties/JoinLemmas.agda      | 290 ++++++++++++++++++
 3 files changed, 296 insertions(+), 261 deletions(-)
 create mode 100644 src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/JoinLemmas.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 626e025e31..9f69962d0e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -192,6 +192,7 @@ New modules
   Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.HeadTail
   Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Insert
   Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Join
+  Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.JoinLemmas
   Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Singleton
   ```
 
@@ -439,7 +440,7 @@ Additions to existing modules
   ```agda
   infix 5 _#[_]_ _#_
   _#[_]_ : (k : Key) (P : Pred (K& V) p) → Pred (Any P t) ℓ₁
-  _#_ : Key → Pred (Any P t) ℓ₁
+  _#_    : Key → Pred (Any P t) ℓ₁
   ```
 
 * In `Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Cast`:
@@ -477,7 +478,7 @@ Additions to existing modules
                    Any P t⁻ → Any P t
   ```
 
-* In `Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Join`:
+* In `Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.JoinLemmas`:
   ```
   joinˡ⁻-here⁺ : (kv : K& V) →
                  (l : Tree⁻ V l [ kv .key ] hˡ) →
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Join.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Join.agda
index 152e51d1fc..68eec7d50b 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Join.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Join.agda
@@ -24,6 +24,9 @@ open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Cast sto
   using (castʳ⁺; castʳ⁻)
 open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.HeadTail sto
   using (headTail⁺; headTail-head⁻; headTail-tail⁻)
+open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.JoinLemmas sto
+  using (joinʳ⁻-left⁺; joinʳ⁻-here⁺; joinʳ⁻-right⁺; joinʳ⁻⁻)
+
 
 private
   variable
@@ -33,265 +36,6 @@ private
     l m u : Key⁺
     hˡ hʳ h : ℕ
 
-  [_]ᵏ : K& V → Key⁺
-  [ kv ]ᵏ = [ kv .key ]
-
-
-----------------------------------------------------------------------
--- joinˡ⁺
-
-joinˡ⁺-here⁺ : (kv : K& V) →
-               (l : Tree⁺ V l [ kv ]ᵏ hˡ) →
-               (r : Tree V [ kv ]ᵏ u hʳ) →
-               (bal : hˡ ∼ hʳ ⊔ h) →
-               P kv → Any P (proj₂ (joinˡ⁺ kv l r bal))
-joinˡ⁺-here⁺ _ (0# , _)                 _ _  p = here p
-joinˡ⁺-here⁺ _ (1# , _)                 _ ∼0 p = here p
-joinˡ⁺-here⁺ _ (1# , _)                 _ ∼+ p = here p
-joinˡ⁺-here⁺ _ (1# , node _ _ _ ∼-)     _ ∼- p = right (here p)
-joinˡ⁺-here⁺ _ (1# , node _ _ _ ∼0)     _ ∼- p = right (here p)
-joinˡ⁺-here⁺ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- p = right (here p)
-
-joinˡ⁺-left⁺ : (kv : K& V) →
-               (l : Tree⁺ V l [ kv ]ᵏ hˡ) →
-               (r : Tree V [ kv ]ᵏ u hʳ) →
-               (bal : hˡ ∼ hʳ ⊔ h) →
-               Any P (proj₂ l) → Any P (proj₂ (joinˡ⁺ kv l r bal))
-joinˡ⁺-left⁺ _ (0# , _)                 _ _  p                 = left p
-joinˡ⁺-left⁺ _ (1# , _)                 _ ∼0 p                 = left p
-joinˡ⁺-left⁺ _ (1# , _)                 _ ∼+ p                 = left p
-joinˡ⁺-left⁺ _ (1# , node _ _ _ ∼-)     _ ∼- (here p)          = here p
-joinˡ⁺-left⁺ _ (1# , node _ _ _ ∼-)     _ ∼- (left p)          = left p
-joinˡ⁺-left⁺ _ (1# , node _ _ _ ∼-)     _ ∼- (right p)         = right (left p)
-joinˡ⁺-left⁺ _ (1# , node _ _ _ ∼0)     _ ∼- (here p)          = here p
-joinˡ⁺-left⁺ _ (1# , node _ _ _ ∼0)     _ ∼- (left p)          = left p
-joinˡ⁺-left⁺ _ (1# , node _ _ _ ∼0)     _ ∼- (right p)         = right (left p)
-joinˡ⁺-left⁺ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- (here p)          = left (here p)
-joinˡ⁺-left⁺ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- (left p)          = left (left p)
-joinˡ⁺-left⁺ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- (right (here p))  = here p
-joinˡ⁺-left⁺ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- (right (left p))  = left (right p)
-joinˡ⁺-left⁺ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- (right (right p)) = right (left p)
-
-joinˡ⁺-right⁺ : (kv : K& V) →
-                (l : Tree⁺ V l [ kv ]ᵏ hˡ) →
-                (r : Tree V [ kv ]ᵏ u hʳ) →
-                (bal : hˡ ∼ hʳ ⊔ h) →
-                Any P r → Any P (proj₂ (joinˡ⁺ kv l r bal))
-joinˡ⁺-right⁺ _ (0# , _)                 _ _  p = right p
-joinˡ⁺-right⁺ _ (1# , _)                 _ ∼0 p = right p
-joinˡ⁺-right⁺ _ (1# , _)                 _ ∼+ p = right p
-joinˡ⁺-right⁺ _ (1# , node _ _ _ ∼-)     _ ∼- p = right (right p)
-joinˡ⁺-right⁺ _ (1# , node _ _ _ ∼0)     _ ∼- p = right (right p)
-joinˡ⁺-right⁺ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- p = right (right p)
-
-joinˡ⁺⁻ : (kv : K& V) →
-          (l : Tree⁺ V l [ kv ]ᵏ hˡ) →
-          (r : Tree V [ kv ]ᵏ u hʳ) →
-          (bal : hˡ ∼ hʳ ⊔ h) →
-          Any P (proj₂ (joinˡ⁺ kv l r bal)) →
-          P kv ⊎ Any P (proj₂ l) ⊎ Any P r
-joinˡ⁺⁻ _ (0# , _)                 _ _  = Any.toSum
-joinˡ⁺⁻ _ (1# , _)                 _ ∼0 = Any.toSum
-joinˡ⁺⁻ _ (1# , _)                 _ ∼+ = Any.toSum
-joinˡ⁺⁻ _ (1# , node _ _ _ ∼-)     _ ∼- = λ where
-  (left p)          → inj₂ (inj₁ (left p))
-  (here p)          → inj₂ (inj₁ (here p))
-  (right (left p))  → inj₂ (inj₁ (right p))
-  (right (here p))  → inj₁ p
-  (right (right p)) → inj₂ (inj₂ p)
-joinˡ⁺⁻ _ (1# , node _ _ _ ∼0)     _ ∼- = λ where
-  (left p)          → inj₂ (inj₁ (left p))
-  (here p)          → inj₂ (inj₁ (here p))
-  (right (left p))  → inj₂ (inj₁ (right p))
-  (right (here p))  → inj₁ p
-  (right (right p)) → inj₂ (inj₂ p)
-joinˡ⁺⁻ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- = λ where
-  (left (left p))   → inj₂ (inj₁ (left p))
-  (left (here p))   → inj₂ (inj₁ (here p))
-  (left (right p))  → inj₂ (inj₁ (right (left p)))
-  (here p)          → inj₂ (inj₁ (right (here p)))
-  (right (left p))  → inj₂ (inj₁ (right (right p)))
-  (right (here p))  → inj₁ p
-  (right (right p)) → inj₂ (inj₂ p)
-
-----------------------------------------------------------------------
--- joinʳ⁺
-
-joinʳ⁺-here⁺ : (kv : K& V) →
-               (l : Tree V l [ kv ]ᵏ hˡ) →
-               (r : Tree⁺ V [ kv ]ᵏ u hʳ) →
-               (bal : hˡ ∼ hʳ ⊔ h) →
-               P kv → Any P (proj₂ (joinʳ⁺ kv l r bal))
-joinʳ⁺-here⁺ _ _ (0# , _)                 _  p = here p
-joinʳ⁺-here⁺ _ _ (1# , _)                 ∼0 p = here p
-joinʳ⁺-here⁺ _ _ (1# , _)                 ∼- p = here p
-joinʳ⁺-here⁺ _ _ (1# , node _ _ _ ∼+)     ∼+ p = left (here p)
-joinʳ⁺-here⁺ _ _ (1# , node _ _ _ ∼0)     ∼+ p = left (here p)
-joinʳ⁺-here⁺ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ p = left (here p)
-
-joinʳ⁺-left⁺ : (kv : K& V) →
-               (l : Tree V l [ kv ]ᵏ hˡ) →
-               (r : Tree⁺ V [ kv ]ᵏ u hʳ) →
-               (bal : hˡ ∼ hʳ ⊔ h) →
-               Any P l → Any P (proj₂ (joinʳ⁺ kv l r bal))
-joinʳ⁺-left⁺ _ _ (0# , _)                 _  p = left p
-joinʳ⁺-left⁺ _ _ (1# , _)                 ∼0 p = left p
-joinʳ⁺-left⁺ _ _ (1# , _)                 ∼- p = left p
-joinʳ⁺-left⁺ _ _ (1# , node _ _ _ ∼+)     ∼+ p = left (left p)
-joinʳ⁺-left⁺ _ _ (1# , node _ _ _ ∼0)     ∼+ p = left (left p)
-joinʳ⁺-left⁺ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ p = left (left p)
-
-joinʳ⁺-right⁺ : (kv : K& V) →
-                (l : Tree V l [ kv ]ᵏ hˡ) →
-                (r : Tree⁺ V [ kv ]ᵏ u hʳ) →
-                (bal : hˡ ∼ hʳ ⊔ h) →
-                Any P (proj₂ r) → Any P (proj₂ (joinʳ⁺ kv l r bal))
-joinʳ⁺-right⁺ _ _ (0# , _)                 _  p                = right p
-joinʳ⁺-right⁺ _ _ (1# , _)                 ∼0 p                = right p
-joinʳ⁺-right⁺ _ _ (1# , _)                 ∼- p                = right p
-joinʳ⁺-right⁺ _ _ (1# , node _ _ _ ∼+)     ∼+ (here p)         = here p
-joinʳ⁺-right⁺ _ _ (1# , node _ _ _ ∼+)     ∼+ (left p)         = left (right p)
-joinʳ⁺-right⁺ _ _ (1# , node _ _ _ ∼+)     ∼+ (right p)        = right p
-joinʳ⁺-right⁺ _ _ (1# , node _ _ _ ∼0)     ∼+ (here p)         = here p
-joinʳ⁺-right⁺ _ _ (1# , node _ _ _ ∼0)     ∼+ (left p)         = left (right p)
-joinʳ⁺-right⁺ _ _ (1# , node _ _ _ ∼0)     ∼+ (right p)        = right p
-joinʳ⁺-right⁺ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ (here p)         = right (here p)
-joinʳ⁺-right⁺ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ (left (here p))  = here p
-joinʳ⁺-right⁺ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ (left (left p))  = left (right p)
-joinʳ⁺-right⁺ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ (left (right p)) = right (left p)
-joinʳ⁺-right⁺ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ (right p)        = right (right p)
-
-joinʳ⁺⁻ : (kv : K& V) →
-          (l : Tree V l [ kv ]ᵏ hˡ) →
-          (r : Tree⁺ V [ kv ]ᵏ u hʳ) →
-          (bal : hˡ ∼ hʳ ⊔ h) →
-          Any P (proj₂ (joinʳ⁺ kv l r bal)) →
-          P kv ⊎ Any P l ⊎ Any P (proj₂ r)
-joinʳ⁺⁻ _ _ (0# , _)                 _  = Any.toSum
-joinʳ⁺⁻ _ _ (1# , _)                 ∼0 = Any.toSum
-joinʳ⁺⁻ _ _ (1# , _)                 ∼- = Any.toSum
-joinʳ⁺⁻ _ _ (1# , node _ _ _ ∼+)     ∼+ = λ where
-  (left (left p))  → inj₂ (inj₁ p)
-  (left (here p))  → inj₁ p
-  (left (right p)) → inj₂ (inj₂ (left p))
-  (here p)         → inj₂ (inj₂ (here p))
-  (right p)        → inj₂ (inj₂ (right p))
-joinʳ⁺⁻ _ _ (1# , node _ _ _ ∼0)     ∼+ = λ where
-  (left (left p))  → inj₂ (inj₁ p)
-  (left (here p))  → inj₁ p
-  (left (right p)) → inj₂ (inj₂ (left p))
-  (here p)         → inj₂ (inj₂ (here p))
-  (right p)        → inj₂ (inj₂ (right p))
-joinʳ⁺⁻ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ = λ where
-  (left (left p))   → inj₂ (inj₁ p)
-  (left (here p))   → inj₁ p
-  (left (right p))  → inj₂ (inj₂ (left (left p)))
-  (here p)          → inj₂ (inj₂ (left (here p)))
-  (right (left p))  → inj₂ (inj₂ (left (right p)))
-  (right (here p))  → inj₂ (inj₂ (here p))
-  (right (right p)) → inj₂ (inj₂ (right p))
-
-----------------------------------------------------------------------
--- joinˡ⁻
-
-joinˡ⁻-here⁺ : (kv : K& V) →
-               (l : Tree⁻ V l [ kv ]ᵏ hˡ) →
-               (r : Tree V [ kv ]ᵏ u hʳ) →
-               (bal : hˡ ∼ hʳ ⊔ h) →
-               P kv → Any P (proj₂ (joinˡ⁻ hˡ kv l r bal))
-joinˡ⁻-here⁺ {hˡ = zero}  _ (leaf⁻ _) _  _  p = here p
-joinˡ⁻-here⁺ {hˡ = suc _} _ (0# , t₁) t₃ ∼+ p =
-  joinʳ⁺-here⁺ _ t₁ (1# , t₃) ∼+ p
-joinˡ⁻-here⁺ {hˡ = suc _} _ (0# , _)  _  ∼0 p = here p
-joinˡ⁻-here⁺ {hˡ = suc _} _ (0# , _)  _  ∼- p = here p
-joinˡ⁻-here⁺ {hˡ = suc _} _ (1# , _)  _  _  p = here p
-
-joinˡ⁻-left⁺ : (kv : K& V) →
-               (l : Tree⁻ V l [ kv ]ᵏ hˡ) →
-               (r : Tree V [ kv ]ᵏ u hʳ) →
-               (bal : hˡ ∼ hʳ ⊔ h) →
-               Any P (proj₂ l) → Any P (proj₂ (joinˡ⁻ hˡ kv l r bal))
-joinˡ⁻-left⁺ {hˡ = zero}  _ (leaf⁻ _)  _  _  p = left p
-joinˡ⁻-left⁺ {hˡ = suc _} _ (0# , t₁)  t₃ ∼+ p =
-  joinʳ⁺-left⁺ _ t₁ (1# , t₃) ∼+ p
-joinˡ⁻-left⁺ {hˡ = suc _} _ (0# , _)   _  ∼0 p = left p
-joinˡ⁻-left⁺ {hˡ = suc _} _ (0# , _)   _  ∼- p = left p
-joinˡ⁻-left⁺ {hˡ = suc _} _ (1# , _)   _  _  p = left p
-
-joinˡ⁻-right⁺ : (kv : K& V) →
-                (l : Tree⁻ V l [ kv ]ᵏ hˡ) →
-                (r : Tree V [ kv ]ᵏ u hʳ) →
-                (bal : hˡ ∼ hʳ ⊔ h) →
-                Any P r → Any P (proj₂ (joinˡ⁻ hˡ kv l r bal))
-joinˡ⁻-right⁺ {hˡ = zero}  _ (leaf⁻ _)  _  _  p = right p
-joinˡ⁻-right⁺ {hˡ = suc _} _ (0# , t₁)  t₃ ∼+ p =
-  joinʳ⁺-right⁺ _ t₁ (1# , t₃) ∼+ p
-joinˡ⁻-right⁺ {hˡ = suc _} _ (0# , _)   _  ∼0 p = right p
-joinˡ⁻-right⁺ {hˡ = suc _} _ (0# , _)   _  ∼- p = right p
-joinˡ⁻-right⁺ {hˡ = suc _} _ (1# , _)   _  _  p = right p
-
-joinˡ⁻⁻ : (kv : K& V) →
-          (l : Tree⁻ V l [ kv ]ᵏ hˡ) →
-          (r : Tree V [ kv ]ᵏ u hʳ) →
-          (bal : hˡ ∼ hʳ ⊔ h) →
-          Any P (proj₂ (joinˡ⁻ hˡ kv l r bal)) →
-          P kv ⊎ Any P (proj₂ l) ⊎ Any P r
-joinˡ⁻⁻ {hˡ = zero}  _ (leaf⁻ _) _  _  = Any.toSum
-joinˡ⁻⁻ {hˡ = suc _} _ (0# , t₁) t₃ ∼+ = joinʳ⁺⁻ _ t₁ (1# , t₃) ∼+
-joinˡ⁻⁻ {hˡ = suc _} _ (0# , _)  _  ∼0 = Any.toSum
-joinˡ⁻⁻ {hˡ = suc _} _ (0# , _)  _  ∼- = Any.toSum
-joinˡ⁻⁻ {hˡ = suc _} _ (1# , _)  _  _  = Any.toSum
-
-----------------------------------------------------------------------
--- joinʳ⁻
-
-joinʳ⁻-here⁺ : (kv : K& V) →
-               (l : Tree V l [ kv ]ᵏ hˡ) →
-               (r : Tree⁻ V [ kv ]ᵏ u hʳ) →
-               (bal : hˡ ∼ hʳ ⊔ h) →
-               P kv → Any P (proj₂ (joinʳ⁻ hʳ kv l r bal))
-joinʳ⁻-here⁺ {hʳ = zero}  _ _  (leaf⁻ _) _  p = here p
-joinʳ⁻-here⁺ {hʳ = suc _} _ t₁ (0# , t₃) ∼- p =
-  joinˡ⁺-here⁺ _ (1# , t₁) t₃ ∼- p
-joinʳ⁻-here⁺ {hʳ = suc _} _ _  (0# , _)  ∼0 p = here p
-joinʳ⁻-here⁺ {hʳ = suc _} _ _  (0# , _)  ∼+ p = here p
-joinʳ⁻-here⁺ {hʳ = suc _} _ _  (1# , _)  _  p = here p
-
-joinʳ⁻-left⁺ : (kv : K& V) →
-               (l : Tree V l [ kv ]ᵏ hˡ) →
-               (r : Tree⁻ V [ kv ]ᵏ u hʳ) →
-               (bal : hˡ ∼ hʳ ⊔ h) →
-               Any P l → Any P (proj₂ (joinʳ⁻ hʳ kv l r bal))
-joinʳ⁻-left⁺ {hʳ = zero}  _ _  (leaf⁻ _) _  p = left p
-joinʳ⁻-left⁺ {hʳ = suc _} _ t₁ (0# , t₃) ∼- p =
-  joinˡ⁺-left⁺ _ (1# , t₁) t₃ ∼- p
-joinʳ⁻-left⁺ {hʳ = suc _} _ _  (0# , _)  ∼0 p = left p
-joinʳ⁻-left⁺ {hʳ = suc _} _ _  (0# , _)  ∼+ p = left p
-joinʳ⁻-left⁺ {hʳ = suc _} _ _  (1# , _)  _  p = left p
-
-joinʳ⁻-right⁺ : (kv : K& V) →
-                (l : Tree V l [ kv ]ᵏ hˡ) →
-                (r : Tree⁻ V [ kv ]ᵏ u hʳ) →
-                (bal : hˡ ∼ hʳ ⊔ h) →
-                Any P (proj₂ r) → Any P (proj₂ (joinʳ⁻ hʳ kv l r bal))
-joinʳ⁻-right⁺ {hʳ = zero}  _ _  (leaf⁻ _) _  p = right p
-joinʳ⁻-right⁺ {hʳ = suc _} _ t₁ (0# , t₃) ∼- p =
-  joinˡ⁺-right⁺ _ (1# , t₁) t₃ ∼- p
-joinʳ⁻-right⁺ {hʳ = suc _} _ _  (0# , _)  ∼0 p = right p
-joinʳ⁻-right⁺ {hʳ = suc _} _ _  (0# , _)  ∼+ p = right p
-joinʳ⁻-right⁺ {hʳ = suc _} _ _  (1# , _)  _  p = right p
-
-joinʳ⁻⁻ : (kv : K& V) →
-          (l : Tree V l [ kv ]ᵏ hˡ) →
-          (r : Tree⁻ V [ kv ]ᵏ u hʳ) →
-          (bal : hˡ ∼ hʳ ⊔ h) →
-          Any P (proj₂ (joinʳ⁻ hʳ kv l r bal)) →
-          P kv ⊎ Any P l ⊎ Any P (proj₂ r)
-joinʳ⁻⁻ {hʳ = zero}  _ _  (leaf⁻ _) _  = Any.toSum
-joinʳ⁻⁻ {hʳ = suc _} _ t₁ (0# , t₃) ∼- = joinˡ⁺⁻ _ (1# , t₁) t₃ ∼-
-joinʳ⁻⁻ {hʳ = suc _} _ _  (0# , _)  ∼0 = Any.toSum
-joinʳ⁻⁻ {hʳ = suc _} _ _  (0# , _)  ∼+ = Any.toSum
-joinʳ⁻⁻ {hʳ = suc _} _ _  (1# , _)  _  = Any.toSum
 
 ----------------------------------------------------------------------
 -- join
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/JoinLemmas.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/JoinLemmas.agda
new file mode 100644
index 0000000000..935e555b66
--- /dev/null
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/JoinLemmas.agda
@@ -0,0 +1,290 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties constant-time join functions related to Any
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Bundles using (StrictTotalOrder)
+
+module Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.JoinLemmas
+  {a ℓ₁ ℓ₂} (sto : StrictTotalOrder a ℓ₁ ℓ₂)
+  where
+
+open import Data.Nat.Base using (ℕ; zero; suc)
+open import Data.Product.Base using (∃; _,_; proj₂)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
+open import Level using (Level)
+open import Relation.Unary using (Pred)
+
+open import Data.Tree.AVL.Indexed sto
+open import Data.Tree.AVL.Indexed.Relation.Unary.Any sto as Any
+
+private
+  variable
+    v p : Level
+    V : Value v
+    P : Pred (K& V) p
+    l u : Key⁺
+    hˡ hʳ h : ℕ
+
+  [_]ᵏ : K& V → Key⁺
+  [ kv ]ᵏ = [ kv .key ]
+
+
+----------------------------------------------------------------------
+-- joinˡ⁺
+
+joinˡ⁺-here⁺ : (kv : K& V) →
+               (l : Tree⁺ V l [ kv ]ᵏ hˡ) →
+               (r : Tree V [ kv ]ᵏ u hʳ) →
+               (bal : hˡ ∼ hʳ ⊔ h) →
+               P kv → Any P (proj₂ (joinˡ⁺ kv l r bal))
+joinˡ⁺-here⁺ _ (0# , _)                 _ _  p = here p
+joinˡ⁺-here⁺ _ (1# , _)                 _ ∼0 p = here p
+joinˡ⁺-here⁺ _ (1# , _)                 _ ∼+ p = here p
+joinˡ⁺-here⁺ _ (1# , node _ _ _ ∼-)     _ ∼- p = right (here p)
+joinˡ⁺-here⁺ _ (1# , node _ _ _ ∼0)     _ ∼- p = right (here p)
+joinˡ⁺-here⁺ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- p = right (here p)
+
+joinˡ⁺-left⁺ : (kv : K& V) →
+               (l@(_ , lt) : Tree⁺ V l [ kv ]ᵏ hˡ) →
+               (r : Tree V [ kv ]ᵏ u hʳ) →
+               (bal : hˡ ∼ hʳ ⊔ h) →
+               Any P lt → Any P (proj₂ (joinˡ⁺ kv l r bal))
+joinˡ⁺-left⁺ _ (0# , _)                 _ _  p                 = left p
+joinˡ⁺-left⁺ _ (1# , _)                 _ ∼0 p                 = left p
+joinˡ⁺-left⁺ _ (1# , _)                 _ ∼+ p                 = left p
+joinˡ⁺-left⁺ _ (1# , node _ _ _ ∼-)     _ ∼- (here p)          = here p
+joinˡ⁺-left⁺ _ (1# , node _ _ _ ∼-)     _ ∼- (left p)          = left p
+joinˡ⁺-left⁺ _ (1# , node _ _ _ ∼-)     _ ∼- (right p)         = right (left p)
+joinˡ⁺-left⁺ _ (1# , node _ _ _ ∼0)     _ ∼- (here p)          = here p
+joinˡ⁺-left⁺ _ (1# , node _ _ _ ∼0)     _ ∼- (left p)          = left p
+joinˡ⁺-left⁺ _ (1# , node _ _ _ ∼0)     _ ∼- (right p)         = right (left p)
+joinˡ⁺-left⁺ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- (here p)          = left (here p)
+joinˡ⁺-left⁺ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- (left p)          = left (left p)
+joinˡ⁺-left⁺ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- (right (here p))  = here p
+joinˡ⁺-left⁺ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- (right (left p))  = left (right p)
+joinˡ⁺-left⁺ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- (right (right p)) = right (left p)
+
+joinˡ⁺-right⁺ : (kv : K& V) →
+                (l : Tree⁺ V l [ kv ]ᵏ hˡ) →
+                (r : Tree V [ kv ]ᵏ u hʳ) →
+                (bal : hˡ ∼ hʳ ⊔ h) →
+                Any P r → Any P (proj₂ (joinˡ⁺ kv l r bal))
+joinˡ⁺-right⁺ _ (0# , _)                 _ _  p = right p
+joinˡ⁺-right⁺ _ (1# , _)                 _ ∼0 p = right p
+joinˡ⁺-right⁺ _ (1# , _)                 _ ∼+ p = right p
+joinˡ⁺-right⁺ _ (1# , node _ _ _ ∼-)     _ ∼- p = right (right p)
+joinˡ⁺-right⁺ _ (1# , node _ _ _ ∼0)     _ ∼- p = right (right p)
+joinˡ⁺-right⁺ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- p = right (right p)
+
+joinˡ⁺⁻ : (kv : K& V) →
+          (l@(_ , lt) : Tree⁺ V l [ kv ]ᵏ hˡ) →
+          (r : Tree V [ kv ]ᵏ u hʳ) →
+          (bal : hˡ ∼ hʳ ⊔ h) →
+          Any P (proj₂ (joinˡ⁺ kv l r bal)) →
+          P kv ⊎ Any P lt ⊎ Any P r
+joinˡ⁺⁻ _ (0# , _)                 _ _  = Any.toSum
+joinˡ⁺⁻ _ (1# , _)                 _ ∼0 = Any.toSum
+joinˡ⁺⁻ _ (1# , _)                 _ ∼+ = Any.toSum
+joinˡ⁺⁻ _ (1# , node _ _ _ ∼-)     _ ∼- = λ where
+  (left p)          → inj₂ (inj₁ (left p))
+  (here p)          → inj₂ (inj₁ (here p))
+  (right (left p))  → inj₂ (inj₁ (right p))
+  (right (here p))  → inj₁ p
+  (right (right p)) → inj₂ (inj₂ p)
+joinˡ⁺⁻ _ (1# , node _ _ _ ∼0)     _ ∼- = λ where
+  (left p)          → inj₂ (inj₁ (left p))
+  (here p)          → inj₂ (inj₁ (here p))
+  (right (left p))  → inj₂ (inj₁ (right p))
+  (right (here p))  → inj₁ p
+  (right (right p)) → inj₂ (inj₂ p)
+joinˡ⁺⁻ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- = λ where
+  (left (left p))   → inj₂ (inj₁ (left p))
+  (left (here p))   → inj₂ (inj₁ (here p))
+  (left (right p))  → inj₂ (inj₁ (right (left p)))
+  (here p)          → inj₂ (inj₁ (right (here p)))
+  (right (left p))  → inj₂ (inj₁ (right (right p)))
+  (right (here p))  → inj₁ p
+  (right (right p)) → inj₂ (inj₂ p)
+
+----------------------------------------------------------------------
+-- joinʳ⁺
+
+joinʳ⁺-here⁺ : (kv : K& V) →
+               (l : Tree V l [ kv ]ᵏ hˡ) →
+               (r : Tree⁺ V [ kv ]ᵏ u hʳ) →
+               (bal : hˡ ∼ hʳ ⊔ h) →
+               P kv → Any P (proj₂ (joinʳ⁺ kv l r bal))
+joinʳ⁺-here⁺ _ _ (0# , _)                 _  p = here p
+joinʳ⁺-here⁺ _ _ (1# , _)                 ∼0 p = here p
+joinʳ⁺-here⁺ _ _ (1# , _)                 ∼- p = here p
+joinʳ⁺-here⁺ _ _ (1# , node _ _ _ ∼+)     ∼+ p = left (here p)
+joinʳ⁺-here⁺ _ _ (1# , node _ _ _ ∼0)     ∼+ p = left (here p)
+joinʳ⁺-here⁺ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ p = left (here p)
+
+joinʳ⁺-left⁺ : (kv : K& V) →
+               (l : Tree V l [ kv ]ᵏ hˡ) →
+               (r : Tree⁺ V [ kv ]ᵏ u hʳ) →
+               (bal : hˡ ∼ hʳ ⊔ h) →
+               Any P l → Any P (proj₂ (joinʳ⁺ kv l r bal))
+joinʳ⁺-left⁺ _ _ (0# , _)                 _  p = left p
+joinʳ⁺-left⁺ _ _ (1# , _)                 ∼0 p = left p
+joinʳ⁺-left⁺ _ _ (1# , _)                 ∼- p = left p
+joinʳ⁺-left⁺ _ _ (1# , node _ _ _ ∼+)     ∼+ p = left (left p)
+joinʳ⁺-left⁺ _ _ (1# , node _ _ _ ∼0)     ∼+ p = left (left p)
+joinʳ⁺-left⁺ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ p = left (left p)
+
+joinʳ⁺-right⁺ : (kv : K& V) →
+                (l : Tree V l [ kv ]ᵏ hˡ) →
+                (r@(_ , rt) : Tree⁺ V [ kv ]ᵏ u hʳ) →
+                (bal : hˡ ∼ hʳ ⊔ h) →
+                Any P rt → Any P (proj₂ (joinʳ⁺ kv l r bal))
+joinʳ⁺-right⁺ _ _ (0# , _)                 _  p                = right p
+joinʳ⁺-right⁺ _ _ (1# , _)                 ∼0 p                = right p
+joinʳ⁺-right⁺ _ _ (1# , _)                 ∼- p                = right p
+joinʳ⁺-right⁺ _ _ (1# , node _ _ _ ∼+)     ∼+ (here p)         = here p
+joinʳ⁺-right⁺ _ _ (1# , node _ _ _ ∼+)     ∼+ (left p)         = left (right p)
+joinʳ⁺-right⁺ _ _ (1# , node _ _ _ ∼+)     ∼+ (right p)        = right p
+joinʳ⁺-right⁺ _ _ (1# , node _ _ _ ∼0)     ∼+ (here p)         = here p
+joinʳ⁺-right⁺ _ _ (1# , node _ _ _ ∼0)     ∼+ (left p)         = left (right p)
+joinʳ⁺-right⁺ _ _ (1# , node _ _ _ ∼0)     ∼+ (right p)        = right p
+joinʳ⁺-right⁺ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ (here p)         = right (here p)
+joinʳ⁺-right⁺ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ (left (here p))  = here p
+joinʳ⁺-right⁺ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ (left (left p))  = left (right p)
+joinʳ⁺-right⁺ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ (left (right p)) = right (left p)
+joinʳ⁺-right⁺ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ (right p)        = right (right p)
+
+joinʳ⁺⁻ : (kv : K& V) →
+          (l : Tree V l [ kv ]ᵏ hˡ) →
+          (r@(_ , rt) : Tree⁺ V [ kv ]ᵏ u hʳ) →
+          (bal : hˡ ∼ hʳ ⊔ h) →
+          Any P (proj₂ (joinʳ⁺ kv l r bal)) →
+          P kv ⊎ Any P l ⊎ Any P rt
+joinʳ⁺⁻ _ _ (0# , _)                 _  = Any.toSum
+joinʳ⁺⁻ _ _ (1# , _)                 ∼0 = Any.toSum
+joinʳ⁺⁻ _ _ (1# , _)                 ∼- = Any.toSum
+joinʳ⁺⁻ _ _ (1# , node _ _ _ ∼+)     ∼+ = λ where
+  (left (left p))  → inj₂ (inj₁ p)
+  (left (here p))  → inj₁ p
+  (left (right p)) → inj₂ (inj₂ (left p))
+  (here p)         → inj₂ (inj₂ (here p))
+  (right p)        → inj₂ (inj₂ (right p))
+joinʳ⁺⁻ _ _ (1# , node _ _ _ ∼0)     ∼+ = λ where
+  (left (left p))  → inj₂ (inj₁ p)
+  (left (here p))  → inj₁ p
+  (left (right p)) → inj₂ (inj₂ (left p))
+  (here p)         → inj₂ (inj₂ (here p))
+  (right p)        → inj₂ (inj₂ (right p))
+joinʳ⁺⁻ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ = λ where
+  (left (left p))   → inj₂ (inj₁ p)
+  (left (here p))   → inj₁ p
+  (left (right p))  → inj₂ (inj₂ (left (left p)))
+  (here p)          → inj₂ (inj₂ (left (here p)))
+  (right (left p))  → inj₂ (inj₂ (left (right p)))
+  (right (here p))  → inj₂ (inj₂ (here p))
+  (right (right p)) → inj₂ (inj₂ (right p))
+
+----------------------------------------------------------------------
+-- joinˡ⁻
+
+joinˡ⁻-here⁺ : (kv : K& V) →
+               (l : Tree⁻ V l [ kv ]ᵏ hˡ) →
+               (r : Tree V [ kv ]ᵏ u hʳ) →
+               (bal : hˡ ∼ hʳ ⊔ h) →
+               P kv → Any P (proj₂ (joinˡ⁻ hˡ kv l r bal))
+joinˡ⁻-here⁺ {hˡ = zero}  _ (leaf⁻ _) _  _  p = here p
+joinˡ⁻-here⁺ {hˡ = suc _} _ (0# , t₁) t₃ ∼+ p =
+  joinʳ⁺-here⁺ _ t₁ (1# , t₃) ∼+ p
+joinˡ⁻-here⁺ {hˡ = suc _} _ (0# , _)  _  ∼0 p = here p
+joinˡ⁻-here⁺ {hˡ = suc _} _ (0# , _)  _  ∼- p = here p
+joinˡ⁻-here⁺ {hˡ = suc _} _ (1# , _)  _  _  p = here p
+
+joinˡ⁻-left⁺ : (kv : K& V) →
+               (l@(_ , lt) : Tree⁻ V l [ kv ]ᵏ hˡ) →
+               (r : Tree V [ kv ]ᵏ u hʳ) →
+               (bal : hˡ ∼ hʳ ⊔ h) →
+               Any P lt → Any P (proj₂ (joinˡ⁻ hˡ kv l r bal))
+joinˡ⁻-left⁺ {hˡ = zero}  _ (leaf⁻ _)  _  _  p = left p
+joinˡ⁻-left⁺ {hˡ = suc _} _ (0# , t₁)  t₃ ∼+ p =
+  joinʳ⁺-left⁺ _ t₁ (1# , t₃) ∼+ p
+joinˡ⁻-left⁺ {hˡ = suc _} _ (0# , _)   _  ∼0 p = left p
+joinˡ⁻-left⁺ {hˡ = suc _} _ (0# , _)   _  ∼- p = left p
+joinˡ⁻-left⁺ {hˡ = suc _} _ (1# , _)   _  _  p = left p
+
+joinˡ⁻-right⁺ : (kv : K& V) →
+                (l : Tree⁻ V l [ kv ]ᵏ hˡ) →
+                (r : Tree V [ kv ]ᵏ u hʳ) →
+                (bal : hˡ ∼ hʳ ⊔ h) →
+                Any P r → Any P (proj₂ (joinˡ⁻ hˡ kv l r bal))
+joinˡ⁻-right⁺ {hˡ = zero}  _ (leaf⁻ _)  _  _  p = right p
+joinˡ⁻-right⁺ {hˡ = suc _} _ (0# , t₁)  t₃ ∼+ p =
+  joinʳ⁺-right⁺ _ t₁ (1# , t₃) ∼+ p
+joinˡ⁻-right⁺ {hˡ = suc _} _ (0# , _)   _  ∼0 p = right p
+joinˡ⁻-right⁺ {hˡ = suc _} _ (0# , _)   _  ∼- p = right p
+joinˡ⁻-right⁺ {hˡ = suc _} _ (1# , _)   _  _  p = right p
+
+joinˡ⁻⁻ : (kv : K& V) →
+          (l@(_ , lt) : Tree⁻ V l [ kv ]ᵏ hˡ) →
+          (r : Tree V [ kv ]ᵏ u hʳ) →
+          (bal : hˡ ∼ hʳ ⊔ h) →
+          Any P (proj₂ (joinˡ⁻ hˡ kv l r bal)) →
+          P kv ⊎ Any P lt ⊎ Any P r
+joinˡ⁻⁻ {hˡ = zero}  _ (leaf⁻ _) _  _  = Any.toSum
+joinˡ⁻⁻ {hˡ = suc _} _ (0# , t₁) t₃ ∼+ = joinʳ⁺⁻ _ t₁ (1# , t₃) ∼+
+joinˡ⁻⁻ {hˡ = suc _} _ (0# , _)  _  ∼0 = Any.toSum
+joinˡ⁻⁻ {hˡ = suc _} _ (0# , _)  _  ∼- = Any.toSum
+joinˡ⁻⁻ {hˡ = suc _} _ (1# , _)  _  _  = Any.toSum
+
+----------------------------------------------------------------------
+-- joinʳ⁻
+
+joinʳ⁻-here⁺ : (kv : K& V) →
+               (l : Tree V l [ kv ]ᵏ hˡ) →
+               (r : Tree⁻ V [ kv ]ᵏ u hʳ) →
+               (bal : hˡ ∼ hʳ ⊔ h) →
+               P kv → Any P (proj₂ (joinʳ⁻ hʳ kv l r bal))
+joinʳ⁻-here⁺ {hʳ = zero}  _ _  (leaf⁻ _) _  p = here p
+joinʳ⁻-here⁺ {hʳ = suc _} _ t₁ (0# , t₃) ∼- p =
+  joinˡ⁺-here⁺ _ (1# , t₁) t₃ ∼- p
+joinʳ⁻-here⁺ {hʳ = suc _} _ _  (0# , _)  ∼0 p = here p
+joinʳ⁻-here⁺ {hʳ = suc _} _ _  (0# , _)  ∼+ p = here p
+joinʳ⁻-here⁺ {hʳ = suc _} _ _  (1# , _)  _  p = here p
+
+joinʳ⁻-left⁺ : (kv : K& V) →
+               (l : Tree V l [ kv ]ᵏ hˡ) →
+               (r : Tree⁻ V [ kv ]ᵏ u hʳ) →
+               (bal : hˡ ∼ hʳ ⊔ h) →
+               Any P l → Any P (proj₂ (joinʳ⁻ hʳ kv l r bal))
+joinʳ⁻-left⁺ {hʳ = zero}  _ _  (leaf⁻ _) _  p = left p
+joinʳ⁻-left⁺ {hʳ = suc _} _ t₁ (0# , t₃) ∼- p =
+  joinˡ⁺-left⁺ _ (1# , t₁) t₃ ∼- p
+joinʳ⁻-left⁺ {hʳ = suc _} _ _  (0# , _)  ∼0 p = left p
+joinʳ⁻-left⁺ {hʳ = suc _} _ _  (0# , _)  ∼+ p = left p
+joinʳ⁻-left⁺ {hʳ = suc _} _ _  (1# , _)  _  p = left p
+
+joinʳ⁻-right⁺ : (kv : K& V) →
+                (l : Tree V l [ kv ]ᵏ hˡ) →
+                (r@(_ , rt) : Tree⁻ V [ kv ]ᵏ u hʳ) →
+                (bal : hˡ ∼ hʳ ⊔ h) →
+                Any P rt → Any P (proj₂ (joinʳ⁻ hʳ kv l r bal))
+joinʳ⁻-right⁺ {hʳ = zero}  _ _  (leaf⁻ _) _  p = right p
+joinʳ⁻-right⁺ {hʳ = suc _} _ t₁ (0# , t₃) ∼- p =
+  joinˡ⁺-right⁺ _ (1# , t₁) t₃ ∼- p
+joinʳ⁻-right⁺ {hʳ = suc _} _ _  (0# , _)  ∼0 p = right p
+joinʳ⁻-right⁺ {hʳ = suc _} _ _  (0# , _)  ∼+ p = right p
+joinʳ⁻-right⁺ {hʳ = suc _} _ _  (1# , _)  _  p = right p
+
+joinʳ⁻⁻ : (kv : K& V) →
+          (l : Tree V l [ kv ]ᵏ hˡ) →
+          (r@(_ , rt) : Tree⁻ V [ kv ]ᵏ u hʳ) →
+          (bal : hˡ ∼ hʳ ⊔ h) →
+          Any P (proj₂ (joinʳ⁻ hʳ kv l r bal)) →
+          P kv ⊎ Any P l ⊎ Any P rt
+joinʳ⁻⁻ {hʳ = zero}  _ _  (leaf⁻ _) _  = Any.toSum
+joinʳ⁻⁻ {hʳ = suc _} _ t₁ (0# , t₃) ∼- = joinˡ⁺⁻ _ (1# , t₁) t₃ ∼-
+joinʳ⁻⁻ {hʳ = suc _} _ _  (0# , _)  ∼0 = Any.toSum
+joinʳ⁻⁻ {hʳ = suc _} _ _  (0# , _)  ∼+ = Any.toSum
+joinʳ⁻⁻ {hʳ = suc _} _ _  (1# , _)  _  = Any.toSum

From ea90fc2d70c71741f66462ce454e2e099ff85651 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 3 Apr 2026 12:30:06 +0100
Subject: [PATCH 29/35] refactor: to use `JoinLemmas`

---
 .../AVL/Indexed/Relation/Unary/Any/Properties/HeadTail.agda     | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/HeadTail.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/HeadTail.agda
index 4b10b2ed48..2a3916ba3a 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/HeadTail.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/HeadTail.agda
@@ -22,7 +22,7 @@ open import Relation.Unary using (Pred)
 
 open import Data.Tree.AVL.Indexed sto
 open import Data.Tree.AVL.Indexed.Relation.Unary.Any sto as Any
-open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.JoinConstFuns sto
+open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.JoinLemmas sto
   using (joinˡ⁻-here⁺; joinˡ⁻-left⁺; joinˡ⁻-right⁺; joinˡ⁻⁻)
 
 private

From 22a7dd61b47af5b5a22d683e3064bb714a26ccbe Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 3 Apr 2026 12:32:25 +0100
Subject: [PATCH 30/35] refactor: standardise bound name for a segment `l < k <
 u`

---
 .../Relation/Unary/Any/Properties/Insert.agda | 27 ++++++++++---------
 1 file changed, 14 insertions(+), 13 deletions(-)

diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Insert.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Insert.agda
index 5a71b3b5d2..404eec068f 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Insert.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Insert.agda
@@ -26,7 +26,7 @@ open import Data.Tree.AVL.Indexed sto as AVL
 open import Data.Tree.AVL.Indexed.Relation.Unary.Any sto as Any
 open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Lookup sto
   using (lookup-result; lookup-bounded; lookup-rebuild-accum)
-open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.JoinConstFuns sto
+open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.JoinLemmas sto
   using (joinˡ⁺-left⁺; joinʳ⁺-right⁺; joinˡ⁺-here⁺; joinʳ⁺-here⁺;
          joinʳ⁺-left⁺; joinˡ⁺-right⁺; joinˡ⁺⁻; joinʳ⁺⁻)
 open StrictTotalOrder sto renaming (Carrier to Key; trans to <-trans); open Eq using (sym; trans)
@@ -125,20 +125,21 @@ module _ {V : Value v} where
       [ k″ ] ≈⟨ [ sym k≈k″ ]ᴱ ⟩
       [ k  ] ∎
 
-  module _ (k : Key) (v : Val k) (t : Tree V l u n) (seg : l < k < u) where
+  module _ (k : Key) (v : Val k) (t : Tree V l u n) (l<k<u : l < k < u) where
 
-    insert-nothing : P (k , v) → ¬ (Any ((k ≈_) ∘′ key) t) → Any P (proj₂ (insert k v t seg))
-    insert-nothing = insertWith-nothing k (F.const v) t seg
+    insert-nothing : P (k , v) → ¬ (Any ((k ≈_) ∘′ key) t) →
+                     Any P (proj₂ (insert k v t l<k<u))
+    insert-nothing = insertWith-nothing k (F.const v) t l<k<u
 
     insert-just : (pr : ∀ k′ → (eq : k ≈ k′) → P (k′ , Val≈ eq v)) →
-                      Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insert k v t seg))
-    insert-just pr = insertWith-just k (F.const v) t seg (λ k′ _ eq → pr k′ eq)
+                  Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insert k v t l<k<u))
+    insert-just pr = insertWith-just k (F.const v) t l<k<u (λ k′ _ eq → pr k′ eq)
 
   module _ (k : Key) (f : Maybe (Val k) → Val k) where
 
-    insertWith⁺ : (t : Tree V l u n) (seg : l < k < u) →
+    insertWith⁺ : (t : Tree V l u n) (l<k<u : l < k < u) →
                   (p : Any P t) → k ≉ lookupKey p →
-                  Any P (proj₂ (insertWith k f t seg))
+                  Any P (proj₂ (insertWith k f t l<k<u))
     insertWith⁺ (node kv@(k′ , v′) l r bal) (l<k , k<u) (here p) k≉
       with compare k k′
     ... | tri< k<k′ _ _ = let l′ = insertWith k f l (l<k , [ k<k′ ]ᴿ)
@@ -163,9 +164,9 @@ module _ {V : Value v} where
                               ih = insertWith⁺ r ([ k′<k ]ᴿ , k<u) p k≉
                           in joinʳ⁺-right⁺ kv l r′ bal ih
 
-  insert⁺ : (k : Key) (v : Val k) (t : Tree V l u n) (seg : l < k < u) →
+  insert⁺ : (k : Key) (v : Val k) (t : Tree V l u n) (l<k<u : l < k < u) →
             (p : Any P t) → k ≉ lookupKey p →
-            Any P (proj₂ (insert k v t seg))
+            Any P (proj₂ (insert k v t l<k<u))
   insert⁺ k v = insertWith⁺ k (F.const v)
 
   module _
@@ -174,10 +175,10 @@ module _ {V : Value v} where
     (k : Key) (v : Val k)
     where
 
-    insert⁻ : (t : Tree V l u n) (seg : l < k < u) →
-              Any P (proj₂ (insert k v t seg)) →
+    insert⁻ : (t : Tree V l u n) (l<k<u : l < k < u) →
+              Any P (proj₂ (insert k v t l<k<u)) →
               P (k , v) ⊎ Any (λ{ (k′ , v′) → k ≉ k′ × P (k′ , v′)}) t
-    insert⁻ (leaf l<u) seg (here p) = inj₁ p
+    insert⁻ (leaf l<u) l<k<u (here p) = inj₁ p
     insert⁻ (node kv′@(k′ , v′) l r bal) (l<k , k<u) p with compare k k′
     insert⁻ (node kv′@(k′ , v′) l r bal) (l<k , k<u) p | tri< k<k′ k≉k′ _
         with joinˡ⁺⁻ kv′ (insert k v l (l<k , [ k<k′ ]ᴿ)) r bal p

From eeaa888d18ba476171b43004212ad515d0e3999b Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 3 Apr 2026 12:48:03 +0100
Subject: [PATCH 31/35] refactor: standardise notation

---
 .../Relation/Unary/Any/Properties/Insert.agda | 31 +++++++++----------
 1 file changed, 15 insertions(+), 16 deletions(-)

diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Insert.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Insert.agda
index 404eec068f..f438d95c8f 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Insert.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Insert.agda
@@ -29,7 +29,10 @@ open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Lookup sto
 open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.JoinLemmas sto
   using (joinˡ⁺-left⁺; joinʳ⁺-right⁺; joinˡ⁺-here⁺; joinʳ⁺-here⁺;
          joinʳ⁺-left⁺; joinˡ⁺-right⁺; joinˡ⁺⁻; joinʳ⁺⁻)
-open StrictTotalOrder sto renaming (Carrier to Key; trans to <-trans); open Eq using (sym; trans)
+open StrictTotalOrder sto
+  using (_<_; _≈_; module Eq; compare; irrefl)
+  renaming (Carrier to Key; trans to <-trans)
+open Eq using (_≉_; sym; trans)
 
 open import Relation.Binary.Construct.Add.Extrema.Strict _<_ using ([<]-injective)
 
@@ -41,20 +44,16 @@ private
     v p : Level
     V : Value v
     l u : Key⁺
-    n : ℕ
+    h : ℕ
     P : Pred (K& V) p
 
-module _ {V : Value v} where
-
-  private
-    Val  = Value.family V
-    Val≈ = Value.respects V
+module _ {V : Value v} (open Value V using (respects) renaming (family to Val)) where
 
   module _ (k : Key) (f : Maybe (Val k) → Val k) where
 
     open <-Reasoning AVL.strictPartialOrder
 
-    insertWith-nothing : (t : Tree V l u n) (seg : l < k < u) →
+    insertWith-nothing : (t : Tree V l u h) (seg : l < k < u) →
                          P (k , f nothing) →
                          ¬ (Any ((k ≈_) ∘′ key) t) →
                          Any P (proj₂ (insertWith k f t seg))
@@ -73,8 +72,8 @@ module _ {V : Value v} where
       ku′  = insertWith k f ku seg′
       ih   = insertWith-nothing ku seg′ pr (λ p → ¬p (right p))
 
-    insertWith-just : (t : Tree V l u n) (seg : l < k < u) →
-                      (pr : ∀ k′ v → (eq : k ≈ k′) → P (k′ , Val≈ eq (f (just (Val≈ (sym eq) v))))) →
+    insertWith-just : (t : Tree V l u h) (seg : l < k < u) →
+                      (pr : ∀ k′ v → (eq : k ≈ k′) → P (k′ , respects eq (f (just (respects (sym eq) v))))) →
                       Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insertWith k f t seg))
     insertWith-just (node kv@(k′ , v) lk ku bal) (l<k , k<u) pr p
       with p | compare k k′
@@ -125,19 +124,19 @@ module _ {V : Value v} where
       [ k″ ] ≈⟨ [ sym k≈k″ ]ᴱ ⟩
       [ k  ] ∎
 
-  module _ (k : Key) (v : Val k) (t : Tree V l u n) (l<k<u : l < k < u) where
+  module _ (k : Key) (v : Val k) (t : Tree V l u h) (l<k<u : l < k < u) where
 
     insert-nothing : P (k , v) → ¬ (Any ((k ≈_) ∘′ key) t) →
                      Any P (proj₂ (insert k v t l<k<u))
     insert-nothing = insertWith-nothing k (F.const v) t l<k<u
 
-    insert-just : (pr : ∀ k′ → (eq : k ≈ k′) → P (k′ , Val≈ eq v)) →
+    insert-just : (pr : ∀ k′ → (eq : k ≈ k′) → P (k′ , respects eq v)) →
                   Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insert k v t l<k<u))
     insert-just pr = insertWith-just k (F.const v) t l<k<u (λ k′ _ eq → pr k′ eq)
 
   module _ (k : Key) (f : Maybe (Val k) → Val k) where
 
-    insertWith⁺ : (t : Tree V l u n) (l<k<u : l < k < u) →
+    insertWith⁺ : (t : Tree V l u h) (l<k<u : l < k < u) →
                   (p : Any P t) → k ≉ lookupKey p →
                   Any P (proj₂ (insertWith k f t l<k<u))
     insertWith⁺ (node kv@(k′ , v′) l r bal) (l<k , k<u) (here p) k≉
@@ -164,18 +163,18 @@ module _ {V : Value v} where
                               ih = insertWith⁺ r ([ k′<k ]ᴿ , k<u) p k≉
                           in joinʳ⁺-right⁺ kv l r′ bal ih
 
-  insert⁺ : (k : Key) (v : Val k) (t : Tree V l u n) (l<k<u : l < k < u) →
+  insert⁺ : (k : Key) (v : Val k) (t : Tree V l u h) (l<k<u : l < k < u) →
             (p : Any P t) → k ≉ lookupKey p →
             Any P (proj₂ (insert k v t l<k<u))
   insert⁺ k v = insertWith⁺ k (F.const v)
 
   module _
     {P : Pred (K& V) p}
-    (P-Resp : ∀ {k k′ v} → (k≈k′ : k ≈ k′) → P (k′ , Val≈ k≈k′ v) → P (k , v))
+    (P-Resp : ∀ {k k′ v} → (k≈k′ : k ≈ k′) → P (k′ , respects k≈k′ v) → P (k , v))
     (k : Key) (v : Val k)
     where
 
-    insert⁻ : (t : Tree V l u n) (l<k<u : l < k < u) →
+    insert⁻ : (t : Tree V l u h) (l<k<u : l < k < u) →
               Any P (proj₂ (insert k v t l<k<u)) →
               P (k , v) ⊎ Any (λ{ (k′ , v′) → k ≉ k′ × P (k′ , v′)}) t
     insert⁻ (leaf l<u) l<k<u (here p) = inj₁ p

From 2dee0d19802e525613ff14277edd2f9c19c45ca8 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 3 Apr 2026 12:50:16 +0100
Subject: [PATCH 32/35] refactor: use `variable`s

---
 .../AVL/Indexed/Relation/Unary/Any/Properties/Cast.agda  | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Cast.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Cast.agda
index 7bba3f78a3..e89ef14b37 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Cast.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Cast.agda
@@ -26,16 +26,15 @@ private
     P : Pred (K& V) p
     l m u : Key⁺
     h : ℕ
+    lm : Tree V l m h
+    m<u : m <⁺ u
 
-
-castʳ⁺ : ∀ {lm : Tree V l m h} {m<u : m <⁺ u} →
-         Any P lm → Any P (castʳ lm m<u)
+castʳ⁺ : Any P lm → Any P (castʳ lm m<u)
 castʳ⁺ (here p)  = here p
 castʳ⁺ (left p)  = left p
 castʳ⁺ (right p) = right (castʳ⁺ p)
 
-castʳ⁻ : ∀ {lm : Tree V l m h} {m<u : m <⁺ u} →
-         Any P (castʳ lm m<u) → Any P lm
+castʳ⁻ : Any P (castʳ lm m<u) → Any P lm
 castʳ⁻ {lm = node _ _ _ _} (here p)  = here p
 castʳ⁻ {lm = node _ _ _ _} (left p)  = left p
 castʳ⁻ {lm = node _ _ _ _} (right p) = right (castʳ⁻ p)

From 8a5f62a052e62a84ec103df62db3da62418584e3 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 3 Apr 2026 12:58:46 +0100
Subject: [PATCH 33/35] refactor: use freshness predicate

---
 .../Relation/Unary/Any/Properties/Delete.agda | 48 ++++++++++---------
 1 file changed, 26 insertions(+), 22 deletions(-)

diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Delete.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Delete.agda
index 4a27c96dfc..4ebb38b7e9 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Delete.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Delete.agda
@@ -27,10 +27,13 @@ open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Lookup sto
   using (lookup-bounded; lookup-result; lookup-rebuild)
 open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Join sto
   using (join-left⁺; join-right⁺; join⁻)
-open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.JoinConstFuns sto
+open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.JoinLemmas sto
   using (joinʳ⁻-here⁺; joinʳ⁻-left⁺; joinʳ⁻-right⁺; joinˡ⁻-here⁺;
          joinˡ⁻-left⁺; joinˡ⁻-right⁺; joinʳ⁻⁻; joinˡ⁻⁻)
-open StrictTotalOrder sto renaming (Carrier to Key; trans to <-trans); open Eq using (sym; trans)
+open StrictTotalOrder sto
+  using (_<_; _≈_; module Eq; compare)
+  renaming (Carrier to Key; trans to <-trans)
+open Eq using (_≉_; sym; trans)
 
 open import Relation.Binary.Construct.Add.Extrema.Strict _<_ using ([<]-injective)
 
@@ -44,10 +47,11 @@ private
     h : ℕ
     P : Pred (K& V) p
 
+
 module _ (k : Key) where
 
   delete⁺ : (t : Tree V l u h) (seg : l < k < u) →
-            (p : Any P t) → lookupKey p ≉ k →
+            (p : Any P t) → k # p →
             Any P (proj₂ (delete k t seg))
   delete⁺ (node (k′ , _) _ _ bal) _ (here pk) p≉k
     with compare k′ k
@@ -100,11 +104,11 @@ module _ (k : Key) where
     with joinʳ⁻⁻ _ _ _ bal p
   ... | inj₁ kp≈k′     = contradiction (trans (sym kp≈k′) kp≈k) k′≉k
   ... | inj₂ (inj₁ pl) = begin-contradiction
-    [ k  ]                ≈⟨ [ sym kp≈k ]ᴱ ⟩
-    [ kp ]                ≈⟨ [ lookup-result pl ]ᴱ ⟩
-    [ Any.lookupKey pl ]  <⟨ proj₂ (lookup-bounded pl) ⟩
-    [ k′ ]                <⟨ [ k′<k ]ᴿ ⟩
-    [ k  ]                ∎
+    [ k  ]            ≈⟨ [ kp≈k ]ᴱ ⟨
+    [ kp ]            ≈⟨ [ lookup-result pl ]ᴱ ⟩
+    [ lookupKey pl ]  <⟨ proj₂ (lookup-bounded pl) ⟩
+    [ k′ ]            <⟨ [ k′<k ]ᴿ ⟩
+    [ k  ]            ∎
   ... | inj₂ (inj₂ pr) = delete-key-∈⁻ k′u ([ k′<k ]ᴿ , k<u) pr kp≈k
   delete-key-∈⁻ (node (k′ , _) lk′ _ bal) (l<k , _) {kp} p kp≈k
     | tri> _ k′≉k k′>k
@@ -112,27 +116,27 @@ module _ (k : Key) where
   ... | inj₁ kp≈k′     = contradiction (trans (sym kp≈k′) kp≈k) k′≉k
   ... | inj₂ (inj₁ pl) = delete-key-∈⁻ lk′ (l<k , [ k′>k ]ᴿ) pl kp≈k
   ... | inj₂ (inj₂ pr) = begin-contradiction
-    [ k  ]                <⟨ [ k′>k ]ᴿ ⟩
-    [ k′ ]                <⟨ proj₁ (lookup-bounded pr) ⟩
-    [ Any.lookupKey pr ]  ≈⟨ [ sym (lookup-result pr) ]ᴱ ⟩
-    [ kp ]                ≈⟨ [ kp≈k ]ᴱ ⟩
-    [ k  ]                ∎
+    [ k  ]            <⟨ [ k′>k ]ᴿ ⟩
+    [ k′ ]            <⟨ proj₁ (lookup-bounded pr) ⟩
+    [ lookupKey pr ]  ≈⟨ [ lookup-result pr ]ᴱ ⟨
+    [ kp ]            ≈⟨ [ kp≈k ]ᴱ ⟩
+    [ k  ]            ∎
   delete-key-∈⁻ (node (k′ , _) _ k′u bal) _ {kp} p kp≈k
     | tri≈ k′≮k _ k′≯k
     with join⁻ _ k′u bal p
   ... | inj₁ p₁ = contradiction
     (begin-strict
-      [ k  ]                ≈⟨ [ sym kp≈k ]ᴱ ⟩
-      [ kp ]                ≈⟨ [ lookup-result p₁ ]ᴱ ⟩
-      [ Any.lookupKey p₁ ]  <⟨ proj₂ (lookup-bounded p₁) ⟩
-      [ k′ ]                ∎)
+      [ k  ]            ≈⟨ [ kp≈k ]ᴱ ⟨
+      [ kp ]            ≈⟨ [ lookup-result p₁ ]ᴱ ⟩
+      [ lookupKey p₁ ]  <⟨ proj₂ (lookup-bounded p₁) ⟩
+      [ k′ ]            ∎)
     (k′≯k ∘′ [<]-injective)
   ... | inj₂ p₂ = contradiction
     (begin-strict
-      [ k′  ]               <⟨ proj₁ (lookup-bounded p₂) ⟩
-      [ Any.lookupKey p₂ ]  ≈⟨ [ sym (lookup-result p₂) ]ᴱ ⟩
-      [ kp ]                ≈⟨ [ kp≈k ]ᴱ ⟩
-      [ k ]                 ∎)
+      [ k′  ]           <⟨ proj₁ (lookup-bounded p₂) ⟩
+      [ lookupKey p₂ ]  ≈⟨ [ lookup-result p₂ ]ᴱ ⟨
+      [ kp ]            ≈⟨ [ kp≈k ]ᴱ ⟩
+      [ k ]             ∎)
     (k′≮k ∘′ [<]-injective)
 
 
@@ -140,6 +144,6 @@ module _ (k : Key) where
 
   delete-key⁻ : (t : Tree V l u h) (seg : l < k < u) →
                 (p : Any P (proj₂ (delete k t seg))) →
-                lookupKey p ≉ k
+                k # p
   delete-key⁻ t seg p kp≈k =
     delete-key-∈⁻ k t seg (lookup-rebuild p Eq.refl) kp≈k

From 28730ef0c3a43646f45be4565fce94e739c84f1f Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 3 Apr 2026 13:35:41 +0100
Subject: [PATCH 34/35] refactor: cosmetic tweaks

---
 src/Data/Tree/AVL/Indexed.agda                | 10 ++---
 .../Relation/Unary/Any/Properties/Insert.agda | 37 ++++++++++---------
 2 files changed, 24 insertions(+), 23 deletions(-)

diff --git a/src/Data/Tree/AVL/Indexed.agda b/src/Data/Tree/AVL/Indexed.agda
index fac711cbec..be14eb2bc5 100644
--- a/src/Data/Tree/AVL/Indexed.agda
+++ b/src/Data/Tree/AVL/Indexed.agda
@@ -233,7 +233,7 @@ module _ {V : Value v} (open Value V using (respects) renaming (family to Val))
 
   insertWith : ∀ k → (Maybe (Val k) → Val k) →  -- Maybe old → result.
                Tree V l u h → l < k < u → Tree⁺ V l u h
-  insertWith k f (leaf l<u) l<k<u = 1# , singleton k (f nothing) l<k<u
+  insertWith k f (leaf _) l<k<u = 1# , singleton k (f nothing) l<k<u
   insertWith k f (node kv@(k′ , v) lk ku bal) (l<k , k<u) with compare k k′
   ... | tri< k<k′ _ _ = joinˡ⁺ kv (insertWith k f lk (l<k , [ k<k′ ]ᴿ)) ku bal
   ... | tri> _ _ k′<k = joinʳ⁺ kv lk (insertWith k f ku ([ k′<k ]ᴿ , k<u)) bal
@@ -252,21 +252,21 @@ module _ {V : Value v} (open Value V using (respects) renaming (family to Val))
   -- comparisons).
 
   delete : ∀ k → Tree V l u h → l < k < u → Tree⁻ V l u h
-  delete k (leaf l<u) l<k<u = 0# , leaf l<u
+  delete k t@(leaf _) _ = 0# , t
   delete k (node kv@(k′ , v) lk ku bal) (l<k , k<u) with compare k′ k
   ... | tri< k′<k _ _ = joinʳ⁻ _ kv lk (delete k ku ([ k′<k ]ᴿ , k<u)) bal
   ... | tri> _ _ k′>k = joinˡ⁻ _ kv (delete k lk (l<k , [ k′>k ]ᴿ)) ku bal
-  ... | tri≈ _ k′≡k _ = join lk ku bal
+  ... | tri≈ _ k′≈k _ = join lk ku bal
 
   -- Looks up a key. Logarithmic in the size of the tree (assuming
   -- constant-time comparisons).
 
   lookup : Tree V l u h → ∀ k → l < k < u → Maybe (Val k)
-  lookup (leaf _)                  k l<k<u       = nothing
+  lookup (leaf _)                _ _           = nothing
   lookup (node (k′ , v) lk ku _) k (l<k , k<u) with compare k′ k
   ... | tri< k′<k _ _ = lookup ku k ([ k′<k ]ᴿ , k<u)
   ... | tri> _ _ k′>k = lookup lk k (l<k , [ k′>k ]ᴿ)
-  ... | tri≈ _ k′≡k _ = just (respects k′≡k v)
+  ... | tri≈ _ k′≈k _ = just (respects k′≈k v)
 
   -- Converts the tree to an ordered list. Linear in the size of the
   -- tree.
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Insert.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Insert.agda
index f438d95c8f..6a3608d7b3 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Insert.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/Insert.agda
@@ -47,48 +47,49 @@ private
     h : ℕ
     P : Pred (K& V) p
 
+
 module _ {V : Value v} (open Value V using (respects) renaming (family to Val)) where
 
   module _ (k : Key) (f : Maybe (Val k) → Val k) where
 
     open <-Reasoning AVL.strictPartialOrder
 
-    insertWith-nothing : (t : Tree V l u h) (seg : l < k < u) →
+    insertWith-nothing : (t : Tree V l u h) (l<k<u : l < k < u) →
                          P (k , f nothing) →
                          ¬ (Any ((k ≈_) ∘′ key) t) →
-                         Any P (proj₂ (insertWith k f t seg))
-    insertWith-nothing (leaf l<u)                   seg         pr ¬p = here pr
+                         Any P (proj₂ (insertWith k f t l<k<u))
+    insertWith-nothing (leaf l<u)                   l<k<u         pr ¬p = here pr
     insertWith-nothing (node kv@(k′ , v) lk ku bal) (l<k , k<u) pr ¬p
       with compare k k′
     ... | tri≈ _ k≈k′ _ = contradiction (here k≈k′) ¬p
     ... | tri< k<k′ _ _ = joinˡ⁺-left⁺ kv lk′ ku bal ih
       where
-      seg′ = l<k , [ k<k′ ]ᴿ
-      lk′  = insertWith k f lk seg′
-      ih   = insertWith-nothing lk seg′ pr (λ p → ¬p (left p))
+      l<k<u′ = l<k , [ k<k′ ]ᴿ
+      lk′  = insertWith k f lk l<k<u′
+      ih   = insertWith-nothing lk l<k<u′ pr (λ p → ¬p (left p))
     ... | tri> _ _ k>k′ = joinʳ⁺-right⁺ kv lk ku′ bal ih
       where
-      seg′ = [ k>k′ ]ᴿ , k<u
-      ku′  = insertWith k f ku seg′
-      ih   = insertWith-nothing ku seg′ pr (λ p → ¬p (right p))
+      l<k<u′ = [ k>k′ ]ᴿ , k<u
+      ku′  = insertWith k f ku l<k<u′
+      ih   = insertWith-nothing ku l<k<u′ pr (λ p → ¬p (right p))
 
-    insertWith-just : (t : Tree V l u h) (seg : l < k < u) →
+    insertWith-just : (t : Tree V l u h) (l<k<u : l < k < u) →
                       (pr : ∀ k′ v → (eq : k ≈ k′) → P (k′ , respects eq (f (just (respects (sym eq) v))))) →
-                      Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insertWith k f t seg))
+                      Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insertWith k f t l<k<u))
     insertWith-just (node kv@(k′ , v) lk ku bal) (l<k , k<u) pr p
       with p | compare k k′
     -- happy paths
     ... | here _   | tri≈ _ k≈k′ _ = here (pr k′ v k≈k′)
     ... | left lp  | tri< k<k′ _ _ =
-      joinˡ⁺-left⁺ kv lk′ ku bal (insertWith-just lk seg′ pr lp)
+      joinˡ⁺-left⁺ kv lk′ ku bal (insertWith-just lk l<k<u′ pr lp)
       where
-      seg′ = l<k , [ k<k′ ]ᴿ
-      lk′  = insertWith k f lk seg′
+      l<k<u′ = l<k , [ k<k′ ]ᴿ
+      lk′  = insertWith k f lk l<k<u′
     ... | right rp | tri> _ _ k>k′ =
-      joinʳ⁺-right⁺ kv lk ku′ bal (insertWith-just ku seg′ pr rp)
+      joinʳ⁺-right⁺ kv lk ku′ bal (insertWith-just ku l<k<u′ pr rp)
       where
-      seg′ = [ k>k′ ]ᴿ , k<u
-      ku′  = insertWith k f ku seg′
+      l<k<u′ = [ k>k′ ]ᴿ , k<u
+      ku′  = insertWith k f ku l<k<u′
 
     -- impossible cases
     ... | here eq  | tri< k<k′ _ _ = begin-contradiction
@@ -132,7 +133,7 @@ module _ {V : Value v} (open Value V using (respects) renaming (family to Val))
 
     insert-just : (pr : ∀ k′ → (eq : k ≈ k′) → P (k′ , respects eq v)) →
                   Any ((k ≈_) ∘′ key) t → Any P (proj₂ (insert k v t l<k<u))
-    insert-just pr = insertWith-just k (F.const v) t l<k<u (λ k′ _ eq → pr k′ eq)
+    insert-just pr = insertWith-just k (F.const v) t l<k<u (λ k′ _ → pr k′)
 
   module _ (k : Key) (f : Maybe (Val k) → Val k) where
 

From 966166e222cc2fc5ada42185dec39c4448367ab6 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 3 Apr 2026 13:41:19 +0100
Subject: [PATCH 35/35] fix: `import`s in `Properties`

---
 src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
index da997648cc..4f6abf38c6 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
@@ -12,12 +12,11 @@ module Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties
   {a ℓ₁ ℓ₂} (sto : StrictTotalOrder a ℓ₁ ℓ₂)
   where
 
-open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Lookup sto public
 open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Cast sto public
 open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Delete sto public
 open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.HeadTail sto public
 open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Insert sto public
-open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.JoinConstFuns sto public
+open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.JoinLemmas sto public
 open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Join sto public
-open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.LookupFun sto public
+open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Lookup sto public
 open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Singleton sto public