diff --git a/CHANGELOG.md b/CHANGELOG.md
index b32fa73de5..9f69962d0e 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`.
 
@@ -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
@@ -183,9 +191,8 @@ 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.JoinLemmas
   Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Singleton
   ```
 
@@ -415,6 +422,27 @@ 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.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)
@@ -450,47 +478,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.JoinLemmas`:
   ```
   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/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
diff --git a/src/Data/Tree/AVL/Indexed.agda b/src/Data/Tree/AVL/Indexed.agda
index 94d1b0782b..be14eb2bc5 100644
--- a/src/Data/Tree/AVL/Indexed.agda
+++ b/src/Data/Tree/AVL/Indexed.agda
@@ -13,21 +13,17 @@ 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 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)
+open StrictTotalOrder strictTotalOrder
+  using (module Eq; compare) renaming (Carrier to Key)
 
 ------------------------------------------------------------------------
 -- Re-export core definitions publicly
@@ -37,33 +33,76 @@ 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 ℓ
+    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.
 --
 -- (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) →
          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
 
-  ordered : ∀ {l u n} → Tree V l u n → l <⁺ u
+------------------------------------------------------------------------
+-- 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 : Tree V l u h → 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
 
-  leaf-injective : ∀ {l u} {p q : l <⁺ u} → (Tree V l u 0 ∋ leaf p) ≡ leaf q → p ≡ q
+  -- 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)
+    tree⁻0 t⁻@(leaf⁻ _) = _ , _ , refl , refl
+
+  -- Injectivity of constructors
+
+  leaf-injective : ∀ {p q : l <⁺ u} → (Tree V l u 0 ∋ leaf p) ≡ leaf q → p ≡ q
   leaf-injective refl = refl
 
   node-injective-key :
@@ -77,6 +116,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 → 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,191 +139,148 @@ 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 → (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<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 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
 
   -- 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 _)                _ _           = 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
 
-  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 t = toDiffList t List.[]
+  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
-
-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
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
index c81599da2a..3a66341576 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,11 @@ 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 +44,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 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ʳ}
           {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 →
@@ -78,14 +80,23 @@ lookup (right p)          = lookup p
 lookupKey : Any P t → Key
 lookupKey = key ∘′ lookup
 
--- If any element satisfies P, then P is satisfied.
+-- 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 → ∃ 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 +115,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
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
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..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
@@ -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,15 +24,17 @@ private
     v p : Level
     V : Value v
     P : Pred (K& V) p
+    l m u : Key⁺
+    h : ℕ
+    lm : Tree V l m h
+    m<u : m <⁺ u
 
-castʳ⁺ : ∀ {l m u h} {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ʳ⁻ : ∀ {l m u h} {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)
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..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))) →
-                Any.lookupKey p ≉ k
+                k # p
   delete-key⁻ t seg p kp≈k =
     delete-key-∈⁻ k t seg (lookup-rebuild p Eq.refl) kp≈k
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..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
@@ -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)
@@ -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
@@ -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
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..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
@@ -26,10 +26,13 @@ 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)
+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,54 +44,52 @@ 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
 
-    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 h) (l<k<u : l < k < u) →
+                         P (k , f nothing) →
+                         ¬ (Any ((k ≈_) ∘′ key) t) →
+                         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   = Any-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   = Any-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
+      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) (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 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 (Any-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 (Any-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
@@ -124,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 h) (l<k<u : 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 l<k<u))
+    insert-nothing = insertWith-nothing k (F.const v) t l<k<u
 
-    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′ , 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′ _ → pr k′)
 
   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 →
-                  Any P (proj₂ (insertWith k f t seg))
+    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≉
       with compare k k′
     ... | tri< k<k′ _ _ = let l′ = insertWith k f l (l<k , [ k<k′ ]ᴿ)
