    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Properties related to Any
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    open import Relation.Binary.Bundles using (StrictTotalOrder)

    module Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties
      {a ℓ₁ ℓ₂} (sto : StrictTotalOrder a ℓ₁ ℓ₂)
      where

    open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; maybe′)
    open import Data.Maybe.Properties using (just-injective)
    open import Data.Maybe.Relation.Unary.All as Maybe using (nothing; just)
    open import Data.Nat.Base using (ℕ)
    open import Data.Product.Base as Prod using (∃; ∃-syntax; _×_; _,_; proj₁; proj₂)
    open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
    open import Function.Base as F using (const; _∘_; id; flip; _∘′_)
    open import Level using (Level)
    open import Relation.Binary.Definitions using (_Respects_; tri<; tri≈; tri>)
    open import Relation.Binary.PropositionalEquality.Core using (_≡_) renaming (refl to ≡-refl)
    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.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)

    import Relation.Binary.Reasoning.StrictPartialOrder as <-Reasoning

    private
      variable
        v p q : Level
        k : Key
        V : Value v
        l u : Key⁺
        n : ℕ
        P Q : Pred (K& V) p

    ------------------------------------------------------------------------
    -- Any.lookup

    lookup-result : {t : Tree V l u n} (p : Any P t) → P (Any.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 = 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 (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 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ˡ⁺-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
    joinˡ⁺-here⁺ k₄ (1# , node k₂ t₁ t₃ ∼-)         t₅ ∼-  p = right (here p)
    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⁺ 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
    joinˡ⁺-left⁺ k₄ (1# , node k₂ t₁ t₃ ∼-)         t₅ ∼-  (here p)          = here p
    joinˡ⁺-left⁺ k₄ (1# , node k₂ t₁ t₃ ∼-)         t₅ ∼-  (left p)          = left p
    joinˡ⁺-left⁺ k₄ (1# , node k₂ t₁ t₃ ∼-)         t₅ ∼-  (right p)         = right (left p)
    joinˡ⁺-left⁺ k₄ (1# , node k₂ t₁ t₃ ∼0)         t₅ ∼-  (here p)          = here p
    joinˡ⁺-left⁺ k₄ (1# , node k₂ t₁ t₃ ∼0)         t₅ ∼-  (left p)          = left p
    joinˡ⁺-left⁺ k₄ (1# , node k₂ t₁ t₃ ∼0)         t₅ ∼-  (right p)         = right (left p)
    joinˡ⁺-left⁺ k₆ (1# , node⁺ k₂ t₁ k₄ t₃ t₅ bal) t₇ ∼-  (here p)          = left (here p)
    joinˡ⁺-left⁺ k₆ (1# , node⁺ k₂ t₁ k₄ t₃ t₅ bal) t₇ ∼-  (left p)          = left (left p)
    joinˡ⁺-left⁺ k₆ (1# , node⁺ k₂ t₁ k₄ t₃ t₅ bal) t₇ ∼-  (right (here p))  = here p
    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ˡ)) →
                    (r : Tree V [ k ] u hʳ) →
                    (bal : hˡ ∼ hʳ ⊔ h) →
                    Any P r → Any P (proj₂ (joinˡ⁺ kv l r bal))
    joinˡ⁺-right⁺ k₂ (0# , t₁)                       t₃ bal p = right p
    joinˡ⁺-right⁺ k₂ (1# , t₁)                       t₃ ∼0  p = right p
    joinˡ⁺-right⁺ k₂ (1# , t₁)                       t₃ ∼+  p = right p
    joinˡ⁺-right⁺ k₄ (1# , node k₂ t₁ t₃ ∼-)         t₅ ∼-  p = right (right p)
    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ʳ)) →
                   (bal : hˡ ∼ hʳ ⊔ h) →
                   P kv → Any P (proj₂ (joinʳ⁺ kv l r bal))
    joinʳ⁺-here⁺ k₂ t₁ (0# , t₃)                       bal p = here p
    joinʳ⁺-here⁺ k₂ t₁ (1# , t₃)                       ∼0  p = here p
    joinʳ⁺-here⁺ k₂ t₁ (1# , t₃)                       ∼-  p = here p
    joinʳ⁺-here⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼+)         ∼+  p = left (here p)
    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⁺ 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
    joinʳ⁺-left⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼+)         ∼+  p = left (left p)
    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ʳ)) →
                    (bal : hˡ ∼ hʳ ⊔ h) →
                    Any P (proj₂ r) → 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
    joinʳ⁺-right⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼+)         ∼+  (here p)         = here p
    joinʳ⁺-right⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼+)         ∼+  (left p)         = left (right p)
    joinʳ⁺-right⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼+)         ∼+  (right p)        = right p
    joinʳ⁺-right⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼0)         ∼+  (here p)         = here p
    joinʳ⁺-right⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼0)         ∼+  (left p)         = left (right p)
    joinʳ⁺-right⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼0)         ∼+  (right p)        = right p
    joinʳ⁺-right⁺ k₂ t₁ (1# , node⁻ k₆ k₄ t₃ t₅ bal t₇) ∼+  (here p)         = right (here p)
    joinʳ⁺-right⁺ k₂ t₁ (1# , node⁻ k₆ k₄ t₃ t₅ bal t₇) ∼+  (left (here p))  = here p
    joinʳ⁺-right⁺ k₂ t₁ (1# , node⁻ k₆ k₄ t₃ t₅ bal t₇) ∼+  (left (left p))  = left (right p)
    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ʳ⁺⁻ k₂ t₁ (0# , t₃)                       bal = Any.toSum
    joinʳ⁺⁻ k₂ t₁ (1# , t₃)                       ∼0  = Any.toSum
    joinʳ⁺⁻ k₂ t₁ (1# , t₃)                       ∼-  = Any.toSum
    joinʳ⁺⁻ k₂ t₁ (1# , node k₄ t₃ t₅ ∼+)         ∼+  = λ where
      (left (left p))  → inj₂ (inj₁ p)
      (left (here p))  → inj₁ p
      (left (right p)) → inj₂ (inj₂ (left p))
      (here p)         → inj₂ (inj₂ (here p))
      (right p)        → inj₂ (inj₂ (right p))
    joinʳ⁺⁻ k₂ t₁ (1# , node k₄ t₃ t₅ ∼0)         ∼+  = λ where
      (left (left p))  → inj₂ (inj₁ p)
      (left (here p))  → inj₁ p
      (left (right p)) → inj₂ (inj₂ (left p))
      (here p)         → inj₂ (inj₂ (here p))
      (right p)        → inj₂ (inj₂ (right p))
    joinʳ⁺⁻ k₂ t₁ (1# , node⁻ k₆ k₄ t₃ t₅ bal t₇) ∼+  = λ where
      (left (left p))   → inj₂ (inj₁ p)
      (left (here p))   → inj₁ p
      (left (right p))  → inj₂ (inj₂ (left (left p)))
      (here p)          → inj₂ (inj₂ (left (here p)))
      (right (left p))  → inj₂ (inj₂ (left (right p)))
      (right (here p))  → inj₂ (inj₂ (here p))
      (right (right p)) → inj₂ (inj₂ (right p))

    module _ {V : Value v} where

      private
        Val  = Value.family V
        Val≈ = Value.respects V

      singleton⁺ : {P : Pred (K& V) p} →
                   (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) →
                   Any P (singleton k v l<k<u) → P (k , v)
      singleton⁻ k v l<k<u (here Pkv) = Pkv

      ----------------------------------------------------------------------
      -- insert

      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
          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))
                              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))
                              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
          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)
        ... | 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)

        -- impossible cases
        ... | here eq  | tri< k<k′ _ _ = begin-contradiction
          [ k  ] <⟨ [ k<k′ ]ᴿ ⟩
          [ k′ ] ≈⟨ [ sym eq ]ᴱ ⟩
          [ k  ] ∎
        ... | here eq  | tri> _ _ k>k′ = begin-contradiction
          [ k  ] ≈⟨ [ eq ]ᴱ ⟩
          [ k′ ] <⟨ [ k>k′ ]ᴿ ⟩
          [ k  ] ∎
        ... | left lp  | tri≈ _ k≈k′ _ = begin-contradiction
          let k″ = Any.lookup lp .key; k≈k″ = lookup-result lp; (_ , k″<k′) = lookup-bounded lp in
          [ k  ] ≈⟨ [ k≈k″ ]ᴱ ⟩
          [ k″ ] <⟨ k″<k′ ⟩
          [ k′ ] ≈⟨ [ sym k≈k′ ]ᴱ ⟩
          [ k  ] ∎
        ... | left lp  | tri> _ _ k>k′ = begin-contradiction
          let k″ = Any.lookup lp .key; k≈k″ = lookup-result lp; (_ , k″<k′) = lookup-bounded lp in
          [ k  ] ≈⟨ [ k≈k″ ]ᴱ ⟩
          [ k″ ] <⟨ k″<k′ ⟩
          [ k′ ] <⟨ [ k>k′ ]ᴿ ⟩
          [ k  ] ∎
        ... | right rp | tri< k<k′ _ _ = begin-contradiction
          let k″ = Any.lookup rp .key; k≈k″ = lookup-result rp; (k′<k″ , _) = lookup-bounded rp in
          [ k  ] <⟨ [ k<k′ ]ᴿ ⟩
          [ k′ ] <⟨ k′<k″ ⟩
          [ k″ ] ≈⟨ [ sym k≈k″ ]ᴱ ⟩
          [ k  ] ∎
        ... | right rp | tri≈ _ k≈k′ _ = begin-contradiction
          let k″ = Any.lookup rp .key; k≈k″ = lookup-result rp; (k′<k″ , _) = lookup-bounded rp in
          [ k  ] ≈⟨ [ k≈k′ ]ᴱ ⟩
          [ k′ ] <⟨ k′<k″ ⟩
          [ 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 →
                      Any P (proj₂ (insertWith k f t seg))
        insertWith⁺ (node kv@(k′ , v′) l r bal) (l<k , k<u) (here p) k≉
          with compare k k′
        ... | tri< k<k′ _ _ = let l′ = insertWith k f l (l<k , [ k<k′ ]ᴿ)
                              in joinˡ⁺-here⁺ kv l′ r bal p
        ... | tri≈ _ k≈k′ _ = contradiction k≈k′ k≉
        ... | tri> _ _ k′<k = let r′ = insertWith k f r ([ k′<k ]ᴿ , k<u)
                              in joinʳ⁺-here⁺ kv l r′ bal p
        insertWith⁺ (node kv@(k′ , v′) l r bal) (l<k , k<u) (left p) k≉
          with compare k k′
        ... | tri< k<k′ _ _ = let l′ = insertWith k f l (l<k , [ k<k′ ]ᴿ)
                                  ih = insertWith⁺ l (l<k , [ k<k′ ]ᴿ) p k≉
                              in joinˡ⁺-left⁺ kv l′ r bal ih
        ... | tri≈ _ k≈k′ _ = left p
        ... | tri> _ _ k′<k = let r′ = insertWith k f r ([ k′<k ]ᴿ , k<u)
                              in joinʳ⁺-left⁺ kv l r′ bal p
        insertWith⁺ (node kv@(k′ , v′) l r bal) (l<k , k<u) (right p) k≉
          with compare k k′
        ... | tri< k<k′ _ _ = let l′ = insertWith k f l (l<k , [ k<k′ ]ᴿ)
                              in joinˡ⁺-right⁺ kv l′ r bal p
        ... | tri≈ _ k≈k′ _ = right p
        ... | tri> _ _ k′<k = let r′ = insertWith k f r ([ k′<k ]ᴿ , k<u)
                                  ih = insertWith⁺ r ([ k′<k ]ᴿ , k<u) p k≉
                              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 _
        {P : Pred (K& V) p}
        (P-Resp : ∀ {k k′ v} → (k≈k′ : k ≈ k′) → P (k′ , Val≈ 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)) →
                  P (k , v) ⊎ Any (λ{ (k′ , v′) → k ≉ k′ × P (k′ , v′)}) t
        insert⁻ (leaf l<u) seg (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
        ... | inj₁ p        = inj₂ (here (k≉k′ , p))
        ... | inj₂ (inj₂ p) = inj₂ (right (lookup-rebuild-accum p k≉p))
          where
          k′<p = [<]-injective (proj₁ (lookup-bounded p))
          k≉p = λ k≈p → irrefl k≈p (<-trans k<k′ k′<p)
        ... | inj₂ (inj₁ p) = Sum.map₂ (λ q → left q) (insert⁻ l (l<k , [ k<k′ ]ᴿ) p)
        insert⁻ (node kv′@(k′ , v′) l r bal) (l<k , k<u) p | tri> _ k≉k′ k′<k
            with joinʳ⁺⁻ kv′ l (insert k v r ([ k′<k ]ᴿ , k<u)) bal p
        ... | inj₁ p        = inj₂ (here (k≉k′ , p))
        ... | inj₂ (inj₁ p) = inj₂ (left (lookup-rebuild-accum p k≉p))
          where
          p<k′ = [<]-injective (proj₂ (lookup-bounded p))
          k≉p = λ k≈p → irrefl (sym k≈p) (<-trans p<k′ k′<k)
        ... | inj₂ (inj₂ p) = Sum.map₂ (λ q → right q) (insert⁻ r ([ k′<k ]ᴿ , k<u) p)
        insert⁻ (node kv′@(k′ , v′) l r bal) (l<k , k<u) p | tri≈ _ k≈k′ _
            with p
        ... | left p  = inj₂ (left (lookup-rebuild-accum p k≉p))
          where
          p<k′ = [<]-injective (proj₂ (lookup-bounded p))
          k≉p = λ k≈p → irrefl (trans (sym k≈p) k≈k′) p<k′
        ... | here p  = inj₁ (P-Resp k≈k′ p)
        ... | right p = inj₂ (right (lookup-rebuild-accum p k≉p))
          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) →
                (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)