data nomal-tree (A : Set) : Set where
  nleaf : (key : !$\mathbb{N}$!) !$\rightarrow$! tree A
  nnode : (key : !$\mathbb{N}$!) !$\rightarrow$! (lnode : nomal-tree A) !$\rightarrow$! (rnode : nomal-tree A) !$\rightarrow$! nomal-tree A

data meta-tree (A : Set) : (key : !$\mathbb{N}$!) !$\rightarrow$! Set where
  mleaf : (key : !$\mathbb{N}$!) !$\rightarrow$! meta-tree A key
  mnode : { l r : !$\mathbb{N}$! } !$\rightarrow$! (key : !$\mathbb{N}$!) !$\rightarrow$! (value : A)
    !$\rightarrow$! (lnode : meta-tree A l)  !$\rightarrow$! (rnode : meta-tree A r)
    !$\rightarrow$! l !$\leq$! key !$\rightarrow$! key !$\leq$! r !$\rightarrow$! metatree A key