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.from_list.kind2 b/book/BBT.from_list.kind2
new file mode 100644
index 00000000..a6dd7fb4
--- /dev/null
+++ b/book/BBT.from_list.kind2
@@ -0,0 +1,14 @@
+BBT.from_list
+: ∀(K: *)
+  ∀(V: *)
+  ∀(cmp: ∀(a: K) ∀(b: K) Cmp)
+  ∀(list: (List (Pair K V)))
+  (BBT K V)
+= λK λV λcmp λlist
+  let P    = λx(BBT K V)
+  let cons = λhead λtail
+    let P   = λx(BBT K V)
+    let new = λkey λval (BBT.set K V cmp key val (BBT.from_list K V cmp tail))
+    (~head P new)
+  let nil  = (BBT.tip K V)
+  (~list P cons nil)
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.has.kind2 b/book/BBT.has.kind2
new file mode 100644
index 00000000..afad16e9
--- /dev/null
+++ b/book/BBT.has.kind2
@@ -0,0 +1,17 @@
+BBT.has
+: ∀(K: *)
+  ∀(V: *)
+  ∀(cmp: ∀(a: K) ∀(b: K) Cmp)
+  ∀(key: K)
+  ∀(map: (BBT K V))
+  Bool
+= λK λV λcmp λkey λmap
+  let P = λx Bool
+  let bin = λnext.size λnext.key λnext.val λnext.lft λnext.rgt
+    let P = λx ∀(cmp: ∀(a: K) ∀(b: K) Cmp) ∀(key: K) Bool
+    let ltn = λcmp λkey (BBT.has K V cmp key next.lft)
+    let eql = λcmp λkey Bool.true
+    let gtn = λcmp λkey (BBT.has K V cmp key next.rgt)
+    ((~(cmp key next.key) P ltn eql gtn) cmp key)
+  let tip = Bool.false
+  (~map P bin tip)
diff --git a/book/BBT.has.linear.kind2 b/book/BBT.has.linear.kind2
new file mode 100644
index 00000000..48301fc3
--- /dev/null
+++ b/book/BBT.has.linear.kind2
@@ -0,0 +1,32 @@
+// Returns a Pair with the boolean (indicating if the key is present) and the original map
+BBT.has.linear
+: ∀(K: *)
+  ∀(V: *)
+  ∀(cmp: ∀(a: K) ∀(b: K) Cmp)
+  ∀(key: K)
+  ∀(map: (BBT K V))
+  (Pair Bool (BBT K V))
+= λK λV λcmp λkey λmap
+  let P = λx(Pair Bool (BBT K V))
+  let bin = λsize λnode_key λval λlft λrgt
+    let P = λx ∀(cmp: ∀(a: K) ∀(b: K) Cmp) ∀(key: K) ∀(lft: (BBT K V)) ∀(rgt: (BBT K V)) (Pair Bool (BBT K V))
+    let ltn = λcmp λsize λhas_key λval λlft λrgt λhas_key
+      let P = λx (Pair Bool (BBT K V))
+      let new = λbool λlft 
+        let map = (BBT.bin K V size node_key val lft rgt)
+        (Pair.new Bool (BBT K V) bool map)
+      (~(BBT.has.linear K V cmp has_key lft) P new)
+    let eql = λcmp λsize λkey λval λlft λrgt λhas_key
+      (Pair.new Bool (BBT K V) Bool.true (BBT.bin K V size node_key val lft rgt))
+
+    let gtn = λcmp λsize λkey λval λlft λrgt λhas_key
+      let P = λx (Pair Bool (BBT K V))
+      let new = λbool λrgt 
+        let map = (BBT.bin K V size node_key val lft rgt)
+        (Pair.new Bool (BBT K V) bool rgt)
+      (~(BBT.has.linear K V cmp has_key rgt) P new)
+
+    ((~(cmp key node_key) P ltn eql gtn) cmp size node_key val lft rgt key)
+
+  let tip = (Pair.new Bool (BBT K V) Bool.false (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/BBT.to_list.kind2 b/book/BBT.to_list.kind2
new file mode 100644
index 00000000..23be5b47
--- /dev/null
+++ b/book/BBT.to_list.kind2
@@ -0,0 +1,15 @@
+BBT.to_list
+: ∀(K: *)
+  ∀(V: *)
+  ∀(map: (BBT K V))
+  (List (Pair K V))
+= λK λV λmap
+  let P = λx(List (Pair K V))
+  let bin = λsize λkey λval λlft λrgt
+    let lft = (BBT.to_list K V lft)
+    let rgt = (BBT.to_list K V rgt)
+    let pair = (Pair.new K V key val)
+    let list = (List.cons (Pair K V) pair (List.concat (Pair K V) lft rgt))
+    list
+  let tip = (List.nil (Pair K V))
+  (~map P bin tip)
diff --git a/book/Bool.show.kind2 b/book/Bool.show.kind2
new file mode 100644
index 00000000..585020ce
--- /dev/null
+++ b/book/Bool.show.kind2
@@ -0,0 +1,8 @@
+Bool.show
+: ∀(x: Bool)
+  String
+= λx
+  let P     = λx(String)
+  let true  = "true"
+  let false = "false"
+  (~x P true false)
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/Kind.API.file.kind2 b/book/Kind.API.file.kind2
deleted file mode 100644
index fd24bfd1..00000000
--- a/book/Kind.API.file.kind2
+++ /dev/null
@@ -1,5 +0,0 @@
-Kind.API.file
-: ∀(name: String)
-  String
-= λname
-  (String.concat name ".kind2")
diff --git a/book/Kind.API.load.kind2 b/book/Kind.API.load.kind2
deleted file mode 100644
index 21979576..00000000
--- a/book/Kind.API.load.kind2
+++ /dev/null
@@ -1,6 +0,0 @@
-// TODO
-Kind.API.load
-: ∀(name: String)
-  Kind.Book
-= λname
-  (Kind.API.load.one name)
diff --git a/book/Kind.API.load.one.kind2 b/book/Kind.API.load.one.kind2
deleted file mode 100644
index dafa7c91..00000000
--- a/book/Kind.API.load.one.kind2
+++ /dev/null
@@ -1,6 +0,0 @@
-Kind.API.load.one
-: ∀(name: String)
-  Kind.Book
-= λname
-  (HVM.load Kind.Book (Kind.API.file name) λdata
-  (Kind.Book.parse data))
diff --git a/book/Kind.Book.String.cons.kind2 b/book/Kind.Book.String.cons.kind2
index 6267c687..dcc461a4 100644
--- a/book/Kind.Book.String.cons.kind2
+++ b/book/Kind.Book.String.cons.kind2
@@ -1,3 +1,3 @@
 Kind.Book.String.cons
 : Kind.Term
-= (Kind.hol "TODO" (List.nil Kind.Term))
\ No newline at end of file
+= (Kind.hol "TODO" (List.nil Kind.Term))
diff --git a/book/Kind.Book.get_refs.go.kind2 b/book/Kind.Book.get_refs.go.kind2
index 5fb87437..51cc2633 100644
--- a/book/Kind.Book.get_refs.go.kind2
+++ b/book/Kind.Book.get_refs.go.kind2
@@ -1,5 +1,5 @@
 Kind.Book.get_refs.go
-: ∀(book: Kind.Book)
+: ∀(book: (List (Pair String Kind.Term)))
   (List.Concatenator String)
 = λbook
   let P    = λx (List.Concatenator String)
diff --git a/book/Kind.Book.get_refs.kind2 b/book/Kind.Book.get_refs.kind2
index 984c4520..ed4bf6e1 100644
--- a/book/Kind.Book.get_refs.kind2
+++ b/book/Kind.Book.get_refs.kind2
@@ -2,4 +2,6 @@ Kind.Book.get_refs
 : ∀(book: Kind.Book)
   (List String)
 = λbook
-  (List.Concatenator.build String (Kind.Book.get_refs.go book))
+  (List.Concatenator.build String
+  (Kind.Book.get_refs.go
+  (String.Map.to_list Kind.Term book)))
diff --git a/book/Kind.Book.kind2 b/book/Kind.Book.kind2
index eaf01742..d69e945c 100644
--- a/book/Kind.Book.kind2
+++ b/book/Kind.Book.kind2
@@ -1,3 +1,3 @@
 Kind.Book
 : *
-= (String.Map Kind.Term)
\ No newline at end of file
+= (String.Map Kind.Term)
diff --git a/book/Kind.Book.parse.kind2 b/book/Kind.Book.parse.kind2
index 9a1671fc..54d8d900 100644
--- a/book/Kind.Book.parse.kind2
+++ b/book/Kind.Book.parse.kind2
@@ -4,5 +4,5 @@ Kind.Book.parse
 = λcode
   let P    = λx(Kind.Book)
   let done = λcode λbook book
-  let fail = λerror (List.nil (Pair String Kind.Term))
+  let fail = λerror (String.Map.new Kind.Term)
   (~(Kind.Book.parser code) P done fail)
diff --git a/book/Kind.Book.parser.kind2 b/book/Kind.Book.parser.kind2
index 2f92093d..09163741 100644
--- a/book/Kind.Book.parser.kind2
+++ b/book/Kind.Book.parser.kind2
@@ -25,4 +25,4 @@ Kind.Book.parser
       (Parser.bind Kind.Book Kind.Book Kind.Book.parser λbook
       (Parser.pure Kind.Book (String.Map.set Kind.Term nam (val (List.nil Kind.Binder)) book)))))
     (~ann P true false)))
