1
open import Relation.Binary
2
open import Relation.Binary.PropositionalEquality
3
open import Data.Product
7
{Index : Set} {Key : Index → Set} {_≈_ _<_ : Rel (∃ Key) zero}
8
(isOrderedKeySet : IsStrictTotalOrder _≈_ _<_)
9
-- Equal keys must have equal indices.
10
(indicesEqual : _≈_ =[ proj₁ ]⇒ _≡_)