@@ -162,21 +164,21 @@ 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) →
-            (p : Any P t) → k ≉ Any.lookupKey p →
-            Any P (proj₂ (insert k v t seg))
+  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) (seg : l < k < u) →
-              Any P (proj₂ (insert k v t seg)) →
+    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) 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
@@ -205,3 +207,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."
+#-}
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..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
@@ -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,14 +20,13 @@ 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⁻)
+open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.JoinLemmas sto
+  using (joinʳ⁻-left⁺; joinʳ⁻-here⁺; joinʳ⁻-right⁺; joinʳ⁻⁻)
+
 
 private
   variable
@@ -37,33 +36,32 @@ private
     l m u : Key⁺
     hˡ hʳ h : ℕ
 
-module _ {V : Value v} where
 
-  join-left⁺ : (t₁ : Tree V l m hˡ) (t₂ : Tree V m 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)
+----------------------------------------------------------------------
+-- 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 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-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 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)
+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/JoinLemmas.agda
similarity index 62%
rename from src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/JoinConstFuns.agda
rename to src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/JoinLemmas.agda
index 079c16ee0b..935e555b66 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/JoinConstFuns.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/JoinLemmas.agda
@@ -8,7 +8,7 @@
 
 open import Relation.Binary.Bundles using (StrictTotalOrder)
 
-module Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.JoinConstFuns
+module Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.JoinLemmas
   {a ℓ₁ ℓ₂} (sto : StrictTotalOrder a ℓ₁ ℓ₂)
   where
 
@@ -29,12 +29,16 @@ private
     l u : Key⁺
     hˡ hʳ h : ℕ
 
+  [_]ᵏ : K& V → Key⁺
+  [ kv ]ᵏ = [ kv .key ]
+
+
 ----------------------------------------------------------------------
 -- joinˡ⁺
 
 joinˡ⁺-here⁺ : (kv : K& V) →
-               (l : ∃ λ i → Tree V l [ kv .key ] (i ⊕ hˡ)) →
-               (r : Tree V [ kv .key ] u hʳ) →
+               (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
@@ -44,11 +48,11 @@ 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ʳ) →
+joinˡ⁺-left⁺ : (kv : K& V) →
+               (l@(_ , lt) : Tree⁺ V l [ kv ]ᵏ hˡ) →
+               (r : Tree V [ kv ]ᵏ u hʳ) →
                (bal : hˡ ∼ hʳ ⊔ h) →
-               Any P (proj₂ l) → Any P (proj₂ (joinˡ⁺ k l r bal))
+               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
@@ -64,9 +68,9 @@ 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ʳ) →
+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
@@ -76,12 +80,12 @@ 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ʳ) →
+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 (proj₂ l) ⊎ Any P r
+          P kv ⊎ Any P lt ⊎ Any P r
 joinˡ⁺⁻ _ (0# , _)                 _ _  = Any.toSum
 joinˡ⁺⁻ _ (1# , _)                 _ ∼0 = Any.toSum
 joinˡ⁺⁻ _ (1# , _)                 _ ∼+ = Any.toSum
@@ -110,8 +114,8 @@ joinˡ⁺⁻ _ (1# , node⁺ _ _ _ _ _ _) _ ∼- = λ where
 -- joinʳ⁺
 
 joinʳ⁺-here⁺ : (kv : K& V) →
-               (l : Tree V l [ kv .key ] hˡ) →
-               (r : ∃ λ i → Tree V [ kv .key ] u (i ⊕ hʳ)) →
+               (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
@@ -122,8 +126,8 @@ 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ʳ)) →
+               (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
@@ -134,10 +138,10 @@ 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ʳ)) →
+                (l : Tree V l [ kv ]ᵏ hˡ) →
+                (r@(_ , rt) : Tree⁺ V [ kv ]ᵏ u hʳ) →
                 (bal : hˡ ∼ hʳ ⊔ h) →
-                Any P (proj₂ r) → Any P (proj₂ (joinʳ⁺ kv l r bal))
+                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
@@ -154,11 +158,11 @@ joinʳ⁺-right⁺ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ (left (right p)) = right
 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ʳ)) →
