diff --git a/lib/Base/Types.fram b/lib/Base/Types.fram
index cab416ea..ff5d4f26 100644
--- a/lib/Base/Types.fram
+++ b/lib/Base/Types.fram
@@ -8,4 +8,6 @@ pub data Pair X Y = (,) of X, Y
 
 pub data Either X Y = Left of X | Right of Y
 
+pub data Ordered = Lt | Eq | Gt
+
 pub data Result A E = Ok of A | Err of E
diff --git a/lib/RedBlackTree.fram b/lib/RedBlackTree.fram
new file mode 100644
index 00000000..010f13b9
--- /dev/null
+++ b/lib/RedBlackTree.fram
@@ -0,0 +1,481 @@
+{# This file is part of DBL, released under MIT license.
+ # See LICENSE for details.
+ #}
+
+# Due to frequent request for understanding this file please
+# see comments at the end of this file
+
+import List
+
+data Color =
+  | Red
+  | Black
+
+pub data rec Tree Value =
+  | Leaf
+  | Node of {
+      color: Color,
+      size: Int,
+      left: Tree Value,
+      value: Value,
+      right: Tree Value
+    }
+
+{# Red-black invariant: 
+#        no red node has a red child
+#        Black height invariant: 
+#           for every t = Node(_, _, left, _, right),
+#           black-height(left) = black-height(right)
+#        Leaves are considered black, but do not contribute to black height.
+#}
+
+data ZipElem Value =
+  | Left of Color, Value, Tree Value
+  | Right of Color, Tree Value, Value
+
+# Empty tree
+pub let empty = Leaf
+
+# Return cached size
+pub let size tree =
+  match tree with
+  | Leaf => 0
+  | Node {size} => size
+  end
+
+# Smart constructor that updates the size of node
+pub let makeNode color left value right =
+  Node {color, size = size left + size right + 1, left, value, right}
+
+# Constructor for node
+pub let construct color size left value right =
+  Node {color,size,left,value,right}
+
+# Walk upward applying recorded decisions (zipper) to rebuild tree
+let rec zip tree zipper =
+  match zipper with
+  | [] => tree
+
+  | Left color value right :: rest =>
+    zip (makeNode color tree value right) rest
+
+  | Right color left value :: rest =>
+    zip (makeNode color left value tree) rest
+
+ end
+
+{# Precondition:
+ #  (zip (Node (RED, size, left, value ,right) zipper) 
+ #  satisfies the black-height invariant, 
+ #  and also satisfies the red-black 
+ #  invariant except possibly locally
+ #}
+let rec zipRed value left right zipper =
+  match zipper with
+  # Root case
+  | [] => makeNode Black left value right
+  
+  # Father is black and we are left child then we recreate the node
+  # and we are rebuilding tree 
+  | Left Black value1 right1 :: rest =>
+    zip (makeNode Black (makeNode Red left value right) value1 right1) rest
+
+  
+  # Father is black and we are right child then we recreate the node
+  # and we are rebuilding tree 
+  | Right Black left1 value1  :: rest =>
+    zip (makeNode Black left1 value1 (makeNode Red left value right)) rest
+
+  # Father is Red and left child, the uncle is Red and we are left child. 
+  # The father and uncle are colored Black.
+  # ZipRed is recursively called on the grandfather.
+  | Left Red value1 right1 ::
+      Left _ value2
+      (Node {color = Red, size = size3, left = left3,
+      value = value3, right = right3}) :: rest =>
+    let left'  = makeNode Red left value right
+    let right' = construct Black size3 left3 value3 right3 in
+    zipRed value2 (makeNode Black left' value1 right1) right' rest
+
+  # Father is Red and right child, the uncle is Red and we are left child. 
+  # The father and uncle are colored Black.
+  # ZipRed is recursively called on the grandfather.
+  | Left Red value1 right1 ::
+      Right _
+      (Node {color = Red, size = size3, left = left3,
+      value = value3, right = right3}) value2 :: rest =>
+    let left'  = construct Black size3 left3 value3 right3
+    let right' = makeNode Red left value right in
+    zipRed value2 left' (makeNode Black right' value1 right1) rest
+
+  # Father is Red and left child, the uncle is Red and we are right child. 
+  # The father and uncle are colored Black.
+  # ZipRed is recursively called on the grandfather.
+  | Right Red left1 value1 ::
+      Left _ value2
+      (Node {color = Red, size = size3, left = left3,
+      value = value3, right = right3}) :: rest =>
+    let left'  = makeNode Red left value right
+    let right' = construct Black size3 left3 value3 right3 in
+    zipRed value2 (makeNode Black left1 value1 left') right' rest
+
+  # Father is Red and right child, the uncle is Red and we are right child. 
+  # The father and uncle are colored Black.
+  # ZipRed is recursively called on the grandfather.
+  | Right Red left1 value1 ::
+      Right _ (Node {color = Red, size = size3, left = left3,
+      value = value3, right = right3}) value2 :: rest =>
+    let left'  = construct Black size3 left3 value3 right3
+    let right' = makeNode Red left value right in
+    zipRed value2 left' (makeNode Black left1 value1 right') rest
+
+  # Father is Red and left child, the uncle is Black and we are left child. 
+  # The father and uncle are colored Red.
+  # The grandfather is then black and we are rebuilding the tree.
+  | Left Red value1 right1 :: Left _ value2 node3 :: rest =>
+    let left'  = makeNode Red left value right
+    let right' = makeNode Red right1 value2 node3 in
+    zip (makeNode Black left' value1 right') rest
+  
+  # Father is Red and right child, the uncle is Black and we are left child. 
+  # The father and uncle are colored Red.
+  # The grandfather is then black and we are rebuilding the tree.
+  | Left Red value1 right1 :: Right _ node3 value2  :: rest =>
+    let left'  = makeNode Red node3 value2 left
+    let right' = makeNode Red right value1 right1 in
+    zip (makeNode Black left' value right') rest
+
+  # Father is Red and left child, the uncle is Black and we are right child. 
+  # The father and uncle are colored Red.
+  # The grandfather is then black and we are rebuilding the tree.
+  | Right Red left1 value1 :: Left _ value2 node3 :: rest =>
+    let left'  = makeNode Red left1 value1 left
+    let right' = makeNode Red right value2 node3 in
+    zip (makeNode Black left' value right') rest
+
+  # Father is Red and right child, the uncle is Black and we are right child. 
+  # The father and uncle are colored Red.
+  # The grandfather is then black and we are rebuilding the tree.
+  | Right Red left1 value1 :: Right _  node3 value2 :: rest =>
+    let left'  = makeNode Red node3 value2 left1
+    let right' = makeNode Red left value right in
+    zip (makeNode Black left' value1 right') rest
+
+  # The father is Red and a root and we are left child.
+  # The functions correct invariant about root.
+  | Left Red value1 right1 :: [] =>
+    makeNode Black (makeNode Red left value right) value1 right1
+
+  # The father is Red and a root and we are right child.
+  # The functions correct invariant about root.
+  | Right Red left1 value1 :: [] =>
+    makeNode Black left1 value1 (makeNode Red left value right)
+
+ end
+
+{# Precondition:
+#       1. tree is black
+#       2. (zip tree zipper) satisfies the red-black invariant, and it
+#          would satisfy the black-height invariant if the black-height of
+#          tree were one higher
+#}
+pub let rec zipBlack tree zipper =
+  match zipper with
+  # Root case
+  | [] => tree
+
+  # Tree is left child, and right nephew is Red.
+  #     father(C)                          brother(C)
+  #     /    \                            /      \
+  # tree      brother       ->        father(B)    rnephew(B)
+  #           /     \                 /     \
+  #       lnephew   rnephew(R)      tree      lnephew
+  # After rotation, the whole tree is reconstructed
+  | Left color1 value1
+      (Node {left = left2, value = value2,
+      right = (Node {color = Red, size = size3,
+      left = left3, value = value3, right = right3})}) ::
+      rest =>
+    let left'  = makeNode Black tree value1 left2
+    let right' = construct Black size3 left3 value3 right3 in
+    zip (makeNode color1 left' value2 right') rest
+
+  # Tree is right child, and left nephew is Red.
+  #             Cfather                   Cbrother
+  #           /        \                 /        \
+  #     brother         tree    ->  Blnephew      Bfather
+  #    /       \                                  /     \
+  # Rlnephew   rnephew                       rnephew    tree
+  # After rotation, the whole tree is reconstructed
+  | Right color1 (Node { left = (Node {color = Red, size = size3, left = left3,
+      value = value3, right = right3}), value = value2, right = right2})
+      value1 :: rest =>
+    let left'  = construct Black size3 left3 value3 right3
+    let right' = makeNode Black right2 value1 tree in
+    zip (makeNode color1 left' value2 right') rest
+  
+  # Tree is left child, and right nephew is Red.
+  #     Cfather                           Crnephew
+  #     /    \                            /      \
+  # tree      brother       ->        Bfather    Bbrother
+  #           /     \                 /    \      /     \
+  #       Rlnephew  Brnephew      tree   left   right   Brnephew
+  #       /      \
+  #     left     right
+  # After rotation, the whole tree is reconstructed
+  | Left color1 value1 (Node {left = (Node {color = Red, left = left3,
+      value = value3, right = right3}),
+      value = value2, right = right2}) :: rest =>
+    let left'  = makeNode Black tree value1 left3
+    let right' = makeNode Black right3 value2 right2 in
+    zip (makeNode color1 left' value3 right') rest
+
+  # Tree is right child, and left nephew is Red.
+  #             Cfather                     Crnephew
+  #           /        \                  /         \
+  #     brother         tree    ->   Bbrother       Bfather
+  #    /       \                     /     \         /    \
+  # Blnephew   Rrnephew          Blnephew  left    right   tree
+  #           /     \
+  #         left    right
+  # After rotation, the whole tree is reconstructed
+  | Right color1 (Node {left = left2, value = value2, right =
+      (Node {color = Red, left = left3, value = value3, right = right3})})
+      value1 :: rest =>
+    let left'  = makeNode Black left2 value2 left3
+    let right' = makeNode Black right3 value1 tree in
+    zip (makeNode color1 left' value3 right') rest
+
+  # The father is red and no nephew is red.
+  # Then father becomes black and brother becomes red
+  # removing therfore the inequality of blackness. 
+  # After that, the whole tree is reconstructed.
+  | Left Red value1 (Node {size = size2, left = left2,
+      value = value2, right = right2}) :: rest =>
+    let right' = construct Red size2 left2 value2 right2 in
+    zip (makeNode Black tree value1 right') rest
+
+  # The father is red and no nephew is red.
+  # Then father becomes black and brother becomes red
+  # removing therfore the inequality of blackness. 
+  # After that, the whole tree is reconstructed.
+  | Right Red (Node {size = size2, left = left2,
+      value = value2, right = right2}) value1 :: rest =>
+    let left' = construct Red size2 left2 value2 right2 in
+    zip (makeNode Black left' value1 tree) rest
+
+  # The father is black and no nephew is red.
+  # Brother becomes red but the inequality of blackness is sustained. 
+  # ZipBlack recursively called on the father.
+  | Left Black value1 (Node {color = Black, size = size2, left = left2,
+      value = value2, right = right2}) :: rest =>
+    let right' = construct Red size2 left2 value2 right2 in
+    zipBlack (makeNode Black tree value1 right') rest
+  
+  # The father is black and no nephew is red.
+  # Brother becomes red but the inequality of blackness is sustained. 
+  # ZipBlack recursively called on the father.
+  | Right Black (Node {color = Black, size = size2, left = left2,
+      value = value2, right = right2}) value1 :: rest =>
+    let left' = construct Red size2 left2 value2 right2 in
+    zipBlack (makeNode Black left' value1 tree) rest
+
+  # The father is black and no nephew is red.
+  # Brother becomes red but the inequality of blackness is sustained. 
+  # ZipBlack recursively called on the father.
+  | Left Black value1 (Node {color = Red, left = left2,
+      value = value2, right = right2}) :: rest =>
+    zipBlack tree (Left Red value1 left2 :: Left Black value2 right2 :: rest)
+
+  # The father is black and no nephew is red.
+  # Brother becomes red but the inequality of blackness is sustained. 
+  # ZipBlack recursively called on the father.
+  | Right Black (Node {color = Red, left = left2, value = value2,
+      right = right2}) value1 :: rest =>
+    let rest' = Right Red right2 value1 :: Right Black left2 value2 :: rest in
+    zipBlack tree rest'
+
+  # Impossible
+  | Left _ _ Leaf :: _ => impossible ()
+
+  | Right _ Leaf _  :: _ => impossible ()
+
+ end
+
+# search splits tree according to compare function and builds zipper
+let rec search func tree zipper =
+  match tree with
+  | Leaf => (Leaf, zipper)
+  | Node {color, left, value, right} =>
+    match func value with
+    | Lt =>
+      search func left (Left color value right :: zipper)
+    | Gt =>
+      search func right (Right color left value  :: zipper)
+    | Eq => (tree, zipper)
+    end
+  end
+
+# serachMin finds smallest element in a tree and builds zipper
+let rec searchMin tree zipper =
+  match tree with
+  | Leaf => zipper
+  | Node {color, left, value, right} =>
+    searchMin left (Left color value right :: zipper)
+  end
+
+# serachMax finds largest element in a tree and builds zipper
+let rec searchMax tree zipper =
+  match tree with
+  | Leaf => zipper
+  | Node {color, left, value, right} =>
+    searchMax right (Right color left value:: zipper)
+  end
+
+{# Removes a node if one of the child is a Leaf and rebuilds tree
+# Precondition:
+#   (zip (Node (color, _, _, Leaf, child)) zipper) is a valid tree,
+#   or (zip (Node (color, _, _, child, Leaf)) zipper) is a valid tree.
+#}
+let deleteNearLeaf color child zipper =
+  match color with
+  {# child cannot be RED, by red-black invariant,
+     so it must be Leaf, by black-height invariant.
+  #}
+  | Red => zip Leaf zipper
+  | Black =>
+    match child with
+    | Node {value} =>
+      # Must be RED with Leaf children, by black-height invariant.
+      zip (makeNode Black Leaf value Leaf) zipper
+    | Leaf => zipBlack Leaf zipper
+    end
+  end
+
+{# Deletes node and adds children correctly to zipper and zip back the tree
+  Precondition:
+    zip (Node (color, _, _, left, right)) zipper is a valid tree.
+#}
+pub let delete color left right zipper =
+  match right with
+  | Leaf =>
+    match left with
+    | Leaf =>
+      match color with
+      | Red => zip Leaf zipper
+      | Black => zipBlack Leaf zipper
+      end
+    | _ =>
+      match searchMax left [] with
+      | Right colorLeftMin leftLeftMin valueLeftMin :: zipperr =>
+        deleteNearLeaf colorLeftMin leftLeftMin
+            (List.append zipperr (Left color valueLeftMin right :: zipper))
+      | _ => Leaf #Fail "postcondition"
+      end
+    end
+  | _ =>
+    match searchMin right [] with
+    | Left colorRightMin valueRightMin rightRightMin :: zipperr =>
+      deleteNearLeaf colorRightMin rightRightMin
+          (List.append zipperr (Right color left valueRightMin :: zipper))
+    | _ => Leaf #Fail "postcondition"
+    end
+  end
+
+# makes a root black
+pub let blacken tree =
+  match tree with
+  | Node {color = Red, size, left, value, right} =>
+    construct Black size left value right
+  | _ => tree
+  end
+
+# returns black height
+pub let rec blackHeight tree acc =
+  match tree with
+  | Leaf => acc
+  | Node {color=Red,left} => blackHeight left acc
+  | Node {color=Black,left} => blackHeight left (1 + acc)
+  end
+
+{#  precondition: blackHeight(tree) >= target >= 0
+    find a black subtree along the left/right spine whose black-height is
+    blackHeight(tree) - target.
+#}
+pub let rec searchHeight leftward target tree zipper =
+  match tree with
+  | Leaf => (Leaf, zipper)
+  | Node {color=Red,left,value,right} =>
+    if leftward then
+      searchHeight leftward target left (Left Red value right :: zipper)
+    else
+      searchHeight leftward target right (Right Red  left value :: zipper)
+  | Node {color=Black,left,value,right} =>
+    if 0 == target then
+      (tree,zipper)
+    else if leftward then
+      searchHeight leftward (target - 1) left
+          (Left Black value right :: zipper)
+    else
+      searchHeight leftward (target - 1) right
+          (Right Black left value :: zipper)
+  end
+
+# adds element to the tree
+pub let joinVal left value right =
+  # without loss of generality, assume left and right have black roots
+  let left = blacken left in
+  let right = blacken right in
+  let lbh = blackHeight left 0 in
+  let rbh = blackHeight right 0 in
+  if lbh == rbh then
+    makeNode Black left value right
+  else if lbh > rbh then
+    (let (_left, zipper) = searchHeight False (lbh-rbh) left [] in
+    # left' and right are both black and both have black height rbh 
+    zipRed value _left right zipper)
+  else
+    (let (_right, zipper) = searchHeight True (rbh-lbh) right [] in
+    # left and right' are both black and both have black height lbh 
+    zipRed value left _right zipper)
+
+# joins two trees
+pub let join left right =
+  match left with
+  | Leaf => right
+  | _ =>
+    match right with
+    | Leaf => left
+    | _ =>
+      match searchMax left [] with
+      | Right color  leftSmall value :: zipper =>
+        joinVal (deleteNearLeaf color leftSmall zipper) value right
+      |_  => left
+      end
+    end
+  end
+
+# Splits tree according to the function 
+pub let rec split compareWithPivot tree =
+  match tree with
+  | Leaf => (None,Leaf,Leaf)
+  | Node {left,value,right} =>
+    match compareWithPivot value with
+    | Eq => (Some value, left, right)
+    | Lt =>
+      let (_v, _l, _r) = split compareWithPivot left in
+      (_v, _l, joinVal _r value right)
+    | Gt => let (_v, _l, _r) = split compareWithPivot right in
+      (_v, joinVal left value  _l, _r)
+    end
+  end
+
+# Papers to read:
+# A dichromatic framework for balanced trees. Leo J. Guibas; Robert Sedgewick
+# DOI: 10.1109/SFCS.1978.3
+# Efficient implementation of red-black trees with split and catenate operations.
+# Ron Wein
+# Updating a balanced search tree in O(1) rotations. Robert Tarjan
+# DOI: 10.1016/0020-0190(83)90099-6
+# Similar implementation: 
+# https://github.com/standardml/cmlib/blob/master/red-black-tree.sml