record Node {n : Level } (a k : Set n) : Set n where
  inductive
  field
    key   : k
    value : a
    right : Maybe (Node a k)
    left  : Maybe (Node a k)
    color : Color {n}
open Node

leafNode : {n : Level } {a k : Set n}  -> k -> a -> Node a k
leafNode k1 value = record {
  key   = k1 ;
  value = value ;
  right = Nothing ;
  left  = Nothing ;
  color = Red
  }
open leafNode

record RedBlackTree {n m : Level } {t : Set m} (a k : Set n) : Set (m Level.⊔ n) where
  field
    root : Maybe (Node a k)
    nodeStack : SingleLinkedStack  (Node a k)
    compare : k -> k -> CompareResult {n}
open RedBlackTree

putRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> k -> a -> (RedBlackTree {n} {m} {t} a k -> t) -> t
putRedBlackTree {n} {m} {a} {k}  {t} tree k1 value next with (root tree)
...                                | Nothing = next (record tree {root = Just (leafNode k1 value) })
...                                | Just n2  = clearSingleLinkedStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next))

-- 以下省略