    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Some code related to indexed AVL trees that relies on the K rule
    ------------------------------------------------------------------------

    {-# OPTIONS --with-K --safe #-}

    open import Relation.Binary.Core using (Rel)
    open import Relation.Binary.Structures using (IsStrictTotalOrder)
    open import Relation.Binary.Bundles using (StrictTotalOrder)
    open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; subst)

    module Data.Tree.AVL.Indexed.WithK
           {k r} (Key : Set k) {_<_ : Rel Key r}
           (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_) where

    strictTotalOrder : StrictTotalOrder _ _ _
    strictTotalOrder = record { isStrictTotalOrder = isStrictTotalOrder }

    open import Data.Tree.AVL.Indexed strictTotalOrder as AVL hiding (Value)

    module _ {v} {V′ : Key → Set v} where

      private
        V : AVL.Value v
        V = AVL.MkValue V′ (subst V′)

      node-injectiveˡ : ∀ {hˡ hʳ h l u k}
        {lk₁ : Tree V l [ k .key ] hˡ} {lk₂ : Tree V l [ k .key ] hˡ}
        {ku₁ : Tree V [ k .key ] u hʳ} {ku₂ : Tree V [ k .key ] u hʳ}
        {bal₁ bal₂ : hˡ ∼ hʳ ⊔ h} →
        node k lk₁ ku₁ bal₁ ≡ node k lk₂ ku₂ bal₂ → lk₁ ≡ lk₂
      node-injectiveˡ refl = refl

      node-injectiveʳ : ∀ {hˡ hʳ h l u k}
        {lk₁ : Tree V l [ k .key ] hˡ} {lk₂ : Tree V l [ k .key ] hˡ}
        {ku₁ : Tree V [ k .key ] u hʳ} {ku₂ : Tree V [ k .key ] u hʳ}
        {bal₁ bal₂ : hˡ ∼ hʳ ⊔ h} →
        node k lk₁ ku₁ bal₁ ≡ node k lk₂ ku₂ bal₂ → ku₁ ≡ ku₂
      node-injectiveʳ refl = refl

      node-injective-bal : ∀ {hˡ hʳ h l u k}
        {lk₁ : Tree V l [ k .key ] hˡ} {lk₂ : Tree V l [ k .key ] hˡ}
        {ku₁ : Tree V [ k .key ] u hʳ} {ku₂ : Tree V [ k .key ] u hʳ}
        {bal₁ bal₂ : hˡ ∼ hʳ ⊔ h} →
        node k lk₁ ku₁ bal₁ ≡ node k lk₂ ku₂ bal₂ → bal₁ ≡ bal₂
      node-injective-bal refl = refl