module work where

open import Level hiding (suc ; zero ; _⊔_ )

open import Data.Nat hiding (compare)
open import Data.Nat.Properties as NatProp
open import Data.Maybe
-- open import Data.Maybe.Properties
open import Data.Empty
open import Data.List
open import Data.Product

open import Function as F hiding (const)

open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import logic

data bt {n : Level} (A : Set n) : Set n where
  leaf : bt A
  node : (key : ℕ) → (value : A) → (left : bt A) → (right : bt A) → bt A