+          (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 (proj₂ r)
+          P kv ⊎ Any P l ⊎ Any P rt
 joinʳ⁺⁻ _ _ (0# , _)                 _  = Any.toSum
 joinʳ⁺⁻ _ _ (1# , _)                 ∼0 = Any.toSum
 joinʳ⁺⁻ _ _ (1# , _)                 ∼- = Any.toSum
@@ -187,108 +191,100 @@ joinʳ⁺⁻ _ _ (1# , node⁻ _ _ _ _ _ _) ∼+ = λ where
 -- joinˡ⁻
 
 joinˡ⁻-here⁺ : (kv : K& V) →
-               (l : ∃ λ i → Tree V l [ kv .key ] pred[ i ⊕ hˡ ]) →
-               (r : Tree V [ kv .key ] u hʳ) →
+               (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}  _ (0# , leaf _) _  _  p = here p
-joinˡ⁻-here⁺ {hˡ = zero}  _ (1# , leaf _) _  _  p = here p
-joinˡ⁻-here⁺ {hˡ = suc _} _ (0# , t₁)     t₃ ∼+ p =
+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ˡ⁻-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ʳ) →
+               (l@(_ , lt) : 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}  _ (0# , leaf _)  _  _  p = left p
-joinˡ⁻-left⁺ {hˡ = zero}  _ (1# , leaf _)  _  _  p = left p
-joinˡ⁻-left⁺ {hˡ = suc _} _ (0# , t₁)      t₃ ∼+ p =
+               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ˡ⁻-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ʳ) →
+                (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}  _ (0# , leaf _)  _  _  p = right p
-joinˡ⁻-right⁺ {hˡ = zero}  _ (1# , leaf _)  _  _  p = right p
-joinˡ⁻-right⁺ {hˡ = suc _} _ (0# , t₁)      t₃ ∼+ p =
+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ˡ⁻-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ʳ) →
+          (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 (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
+          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 .key ] hˡ) →
-               (r : ∃ λ i → Tree V [ kv .key ] u pred[ i ⊕ hʳ ]) →
+               (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}  _ _  (0# , leaf _) _  p = here p
-joinʳ⁻-here⁺ {hʳ = zero}  _ _  (1# , leaf _) _  p = here p
-joinʳ⁻-here⁺ {hʳ = suc _} _ t₁ (0# , t₃)     ∼- p =
+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ʳ⁻-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ʳ ]) →
+               (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}  _ _  (0# , leaf _) _  p = left p
-joinʳ⁻-left⁺ {hʳ = zero}  _ _  (1# , leaf _) _  p = left p
-joinʳ⁻-left⁺ {hʳ = suc _} _ t₁ (0# , t₃)     ∼- p =
+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ʳ⁻-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ʳ ]) →
+                (l : Tree V l [ kv ]ᵏ hˡ) →
+                (r@(_ , rt) : 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}  _ _  (0# , leaf _) _  p = right p
-joinʳ⁻-right⁺ {hʳ = zero}  _ _  (1# , leaf _) _  p = right p
-joinʳ⁻-right⁺ {hʳ = suc _} _ t₁ (0# , t₃)     ∼- p =
+                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ʳ⁻-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ʳ ]) →
+          (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 (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
+          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
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..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
@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Properties related to Any.lookup
+-- Properties of lookup related to Any
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
@@ -12,39 +12,91 @@ 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
     v p : Level
     V : Value v
     l u : Key⁺
-    n : ℕ
+    h : ℕ
     P Q : Pred (K& V) p
+    t : Tree V l u h
+
+
+
+----------------------------------------------------------------------
+-- lookup
 
-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 {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 : (p : Any P {l = l} {u = u} t) → l < lookupKey p < u
+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 : {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)
+
+
+----------------------------------------------------------------------
+-- 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) (l<k<u : l < k < u) →
+            (p : Any P t) →
+            k # 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
+  ... | 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 38747f6713..0000000000
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/LookupFun.agda
+++ /dev/null
@@ -1,75 +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 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
-
-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
-
-  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))))
-  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 → Val≈ 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/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
diff --git a/src/Data/Tree/AVL/Value.agda b/src/Data/Tree/AVL/Value.agda
index 6305bd5c2c..f6662512d3 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 Function.id