diff --git a/book/BBT.balance.kind2 b/book/BBT.balance.kind2
new file mode 100644
index 00000000..f462453a
--- /dev/null
+++ b/book/BBT.balance.kind2
@@ -0,0 +1,100 @@
+BBT.balance
+: ∀(K: *)
+  ∀(V: *)
+  ∀(cmp: ∀(a: K) ∀(b: K) Cmp)
+  ∀(set_key: K)
+  ∀(node_key: K)
+  ∀(val: V)
+  ∀(lft: (BBT K V))
+  ∀(rgt: (BBT K V))
+  (BBT K V)
+= λK λV λcmp λset_key λnode_key λval λlft λrgt
+  let P   = λx(BBT K V)
+  let new = λlft.size λlft
+    let P   = λx(BBT K V)
+    let new = λrgt.size λrgt
+      let new_size = #(+ #1 (U60.max lft.size rgt.size))
+      let balance  = (U60.abs_diff lft.size rgt.size)
+      let P     = λx ∀(new_size: #U60) ∀(node_key: K) ∀(val: V) ∀(lft: (BBT K V)) ∀(rgt: (BBT K V)) (BBT K V)
+
+      // Unbalanced Trees
+      let true  = λnew_size λnode_key λval λlft λrgt
+        let P = λx ∀(K: *) ∀(V: *) ∀(cmp: ∀(a: K) ∀(b: K) Cmp) ∀(new_size: #U60) ∀(node_key: K) ∀(set_key: K) ∀(val: V) ∀(lft: (BBT K V)) ∀(rgt: (BBT K V)) (BBT K V)
+        let true  = BBT.balance.lft_heavier
+        let false = BBT.balance_rgt_heavier
+        ((~(U60.to_bool #(< rgt.size lft.size)) P true false) K V cmp new_size node_key set_key val lft rgt)
+      
+      // Balanced Trees
+      let false = λnew_size λnode_key λval λlft λrgt
+        (BBT.bin K V new_size node_key val lft rgt)
+
+      ((~(U60.to_bool #(> balance #1)) P true false) new_size node_key val lft rgt)
+    (~(BBT.got_size K V rgt) P new)
+  (~(BBT.got_size K V lft) P new)
+
+
+
+BBT.balance.lft_heavier
+: ∀(K: *)
+  ∀(V: *)
+  ∀(cmp: ∀(a: K) ∀(b: K) Cmp)
+  ∀(new_size: #U60)
+  ∀(node_key: K)
+  ∀(set_key: K)
+  ∀(val: V)
+  ∀(lft: (BBT K V))
+  ∀(rgt: (BBT K V))
+  (BBT K V)
+= λK λV λcmp λnew_size λnode_key λset_key λval λlft λrgt
+  let P = λx(BBT K V)
+  let bin = λlft.size λlft.key λlft.val λlft.lft λlft.rgt
+    let P     = λx ∀(new_size: #U60) ∀(key: K) ∀(val: V) ∀(lft.key: K) ∀(lft.val: V) ∀(lft.lft: (BBT K V)) ∀(lft.rgt: (BBT K V)) ∀(rgt: (BBT K V)) (BBT K V)
+
+    // key > lft.key
+    let true  = λnew_size λkey λval λlft.key λlft.val λlft.lft λlft.rgt λrgt  
+      let lft = (BBT.lft_rotate K V lft.size lft.key lft.val lft.lft lft.rgt)
+      (BBT.rgt_rotate K V new_size key val lft rgt)
+
+    // key < lft.key
+    let false = λnew_size λkey λval λlft.key λlft.val λlft.lft λlft.rgt λrgt  
+      let lft = (BBT.bin K V lft.size lft.key lft.val lft.lft lft.rgt)
+      (BBT.rgt_rotate K V new_size key val lft rgt)
+      
+    ((~(Cmp.is_gtn (cmp set_key lft.key)) P true false) new_size node_key val lft.key lft.val lft.lft lft.rgt rgt)
+
+  // unreachable case 
+  // Left can't be a tip and greater than right at the same time
+  let tip = (BBT.tip K V)
+  (~lft P bin tip)
+
+BBT.balance_rgt_heavier
+: ∀(K: *)
+  ∀(V: *)
+  ∀(cmp: ∀(a: K) ∀(b: K) Cmp)
+  ∀(new_size: #U60)
+  ∀(node_key: K)
+  ∀(set_key: K)
+  ∀(val: V)
+  ∀(lft: (BBT K V))
+  ∀(rgt: (BBT K V))
+  (BBT K V)
+= λK λV λcmp λnew_size λnode_key λset_key λval λlft λrgt  
+  let P = λx(BBT K V)
+  let bin = λrgt.size λrgt.key λrgt.val λrgt.lft λrgt.rgt
+    let P     = λx ∀(new_size: #U60) ∀(key: K) ∀(val: V) ∀(lft: (BBT K V)) ∀(rgt.key: K) ∀(rgt.val: V) ∀(rgt.lft: (BBT K V)) ∀(rgt.rgt: (BBT K V)) (BBT K V)
+      
+    // key > rgt.key
+    let true = λnew_size λkey λval λlft λrgt.key λrgt.val λrgt.lft λrgt.rgt  
+      let rgt = (BBT.bin K V rgt.size rgt.key rgt.val rgt.lft rgt.rgt)
+      (BBT.lft_rotate K V new_size key val lft rgt)
+
+    // key < rgt.key
+    let false = λnew_size λkey λval λlft λrgt.key λrgt.val λrgt.lft λrgt.rgt  
+      let rgt = (BBT.rgt_rotate K V rgt.size rgt.key rgt.val rgt.lft rgt.rgt)
+      (BBT.lft_rotate K V new_size key val lft rgt)
+    ((~(Cmp.is_gtn (cmp set_key rgt.key)) P true false) new_size node_key val lft rgt.key rgt.val rgt.lft rgt.rgt)
+  
+  // Unreachable case
+  // Right can't be a tip and greater than left at the same time
+  let tip = (BBT.tip K V)
+  (~rgt P bin tip)
\ No newline at end of file
diff --git a/book/BBT.bin.kind2 b/book/BBT.bin.kind2
new file mode 100644
index 00000000..88802c7b
--- /dev/null
+++ b/book/BBT.bin.kind2
@@ -0,0 +1,14 @@
+BBT.bin
+: ∀(K: *)
+  ∀(V: *)
+  ∀(size: #U60)
+  ∀(key: K)
+  ∀(val: V)
+  ∀(lft: (BBT K V))
+  ∀(rgt: (BBT K V))
+  (BBT K V)
+= λK λV λsize λkey λval λlft λrgt
+  ~λP λbin λtip
+  (bin size key val lft rgt)
+  
+  
diff --git a/book/BBT.get.kind2 b/book/BBT.get.kind2
new file mode 100644
index 00000000..08256f3b
--- /dev/null
+++ b/book/BBT.get.kind2
@@ -0,0 +1,17 @@
+BBT.get
+: ∀(K: *)
+  ∀(V: *)
+  ∀(cmp: ∀(a: K) ∀(b: K) Cmp)
+  ∀(key: K)
+  ∀(map: (BBT K V))
+  (Maybe V)
+= λK λV λcmp λkey λmap
+  let P = λx(Maybe V)
+  let bin = λ_size λnext.key λnext.val λnext.lft λnext.rgt
+    let P = λx ∀(cmp: ∀(a: K) ∀(b: K) Cmp) ∀(key: K) (Maybe V)
+    let ltn = λcmp λkey (BBT.get K V cmp key next.lft)
+    let eql = λcmp λkey (Maybe.some V next.val)
+    let gtn = λcmp λkey (BBT.get K V cmp key next.rgt)
+    ((~(cmp key next.key) P ltn eql gtn) cmp key)
+  let tip = (Maybe.none V)
+  (~map P bin tip)
\ No newline at end of file
diff --git a/book/BBT.got.kind2 b/book/BBT.got.kind2
new file mode 100644
index 00000000..bc12bcf9
--- /dev/null
+++ b/book/BBT.got.kind2
@@ -0,0 +1,32 @@
+// Returns a pair with the value and the new map
+BBT.got
+: ∀(K: *)
+  ∀(V: *)
+  ∀(cmp: ∀(a: K) ∀(b: K) Cmp)
+  ∀(key: K)
+  ∀(map: (BBT K V))
+  (Pair (Maybe V) (BBT K V))
+= λK λV λcmp λkey λmap
+  let P = λx(Pair (Maybe V) (BBT K V))
+  let bin = λsize λnext.key λnext.val λnext.lft λnext.rgt
+    let P = λx ∀(cmp: ∀(a: K) ∀(b: K) Cmp) ∀(key: K) (Pair (Maybe V) (BBT K V))
+    let ltn = λcmp λkey 
+      let new_pair = (BBT.got K V cmp key next.lft)
+      let P   = λx(Pair (Maybe V) (BBT K V))
+      let new = λval λlft
+        let map = (BBT.bin K V size next.key next.val lft next.rgt)
+        (Pair.new (Maybe V) (BBT K V) val map)
+      (~new_pair P new)
+    let eql = λcmp λkey
+      let map = (BBT.bin K V size next.key next.val next.lft next.rgt)
+      (Pair.new (Maybe V) (BBT K V) (Maybe.some V next.val) map)
+    let gtn = λcmp λkey 
+      let new_pair = (BBT.got K V cmp key next.rgt)
+      let P   = λx(Pair (Maybe V) (BBT K V))
+      let new = λval λrgt
+        let map = (BBT.bin K V size next.key next.val next.lft rgt)
+        (Pair.new (Maybe V) (BBT K V) val map)
+      (~new_pair P new)
+    ((~(cmp key next.key) P ltn eql gtn) cmp key)
+  let tip = (Pair.new (Maybe V) (BBT K V) (Maybe.none V) (BBT.tip K V))
+  (~map P bin tip)
\ No newline at end of file
diff --git a/book/BBT.got_size.kind2 b/book/BBT.got_size.kind2
new file mode 100644
index 00000000..13eb3aea
--- /dev/null
+++ b/book/BBT.got_size.kind2
@@ -0,0 +1,13 @@
+// Returns a pair with the size of the map and the reconstructed map
+BBT.got_size
+: ∀(K: *)
+  ∀(V: *)
+  ∀(map: (BBT K V))
+  (Pair #U60 (BBT K V))
+= λK λV λmap
+  let P = λx(Pair #U60 (BBT K V))
+  let bin = λsize λnext.key λnext.val λnext.lft λnext.rgt
+    let map = (BBT.bin K V size next.key next.val next.lft next.rgt)
+    (Pair.new #U60 (BBT K V) size map)
+  let tip = (Pair.new #U60 (BBT K V) #0 (BBT.tip K V))
+  (~map P bin tip)  
diff --git a/book/BBT.kind2 b/book/BBT.kind2
new file mode 100644
index 00000000..51efecad
--- /dev/null
+++ b/book/BBT.kind2
@@ -0,0 +1,10 @@
+BBT
+: ∀(K: *) // Key type
+  ∀(V: *) // Value type
+  *
+= λK λV
+  $self
+  ∀(P: ∀(bbt: (BBT K V)) *)
+  ∀(bin: ∀(size: #U60) ∀(key: K) ∀(val: V) ∀(lft: (BBT K V)) ∀(rgt: (BBT K V)) (P (BBT.bin K V size key val lft rgt)))
+  ∀(tip: (P (BBT.tip K V)))
+  (P self)
diff --git a/book/BBT.lft_rotate.kind2 b/book/BBT.lft_rotate.kind2
new file mode 100644
index 00000000..145f3a7a
--- /dev/null
+++ b/book/BBT.lft_rotate.kind2
@@ -0,0 +1,23 @@
+// b = (left ~ right.left)
+// a = (b ~ right.right)
+// return a
+BBT.lft_rotate
+: ∀(K: *)
+  ∀(V: *)
+  ∀(size: #U60)
+  ∀(key: K)
+  ∀(val: V)
+  ∀(lft: (BBT K V))
+  ∀(rgt: (BBT K V))
+  (BBT K V)
+= λK λV λsize λkey λval λlft λrgt
+  let P   = λx ∀(key: K) ∀(val: V) ∀(lft: (BBT K V)) (BBT K V)
+  let bin = λ_size λrgt.key λrgt.val λrgt.lft λrgt.rgt 
+            λkey λval λlft  
+    let b = (BBT.new_node K V key     val     lft rgt.lft)
+    let a = (BBT.new_node K V rgt.key rgt.val b   rgt.rgt)
+    a
+  let tip = 
+            λkey λval λlft  
+    (BBT.bin K V size key val lft (BBT.tip K V))
+  ((~rgt P bin tip) key val lft)
diff --git a/book/BBT.new_node.kind2 b/book/BBT.new_node.kind2
new file mode 100644
index 00000000..07c958c9
--- /dev/null
+++ b/book/BBT.new_node.kind2
@@ -0,0 +1,18 @@
+// Creates a new node with size = 1 + (max lft.size rgt.size)
+ BBT.new_node
+: ∀(K: *)
+  ∀(V: *)
+  ∀(key: K)
+  ∀(val: V)
+  ∀(lft: (BBT K V))
+  ∀(rgt: (BBT K V))
+  (BBT K V)
+= λK λV λkey λval λlft λrgt
+  let P   = λx(BBT K V)
+  let new = λlft.size λlft
+    let P   = λx(BBT K V)
+    let new = λrgt.size λrgt
+      let new_size = #(+ #1 (U60.max rgt.size lft.size))
+      (BBT.bin K V new_size key val lft rgt)
+    (~(BBT.got_size K V rgt) P new)
+  (~(BBT.got_size K V lft) P new)
\ No newline at end of file
diff --git a/book/BBT.rgt_rotate.kind2 b/book/BBT.rgt_rotate.kind2
new file mode 100644
index 00000000..71723b0f
--- /dev/null
+++ b/book/BBT.rgt_rotate.kind2
@@ -0,0 +1,23 @@
+// b = (left.right ~ right)
+// a = (left.left ~ b)
+// return a
+BBT.rgt_rotate
+: ∀(K: *)
+  ∀(V: *)
+  ∀(size: #U60)
+  ∀(key: K)
+  ∀(val: V)
+  ∀(lft: (BBT K V))
+  ∀(rgt: (BBT K V))
+  (BBT K V)
+= λK λV λsize λkey λval λlft λrgt
+  let P   = λx ∀(key: K) ∀(val: V) ∀(rgt: (BBT K V)) (BBT K V)
+  let bin = λ_size λlft.key λlft.val λlft.lft λlft.rgt 
+            λkey λval λrgt  
+    let b = (BBT.new_node K V  key     val     lft.rgt rgt)
+    let a = (BBT.new_node K V  lft.key lft.val lft.lft b  )
+    a
+  let tip = 
+            λkey λval λrgt  
+    (BBT.bin K V size key val (BBT.tip K V) rgt)
+  ((~lft P bin tip) key val rgt)
diff --git a/book/BBT.set.kind2 b/book/BBT.set.kind2
new file mode 100644
index 00000000..268bf815
--- /dev/null
+++ b/book/BBT.set.kind2
@@ -0,0 +1,34 @@
+BBT.set
+: ∀(K: *)
+  ∀(V: *)
+  ∀(cmp: ∀(a: K) ∀(b: K) Cmp)
+  ∀(key: K)
+  ∀(val: V)
+  ∀(map: (BBT K V))
+  (BBT K V)
+= λK λV λcmp λkey λval λmap
+  let P = λx ∀(key: K) ∀(val: V) (BBT K V)
+  let bin = λsize λnext.key λnext.val λnext.lft λnext.rgt λkey λval     
+    let P = λx ∀(key: K) ∀(next.key: K) ∀(next.val: V) ∀(next.lft: (BBT K V)) ∀(next.rgt: (BBT K V)) (BBT K V)
+    
+    // Go left
+    let ltn = λkey λnext.key  λnext.val λnext.lft λnext.rgt
+      let new_lft = (BBT.set K V cmp key val next.lft)
+      (BBT.balance K V cmp key next.key next.val new_lft next.rgt)
+
+    // Same key, update value
+    // Should we update the value or return the same tree?
+    let eql = λkey λnext.key λnext.val λnext.lft λnext.rgt
+      (BBT.bin K V size next.key val next.lft next.rgt)
+
+    // Go right
+    let gtn = λkey λnext.key λnext.val λnext.lft λnext.rgt
+      let new_rgt = (BBT.set K V cmp key val next.rgt)
+      (BBT.balance K V cmp key next.key next.val next.lft new_rgt)
+    ((~(cmp key next.key) P ltn eql gtn) key next.key next.val next.lft next.rgt)
+
+  // Empty tree, create new node
+  let tip = λkey λval 
+    (BBT.singleton K V key val)
+  ((~map P bin tip) key val)
+
diff --git a/book/BBT.singleton.kind2 b/book/BBT.singleton.kind2
new file mode 100644
index 00000000..60ae49bb
--- /dev/null
+++ b/book/BBT.singleton.kind2
@@ -0,0 +1,8 @@
+BBT.singleton
+: ∀(K: *)
+  ∀(V: *)
+  ∀(key: K)
+  ∀(val: V)
+  (BBT K V)
+= λK λV λkey λval
+  (BBT.bin K V #1 key val (BBT.tip K V) (BBT.tip K V))
\ No newline at end of file
diff --git a/book/BBT.tip.kind2 b/book/BBT.tip.kind2
new file mode 100644
index 00000000..a8a2737d
--- /dev/null
+++ b/book/BBT.tip.kind2
@@ -0,0 +1,8 @@
+BBT.tip
+: ∀(K: *)
+  ∀(V: *)
+  (BBT K V)
+= λK λV
+  ~λP λbin λtip
+  tip
+
diff --git a/book/Cmp.eql.kind2 b/book/Cmp.eql.kind2
new file mode 100644
index 00000000..b478903d
--- /dev/null
+++ b/book/Cmp.eql.kind2
@@ -0,0 +1,4 @@
+Cmp.eql
+: Cmp
+= ~λP λltn λeql λgtn
+  eql
\ No newline at end of file
diff --git a/book/Cmp.gtn.kind2 b/book/Cmp.gtn.kind2
new file mode 100644
index 00000000..cd359d8e
--- /dev/null
+++ b/book/Cmp.gtn.kind2
@@ -0,0 +1,4 @@
+Cmp.gtn
+: Cmp
+= ~λP λltn λeql λgtn
+  gtn
\ No newline at end of file
diff --git a/book/Cmp.is_gtn.kind2 b/book/Cmp.is_gtn.kind2
new file mode 100644
index 00000000..a8bc5c8b
--- /dev/null
+++ b/book/Cmp.is_gtn.kind2
@@ -0,0 +1,9 @@
+Cmp.is_gtn
+: ∀(cmp: Cmp)
+  Bool
+= λcmp
+  let P = λx(Bool)
+  let ltn = Bool.false
+  let eql = Bool.false
+  let gtn = Bool.true
+  (~cmp P ltn eql gtn)
\ No newline at end of file
diff --git a/book/Cmp.kind2 b/book/Cmp.kind2
new file mode 100644
index 00000000..d1b99af1
--- /dev/null
+++ b/book/Cmp.kind2
@@ -0,0 +1,8 @@
+Cmp
+: *
+= $self
+  ∀(P: ∀(cmp: Cmp) *)
+  ∀(ltn: (P Cmp.ltn))
+  ∀(eql: (P Cmp.eql))
+  ∀(gtn: (P Cmp.gtn))
+  (P self)
\ No newline at end of file
diff --git a/book/Cmp.ltn.kind2 b/book/Cmp.ltn.kind2
new file mode 100644
index 00000000..6e9655d6
--- /dev/null
+++ b/book/Cmp.ltn.kind2
@@ -0,0 +1,4 @@
+Cmp.ltn
+: Cmp
+= ~λP λltn λeql λgtn
+  ltn
diff --git a/book/String.Map.kind2 b/book/String.Map.kind2
index b465499e..577087a9 100644
--- a/book/String.Map.kind2
+++ b/book/String.Map.kind2
@@ -25,3 +25,41 @@ String.Map.new
 : ∀(V: *)
   (String.Map V)
 = λV (List.Map.new String V)
+
+// BBT Version
+
+// String.Map 
+// :  ∀(V: *) 
+//    *
+// = λV (BBT String V)
+
+// String.Map.get
+// : ∀(V: *)
+//   ∀(key: String)
+//   ∀(map: (String.Map V))
+//   (Maybe V)
+// = λV λkey λmap
+//   (BBT.get String V String.cmp key map)
+
+// String.Map.got 
+// : ∀(V: *)
+//   ∀(key: String)
+//   ∀(map: (String.Map V))
+//   (Pair (Maybe V) (String.Map V))
+// = λV λkey λmap
+//   (BBT.got String V String.cmp key map)
+
+// String.Map.set
+// : ∀(V: *)
+//   ∀(key: String)
+//   ∀(val: V)
+//   ∀(map: (String.Map V))
+//   (String.Map V)
+// = λV λkey λval λmap
+//   (BBT.set String V String.cmp key val map)
+
+// String.Map.new
+// :  ∀(V: *)
+//   (String.Map V)
+// = λV (BBT.tip String V)
+
diff --git a/book/String.cmp.kind2 b/book/String.cmp.kind2
new file mode 100644
index 00000000..1f33e9d3
--- /dev/null
+++ b/book/String.cmp.kind2
@@ -0,0 +1,22 @@
+String.cmp
+: ∀(a: String)
+  ∀(b: String)
+  Cmp
+= λa λb
+  let P    = λx ∀(b: String) (Cmp)
+  let cons = λa.head λa.tail λb
+    let P    = λx ∀(a.head: Char) ∀(a.tail: String) (Cmp)
+    let cons = λb.head λb.tail λa.head λa.tail
+      let P = λx Cmp
+      let ltn = Cmp.ltn
+      let eql = (String.cmp a.tail b.tail)
+      let gtn = Cmp.gtn
+      (~(U60.cmp a.head b.head) P ltn eql gtn)
+    let nil  = λa.head λa.tail Cmp.gtn
+    ((~b P cons nil) a.head a.tail)
+  let nil  = λb
+    let P    = λx Cmp
+    let cons = λb.head λb.tail Cmp.ltn
+    let nil  = Cmp.eql
+    (~b P cons nil)
+  (~a P cons nil b)
\ No newline at end of file
diff --git a/book/U60.Map.kind2 b/book/U60.Map.kind2
index ee14a2a3..5503d47f 100644
--- a/book/U60.Map.kind2
+++ b/book/U60.Map.kind2
@@ -1,3 +1,4 @@
+
 // Temporarily just a list of key/val
 
 U60.Map
@@ -25,3 +26,41 @@ U60.Map.new
 : ∀(V: *)
   (U60.Map V)
 = λV (List.Map.new #U60 V)
+
+
+// BBT Version
+
+// U60.Map
+// : ∀(V: *)
+//   *
+// = λV (BBT #U60 V)
+
+// U60.Map.get
+// : ∀(V: *)
+//   ∀(key: #U60)
+//   ∀(map: (U60.Map V))
+//   (Maybe V)
+// = λV λkey λmap
+//   (BBT.get #U60 V U60.cmp key map)
+
+// U60.Map.got
+// : ∀(V: *)
+//   ∀(key: #U60)
+//   ∀(map: (U60.Map V))
+//   (Pair (Maybe V) (U60.Map V))
+// = λV λkey λmap
+//   (BBT.got #U60 V U60.cmp key map)
+
+// U60.Map.set
+// : ∀(V: *)
+//   ∀(key: #U60)
+//   ∀(val: V)
+//   ∀(map: (U60.Map V))
+//   (U60.Map V)
+// = λV λkey λval λmap
+//   (BBT.set #U60 V U60.cmp key val map)
+
+// U60.Map.new
+// : ∀(V: *)
+//   (U60.Map V)
+// = λV (BBT.tip #U60 V)
diff --git a/book/U60.abs_diff.kind2 b/book/U60.abs_diff.kind2
new file mode 100644
index 00000000..0380546a
--- /dev/null
+++ b/book/U60.abs_diff.kind2
@@ -0,0 +1,10 @@
+// Returns the absolute difference between two U60s
+U60.abs_diff
+: ∀(a: #U60)
+  ∀(b: #U60)
+  #U60
+= λa λb
+  let P = λx(#U60)
+  let true  = #(- b a)
+  let false = #(- a b)
+  (~(U60.to_bool #(< a b)) P true false)
\ No newline at end of file
diff --git a/book/U60.cmp.kind2 b/book/U60.cmp.kind2
new file mode 100644
index 00000000..530f233f
--- /dev/null
+++ b/book/U60.cmp.kind2
@@ -0,0 +1,7 @@
+U60.cmp
+: ∀(a: #U60)
+  ∀(b: #U60)
+  (Cmp)
+= λa λb
+  (U60.if #(== a b) Cmp (U60.if #(< a b) Cmp Cmp.gtn Cmp.ltn) Cmp.eql)
+ 
\ No newline at end of file
diff --git a/book/U60.max.kind2 b/book/U60.max.kind2
new file mode 100644
index 00000000..7d289348
--- /dev/null
+++ b/book/U60.max.kind2
@@ -0,0 +1,6 @@
+U60.max
+: ∀(a: #U60)
+  ∀(b: #U60)
+  #U60
+= λa λb
+  (~(U60.to_bool #(> a b)) λx(#U60) a b)
diff --git a/book/U60.min.kind2 b/book/U60.min.kind2
new file mode 100644
index 00000000..a1515e7b
--- /dev/null
+++ b/book/U60.min.kind2
@@ -0,0 +1,6 @@
+U60.min
+: ∀(a: #U60)
+  ∀(b: #U60)
+  #U60
+= λa λb
+  (~(U60.to_bool #(< a b)) λx(#U60) a b)
\ No newline at end of file
diff --git a/book/test6.kind2 b/book/test6.kind2
index 11f74006..fa05fb37 100644
--- a/book/test6.kind2
+++ b/book/test6.kind2
@@ -2,4 +2,3 @@ test6
 : Nat
 = (Nat.succ (Nat.succ (Nat.succ Nat.zero)))
 
-
diff --git a/book/testBBT.kind2 b/book/testBBT.kind2
new file mode 100644
index 00000000..93ccef0f
--- /dev/null
+++ b/book/testBBT.kind2
@@ -0,0 +1,179 @@
+// Add_spaces
+// : ∀(n: #U60)
+//   (String)
+// = λn
+//   (U60.if #(== n #0) String (String.concat "  " (Add_spaces #(- n #1))) "")
+
+// U60.Map_show
+// : ∀(map: (U60.Map String))
+//   ∀(depth: #U60)
+//   (String)
+// = λmap λdepth
+//   let P = λx(String)
+//   let bin = λsize λkey λval λlft λrgt
+//     let cct = λa λb (String.concat a b)
+//     let spc = λx (cct (Add_spaces depth) x)
+//     let nnl = λx (cct String.newline x)
+//     let key  = (U60.show key)
+//     let size = (U60.show size)
+//     let a = (nnl (spc (cct "key: " key)))
+//     let b = (cct ", size: " size)
+//     let c = (cct ", value: " val)
+//     let d = (nnl (spc (cct "left: " (U60.Map_show lft #(+ #1 depth)))))
+//     let e = (nnl (spc (cct "right: " (U60.Map_show rgt #(+ #1 depth)))))
+//     (cct a (cct b (cct c (cct d e ))))
+//   let tip = ""
+//   (~map P bin tip)
+
+// U60.Map.gen
+// : ∀(V: *)
+//   ∀(to_val: ∀(n: #U60) V)
+//   ∀(n: #U60)
+//   (U60.Map V)
+// = λV λto_val λn
+//   (U60.Map.gen.go V to_val n (U60.Map.new V))
+
+// U60.Map.gen.go
+// : ∀(V: *)
+//   ∀(to_val: ∀(n: #U60) V)
+//   ∀(n: #U60)
+//   ∀(map: (U60.Map V))
+//   (U60.Map V)
+// = λV λto_val λn λmap
+//   let P     = λx ∀(map: (U60.Map String)) (U60.Map String)
+//   let true  = λmap (U60.Map.set String n (to_val n) map)
+//   let false = λmap (U60.Map.gen.go V to_val #(- n #1) (U60.Map.set String n (to_val n) map))
+//   ((~(U60.to_bool #(== n #0)) P true false) map)
+
+
+// U60.fold
+// : ∀(A: *)
+//   ∀(f: ∀(n: #U60) ∀(acc: A) A)
+//   ∀(nil: A)
+//   ∀(n: #U60)
+//   A
+// = λA λf λnil λn
+//   (U60.fold.go A f nil n)
+
+// U60.fold.go
+// : ∀(A: *)
+//   ∀(f: ∀(n: #U60) ∀(acc: A) A)
+//   ∀(acc: A)
+//   ∀(n: #U60)
+//   A
+// = λA λf λacc λn
+//   (~(U60.to_bool n) λx(A) (U60.fold.go A f (f n acc) #(- n #1)) acc)
+
+
+// AscendingMap
+// : (U60.Map #U60)
+// = 
+//   let nil = (U60.Map.new #U60)
+//   let f = λn λacc (U60.Map.set #U60 #(- #11 n) #(- #11 n) acc)
+//   (U60.fold (U60.Map #U60) f nil #10)
+
+// DescendingMap
+// : (U60.Map #U60)
+// = 
+//   let nil = (U60.Map.new #U60)
+//   let f = λn λacc (U60.Map.set #U60 #(+ n #0) n acc)
+//   (U60.fold (U60.Map #U60) f nil #10)
+
+// U60.Map.sum
+// : ∀(map: (U60.Map #U60))
+//   (#U60)
+// = λmap
+//   let P = λx(#U60)
+//   let bin = λsize λkey λval λlft λrgt
+//     let sum = #(+ #(+ key (U60.Map.sum lft)) (U60.Map.sum rgt))
+//     sum
+//   let tip = #0 
+//   (~map P bin tip)
+
+// Test1
+// : (Maybe String)
+// = 
+//   let emptyMap   = (BBT.tip #U60 String)
+//   let updatedMap = (U60.Map.set String #5 "value5" emptyMap)
+//   let value      = (U60.Map.get String #5 updatedMap)
+//   let is_equal   = (String.equal (~value λx(String) λsome(some) "none") "value5")
+//   (~is_equal λx(Maybe String) (Maybe.none String) (Maybe.some String "Test 1 Failed!"))
+
+// Test2
+// : (Maybe String)
+// = 
+//   let initialMap = (U60.Map.set String #10 "initialValue" (U60.Map.new String))
+//   let updatedMap = (U60.Map.set String #10 "updatedValue" initialMap)
+//   let value      = (U60.Map.get String #10 updatedMap)
+//   let is_equal   = (String.equal (~value λx(String) λsome(some) "none") "updatedValue")
+//   (~is_equal λx(Maybe String) (Maybe.none String) (Maybe.some String "Test 2 Failed!"))
+
+// Test3
+// : (Maybe String)
+// = 
+//   let map = (U60.Map.gen String U60.show #24)
+//   let value = (U60.Map.get String #7 map)
+//   let is_equal = (String.equal (~value λx(String) λsome(some) "none") "7")
+//   (~is_equal λx(Maybe String) (Maybe.none String) (Maybe.some String "Test 3 Failed!"))
+
+// Test4
+// : (Maybe String)
+// = 
+//   let map = (U60.Map.gen String U60.show #5) 
+//   let value = (U60.Map.get String #6 map) 
+//   let is_none = (~value λx(Bool) λval(Bool.false) Bool.true) 
+//   (~is_none λx(Maybe String) (Maybe.none String) (Maybe.some String "Test 4 Failed!"))
+
+// Test5
+// : (Maybe String)
+// = 
+//   let map = AscendingMap 
+//   let sum = (U60.Map.sum map) 
+//   let expected_sum = #55 
+//   let is_equal = (U60.equal sum expected_sum) 
+//   (~is_equal λx(Maybe String) (Maybe.none String) (Maybe.some String "Test 5 Failed!"))
+
+// Test6
+// : (Maybe String)
+// = 
+//   let map = (U60.Map.gen #U60 λx(x) #20) 
+//   let new = λfirst_value λmap
+//     let new = λlast_value λmap
+//       let is_first_correct = (U60.equal (~first_value λx(#U60) λsome(some) #0) #3) 
+//       let is_last_correct  = (U60.equal (~last_value λx(#U60) λsome(some) #0) #10) 
+//       let are_both_correct = (Bool.and is_first_correct is_last_correct) 
+//       (~are_both_correct λx(Maybe String) (Maybe.none String) (Maybe.some String "Test 6 Failed!"))
+//     (~(U60.Map.got #U60 #10 map) λx(Maybe String) new)
+//   (~(U60.Map.got #U60 #3 map) λx(Maybe String) new)
+
+
+// Tests.run
+// : ∀(tests: (List (Maybe String)))
+//   String
+// = λtests
+//   let folder = (List.fold (Maybe String) tests)
+//   (folder String (λhead λtail (~head λx(String) λsome(some) tail)) "All tests passed!")
+
+// RunTests
+// : (String)
+// =
+//   let tests = (List.nil (Maybe String))
+//   let tests = (List.cons (Maybe String) Test1 tests)
+//   let tests = (List.cons (Maybe String) Test2 tests)
+//   let tests = (List.cons (Maybe String) Test3 tests)
+//   let tests = (List.cons (Maybe String) Test4 tests)
+//   let tests = (List.cons (Maybe String) Test5 tests)
+//   let tests = (List.cons (Maybe String) Test6 tests)
+//   let solution = (Tests.run tests)
+//   solution
+
+testBBT
+: String
+= 
+"
+File commented for backward compatibility.
+To run the tests, uncomment the code on:
+  testBBT.kind2
+  U60.Map
+"
+  // RunTests