-  (~is_eof P true false))
\ No newline at end of file
+  (~is_eof P true false))
diff --git a/book/Kind.Book.show.go.kind2 b/book/Kind.Book.show.go.kind2
index 803309ea..52a81965 100644
--- a/book/Kind.Book.show.go.kind2
+++ b/book/Kind.Book.show.go.kind2
@@ -1,5 +1,5 @@
 Kind.Book.show.go
-: ∀(book: Kind.Book)
+: ∀(book: (List (Pair String Kind.Term)))
   String.Concatenator
 = λbook
   let P    = λx String.Concatenator
@@ -14,4 +14,4 @@ Kind.Book.show.go
       nil)))))))))
     (~head P new)
   let nil  = λnil nil
-  (~book P cons nil)
\ No newline at end of file
+  (~book P cons nil)
diff --git a/book/Kind.Book.show.kind2 b/book/Kind.Book.show.kind2
index 245398f4..ff182240 100644
--- a/book/Kind.Book.show.kind2
+++ b/book/Kind.Book.show.kind2
@@ -2,4 +2,4 @@ Kind.Book.show
 : ∀(book: Kind.Book)
   String
 = λbook
-  (String.Concatenator.build (Kind.Book.show.go book))
\ No newline at end of file
+  (String.Concatenator.build (Kind.Book.show.go (String.Map.to_list Kind.Term book)))
diff --git a/book/Kind.Book.to_hvm.go.kind2 b/book/Kind.Book.to_hvm.go.kind2
index 282b1b27..4fca45d1 100644
--- a/book/Kind.Book.to_hvm.go.kind2
+++ b/book/Kind.Book.to_hvm.go.kind2
@@ -1,5 +1,5 @@
 Kind.Book.to_hvm.go
-: ∀(book: Kind.Book)
+: ∀(book: (List (Pair String Kind.Term)))
   String.Concatenator
 = λbook
   let P    = λx String.Concatenator
diff --git a/book/Kind.Book.to_hvm.kind2 b/book/Kind.Book.to_hvm.kind2
index d0686f95..7c100f47 100644
--- a/book/Kind.Book.to_hvm.kind2
+++ b/book/Kind.Book.to_hvm.kind2
@@ -2,4 +2,6 @@ Kind.Book.to_hvm
 : ∀(book: Kind.Book)
   String
 = λbook
-  (String.Concatenator.build (Kind.Book.to_hvm.go book))
+  (String.Concatenator.build
+  (Kind.Book.to_hvm.go
+  (String.Map.to_list Kind.Term book)))
diff --git a/book/Kind.load.kind2 b/book/Kind.load.kind2
new file mode 100644
index 00000000..b20d6827
--- /dev/null
+++ b/book/Kind.load.kind2
@@ -0,0 +1,118 @@
+
+//// TODO
+//Kind.load
+//: ∀(name: String)
+  //Kind.Book
+//= λname
+  //(Kind.load.name #5 name (String.Map.new Kind.Term))
+
+//// Gets the source file of a definition
+//Kind.load.file_of
+//: ∀(name: String)
+  //String
+//= λname
+  //(String.concat name ".kind2")
+
+//// Loads a file into a new book
+//Kind.load.file
+//: ∀(file: String)
+  //Kind.Book
+//= λfile
+  //(HVM.load Kind.Book file λdata
+  //(Kind.Book.parse data))
+
+//// Loads a name into a book
+//Kind.load.name
+//: ∀(lims: #U60)
+  //∀(name: String)
+  //∀(book: Kind.Book)
+  //Kind.Book
+//= λlims
+  //(HVM.log #U60 ∀(name:String)∀(book:Kind.Book)Kind.Book lims
+  //#match lims = lims {
+    //#0: λname λbook book
+    //#+: λname λbook
+      //(HVM.print Kind.Book (String.concat "LOAD:" name)
+      //// Checks if name is already on book
+      //let P   = λx (Kind.Book)
+      //let new = λhas λbook
+        //// If it is, do nothing; otherwise, define it
+        //let P     = λx ∀(book: Kind.Book) (Kind.Book)
+        //let true  = λbook
+          //(HVM.print Kind.Book (String.concat (String.concat "OLD!:" name) (String.concat " -- " (Kind.keys book))) book)
+        //let false = λbook
+          //(HVM.print Kind.Book (String.concat (String.concat "NEW!:" name) (String.concat " -- " (Kind.keys book)))
+          //let file = (Kind.load.file (Kind.load.file_of name))
+          //let defs = (String.Map.to_list Kind.Term file)
+          //let bok1 = (Kind.load.define defs book)
+          //let file = (Kind.load.file (Kind.load.file_of name))
+          //let refs = (Kind.Book.get_refs file)
+          //let bok2 = (HVM.print ?a (String.concat "REC!:" (Kind.keys bok1)) (Kind.load.name.many lims-1 refs bok1))
+          //bok2)
+          ////(HVM.print.many Kind.Book refs book)
+
+        //((~has P true false) book)
+      //(~(String.Map.has.linear Kind.Term name book) P new))
+  //}: ∀(name: String) ∀(book: Kind.Book) Kind.Book)
+
+//// Loads many names into a book
+//Kind.load.name.many
+//: ∀(lims: #U60)
+  //∀(list: (List String))
+  //∀(book: Kind.Book)
+  //Kind.Book
+//= λlims λlist λbook
+  //let P    = λx ∀(book: Kind.Book) (Kind.Book)
+  //let cons = λhead λtail λbook 
+    ////(HVM.print Kind.Book
+      ////(String.concat "DEP:"
+      ////(String.concat head
+      ////(String.concat " BOOK:"
+      ////(Kind.Book.show book))))
+    //let bok2 = (Kind.load.name lims head book)
+    //(Kind.load.name.many lims tail bok2)
+  //let nil  = λbook book
+  //((~list P cons nil) book)
+
+//// Defines a term and loads its dependencies
+////Kind.load.define
+////: ∀(name: String)
+  ////∀(term: Kind.Term)
+  ////∀(book: Kind.Book)
+  ////Kind.Book
+////= λname λterm λbook
+  ////let book = (String.Map.set Kind.Term name term book)
+  ////let refs = (Kind.Term.get_refs term)
+  ////let book = (Kind.load.name.many refs book)
+  ////book
+
+//// Defines many terms
+//Kind.load.define
+//: ∀(defs: (List (Pair String Kind.Term)))
+  //∀(book: Kind.Book)
+  //Kind.Book
+//= λdefs λbook
+  //// If defs list isn't empty...
+  //let P    = λx ∀(book: Kind.Book) (Kind.Book)
+  //let cons = λdefs.head λdefs.tail λbook
+    //// Gets the def name/term
+    //let P   = λx (Kind.Book)
+    //let new = λname λterm 
+      //// Writes it to the book
+      //let bok2 = (String.Map.set Kind.Term name term book)
+      //(HVM.print Kind.Book (String.concat "DEF!:" name)
+      //// Recurses
+      //(Kind.load.define defs.tail bok2))
+    //(~defs.head P new)
+  //// If defs list is empty, return the book
+  //let nil  = λbook book
+  //((~defs P cons nil) book)
+
+
+//Kind.keys
+//: ∀(book: Kind.Book)
+  //String
+//= λbook
+  //let defs = (String.Map.to_list Kind.Term book)
+  //let defs = (List.app (Pair String Kind.Term) String (Pair.fst String Kind.Term) defs)
+  //(String.join defs)
diff --git a/book/List.app.kind2 b/book/List.app.kind2
new file mode 100644
index 00000000..3584a679
--- /dev/null
+++ b/book/List.app.kind2
@@ -0,0 +1,11 @@
+List.app
+: ∀(A: *)
+  ∀(B: *)
+  ∀(f: ∀(x: A) B)
+  ∀(x: (List A))
+  (List B)
+= λA λB λf λx
+  let P    = λx(List B)
+  let cons = λh λt (List.cons B (f h) (List.app A B f t))
+  let nil  = (List.nil B)
+  (~x P cons nil)
diff --git a/book/Main.kind2 b/book/Main.kind2
index d0b3dcbe..6cb672ee 100644
--- a/book/Main.kind2
+++ b/book/Main.kind2
@@ -1,8 +1,45 @@
-Main
-: Kind.Book
-=
-  let book = (Kind.API.load "Bool.and")
-  book
+//Main
+//: Unit
+//= let map = (String.Map.new Unit)
+  //let map = (String.Map.set Unit "Bool" Unit.one map)
+  //let map = (String.Map.set Unit "Bool.true" Unit.one map)
+  //let has = (String.Map.has Unit "Bool.false" map)
+  //(HVM.print Unit (Bool.show has)
+  //Unit.one)
+
+//Main
+//: Unit
+//= let book = (Kind.load "Bool")
+  //(HVM.print Unit (Kind.Book.show book)
+  //Unit.one)
+
+//Main = Kind.load.name
+
+//Main = Kind.load.go.defs
+
+//Main
+//: Unit
+//=
+////= (HVM.print Unit (Kind.Book.to_hvm (Kind.API.load "Bool.and"))
+  //Unit.one
+  //)
+
+//Main
+//: (Maybe #U60)
+//= let map = (String.Map.new #U60)
+  //let map = (String.Map.set #U60 "foo" #1 map)
+  //let map = (String.Map.set #U60 "bar" #2 map)
+  //let map = (String.Map.set #U60 "tic" #3 map)
+  //let map = (String.Map.set #U60 "tac" #4 map)
+  //let val = (String.Map.get #U60 "bar" map)
+  //val
+
+//Main
+//: Kind.Book
+//=
+  //let book = (Kind.API.load "Bool.and")
+  //book
+
   //let code = (Kind.Book.to_hvm book)
   //let refs = (Kind.Book.get_refs book)
   //(HVM.print Unit code
