--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/work.agda~	Mon Jul 10 19:59:14 2023 +0900
@@ -0,0 +1,22 @@
+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