diff --git a/CHANGELOG.md b/CHANGELOG.md
index 99dea4e749..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
@@ -397,6 +405,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)) →
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..fac711cbec 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<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
 
-  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..100584948c 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,14 @@ 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 → ∃ 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 +106,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 c2762172b9..5a14794b09 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
@@ -26,7 +26,7 @@ open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Decidable.Core as Dec using (Dec; yes; no)
 open import Relation.Unary using (Pred; _∩_)
 
-open import Data.Tree.AVL.Indexed sto as AVL
+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 renaming (Carrier to Key; trans to <-trans); open Eq using (sym; trans)
 
@@ -40,38 +40,40 @@ private
     k : Key
     V : Value v
     l u : Key⁺
-    n : ℕ
+    hˡ hʳ h : ℕ
     P Q : Pred (K& V) p
 
 ------------------------------------------------------------------------
--- Any.lookup
+-- lookup
 
-lookup-result : {t : Tree V l u n} (p : Any P t) → P (Any.lookup p)
+lookup-result : {t : Tree V l u h} (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 < Any.lookup p .key < u
+lookup-bounded : {t : Tree V l u h} (p : Any P 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 (Any.lookup p) → Any Q t
+lookup-rebuild : {t : Tree V l u h} (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 (Any.lookup p) → Any (Q ∩ P) t
+lookup-rebuild-accum : {t : Tree V l u h} (p : Any P t) → Q (lookup p) → Any (Q ∩ P) t
 lookup-rebuild-accum p q = lookup-rebuild p (q , lookup-result p)
 
-joinˡ⁺-here⁺ : ∀ {l u hˡ hʳ h} →
-             (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ˡ⁺
+
+joinˡ⁺-here⁺ : (kv@(k , _) : K& V) →
+               (l : Tree⁺ V l [ k ] hˡ) →
+               (r : Tree V [ k ] u hʳ) →
+               (bal : hˡ ∼ hʳ ⊔ h) →
+               P kv → Any P (proj₂ (joinˡ⁺ kv l r bal))
 joinˡ⁺-here⁺ k₂ (0# , t₁)                       t₃ bal p = here p
 joinˡ⁺-here⁺ k₂ (1# , t₁)                       t₃ ∼0  p = here p
 joinˡ⁺-here⁺ k₂ (1# , t₁)                       t₃ ∼+  p = here p
@@ -79,12 +81,11 @@ joinˡ⁺-here⁺ k₄ (1# , node k₂ t₁ t₃ ∼-)         t₅ ∼-  p = ri
 joinˡ⁺-here⁺ k₄ (1# , node k₂ t₁ t₃ ∼0)         t₅ ∼-  p = right (here p)
 joinˡ⁺-here⁺ k₆ (1# , node⁺ k₂ t₁ k₄ t₃ t₅ bal) t₇ ∼-  p = right (here p)
 
-joinˡ⁺-left⁺ : ∀ {l u hˡ hʳ h} →
-             (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⁺ : (kv@(k , _) : K& V) →
+               (l@(_ , t) : Tree⁺ V l [ k ] hˡ) →
+               (r : Tree V [ k ] u hʳ) →
+               (bal : hˡ ∼ hʳ ⊔ h) →
+               Any P t → Any P (proj₂ (joinˡ⁺ kv l r bal))
 joinˡ⁺-left⁺ k₂ (0# , t₁)                       t₃ bal p                 = left p
 joinˡ⁺-left⁺ k₂ (1# , t₁)                       t₃ ∼0  p                 = left p
 joinˡ⁺-left⁺ k₂ (1# , t₁)                       t₃ ∼+  p                 = left p
@@ -100,9 +101,8 @@ joinˡ⁺-left⁺ k₆ (1# , node⁺ k₂ t₁ k₄ t₃ t₅ bal) t₇ ∼-  (r
 joinˡ⁺-left⁺ k₆ (1# , node⁺ k₂ t₁ k₄ t₃ t₅ bal) t₇ ∼-  (right (left p))  = left (right p)
 joinˡ⁺-left⁺ k₆ (1# , node⁺ k₂ t₁ k₄ t₃ t₅ bal) t₇ ∼-  (right (right p)) = right (left p)
 
-joinˡ⁺-right⁺ : ∀ {l u hˡ hʳ h} →
-                (kv@(k , v) : K& V) →
-                (l : ∃ λ i → Tree V l [ k ] (i ⊕ hˡ)) →
+joinˡ⁺-right⁺ : (kv@(k , _) : K& V) →
+                (l : Tree⁺ V l [ k ] hˡ) →
                 (r : Tree V [ k ] u hʳ) →
                 (bal : hˡ ∼ hʳ ⊔ h) →
                 Any P r → Any P (proj₂ (joinˡ⁺ kv l r bal))
@@ -113,10 +113,42 @@ joinˡ⁺-right⁺ k₄ (1# , node k₂ t₁ t₃ ∼-)         t₅ ∼-  p = r
 joinˡ⁺-right⁺ k₄ (1# , node k₂ t₁ t₃ ∼0)         t₅ ∼-  p = right (right p)
 joinˡ⁺-right⁺ k₆ (1# , node⁺ k₂ t₁ k₄ t₃ t₅ bal) t₇ ∼-  p = right (right p)
 
-joinʳ⁺-here⁺ : ∀ {l u hˡ hʳ h} →
-               (kv : K& V) →
-               (l : Tree V l [ kv .key ] hˡ) →
-               (r : ∃ λ i → Tree V [ kv .key ] u (i ⊕ hʳ)) →
+joinˡ⁺⁻ : (kv@(k , v) : K& V) →
+          (l@(_ , t) : Tree⁺ V l [ k ] hˡ) →
+          (r : Tree V [ k ] u hʳ) →
+          (bal : hˡ ∼ hʳ ⊔ h) →
+          Any P (proj₂ (joinˡ⁺ kv l r bal)) →
+          P kv ⊎ Any P t ⊎ Any P r
+joinˡ⁺⁻ k₂ (0# , t₁)                       t₃ ba = Any.toSum
+joinˡ⁺⁻ k₂ (1# , t₁)                       t₃ ∼0 = Any.toSum
+joinˡ⁺⁻ k₂ (1# , t₁)                       t₃ ∼+ = Any.toSum
+joinˡ⁺⁻ k₄ (1# , node k₂ t₁ t₃ ∼-)         t₅ ∼- = λ 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ˡ⁺⁻ k₄ (1# , node k₂ t₁ t₃ ∼0)         t₅ ∼- = λ 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ˡ⁺⁻ k₆ (1# , node⁺ k₂ t₁ k₄ t₃ t₅ bal) t₇ ∼- = λ 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 , _) : K& V) →
+               (l : Tree V l [ k ] hˡ) →
+               (r : Tree⁺ V [ k ] u hʳ) →
                (bal : hˡ ∼ hʳ ⊔ h) →
                P kv → Any P (proj₂ (joinʳ⁺ kv l r bal))
 joinʳ⁺-here⁺ k₂ t₁ (0# , t₃)                       bal p = here p
@@ -126,12 +158,11 @@ joinʳ⁺-here⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼+)         ∼+  p = le
 joinʳ⁺-here⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼0)         ∼+  p = left (here p)
 joinʳ⁺-here⁺ k₂ t₁ (1# , node⁻ k₆ k₄ t₃ t₅ bal t₇) ∼+  p = left (here p)
 
-joinʳ⁺-left⁺ : ∀ {l u hˡ hʳ h} →
-              (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⁺ : (kv@(k , _) : K& V) →
+               (l : Tree V l [ k ] hˡ) →
+               (r : Tree⁺ V [ k ] u hʳ) →
+               (bal : hˡ ∼ hʳ ⊔ h) →
+               Any P l → Any P (proj₂ (joinʳ⁺ kv l r bal))
 joinʳ⁺-left⁺ k₂ t₁ (0# , t₃)                       bal p = left p
 joinʳ⁺-left⁺ k₂ t₁ (1# , t₃)                       ∼0  p = left p
 joinʳ⁺-left⁺ k₂ t₁ (1# , t₃)                       ∼-  p = left p
@@ -139,12 +170,11 @@ joinʳ⁺-left⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼+)         ∼+  p = le
 joinʳ⁺-left⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼0)         ∼+  p = left (left p)
 joinʳ⁺-left⁺ k₂ t₁ (1# , node⁻ k₆ k₄ t₃ t₅ bal t₇) ∼+  p = left (left p)
 
-joinʳ⁺-right⁺ : ∀ {l u hˡ hʳ h} →
-                (kv : K& V) →
-                (l : Tree V l [ kv .key ] hˡ) →
-                (r : ∃ λ i → Tree V [ kv .key ] u (i ⊕ hʳ)) →
+joinʳ⁺-right⁺ : (kv@(k , _) : K& V) →
+                (l : Tree V l [ k ] hˡ) →
+                (r@(_ , t) : Tree⁺ V [ k ] u hʳ) →
                 (bal : hˡ ∼ hʳ ⊔ h) →
-                Any P (proj₂ r) → Any P (proj₂ (joinʳ⁺ kv l r bal))
+                Any P t → Any P (proj₂ (joinʳ⁺ kv l r bal))
 joinʳ⁺-right⁺ k₂ t₁ (0# , t₃)                       bal p                = right p
 joinʳ⁺-right⁺ k₂ t₁ (1# , t₃)                       ∼0  p                = right p
 joinʳ⁺-right⁺ k₂ t₁ (1# , t₃)                       ∼-  p                = right p
@@ -160,44 +190,12 @@ joinʳ⁺-right⁺ k₂ t₁ (1# , node⁻ k₆ k₄ t₃ t₅ bal t₇) ∼+  (
 joinʳ⁺-right⁺ k₂ t₁ (1# , node⁻ k₆ k₄ t₃ t₅ bal t₇) ∼+  (left (right p)) = right (left p)
 joinʳ⁺-right⁺ k₂ t₁ (1# , node⁻ k₆ k₄ t₃ t₅ bal t₇) ∼+  (right p)        = right (right p)
 
-joinˡ⁺⁻ : ∀ {l u hˡ hʳ h} →
-            (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ˡ⁺⁻ k₂ (0# , t₁)                       t₃ ba = Any.toSum
-joinˡ⁺⁻ k₂ (1# , t₁)                       t₃ ∼0 = Any.toSum
-joinˡ⁺⁻ k₂ (1# , t₁)                       t₃ ∼+ = Any.toSum
-joinˡ⁺⁻ k₄ (1# , node k₂ t₁ t₃ ∼-)         t₅ ∼- = λ 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ˡ⁺⁻ k₄ (1# , node k₂ t₁ t₃ ∼0)         t₅ ∼- = λ 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ˡ⁺⁻ k₆ (1# , node⁺ k₂ t₁ k₄ t₃ t₅ bal) t₇ ∼- = λ 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ʳ⁺⁻ : ∀ {l u hˡ hʳ h} →
-            (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ʳ⁺⁻ : (kv@(k , _) : K& V) →
+          (l : Tree V l [ k ] hˡ) →
+          (r@(_ , t) : Tree⁺ V [ k ] u hʳ) →
+          (bal : hˡ ∼ hʳ ⊔ h) →
+          Any P (proj₂ (joinʳ⁺ kv l r bal)) →
+          P kv ⊎ Any P l ⊎ Any P t
 joinʳ⁺⁻ k₂ t₁ (0# , t₃)                       bal = Any.toSum
 joinʳ⁺⁻ k₂ t₁ (1# , t₃)                       ∼0  = Any.toSum
 joinʳ⁺⁻ k₂ t₁ (1# , t₃)                       ∼-  = Any.toSum
@@ -222,23 +220,19 @@ joinʳ⁺⁻ k₂ t₁ (1# , node⁻ k₆ k₄ t₃ t₅ bal t₇) ∼+  = λ wh
   (right (here p))  → inj₂ (inj₂ (here p))
   (right (right p)) → inj₂ (inj₂ (right p))
 
-module _ {V : Value v} where
+----------------------------------------------------------------------
+-- Properties of tree construction operations
 
-  private
-    Val  = Value.family V
-    Val≈ = Value.respects V
+module _ {V : Value v} (open Value V using (respects) renaming (family to Val)) where
+
+  ----------------------------------------------------------------------
+  -- singleton
 
-  singleton⁺ : {P : Pred (K& V) p} →
-               (k : Key) →
-               (v : Val k) →
-               (l<k<u : l < k < u) →
+  singleton⁺ : (k : Key) (v : Val k) (l<k<u : l < k < u) →
                P (k , v) → Any P (singleton k v l<k<u)
   singleton⁺ k v l<k<u Pkv = here Pkv
 
-  singleton⁻ : {P : Pred (K& V) p} →
-               (k : Key) →
-               (v : Val k) →
-               (l<k<u : l < k < u) →
+  singleton⁻ : (k : Key) (v : Val k) (l<k<u : l < k < u) →
                Any P (singleton k v l<k<u) → P (k , v)
   singleton⁻ k v l<k<u (here Pkv) = Pkv
 
@@ -249,31 +243,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 h) (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 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′
     -- 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
@@ -309,19 +305,8 @@ 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
-
-    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)) →
-                      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
-
-    insertWith⁺ : (t : Tree V l u n) (seg : l < k < u) →
-                  (p : Any P t) → k ≉ Any.lookupKey p →
+    insertWith⁺ : (t : Tree V l u h) (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≉
       with compare k k′
@@ -347,18 +332,27 @@ 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 v = insertWith⁺ k (F.const v)
+  module _ (k : Key) (v : Val k) (t : Tree V l u h) (seg : 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-just : (pr : ∀ k′ → (eq : k ≈ k′) → P (k′ , respects 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⁺ : (p : Any P t) → k ≉ lookupKey p →
+              Any P (proj₂ (insert k v t seg))
+    insert⁺ = insertWith⁺ k (F.const v) t seg
 
   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) →
+    insert⁻ : (t : Tree V l u h) (seg : l < k < u) →
               Any P (proj₂ (insert k v t seg)) →
               P (k , v) ⊎ Any (λ{ (k′ , v′) → k ≉ k′ × P (k′ , v′)}) t
     insert⁻ (leaf l<u) seg (here p) = inj₁ p
@@ -391,9 +385,9 @@ module _ {V : Value v} where
       k′<p = [<]-injective (proj₁ (lookup-bounded p))
       k≉p = λ k≈p → irrefl (trans (sym k≈k′) k≈p) k′<p
 
-  lookup⁺ : (t : Tree V l u n) (k : Key) (seg : l < k < u) →
+  lookup⁺ : (t : Tree V l u h) (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 (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
@@ -410,10 +404,40 @@ module _ {V : Value v} where
   ... | 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) →
+  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 → 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)
   ... | 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."
+#-}
diff --git a/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda b/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda
index 5e472cfe2b..d576c3bfa7 100644
--- a/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda
+++ b/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda
@@ -72,10 +72,10 @@ private
 -- singleton
 
 ∈ₖᵥ-singleton⁺ : (k , x) ∈ₖᵥ singleton k x
-∈ₖᵥ-singleton⁺ = tree (IAnyₚ.singleton⁺ _ _ _ (refl , ≡-refl))
+∈ₖᵥ-singleton⁺ = tree {!IAnyₚ.singleton⁺ _ _ _ (refl , ≡-refl)!}
 
 ∈ₖᵥ-singleton⁻ : (k , x) ∈ₖᵥ singleton k′ x′ → k ≈ k′ × x ≡ x′
-∈ₖᵥ-singleton⁻ (tree p) = IAnyₚ.singleton⁻ _ _ _ p
+∈ₖᵥ-singleton⁻ (tree p) = {!IAnyₚ.singleton⁻ _ _ _ p!}
 
 private
   ≈-lookup : (p : (k , x) ∈ₖᵥ m) → k ≈ Any.lookupKey p
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