diff --git a/book/Pair.fst.kind2 b/book/Pair.fst.kind2
new file mode 100644
index 00000000..b352a7a2
--- /dev/null
+++ b/book/Pair.fst.kind2
@@ -0,0 +1,9 @@
+Pair.fst
+: ∀(A: *)
+  ∀(B: *)
+  ∀(p: (Pair A B))
+  A
+= λA λB λp
+  let P   = λx(A)
+  let new = λa λb a
+  (~p P new)
diff --git a/book/Pair.snd.kind2 b/book/Pair.snd.kind2
new file mode 100644
index 00000000..7996ff0a
--- /dev/null
+++ b/book/Pair.snd.kind2
@@ -0,0 +1,9 @@
+Pair.snd
+: ∀(A: *)
+  ∀(B: *)
+  ∀(p: (Pair A B))
+  B
+= λA λB λp
+  let P   = λx(B)
+  let new = λa λb b
+  (~p P new)
diff --git a/book/String.Map.from_list.kind2 b/book/String.Map.from_list.kind2
new file mode 100644
index 00000000..022e6d1b
--- /dev/null
+++ b/book/String.Map.from_list.kind2
@@ -0,0 +1,6 @@
+String.Map.from_list
+: ∀(V: *)
+  ∀(list: (List (Pair String V)))
+  (String.Map V)
+= λV λlist
+  (BBT.from_list String V String.cmp list)
diff --git a/book/String.Map.has.kind2 b/book/String.Map.has.kind2
new file mode 100644
index 00000000..8154962e
--- /dev/null
+++ b/book/String.Map.has.kind2
@@ -0,0 +1,7 @@
+String.Map.has
+: ∀(V: *)
+  ∀(key: String)
+  ∀(map: (BBT String V))
+  Bool
+= λV λkey λmap
+  (BBT.has String V String.cmp key map)
diff --git a/book/String.Map.has.linear.kind2 b/book/String.Map.has.linear.kind2
new file mode 100644
index 00000000..90c1614e
--- /dev/null
+++ b/book/String.Map.has.linear.kind2
@@ -0,0 +1,7 @@
+String.Map.has.linear
+: ∀(V: *)
+  ∀(key: String)
+  ∀(map: (BBT String V))
+  (Pair Bool (BBT String V))
+= λV λkey λmap
+  (BBT.has.linear String V String.cmp key map)
diff --git a/book/String.Map.kind2 b/book/String.Map.kind2
new file mode 100644
index 00000000..7e141ecd
--- /dev/null
+++ b/book/String.Map.kind2
@@ -0,0 +1,35 @@
+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.Map.to_list.kind2 b/book/String.Map.to_list.kind2
new file mode 100644
index 00000000..ccb0cbe5
--- /dev/null
+++ b/book/String.Map.to_list.kind2
@@ -0,0 +1,6 @@
+String.Map.to_list
+: ∀(V: *)
+  ∀(map: (String.Map V))
+  (List (Pair String V))
+= λV λmap
+  (BBT.to_list String V map)
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/String.join.kind2 b/book/String.join.kind2
new file mode 100644
index 00000000..96162bca
--- /dev/null
+++ b/book/String.join.kind2
@@ -0,0 +1,8 @@
+String.join
+: ∀(strs: (List String))
+  String
+= λstrs
+  let P    = λx(String)
+  let cons = λhλt(String.concat h (String.join t))
+  let nil  = String.nil
+  (~strs P cons nil)
diff --git a/book/U60.Map.kind2 b/book/U60.Map.kind2
new file mode 100644
index 00000000..8b482e3e
--- /dev/null
+++ b/book/U60.Map.kind2
@@ -0,0 +1,34 @@
+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/_compile.kind2 b/book/_compile.kind2
index 32e49e13..6171864d 100644
--- a/book/_compile.kind2
+++ b/book/_compile.kind2
@@ -1,4 +1,180 @@
-_compile : String = (Kind.Book.to_hvm (Kind.Book.parse `test9
+_compile : String = (Kind.Book.to_hvm (Kind.Book.parse `// 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
-= (String.unpar '(' ')' "((foo))")
+= 
+"
+File commented for backward compatibility.
+To run the tests, uncomment the code on:
+  testBBT.kind2
+  U60.Map
+"
+  // RunTests
 `))
\ 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
diff --git a/bootstrap.hvm1 b/bootstrap.hvm1
index f57e3ea4..2717a876 100644
--- a/bootstrap.hvm1
+++ b/bootstrap.hvm1
@@ -7,12 +7,203 @@
 (Str.view str)        = (str 0 λhλt(String.cons h (Str.view t)) String.nil)
 (Strs.view strs)      = (List.view λx(Str.view x) strs)
 (List.view elem list) = (list 0 λhλt(List.cons (elem h) (List.view elem t)) List.nil)
-
-Book.A.one = λ_P λ_new (_new 0)
+`
+Book.A.match = λ_a λ_P λ_t ((_a _P) λ_tag (U60.match _tag _t λ_tag_1(λ_x (_x λ_x 0))))
+Book.A = 0
 Book.A.bad = λ_P λ_new ((_new 1) 0)
 Book.A.sel = λ_P λ_k (U60.match _k (_P (Book.A.one)) λ_tag_1(0))
-Book.A = 0
-Book.A.match = λ_a λ_P λ_t ((_a _P) λ_tag (U60.match _tag _t λ_tag_1(λ_x (_x λ_x 0))))
+Book.A.one = λ_P λ_new (_new 0)
+
+Book.BBT.balance.lft_heavier = λ_K λ_V λ_cmp λ_new_size λ_node_key λ_set_key λ_val λ_lft λ_rgt 
+  let _P = λ_x (((Book.BBT) _K) _V) 
+  let _bin = λ_lft.size λ_lft.key λ_lft.val λ_lft.lft λ_lft.rgt 
+    let _P = λ_x 0 
+    let _true = λ_new_size λ_key λ_val λ_lft.key λ_lft.val λ_lft.lft λ_lft.rgt λ_rgt 
+      let _lft = ((((((((Book.BBT.lft_rotate) _K) _V) _lft.size) _lft.key) _lft.val) _lft.lft) _lft.rgt) 
+      ((((((((Book.BBT.rgt_rotate) _K) _V) _new_size) _key) _val) _lft) _rgt) 
+    let _false = λ_new_size λ_key λ_val λ_lft.key λ_lft.val λ_lft.lft λ_lft.rgt λ_rgt 
+      let _lft = ((((((((Book.BBT.bin) _K) _V) _lft.size) _lft.key) _lft.val) _lft.lft) _lft.rgt) 
+      ((((((((Book.BBT.rgt_rotate) _K) _V) _new_size) _key) _val) _lft) _rgt) 
+    (((((((((((((Book.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) 
+  let _tip = (((Book.BBT.tip) _K) _V) 
+  (((_lft _P) _bin) _tip)
+Book.BBT.balance = λ_K λ_V λ_cmp λ_set_key λ_node_key λ_val λ_lft λ_rgt 
+  let _P = λ_x (((Book.BBT) _K) _V) 
+  let _new = λ_lft.size λ_lft 
+    let _P = λ_x (((Book.BBT) _K) _V) 
+    let _new = λ_rgt.size λ_rgt 
+      let _new_size = (+ 1 (((Book.U60.max) _lft.size) _rgt.size)) 
+      let _balance = (((Book.U60.abs_diff) _lft.size) _rgt.size) 
+      let _P = λ_x 0 
+      let _true = λ_new_size λ_node_key λ_val λ_lft λ_rgt 
+        let _P = λ_x 0 
+        let _true = (Book.BBT.balance.lft_heavier) 
+        let _false = (Book.BBT.balance_rgt_heavier) 
+        ((((((((((((((Book.U60.to_bool) (< _rgt.size _lft.size)) _P) _true) _false) _K) _V) _cmp) _new_size) _node_key) _set_key) _val) _lft) _rgt) 
+      let _false = λ_new_size λ_node_key λ_val λ_lft λ_rgt ((((((((Book.BBT.bin) _K) _V) _new_size) _node_key) _val) _lft) _rgt) 
+      ((((((((((Book.U60.to_bool) (> _balance 1)) _P) _true) _false) _new_size) _node_key) _val) _lft) _rgt) 
+    ((((((Book.BBT.got_size) _K) _V) _rgt) _P) _new) 
+  ((((((Book.BBT.got_size) _K) _V) _lft) _P) _new)
+Book.BBT.balance_rgt_heavier = λ_K λ_V λ_cmp λ_new_size λ_node_key λ_set_key λ_val λ_lft λ_rgt 
+  let _P = λ_x (((Book.BBT) _K) _V) 
+  let _bin = λ_rgt.size λ_rgt.key λ_rgt.val λ_rgt.lft λ_rgt.rgt 
+    let _P = λ_x 0 
+    let _true = λ_new_size λ_key λ_val λ_lft λ_rgt.key λ_rgt.val λ_rgt.lft λ_rgt.rgt 
+      let _rgt = ((((((((Book.BBT.bin) _K) _V) _rgt.size) _rgt.key) _rgt.val) _rgt.lft) _rgt.rgt) 
+      ((((((((Book.BBT.lft_rotate) _K) _V) _new_size) _key) _val) _lft) _rgt) 
+    let _false = λ_new_size λ_key λ_val λ_lft λ_rgt.key λ_rgt.val λ_rgt.lft λ_rgt.rgt 
+      let _rgt = ((((((((Book.BBT.rgt_rotate) _K) _V) _rgt.size) _rgt.key) _rgt.val) _rgt.lft) _rgt.rgt) 
+      ((((((((Book.BBT.lft_rotate) _K) _V) _new_size) _key) _val) _lft) _rgt) 
+    (((((((((((((Book.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) 
+  let _tip = (((Book.BBT.tip) _K) _V) 
+  (((_rgt _P) _bin) _tip)
+
+Book.BBT.bin = λ_K λ_V λ_size λ_key λ_val λ_lft λ_rgt λ_P λ_bin λ_tip (((((_bin _size) _key) _val) _lft) _rgt)
+
+Book.BBT.from_list = λ_K λ_V λ_cmp λ_list 
+  let _P = λ_x (((Book.BBT) _K) _V) 
+  let _cons = λ_head λ_tail 
+    let _P = λ_x (((Book.BBT) _K) _V) 
+    let _new = λ_key λ_val (((((((Book.BBT.set) _K) _V) _cmp) _key) _val) (((((Book.BBT.from_list) _K) _V) _cmp) _tail)) 
+    ((_head _P) _new) 
+  let _nil = (((Book.BBT.tip) _K) _V) 
+  (((_list _P) _cons) _nil)
+
+Book.BBT.get = λ_K λ_V λ_cmp λ_key λ_map 
+  let _P = λ_x ((Book.Maybe) _V) 
+  let _bin = λ__size λ_next.key λ_next.val λ_next.lft λ_next.rgt 
+    let _P = λ_x 0 
+    let _ltn = λ_cmp λ_key ((((((Book.BBT.get) _K) _V) _cmp) _key) _next.lft) 
+    let _eql = λ_cmp λ_key (((Book.Maybe.some) _V) _next.val) 
+    let _gtn = λ_cmp λ_key ((((((Book.BBT.get) _K) _V) _cmp) _key) _next.rgt) 
+    ((((((((_cmp _key) _next.key) _P) _ltn) _eql) _gtn) _cmp) _key) 
+  let _tip = ((Book.Maybe.none) _V) 
+  (((_map _P) _bin) _tip)
+
+Book.BBT.got = λ_K λ_V λ_cmp λ_key λ_map 
+  let _P = λ_x (((Book.Pair) ((Book.Maybe) _V)) (((Book.BBT) _K) _V)) 
+  let _bin = λ_size λ_next.key λ_next.val λ_next.lft λ_next.rgt 
+    let _P = λ_x 0 
+    let _ltn = λ_cmp λ_key 
+      let _new_pair = ((((((Book.BBT.got) _K) _V) _cmp) _key) _next.lft) 
+      let _P = λ_x (((Book.Pair) ((Book.Maybe) _V)) (((Book.BBT) _K) _V)) 
+      let _new = λ_val λ_lft 
+        let _map = ((((((((Book.BBT.bin) _K) _V) _size) _next.key) _next.val) _lft) _next.rgt) 
+        (((((Book.Pair.new) ((Book.Maybe) _V)) (((Book.BBT) _K) _V)) _val) _map) 
+      ((_new_pair _P) _new) 
+    let _eql = λ_cmp λ_key 
+      let _map = ((((((((Book.BBT.bin) _K) _V) _size) _next.key) _next.val) _next.lft) _next.rgt) 
+      (((((Book.Pair.new) ((Book.Maybe) _V)) (((Book.BBT) _K) _V)) (((Book.Maybe.some) _V) _next.val)) _map) 
+    let _gtn = λ_cmp λ_key 
+      let _new_pair = ((((((Book.BBT.got) _K) _V) _cmp) _key) _next.rgt) 
+      let _P = λ_x (((Book.Pair) ((Book.Maybe) _V)) (((Book.BBT) _K) _V)) 
+      let _new = λ_val λ_rgt 
+        let _map = ((((((((Book.BBT.bin) _K) _V) _size) _next.key) _next.val) _next.lft) _rgt) 
+        (((((Book.Pair.new) ((Book.Maybe) _V)) (((Book.BBT) _K) _V)) _val) _map) 
+      ((_new_pair _P) _new) 
+    ((((((((_cmp _key) _next.key) _P) _ltn) _eql) _gtn) _cmp) _key) 
+  let _tip = (((((Book.Pair.new) ((Book.Maybe) _V)) (((Book.BBT) _K) _V)) ((Book.Maybe.none) _V)) (((Book.BBT.tip) _K) _V)) 
+  (((_map _P) _bin) _tip)
+
+Book.BBT.got_size = λ_K λ_V λ_map 
+  let _P = λ_x (((Book.Pair) 0) (((Book.BBT) _K) _V)) 
+  let _bin = λ_size λ_next.key λ_next.val λ_next.lft λ_next.rgt 
+    let _map = ((((((((Book.BBT.bin) _K) _V) _size) _next.key) _next.val) _next.lft) _next.rgt) 
+    (((((Book.Pair.new) 0) (((Book.BBT) _K) _V)) _size) _map) 
+  let _tip = (((((Book.Pair.new) 0) (((Book.BBT) _K) _V)) 0) (((Book.BBT.tip) _K) _V)) 
+  (((_map _P) _bin) _tip)
+
+Book.BBT.has = λ_K λ_V λ_cmp λ_key λ_map 
+  let _P = λ_x (Book.Bool) 
+  let _bin = λ_next.size λ_next.key λ_next.val λ_next.lft λ_next.rgt 
+    let _P = λ_x 0 
+    let _ltn = λ_cmp λ_key ((((((Book.BBT.has) _K) _V) _cmp) _key) _next.lft) 
+    let _eql = λ_cmp λ_key (Book.Bool.true) 
+    let _gtn = λ_cmp λ_key ((((((Book.BBT.has) _K) _V) _cmp) _key) _next.rgt) 
+    ((((((((_cmp _key) _next.key) _P) _ltn) _eql) _gtn) _cmp) _key) 
+  let _tip = (Book.Bool.false) 
+  (((_map _P) _bin) _tip)
+
+Book.BBT.has.linear = λ_K λ_V λ_cmp λ_key λ_map 
+  let _P = λ_x (((Book.Pair) (Book.Bool)) (((Book.BBT) _K) _V)) 
+  let _bin = λ_size λ_node_key λ_val λ_lft λ_rgt 
+    let _P = λ_x 0 
+    let _ltn = λ_cmp λ_size λ_has_key λ_val λ_lft λ_rgt λ_has_key 
+      let _P = λ_x (((Book.Pair) (Book.Bool)) (((Book.BBT) _K) _V)) 
+      let _new = λ_bool λ_lft 
+        let _map = ((((((((Book.BBT.bin) _K) _V) _size) _node_key) _val) _lft) _rgt) 
+        (((((Book.Pair.new) (Book.Bool)) (((Book.BBT) _K) _V)) _bool) _map) 
+      ((((((((Book.BBT.has.linear) _K) _V) _cmp) _has_key) _lft) _P) _new) 
+    let _eql = λ_cmp λ_size λ_key λ_val λ_lft λ_rgt λ_has_key (((((Book.Pair.new) (Book.Bool)) (((Book.BBT) _K) _V)) (Book.Bool.true)) ((((((((Book.BBT.bin) _K) _V) _size) _node_key) _val) _lft) _rgt)) 
+    let _gtn = λ_cmp λ_size λ_key λ_val λ_lft λ_rgt λ_has_key 
+      let _P = λ_x (((Book.Pair) (Book.Bool)) (((Book.BBT) _K) _V)) 
+      let _new = λ_bool λ_rgt 
+        let _map = ((((((((Book.BBT.bin) _K) _V) _size) _node_key) _val) _lft) _rgt) 
+        (((((Book.Pair.new) (Book.Bool)) (((Book.BBT) _K) _V)) _bool) _rgt) 
+      ((((((((Book.BBT.has.linear) _K) _V) _cmp) _has_key) _rgt) _P) _new) 
+    (((((((((((((_cmp _key) _node_key) _P) _ltn) _eql) _gtn) _cmp) _size) _node_key) _val) _lft) _rgt) _key) 
+  let _tip = (((((Book.Pair.new) (Book.Bool)) (((Book.BBT) _K) _V)) (Book.Bool.false)) (((Book.BBT.tip) _K) _V)) 
+  (((_map _P) _bin) _tip)
+
+Book.BBT = λ_K λ_V 0
+
+Book.BBT.lft_rotate = λ_K λ_V λ_size λ_key λ_val λ_lft λ_rgt 
+  let _P = λ_x 0 
+  let _bin = λ__size λ_rgt.key λ_rgt.val λ_rgt.lft λ_rgt.rgt λ_key λ_val λ_lft 
+    let _b = (((((((Book.BBT.new_node) _K) _V) _key) _val) _lft) _rgt.lft) 
+    let _a = (((((((Book.BBT.new_node) _K) _V) _rgt.key) _rgt.val) _b) _rgt.rgt) 
+    _a 
+  let _tip = λ_key λ_val λ_lft ((((((((Book.BBT.bin) _K) _V) _size) _key) _val) _lft) (((Book.BBT.tip) _K) _V)) 
+  ((((((_rgt _P) _bin) _tip) _key) _val) _lft)
+
+Book.BBT.new_node = λ_K λ_V λ_key λ_val λ_lft λ_rgt 
+  let _P = λ_x (((Book.BBT) _K) _V) 
+  let _new = λ_lft.size λ_lft 
+    let _P = λ_x (((Book.BBT) _K) _V) 
+    let _new = λ_rgt.size λ_rgt 
+      let _new_size = (+ 1 (((Book.U60.max) _rgt.size) _lft.size)) 
+      ((((((((Book.BBT.bin) _K) _V) _new_size) _key) _val) _lft) _rgt) 
+    ((((((Book.BBT.got_size) _K) _V) _rgt) _P) _new) 
+  ((((((Book.BBT.got_size) _K) _V) _lft) _P) _new)
+
+Book.BBT.rgt_rotate = λ_K λ_V λ_size λ_key λ_val λ_lft λ_rgt 
+  let _P = λ_x 0 
+  let _bin = λ__size λ_lft.key λ_lft.val λ_lft.lft λ_lft.rgt λ_key λ_val λ_rgt 
+    let _b = (((((((Book.BBT.new_node) _K) _V) _key) _val) _lft.rgt) _rgt) 
+    let _a = (((((((Book.BBT.new_node) _K) _V) _lft.key) _lft.val) _lft.lft) _b) 
+    _a 
+  let _tip = λ_key λ_val λ_rgt ((((((((Book.BBT.bin) _K) _V) _size) _key) _val) (((Book.BBT.tip) _K) _V)) _rgt) 
+  ((((((_lft _P) _bin) _tip) _key) _val) _rgt)
+
+Book.BBT.set = λ_K λ_V λ_cmp λ_key λ_val λ_map 
+  let _P = λ_x 0 
+  let _bin = λ_size λ_next.key λ_next.val λ_next.lft λ_next.rgt λ_key λ_val 
+    let _P = λ_x 0 
+    let _ltn = λ_key λ_next.key λ_next.val λ_next.lft λ_next.rgt 
+      let _new_lft = (((((((Book.BBT.set) _K) _V) _cmp) _key) _val) _next.lft) 
+      (((((((((Book.BBT.balance) _K) _V) _cmp) _key) _next.key) _next.val) _new_lft) _next.rgt) 
+    let _eql = λ_key λ_next.key λ_next.val λ_next.lft λ_next.rgt ((((((((Book.BBT.bin) _K) _V) _size) _next.key) _val) _next.lft) _next.rgt) 
+    let _gtn = λ_key λ_next.key λ_next.val λ_next.lft λ_next.rgt 
+      let _new_rgt = (((((((Book.BBT.set) _K) _V) _cmp) _key) _val) _next.rgt) 
+      (((((((((Book.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) 
+  let _tip = λ_key λ_val (((((Book.BBT.singleton) _K) _V) _key) _val) 
+  (((((_map _P) _bin) _tip) _key) _val)
+
+Book.BBT.singleton = λ_K λ_V λ_key λ_val ((((((((Book.BBT.bin) _K) _V) 1) _key) _val) (((Book.BBT.tip) _K) _V)) (((Book.BBT.tip) _K) _V))
+
+Book.BBT.tip = λ_K λ_V λ_P λ_bin λ_tip _tip
+
+Book.BBT.to_list = λ_K λ_V λ_map 
+  let _P = λ_x ((Book.List) (((Book.Pair) _K) _V)) 
+  let _bin = λ_size λ_key λ_val λ_lft λ_rgt 
+    let _lft = ((((Book.BBT.to_list) _K) _V) _lft) 
+    let _rgt = ((((Book.BBT.to_list) _K) _V) _rgt) 
+    let _pair = (((((Book.Pair.new) _K) _V) _key) _val) 
+    let _list = ((((Book.List.cons) (((Book.Pair) _K) _V)) _pair) ((((Book.List.concat) (((Book.Pair) _K) _V)) _lft) _rgt)) 
+    _list 
+  let _tip = ((Book.List.nil) (((Book.Pair) _K) _V)) 
+  (((_map _P) _bin) _tip)
 
 Book.Bool.and = λ_a 
   let _P = λ_a 0 
@@ -42,6 +233,12 @@ Book.Bool.or = λ_a
   let _false = λ_b _b 
   (((_a _P) _true) _false)
 
+Book.Bool.show = λ_x 
+  let _P = λ_x (Book.String) 
+  let _true = (Str "true") 
+  let _false = (Str "false") 
+  (((_x _P) _true) _false)
+
 Book.Bool.true = λ_P λ_t λ_f _t
 
 Book.Char.equal = (Book.U60.equal)
@@ -66,6 +263,21 @@ Book.Char = 0
 
 Book.Char.slash = 92
 
+Book.Cmp.eql = λ_P λ_ltn λ_eql λ_gtn _eql
+
+Book.Cmp.gtn = λ_P λ_ltn λ_eql λ_gtn _gtn
+
+Book.Cmp.is_gtn = λ_cmp 
+  let _P = λ_x (Book.Bool) 
+  let _ltn = (Book.Bool.false) 
+  let _eql = (Book.Bool.false) 
+  let _gtn = (Book.Bool.true) 
+  ((((_cmp _P) _ltn) _eql) _gtn)
+
+Book.Cmp = 0
+
+Book.Cmp.ltn = λ_P λ_ltn λ_eql λ_gtn _ltn
+
 Book.Empty.absurd = λ_e λ_P (_e λ_x _P)
 
 Book.Empty = 0
@@ -76,6 +288,20 @@ Book.Equal = λ_A λ_a λ_b 0
 
 Book.Equal.refl = λ_A λ_a λ_P λ_p _p
 
+Book.HVM.load = λ_A λ_file λ_cont (_cont (Book.String.nil))
+
+Book.HVM.log = λ_A λ_B λ_msg λ_ret _ret
+
+Book.HVM.print = λ_A λ_msg λ_ret _ret
+
+Book.HVM.print.many = λ_A λ_msgs λ_ret 
+  let _P = λ_x _A 
+  let _cons = λ_msg λ_msgs ((((Book.HVM.print) _A) _msg) ((((Book.HVM.print.many) _A) _msgs) _ret)) 
+  let _nil = _ret 
+  (((_msgs _P) _cons) _nil)
+
+Book.HVM.save = λ_A λ_file λ_data λ_cont _cont
+
 Book.Kind.Binder = (((Book.Pair) (Book.String)) (Book.Kind.Term))
 
 Book.Kind.Binder.new = λ_nam λ_typ (((((Book.Pair.new) (Book.String)) (Book.Kind.Term)) _nam) _typ)
@@ -95,14 +321,14 @@ Book.Kind.Book.get_refs.go = λ_book
   let _nil = λ_nil _nil 
   (((_book _P) _cons) _nil)
 
-Book.Kind.Book.get_refs = λ_book (((Book.List.Concatenator.build) (Book.String)) ((Book.Kind.Book.get_refs.go) _book))
+Book.Kind.Book.get_refs = λ_book (((Book.List.Concatenator.build) (Book.String)) ((Book.Kind.Book.get_refs.go) (((Book.String.Map.to_list) (Book.Kind.Term)) _book)))
 
 Book.Kind.Book = ((Book.String.Map) (Book.Kind.Term))
 
 Book.Kind.Book.parse = λ_code 
   let _P = λ_x (Book.Kind.Book) 
   let _done = λ_code λ_book _book 
-  let _fail = λ_error ((Book.List.nil) (((Book.Pair) (Book.String)) (Book.Kind.Term))) 
+  let _fail = λ_error ((Book.String.Map.new) (Book.Kind.Term)) 
   (((((Book.Kind.Book.parser) _code) _P) _done) _fail)
 
 Book.Kind.Book.parser = (((((Book.Parser.bind) (Book.Bool)) (Book.Kind.Book)) (Book.Parser.is_eof)) λ_is_eof 
@@ -124,7 +350,7 @@ Book.Kind.Book.show.go = λ_book
   let _nil = λ_nil _nil 
   (((_book _P) _cons) _nil)
 
-Book.Kind.Book.show = λ_book ((Book.String.Concatenator.build) ((Book.Kind.Book.show.go) _book))
+Book.Kind.Book.show = λ_book ((Book.String.Concatenator.build) ((Book.Kind.Book.show.go) (((Book.String.Map.to_list) (Book.Kind.Term)) _book)))
 
 Book.Kind.Book.to_hvm.go = λ_book 
   let _P = λ_x (Book.String.Concatenator) 
@@ -135,7 +361,7 @@ Book.Kind.Book.to_hvm.go = λ_book
   let _nil = λ_nil _nil 
   (((_book _P) _cons) _nil)
 
-Book.Kind.Book.to_hvm = λ_book ((Book.String.Concatenator.build) ((Book.Kind.Book.to_hvm.go) _book))
+Book.Kind.Book.to_hvm = λ_book ((Book.String.Concatenator.build) ((Book.Kind.Book.to_hvm.go) (((Book.String.Map.to_list) (Book.Kind.Term)) _book)))
 
 Book.Kind.Oper.add = λ_P λ_add λ_mul λ_sub λ_div λ_mod λ_eq λ_ne λ_lt λ_gt λ_lte λ_gte λ_and λ_or λ_xor λ_lsh λ_rsh _add
 
@@ -485,6 +711,7 @@ Book.Kind.equal.minor = λ_e λ_a λ_b λ_dep
     (((((Book.Kind.equal.major) ((((Book.Kind.identical) _a_wnf) _b_wnf) _dep)) _a_wnf) _b_wnf) _dep) 
   ((((((_e _P) _true) _false) _a) _b) _dep)
 
+
 Book.Kind.hol = λ_nam λ_ctx λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var ((_hol _nam) _ctx)
 
 Book.Kind.identical = λ_a λ_b λ_dep (((((Book.Kind.comparer) (Book.Kind.identical)) _a) _b) _dep)
@@ -847,6 +1074,7 @@ Book.Kind =
 
 Book.Kind.lam = λ_nam λ_bod λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var ((_lam _nam) _bod)
 
+
 Book.Kind.mat = λ_nam λ_x λ_z λ_s λ_p λ_P λ_all λ_lam λ_app λ_ann λ_slf λ_ins λ_ref λ_def λ_set λ_u60 λ_num λ_op2 λ_mat λ_txt λ_hol λ_var (((((_mat _nam) _x) _z) _s) _p)
 
 Book.Kind.normal.go = λ_maj λ_term λ_dep 
@@ -1018,21 +1246,11 @@ Book.List.Folder = λ_T 0
 
 Book.List.Folder.nil = λ_T λ_P λ_cons λ_nil _nil
 
-Book.List.Map = λ_K λ_V ((Book.List) (((Book.Pair) _K) _V))
-Book.List.Map.get = λ_K λ_V λ_eql λ_key λ_map 
-  let _P = λ_x ((Book.Maybe) _V) 
-  let _cons = λ_head λ_tail 
-    let _P = λ_x ((Book.Maybe) _V) 
-    let _new = λ_head.fst λ_head.snd 
-      let _P = λ_x ((Book.Maybe) _V) 
-      let _true = (((Book.Maybe.some) _V) _head.snd) 
-      let _false = ((((((Book.List.Map.get) _K) _V) _eql) _key) _tail) 
-      (((((_eql _head.fst) _key) _P) _true) _false) 
-    ((_head _P) _new) 
-  let _nil = ((Book.Maybe.none) _V) 
-  (((_map _P) _cons) _nil)
-Book.List.Map.set = λ_K λ_V λ_key λ_val λ_map ((((Book.List.cons) (((Book.Pair) _K) _V)) (((((Book.Pair.new) _K) _V) _key) _val)) _map)
-Book.List.Map.new = λ_K λ_V ((Book.List.nil) (((Book.Pair) _K) _V))
+Book.List.app = λ_A λ_B λ_f λ_x 
+  let _P = λ_x ((Book.List) _B) 
+  let _cons = λ_h λ_t ((((Book.List.cons) _B) (_f _h)) (((((Book.List.app) _A) _B) _f) _t)) 
+  let _nil = ((Book.List.nil) _B) 
+  (((_x _P) _cons) _nil)
 
 Book.List.begin = λ_A λ_list 
   let _P = λ_x ((Book.List) _A) 
@@ -1096,8 +1314,8 @@ Book.Maybe.pure = (Book.Maybe.some)
 
 Book.Maybe.some = λ_T λ_value λ_P λ_some λ_none (_some _value)
 
-Book.Monad = λ_M 0
 Book.Monad.new = λ_M λ_bind λ_pure λ_P λ_new ((_new _bind) _pure)
+Book.Monad = λ_M 0
 
 Book.Nat.double = λ_n (((_n λ_x (Book.Nat)) λ_pred ((Book.Nat.succ) ((Book.Nat.succ) ((Book.Nat.double) _pred)))) (Book.Nat.zero))
 
@@ -1125,12 +1343,22 @@ Book.Nat.succ = λ_n λ_P λ_succ λ_zero (_succ _n)
 
 Book.Nat.zero = λ_P λ_succ λ_zero _zero
 
+Book.Pair.fst = λ_A λ_B λ_p 
+  let _P = λ_x _A 
+  let _new = λ_a λ_b _a 
+  ((_p _P) _new)
+
 Book.Pair.get = λ_A λ_B λ_p λ_P λ_f ((_p λ_x _P) _f)
 
 Book.Pair = λ_A λ_B 0
 
 Book.Pair.new = λ_A λ_B λ_a λ_b λ_P λ_new ((_new _a) _b)
 
+Book.Pair.snd = λ_A λ_B λ_p 
+  let _P = λ_x _B 
+  let _new = λ_a λ_b _b 
+  ((_p _P) _new)
+
 Book.Parser.Guard.get = λ_A (((Book.Pair.get) ((Book.Parser) (Book.Bool))) ((Book.Parser) _A))
 
 Book.Parser.Guard = λ_A (((Book.Pair) ((Book.Parser) (Book.Bool))) ((Book.Parser) _A))
@@ -1261,19 +1489,19 @@ Book.Parser.variant = λ_A λ_variants
   let _nil = (((Book.Parser.fail) _A) (Str "error")) 
   (((_variants _P) _cons) _nil)
 
-Book.QBool.true = λ_P λ_S λ_p ((_p 0) λ_x _x)
 Book.QBool.false = λ_P λ_S λ_p ((_p 1) λ_x _x)
 Book.QBool = 0
 Book.QBool.match = λ_a λ_P λ_t λ_f (((_a _P) λ_x (_P _a)) λ_tag (U60.match _tag λ_x (_x _t) λ_tag_1(λ_x ((U60.match _tag_1 λ_x (_x _f) λ_tag_1_1(λ_x (_x λ_e (((Book.Empty.absurd) _e) 0)))) _x))))
+Book.QBool.true = λ_P λ_S λ_p ((_p 0) λ_x _x)
 
-Book.QBool2.true = λ_P λ_new (_new 0)
-Book.QBool2.false = λ_P λ_new (_new 1)
 Book.QBool2.bad = λ_P λ_new ((_new 2) 0)
 Book.QBool2 = 0
 Book.QBool2.match = λ_a λ_P λ_t λ_f ((_a _P) λ_tag (U60.match _tag _t λ_tag_1((U60.match _tag_1 _f λ_tag_1_1(λ_e (_e λ_x 0))))))
+Book.QBool2.false = λ_P λ_new (_new 1)
+Book.QBool2.true = λ_P λ_new (_new 0)
 
-Book.QUnit.one = λ_P λ_SP λ_new ((_new 0) λ_one _one)
 Book.QUnit = 0
+Book.QUnit.one = λ_P λ_SP λ_new ((_new 0) λ_one _one)
 
 Book.Sigma = λ_A λ_B 0
 
@@ -1289,13 +1517,41 @@ Book.String.Concatenator.join = ((Book.List.Concatenator.join) (Book.Char))
 
 Book.String.Concatenator = ((Book.List.Concatenator) (Book.Char))
 
-Book.String.Map = ((Book.List.Map) (Book.String))
-Book.String.Map.get = λ_A λ_key λ_map ((((((Book.List.Map.get) (Book.String)) _A) (Book.String.equal)) _key) _map)
-Book.String.Map.set = λ_A λ_key λ_val λ_map ((((((Book.List.Map.set) (Book.String)) _A) _key) _val) _map)
-Book.String.Map.new = λ_V (((Book.List.Map.new) (Book.String)) _V)
+Book.String.Map.from_list = λ_V λ_list (((((Book.BBT.from_list) (Book.String)) _V) (Book.String.cmp)) _list)
+
+Book.String.Map.has = λ_V λ_key λ_map ((((((Book.BBT.has) (Book.String)) _V) (Book.String.cmp)) _key) _map)
+
+Book.String.Map.has.linear = λ_V λ_key λ_map ((((((Book.BBT.has.linear) (Book.String)) _V) (Book.String.cmp)) _key) _map)
+
+Book.String.Map.new = λ_V (((Book.BBT.tip) (Book.String)) _V)
+Book.String.Map.get = λ_V λ_key λ_map ((((((Book.BBT.get) (Book.String)) _V) (Book.String.cmp)) _key) _map)
+Book.String.Map = λ_V (((Book.BBT) (Book.String)) _V)
+Book.String.Map.got = λ_V λ_key λ_map ((((((Book.BBT.got) (Book.String)) _V) (Book.String.cmp)) _key) _map)
+Book.String.Map.set = λ_V λ_key λ_val λ_map (((((((Book.BBT.set) (Book.String)) _V) (Book.String.cmp)) _key) _val) _map)
+
+Book.String.Map.to_list = λ_V λ_map ((((Book.BBT.to_list) (Book.String)) _V) _map)
 
 Book.String.begin = λ_str (((Book.List.begin) (Book.Char)) _str)
 
+Book.String.cmp = λ_a λ_b 
+  let _P = λ_x 0 
+  let _cons = λ_a.head λ_a.tail λ_b 
+    let _P = λ_x 0 
+    let _cons = λ_b.head λ_b.tail λ_a.head λ_a.tail 
+      let _P = λ_x (Book.Cmp) 
+      let _ltn = (Book.Cmp.ltn) 
+      let _eql = (((Book.String.cmp) _a.tail) _b.tail) 
+      let _gtn = (Book.Cmp.gtn) 
+      (((((((Book.U60.cmp) _a.head) _b.head) _P) _ltn) _eql) _gtn) 
+    let _nil = λ_a.head λ_a.tail (Book.Cmp.gtn) 
+    (((((_b _P) _cons) _nil) _a.head) _a.tail) 
+  let _nil = λ_b 
+    let _P = λ_x (Book.Cmp) 
+    let _cons = λ_b.head λ_b.tail (Book.Cmp.ltn) 
+    let _nil = (Book.Cmp.eql) 
+    (((_b _P) _cons) _nil) 
+  ((((_a _P) _cons) _nil) _b)
+
 Book.String.concat = ((Book.List.concat) (Book.Char))
 
 Book.String.cons = λ_head λ_tail λ_P λ_cons λ_nil ((_cons _head) _tail)
@@ -1320,6 +1576,12 @@ Book.String.indent = λ_tab
   let _zero = (Book.String.nil) 
   (((_tab _P) _succ) _zero)
 
+Book.String.join = λ_strs 
+  let _P = λ_x (Book.String) 
+  let _cons = λ_h λ_t (((Book.String.concat) _h) ((Book.String.join) _t)) 
+  let _nil = (Book.String.nil) 
+  (((_strs _P) _cons) _nil)
+
 Book.String = ((Book.List) (Book.Char))
 
 Book.String.length = λ_a (((Book.List.length) (Book.Char)) _a)
@@ -1330,6 +1592,15 @@ Book.String.nil = λ_P λ_cons λ_nil _nil
 
 Book.String.quote = (((Book.String.cons) 34) (Book.String.nil))
 
+Book.String.skip.comment = λ_str 
+  let _P = λ_x (Book.String) 
+  let _cons = λ_c0 λ_cs 
+    let _P = λ_x 0 
+    let _true = λ_c0 λ_cs ((Book.String.skip) _cs) 
+    let _false = λ_c0 λ_cs ((Book.String.skip.comment) _cs) 
+    (((((((Book.Char.is_newline) _c0) _P) _true) _false) _c0) _cs) 
+  let _nil = (Book.String.nil) 
+  (((_str _P) _cons) _nil)
 Book.String.skip = λ_str 
   let _P = λ_x (Book.String) 
   let _cons = λ_c0 λ_cs 
@@ -1351,15 +1622,6 @@ Book.String.skip = λ_str
     (((((((Book.Char.is_blank) _c0) _P) _true) _false) _c0) _cs) 
   let _nil = (Book.String.nil) 
   (((_str _P) _cons) _nil)
-Book.String.skip.comment = λ_str 
-  let _P = λ_x (Book.String) 
-  let _cons = λ_c0 λ_cs 
-    let _P = λ_x 0 
-    let _true = λ_c0 λ_cs ((Book.String.skip) _cs) 
-    let _false = λ_c0 λ_cs ((Book.String.skip.comment) _cs) 
-    (((((((Book.Char.is_newline) _c0) _P) _true) _false) _c0) _cs) 
-  let _nil = (Book.String.nil) 
-  (((_str _P) _cons) _nil)
 
 Book.String.unpar = λ_fst λ_lst λ_str 
   let _P = λ_x (Book.String) 
@@ -1371,10 +1633,19 @@ Book.String.unpar = λ_fst λ_lst λ_str
   let _nil = (Book.String.nil) 
   (((_str _P) _cons) _nil)
 
-Book.U60.Map = ((Book.List.Map) 0)
-Book.U60.Map.get = λ_A λ_key λ_map ((((((Book.List.Map.get) 0) _A) (Book.U60.equal)) _key) _map)
-Book.U60.Map.set = λ_A λ_key λ_val λ_map ((((((Book.List.Map.set) 0) _A) _key) _val) _map)
-Book.U60.Map.new = λ_V (((Book.List.Map.new) 0) _V)
+Book.U60.Map.new = λ_V (((Book.BBT.tip) 0) _V)
+Book.U60.Map.get = λ_V λ_key λ_map ((((((Book.BBT.get) 0) _V) (Book.U60.cmp)) _key) _map)
+Book.U60.Map = λ_V (((Book.BBT) 0) _V)
+Book.U60.Map.got = λ_V λ_key λ_map ((((((Book.BBT.got) 0) _V) (Book.U60.cmp)) _key) _map)
+Book.U60.Map.set = λ_V λ_key λ_val λ_map (((((((Book.BBT.set) 0) _V) (Book.U60.cmp)) _key) _val) _map)
+
+Book.U60.abs_diff = λ_a λ_b 
+  let _P = λ_x 0 
+  let _true = (- _b _a) 
+  let _false = (- _a _b) 
+  (((((Book.U60.to_bool) (< _a _b)) _P) _true) _false)
+
+Book.U60.cmp = λ_a λ_b (((((Book.U60.if) (== _a _b)) (Book.Cmp)) (((((Book.U60.if) (< _a _b)) (Book.Cmp)) (Book.Cmp.gtn)) (Book.Cmp.ltn))) (Book.Cmp.eql))
 
 Book.U60.equal = λ_a λ_b (U60.match (== _a _b) (Book.Bool.false) λ_x_1((Book.Bool.true)))
 
@@ -1388,6 +1659,10 @@ Book.U60.if = λ_x λ_P λ_t λ_f (U60.match _x _t λ_x_1(_f))
 
 Book.U60.match = λ_x λ_P λ_s λ_z (U60.match _x _z λ_self_1((_s _self_1)))
 
+Book.U60.max = λ_a λ_b (((((Book.U60.to_bool) (> _a _b)) λ_x 0) _a) _b)
+
+Book.U60.min = λ_a λ_b (((((Book.U60.to_bool) (< _a _b)) λ_x 0) _a) _b)
+
 Book.U60.name.go = λ_n (U60.match _n λ_nil _nil λ_n_1(λ_nil (((Book.String.cons) (+ 97 (% _n_1 26))) (((Book.U60.name.go) (/ _n_1 26)) _nil))))
 
 Book.U60.name = λ_n ((Book.String.Concatenator.build) ((Book.U60.name.go) (+ _n 1)))
@@ -1410,13 +1685,15 @@ Book.test0 = λ_A λ_B λ_aa λ_ab λ_ba λ_bb λ_a λ_b (_ba (_ab (_aa (_aa _a)
 
 Book.test1 = λ_x (+ 50 12)
 
-Book._EXP = ((((Book.Kind.all) (Str "n")) (Book._Nat)) λ_n ((((Book.Kind.all) (Str "m")) (Book._Nat)) λ_m (Book._Nat)))
-Book._exp = (((Book.Kind.lam) (Str "n")) λ_n (((Book.Kind.lam) (Str "m")) λ_m (((Book.Kind.lam) (Str "P")) λ_P (((Book.Kind.app) (((Book.Kind.app) _m) ((((Book.Kind.all) (Str "x")) _P) λ_x _P))) (((Book.Kind.app) _n) _P)))))
-Book._C2 = (Book._Nat)
 Book._c2 = (((Book.Kind.lam) (Str "P")) λ_P (((Book.Kind.lam) (Str "s")) λ_s (((Book.Kind.lam) (Str "z")) λ_z (((Book.Kind.app) _s) (((Book.Kind.app) _s) _z)))))
+Book._C2 = (Book._Nat)
+Book._EXP = ((((Book.Kind.all) (Str "n")) (Book._Nat)) λ_n ((((Book.Kind.all) (Str "m")) (Book._Nat)) λ_m (Book._Nat)))
 Book.test10 = 
   let _term = (((Book.Kind.app) (((Book.Kind.app) (Book._exp)) (Book._c2))) (Book._c2)) 
   (((Book.Kind.Term.show) ((((Book.Kind.normal) (Book.Bool.true)) _term) (Book.Nat.zero))) (Book.Nat.zero))
+Book._exp = (((Book.Kind.lam) (Str "n")) λ_n (((Book.Kind.lam) (Str "m")) λ_m (((Book.Kind.lam) (Str "P")) λ_P (((Book.Kind.app) (((Book.Kind.app) _m) ((((Book.Kind.all) (Str "x")) _P) λ_x _P))) (((Book.Kind.app) _n) _P)))))
+
+Book.test11 = 0
 
 Book.test2 = 
   let _xs = ((((Book.List.cons) 0) 0) ((((Book.List.cons) 0) 1) ((((Book.List.cons) 0) 2) ((Book.List.nil) 0)))) 
@@ -1437,12 +1714,9 @@ Book.test8 = λ_a ((((Book.U60.if) _a) 0) (Str "test"))
 
 Book.test9 = ((((Book.String.unpar) 40) 41) (Str "((foo))"))
 
-
-Main = (Str.view ((Book.Kind.Book.to_hvm) ((Book.Kind.Book.parse) (Str "F = λf λx (f (f x))"))))
-
-
-
-
-
-
-
+Book.testBBT = (Str "
+File commented for backward compatibility.
+To run the tests, uncomment the code on:
+  testBBT.kind2
+  U60.Map
+")
diff --git a/bootstrap.js b/bootstrap.js
index 6865ee87..6cf40697 100644
--- a/bootstrap.js
+++ b/bootstrap.js
@@ -28,7 +28,7 @@ fs.readdirSync(bookDir).forEach(file => {
 });
 
 // Loads prelude
-var prelude = fs.readFileSync("./book/Kind.Book.to_hvm.prelude", "utf8");
+var prelude = fs.readFileSync("./book/Kind.Book.to_hvm.prelude.kind2", "utf8");
 const lines = prelude.split("\n");
 lines.shift();
 lines.pop();
diff --git a/kind2.hvm1 b/kind2.hvm1
index dcc15182..26f044f0 100644
--- a/kind2.hvm1
+++ b/kind2.hvm1
@@ -101,7 +101,7 @@
 (Reduce 1 (Txt txt))         = (Reduce.txt 1 txt)
 (Reduce r val)               = val
 
-(Reduce.app r (Lam nam bod)     arg) = (Reduce r (bod (Reduce r arg)))
+(Reduce.app r (Lam nam bod)     arg) = (Reduce r (bod (Reduce 0 arg)))
 //(Reduce.app r (Hol nam ctx ars) arg) = (Hol nam ctx (List.cons arg ars))
 (Reduce.app r fun               arg) = (App fun arg)
 
@@ -155,6 +155,7 @@
 // --------
 
 // Check if two terms are identical. If not...
+(Equal a b 24)  = 0 // limits depth FIXME: won't be necessary with better ref-ids equality
 (Equal a b dep) = (Equal.minor (Identical a b dep) a b dep)
 
 // Check if they're identical after a minor weak reduction. If not...
@@ -418,7 +419,8 @@ Compile.primitives = [
 
 (Normalizer (Ref nam val)) = (Normalizer val)
 (Normalizer (Ann val typ)) = (Normalizer val)
-(Normalizer val)           = (Compile val)
+//(Normalizer val)           = (Compile val)
+(Normalizer val)           = (Str.view (Compile val))
 
 (Checker (Ref nam val)) = (Checker val)
 (Checker (Ann val typ)) = (Checker.report (Check val typ 0))
@@ -426,4 +428,3 @@ Compile.primitives = [
 
 (Checker.report (Some x)) = (HVM.print "Check!" OK)
 (Checker.report None)     = (HVM.print "Error." ERR)
-
diff --git a/kind2.ts b/kind2.ts
index e8f84219..2a7357ba 100644
--- a/kind2.ts
+++ b/kind2.ts
@@ -1,3 +1,123 @@
+//// TODO
+//Kind.load
+//: ∀(name: String)
+  //Kind.Book
+//= λname
+  //(Kind.load.name #5 name (String.Map.new Kind.Term))
+
+//// Gets the source file of a definition
+//Kind.load.file_of
+//: ∀(name: String)
+  //String
+//= λname
+  //(String.concat name ".kind2")
+
+//// Loads a file into a new book
+//Kind.load.file
+//: ∀(file: String)
+  //Kind.Book
+//= λfile
+  //(HVM.load Kind.Book file λdata
+  //(Kind.Book.parse data))
+
+//// Loads a name into a book
+//Kind.load.name
+//: ∀(lims: #U60)
+  //∀(name: String)
+  //∀(book: Kind.Book)
+  //Kind.Book
+//= λlims
+  //(HVM.log #U60 ∀(name:String)∀(book:Kind.Book)Kind.Book lims
+  //#match lims = lims {
+    //#0: λname λbook book
+    //#+: λname λbook
+      //(HVM.print Kind.Book (String.concat "LOAD:" name)
+      //// Checks if name is already on book
+      //let P   = λx (Kind.Book)
+      //let new = λhas λbook
+        //// If it is, do nothing; otherwise, define it
+        //let P     = λx ∀(book: Kind.Book) (Kind.Book)
+        //let true  = λbook
+          //(HVM.print Kind.Book (String.concat (String.concat "OLD!:" name) (String.concat " -- " (Kind.keys book))) book)
+        //let false = λbook
+          //(HVM.print Kind.Book (String.concat (String.concat "NEW!:" name) (String.concat " -- " (Kind.keys book)))
+          //let file = (Kind.load.file (Kind.load.file_of name))
+          //let defs = (String.Map.to_list Kind.Term file)
+          //let bok1 = (Kind.load.define defs book)
+          //let file = (Kind.load.file (Kind.load.file_of name))
+          //let refs = (Kind.Book.get_refs file)
+          //let bok2 = (HVM.print ?a (String.concat "REC!:" (Kind.keys bok1)) (Kind.load.name.many lims-1 refs bok1))
+          //bok2)
+          ////(HVM.print.many Kind.Book refs book)
+
+        //((~has P true false) book)
+      //(~(String.Map.has.linear Kind.Term name book) P new))
+  //}: ∀(name: String) ∀(book: Kind.Book) Kind.Book)
+
+//// Loads many names into a book
+//Kind.load.name.many
+//: ∀(lims: #U60)
+  //∀(list: (List String))
+  //∀(book: Kind.Book)
+  //Kind.Book
+//= λlims λlist λbook
+  //let P    = λx ∀(book: Kind.Book) (Kind.Book)
+  //let cons = λhead λtail λbook 
+    ////(HVM.print Kind.Book
+      ////(String.concat "DEP:"
+      ////(String.concat head
+      ////(String.concat " BOOK:"
+      ////(Kind.Book.show book))))
+    //let bok2 = (Kind.load.name lims head book)
+    //(Kind.load.name.many lims tail bok2)
+  //let nil  = λbook book
+  //((~list P cons nil) book)
+
+//// Defines a term and loads its dependencies
+////Kind.load.define
+////: ∀(name: String)
+  ////∀(term: Kind.Term)
+  ////∀(book: Kind.Book)
+  ////Kind.Book
+////= λname λterm λbook
+  ////let book = (String.Map.set Kind.Term name term book)
+  ////let refs = (Kind.Term.get_refs term)
+  ////let book = (Kind.load.name.many refs book)
+  ////book
+
+//// Defines many terms
+//Kind.load.define
+//: ∀(defs: (List (Pair String Kind.Term)))
+  //∀(book: Kind.Book)
+  //Kind.Book
+//= λdefs λbook
+  //// If defs list isn't empty...
+  //let P    = λx ∀(book: Kind.Book) (Kind.Book)
+  //let cons = λdefs.head λdefs.tail λbook
+    //// Gets the def name/term
+    //let P   = λx (Kind.Book)
+    //let new = λname λterm 
+      //// Writes it to the book
+      //let bok2 = (String.Map.set Kind.Term name term book)
+      //(HVM.print Kind.Book (String.concat "DEF!:" name)
+      //// Recurses
+      //(Kind.load.define defs.tail bok2))
+    //(~defs.head P new)
+  //// If defs list is empty, return the book
+  //let nil  = λbook book
+  //((~defs P cons nil) book)
+
+
+//Kind.keys
+//: ∀(book: Kind.Book)
+  //String
+//= λbook
+  //let defs = (String.Map.to_list Kind.Term book)
+  //let defs = (List.app (Pair String Kind.Term) String (Pair.fst String Kind.Term) defs)
+  //(String.join defs)
+
+
+
 import { execSync } from 'child_process';
 import * as fs from 'fs';
 
@@ -15,10 +135,6 @@ export function str(result: string): string {
   return result.slice(1,-1).trim();
 }
 
-export function load(name: string): string {
-  return fs.readFileSync("./book/"+name+".kind2", "utf8");
-}
-
 export function get_refs(code: string): string {
   return run(`(Strs.view ((Book.Kind.Book.get_refs) ((Book.Kind.Book.parse) (Str \`${code}\`))))`).trim();
 }
@@ -27,4 +143,43 @@ export function to_hvm(code: string): string {
   return str(run(`(Str.view ((Book.Kind.Book.to_hvm) ((Book.Kind.Book.parse) (Str \`${code}\`))))`).trim());
 }
 
-console.log(get_refs(`plus2 = λx (Nat.succ (Nat.succ x))`));
+//// Loads a name into a book
+//Kind.load.name
+//: ∀(lims: #U60)
+  //∀(name: String)
+  //∀(book: Kind.Book)
+  //Kind.Book
+//= λlims
+  //(HVM.log #U60 ∀(name:String)∀(book:Kind.Book)Kind.Book lims
+  //#match lims = lims {
+    //#0: λname λbook book
+    //#+: λname λbook
+      //(HVM.print Kind.Book (String.concat "LOAD:" name)
+      //// Checks if name is already on book
+      //let P   = λx (Kind.Book)
+      //let new = λhas λbook
+        //// If it is, do nothing; otherwise, define it
+        //let P     = λx ∀(book: Kind.Book) (Kind.Book)
+        //let true  = λbook
+          //(HVM.print Kind.Book (String.concat (String.concat "OLD!:" name) (String.concat " -- " (Kind.keys book))) book)
+        //let false = λbook
+          //(HVM.print Kind.Book (String.concat (String.concat "NEW!:" name) (String.concat " -- " (Kind.keys book)))
+          //let file = (Kind.load.file (Kind.load.file_of name))
+          //let defs = (String.Map.to_list Kind.Term file)
+          //let bok1 = (Kind.load.define defs book)
+          //let file = (Kind.load.file (Kind.load.file_of name))
+          //let refs = (Kind.Book.get_refs file)
+          //let bok2 = (HVM.print ?a (String.concat "REC!:" (Kind.keys bok1)) (Kind.load.name.many lims-1 refs bok1))
+          //bok2)
+          ////(HVM.print.many Kind.Book refs book)
+        //((~has P true false) book)
+      //(~(String.Map.has.linear Kind.Term name book) P new))
+  //}: ∀(name: String) ∀(book: Kind.Book) Kind.Book)
+
+export function load_file(file: string): string {
+  return fs.readFileSync("./book/"+file, "utf8");
+}
+
+export function load_name(
+
+console.log(get_refs(load("Bool")));