diff --git a/Cargo.toml b/Cargo.toml
index 0e49799d..82807205 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "kind2"
-version = "0.2.69"
+version = "0.2.70"
 edition = "2021"
 description = "A pure functional functional language that uses the HVM."
 repository = "https://github.com/Kindelia/Kind2"
diff --git a/README.md b/README.md
index 5902a953..de012177 100644
--- a/README.md
+++ b/README.md
@@ -1,62 +1,64 @@
 Kind2
 =====
 
-Kind2 is a pure functional, lazy, non-garbage-collected, general-purpose,
-dependently typed programming language focusing on performance and usability. It
-features a blazingly fast type-checker based on **optimal
-[normalization-by-evaluation](https://en.wikipedia.org/wiki/Normalisation_by_evaluation)**. It can also
-compile programs to [HVM](https://github.com/kindelia/hvm) and [Kindelia](https://github.com/kindelia/kindelia),
-and can be used to prove and verify mathematical theorems.
+**Kind2** is a **functional programming language** and **proof assistant**.
+
+It is a complete rewrite of [Kind1](https://github.com/kindelia/kind-legacy), based on
+[HVM](https://github.com/kindelia/hvm), a **lazy**, **non-garbage-collected** and **massively parallel** virtual
+machine. In [our benchmarks](https://github.com/kindelia/functional-benchmarks), its type-checker outperforms every
+alternative proof assistant by a far margin, and its programs can offer exponential speedups over Haskell's GHC. Kind2
+unleashes the [inherent parallelism of the Lambda
+Calculus](https://github.com/VictorTaelin/Symmetric-Interaction-Calculus) to become the ultimate programming language of
+the next century.
+
+**Welcome to the inevitable parallel, functional future of computers!**
 
 Examples
 --------
 
-Pure functions can be defined using an equational notation that resembles [Haskell](https://www.haskell.org/):
+Pure functions are defined via equations, as in [Haskell](https://www.haskell.org/):
 
-```idris
-List.map <a: Type> <b: Type> (x: (List a)) (f: (x: a) b) : (List b)
-List.map a b (Nil t)       f = (Nil b)
-List.map a b (Cons t x xs) f = (Cons b (f x) (List.map xs f))
+```javascript
+// Applies a function to every element of a list
+map <a> <b> (list: List a) (f: a -> b) : List b
+map a b Nil              f = Nil
+map a b (Cons head tail) f = Cons (f x) (map tail f)
 ```
 
-Mathematical theorems can be proved via inductive reasoning, as in [Idris](https://www.idris-lang.org/) and [Agda](https://wiki.portal.chalmers.se/agda/pmwiki.php):
+Side-effective programs are written via monadic monads, resembling [Rust](https://www.rust-lang.org/) and [TypeScript](https://www.typescriptlang.org/):
 
-```idris
-Nat.commutes (a: Nat) (b: Nat) : (Nat.add a b) == (Nat.add b a)
-Nat.commutes Zero     b = (Nat.comm.a b)
-Nat.commutes (Succ a) b =
-  let e0 = (Equal.apply @x(Succ x) (Nat.commutes a b))
-  let e1 = (Equal.mirror (Nat.commutes.b b a))
-  (Equal.chain e0 e1)
-```
-
-Normal programs can be written in a monadic syntax that is inspired by [Rust](https://www.rust-lang.org/) and [TypeScript](https://www.typescriptlang.org/):
-
-```idris
-Main : (IO (Result () String)) {
-  ask limit = (IO.prompt "Enter limit:")
+```javascript
+// Prints the double of every numbet up to a limit
+Main : IO (Result () String) {
+  ask limit = IO.prompt "Enter limit:"
   for x in (List.range limit) {
-    (IO.print "{} * 2 = {}" x (Nat.double x))
+    IO.print "{} * 2 = {}" x (Nat.double x)
   }
-  return (Ok ())
+  return Ok ()
 }
 ```
 
+Theorems can be proved inductivelly, as in [Agda](https://wiki.portal.chalmers.se/agda/pmwiki.php) and [Idris](https://www.idris-lang.org/):
+
+```javascript
+// Black Friday Theorem. Proof that, for every Nat n: n * 2 / 2 == n.
+black_friday_theorem (n: Nat) : Equal Nat (Nat.half (Nat.double n)) n
+black_friday_theorem Nat.zero     = Equal.refl
+black_friday_theorem (Nat.succ n) = Equal.apply (x => Nat.succ x) (black_friday_theorem n)
+```
+
 For more examples, check the [Wikind](https://github.com/kindelia/wikind).
 
-Installation
-------------
+Usage
+-----
 
-Install [Rust](https://www.rust-lang.org/tools/install) first, then enter:
+First, install [Rust](https://www.rust-lang.org/tools/install) first, then enter:
 
 ```
 cargo install kind2
 ```
 
-Enter `kind2` on the terminal to make sure it worked.
-
-Usage
------
+Then, use any of the commands below:
 
 Command    | Usage                     | Note
 ---------- | ------------------------- | --------------------------------------------------------------
@@ -64,9 +66,13 @@ Check      | `kind2 check  file.kind2` | Checks all definitions.
 Eval       | `kind2 eval   file.kind2` | Runs using the type-checker's evaluator.
 Run        | `kind2 run    file.kind2` | Runs using HVM's evaluator, on Rust-mode.
 To-HVM     | `kind2 to-hvm file.kind2` | Generates a [.hvm](https://github.com/kindelia/hvm) file. Can then be compiled to C.
-To-KDL     | `kind2 to-kdl file.kind2` | Generates a [.kdl](https://github.com/kindelia/kindelia) file. Can then be deployed to Kindelia.
+To-KDL     | `kind2 to-kdl file.kind2` | Generates a [.kdl](https://github.com/kindelia/kindelia) file. Can then be deployed to [Kindelia](https://github.com/kindelia/kindelia).
 
-Benchmarks
-----------
+Executables can be generated via HVM:
 
-In preliminary [benchmarks](/bench), Kind2's type-checker has outperformed Agda, Idris by 90x to 900x, which is an expressive difference. That said, we only tested a few small programs, so there isn't enough data to draw a conclusion yet. We're working on a more extensive benchmark suite. 
+```
+kind2 to-hvm file.kind2
+hvm compile file.hvm
+clang -O2 file.c -o file
+./file
+```
diff --git a/bench/conv_eval.idr b/bench/conv_eval.idr
deleted file mode 100644
index b1e11892..00000000
--- a/bench/conv_eval.idr
+++ /dev/null
@@ -1,239 +0,0 @@
-CBool : Type
-CBool = (B : Type) -> B -> B -> B
-
-toBool : CBool -> Bool
-toBool = \b => b Bool True False
-
-ctrue : CBool
-ctrue = \b, t, f => t
-
-and : CBool -> CBool -> CBool
-and = \a, b, bb, t, f => a bb (b bb t f) f
-
-CNat : Type
-CNat = (n : Type) -> (n -> n) -> n -> n
-
-add : CNat -> CNat -> CNat
-add = \a, b, n, s, z => a n s (b n s z)
-
-cmul : CNat -> CNat -> CNat
-cmul = \a, b, n, s => a n (b n s)
-
-suc : CNat -> CNat
-suc = \a, n, s, z => s (a n s z)
-
-CEq : {A : Type} -> A -> A -> Type
-CEq = \x, y => (P : A -> Type) -> P x -> P y
-
-crefl : {A : Type} -> {x : A} -> CEq {A} x x
-crefl = \p, px => px
-
-n2 : CNat
-n2 = \n, s, z => s (s z)
-
-n3 : CNat
-n3 = \n, s, z => s (s (s z))
-
-n4 : CNat
-n4 = \n, s, z => s (s (s (s z)))
-
-n5 : CNat
-n5 = \n, s, z => s (s (s (s (s z))))
-
-n10 : CNat
-n10  = cmul n2 n5
-
-n10b : CNat
-n10b = cmul n5 n2
-
-n15 : CNat
-n15 = add n10  n5
-
-n15b : CNat
-n15b   = add n10b n5
-
-n18 : CNat
-n18    = add n15  n3
-
-n18b : CNat
-n18b   = add n15b n3
-
-n19 : CNat
-n19    = add n15  n4
-
-n19b : CNat
-n19b   = add n15b n4
-
-n20 : CNat
-n20    = cmul n2 n10
-
-n20b : CNat
-n20b   = cmul n2 n10b
-
-n21 : CNat
-n21    = suc n20
-
-n21b : CNat
-n21b   = suc n20b
-
-n22 : CNat
-n22    = suc n21
-
-n22b : CNat
-n22b   = suc n21b
-
-n23 : CNat
-n23    = suc n22
-
-n23b : CNat
-n23b   = suc n22b
-
-n100 : CNat
-n100   = cmul n10   n10
-
-n100b : CNat
-n100b  = cmul n10b  n10b
-
-n10k : CNat
-n10k   = cmul n100  n100
-
-n10kb : CNat
-n10kb  = cmul n100b n100b
-
-n100k : CNat
-n100k  = cmul n10k  n10
-
-n100kb : CNat
-n100kb = cmul n10kb n10b
-
-n1M : CNat
-n1M    = cmul n10k  n100
-
-n1Mb : CNat
-n1Mb   = cmul n10kb n100b
-
-n5M : CNat
-n5M    = cmul n1M   n5
-
-n5Mb : CNat
-n5Mb   = cmul n1Mb  n5
-
-n10M : CNat
-n10M   = cmul n5M   n2
-
-n10Mb : CNat
-n10Mb  = cmul n5Mb  n2
-
-Tree : Type
-Tree = (T : Type) -> (T -> T -> T) -> T -> T
-
-leaf : Tree
-leaf = \t, n, l => l
-
-node : Tree -> Tree -> Tree
-node = \t1, t2, t, n, l => n (t1 t n l) (t2 t n l)
-
-fullTree : CNat -> Tree
-fullTree = \n => n Tree (\t => node t t) leaf
-
--- full tree with given trees at bottom level
-fullTreeWithLeaf : Tree -> CNat -> Tree
-fullTreeWithLeaf = \bottom, n => n Tree (\t => node t t) bottom
-
-forceTree : Tree -> CBool
-forceTree = \t => t CBool and ctrue
-
-t15 : Tree
-t15  = fullTree n15
-t15b : Tree
-t15b = fullTree n15b
-t18 : Tree
-t18  = fullTree n18
-t18b : Tree
-t18b = fullTree n18b
-t19 : Tree
-t19  = fullTree n19
-t19b : Tree
-t19b = fullTree n19b
-t20 : Tree
-t20  = fullTree n20
-t20b : Tree
-t20b = fullTree n20b
-t21 : Tree
-t21  = fullTree n21
-t21b : Tree
-t21b = fullTree n21b
-t22 : Tree
-t22  = fullTree n22
-t22b : Tree
-t22b = fullTree n22b
-t23 : Tree
-t23  = fullTree n23
-t23b : Tree
-t23b = fullTree n23b
-
--- CNat conversion
---------------------------------------------------------------------------------
-
-convn1M : CEq Main.n1M Main.n1Mb
-convn1M = crefl
-
--- convn5M : CEq Main.n5M Main.n5Mb
--- convn5M = crefl
-
--- convn10M : CEq Main.n10M Main.n10Mb
--- convn10M = crefl
-
--- Full tree conversion
---------------------------------------------------------------------------------
-
--- convt15  : CEq Main.t15  Main.t15b
--- convt15  = crefl
--- convt18  : CEq Main.t18  Main.t18b
--- convt18  = crefl
--- convt19  : CEq Main.t19  Main.t19b
--- convt19  = crefl
--- convt20  : CEq Main.t20  Main.t20b
--- convt20  = crefl
--- convt21  : CEq Main.t21  Main.t21b
--- convt21  = crefl
--- convt22  : CEq Main.t22  Main.t22b
--- convt22  = crefl
--- convt23  : CEq Main.t23  Main.t23b
--- convt23  = crefl
-
--- Full meta-containing tree conversion
---------------------------------------------------------------------------------
-
--- convmt15 : CEq Main.t15b  (fullTreeWithLeaf ? Main.n15 )
--- convmt15 = crefl
--- convmt18 : CEq Main.t18b  (fullTreeWithLeaf ? Main.n18 )
--- convmt18 = crefl
--- convmt19 : CEq Main.t19b  (fullTreeWithLeaf ? Main.n19 )
--- convmt19 = crefl
--- convmt20 : CEq Main.t20b  (fullTreeWithLeaf ? Main.n20 )
--- convmt20 = crefl
--- convmt21 : CEq Main.t21b  (fullTreeWithLeaf ? Main.n21 )
--- convmt21 = crefl
--- convmt22 : CEq Main.t22b  (fullTreeWithLeaf ? Main.n22 )
--- convmt22 = crefl
--- convmt23 : CEq Main.t23b  (fullTreeWithLeaf ? Main.n23 )
--- convmt23 = crefl
-
--- Full tree forcing
---------------------------------------------------------------------------------
-
--- forcet15 : CEq (toBool (forceTree Main.t15)) True
--- forcet15 = crefl
--- forcet18 : CEq (toBool (forceTree Main.t18)) True
--- forcet18 = crefl
--- forcet19 : CEq (toBool (forceTree Main.t19)) True
--- forcet19 = crefl
--- forcet20 : CEq (toBool (forceTree Main.t20)) True
--- forcet20 = crefl
--- forcet21 : CEq (toBool (forceTree Main.t21)) True
--- forcet21 = crefl
---forcet22 : CEq (toBool (forceTree Main.t22)) True
---forcet22 = crefl
--- forcet23 : CEq (toBool (forceTree Main.t23)) True
--- forcet23 = crefl
diff --git a/bench/conv_eval.kind2 b/bench/conv_eval.kind2
deleted file mode 100644
index 2a45f7f2..00000000
--- a/bench/conv_eval.kind2
+++ /dev/null
@@ -1,156 +0,0 @@
-Bool : Type
-True : Bool
-False : Bool
-
-CBool : Type
-CBool = (t: Type) t -> t -> t
-
-CBool.to_bool (x : CBool) : Bool
-CBool.to_bool x = (x Bool True False)
-
-CTrue : CBool
-CTrue = p => t => f => t
-
-CFalse : CBool
-CFalse = p => t => f => f
-
-And (a: CBool) (b: CBool) : CBool
-And a b = p => t => f => (a p (b p t f) f)
-
-CNat : Type
-CNat = (n: Type) (n -> n) -> n -> n
-
-Add (a: CNat) (b: CNat) : CNat
-Add a b = n => s => z => (a n s (b n s z))
-
-CMul (a: CNat) (b: CNat) : CNat
-CMul a b = n => s => (a n (b n s))
-
-Suc (a: CNat) : CNat
-Suc a = n => s => z => (s (a n s z))
-
-CEqual (t: Type) (a: t) (b: t) : Type
-CEqual t a b = (p: t -> Type) (p a) -> (p b)
-
-CRefl (t: Type) (x: t) : (CEqual t x x)
-CRefl t x = p => px => px
-
-N0 : CNat
-N0 = n => s => z => z
-
-N2 : CNat
-N2 = n => s => z => (s (s z))
-
-N3 : CNat
-N3 = n => s => z => (s (s (s z)))
-
-N4 : CNat
-N4 = n => s => z => (s (s (s (s z))))
-
-N5 : CNat
-N5 = n => s => z => (s (s (s (s (s z)))))
-
-N10 : CNat
-N10 = (CMul N2 N5)
-
-N10b : CNat
-N10b = (CMul N5 N2)
-
-N15 : CNat
-N15 = (Add N10 N5)
-
-N15b : CNat
-N15b = (Add N10b N5)
-
-N18 : CNat
-N18 = (Add N15 N3)
-
-N18b : CNat
-N18b = (Add N15b N3)
-
-N19 : CNat
-N19 = (Add N15 N4)
-
-N19b : CNat
-N19b = (Add N15b N4)
-
-N20 : CNat
-N20 = (CMul N2 N10)
-
-N20b : CNat
-N20b = (CMul N2 N10b)
-
-N21 : CNat
-N21 = (Suc N20)
-
-N21b : CNat
-N21b = (Suc N20b)
-
-N22 : CNat
-N22 = (Suc N21)
-
-N22b : CNat
-N22b = (Suc N21b)
-
-N23 : CNat
-N23 = (Suc N22)
-
-N23b : CNat
-N23b = (Suc N22b)
-
-N100 : CNat
-N100 = (CMul N10 N10)
-
-N100b : CNat
-N100b = (CMul N10b N10b)
-
-N10k : CNat
-N10k = (CMul N100 N100)
-
-N10kb : CNat
-N10kb = (CMul N100b N100b)
-
-N100k : CNat
-N100k = (CMul N10k N10)
-
-N100kb : CNat
-N100kb = (CMul N10kb N10b)
-
-N1M : CNat
-N1M = (CMul N10k N100)
-
-N1Mb : CNat
-N1Mb = (CMul N10kb N100b)
-
-N5M : CNat
-N5M = (CMul N1M N5)
-
-N5Mb : CNat
-N5Mb = (CMul N1Mb N5)
-
-N10M : CNat
-N10M = (CMul N5M N2)
-
-N10Mb : CNat
-N10Mb = (CMul N5Mb N2)
-
-CTree : Type
-CTree = (t: Type) (t -> t -> t) -> t -> t
-
-CLeaf : CTree
-CLeaf = t => n => l => l
-
-CNode (t1: CTree) (t2: CTree) : CTree
-CNode t1 t2 = t => n => l => (n (t1 t n l) (t2 t n l))
-
-FullCTree (n: CNat) : CTree
-FullCTree n = (n CTree (t => CNode t t) CLeaf)
-
-Num : CNat
-Num = N2
-
-Force (n: CNat) : Bool
-Force n = (n Bool (x => x) True)
-
-Main : (CEqual CNat N1M N1Mb)
-Main = (CRefl CNat N1M)
diff --git a/bench/nat_exp.agda b/bench/nat_exp.agda
deleted file mode 100644
index 799345ea..00000000
--- a/bench/nat_exp.agda
+++ /dev/null
@@ -1,25 +0,0 @@
-data Nat : Set where
-  z : Nat
-  s : Nat -> Nat
-
-data The : (x : Nat) -> Set where
-  val : (x : Nat) -> The x
-
-add : Nat -> Nat -> Nat
-add a (s b) = s (add a b)
-add a z     = a
-
-mul : Nat -> Nat -> Nat
-mul a (s b) = add a (mul a b)
-mul a z     = z
-
-exp : Nat -> Nat -> Nat
-exp a (s b) = mul a (exp a b)
-exp a     z = s z
-
-nul : Nat -> Nat
-nul (s a) = (nul a)
-nul z     = z
-
-work : The (nul (exp (s (s (s z))) (s (s (s (s (s (s (s (s z))))))))))
-work = val z
diff --git a/bench/nat_exp.idr b/bench/nat_exp.idr
deleted file mode 100644
index 13c3a196..00000000
--- a/bench/nat_exp.idr
+++ /dev/null
@@ -1,26 +0,0 @@
-data NAT : Type where
-  Z : NAT
-  S : NAT -> NAT
-
-data The : NAT -> Type where
-  Val : (x : NAT) -> The x
-
-add : NAT -> NAT -> NAT
-add a (S b) = S (add a b)
-add a Z     = a
-
-mul : NAT -> NAT -> NAT
-mul a (S b) = add a (mul a b)
-mul a Z     = Z
-
-exp : NAT -> NAT -> NAT
-exp a (S b) = mul a (exp a b)
-exp a     Z = S Z
-
-nul : NAT -> NAT
-nul (S a) = nul a
-nul Z     = Z
-
-work : The (nul (exp (S (S (S Z))) (S (S (S (S (S (S (S (S Z))))))))))
-work = Val Z
-
diff --git a/bench/nat_exp.kind2 b/bench/nat_exp.kind2
deleted file mode 100644
index 626cfa6b..00000000
--- a/bench/nat_exp.kind2
+++ /dev/null
@@ -1,26 +0,0 @@
-Nat : Type
-Z : Nat
-S (pred: Nat) : Nat
-
-The (x: Nat) : Type
-Val (x: Nat) : (The x)
-
-Add (a: Nat) (b: Nat) : Nat
-Add a (S b) = (S (Add a b))
-Add a (Z)   = a
-
-Mul (a: Nat) (b: Nat) : Nat
-Mul a (S b) = (Add a (Mul a b))
-Mul a (Z)   = (Z)
-
-Exp (a: Nat) (b: Nat) : Nat
-Exp a (S b) = (Mul a (Exp a b))
-Exp a (Z)   = (S Z)
-
-Nul (n: Nat) : Nat
-Nul (S a) = (Nul a)
-Nul (Z)   = (Z)
-
-Work : (The (Nul (Exp (S (S (S Z))) (S (S (S (S (S (S (S (S Z))))))))))) {
-  (Val Z)
-}
diff --git a/bench/nat_exp.lean b/bench/nat_exp.lean
deleted file mode 100644
index cf98a958..00000000
--- a/bench/nat_exp.lean
+++ /dev/null
@@ -1,25 +0,0 @@
-inductive NAT where
-  | Z : NAT
-  | S : NAT -> NAT
-
-inductive The : NAT -> Type where
-  | val : (x : NAT) -> The x
-
-def add : NAT -> NAT -> NAT
-  | a, NAT.S b => NAT.S (add a b)
-  | a, NAT.Z   => a
-
-def mul : NAT -> NAT -> NAT
-  | a, NAT.S b => add a (mul a b)
-  | _, NAT.Z   => NAT.Z
-
-def exp : NAT -> NAT -> NAT
-  | a, NAT.S b => mul a (exp a b)
-  | _, NAT.Z   => NAT.S NAT.Z
-
-def nul : NAT -> NAT
-  | NAT.S a => nul a
-  | NAT.Z   => NAT.Z
- 
-def work : The (nul (exp (NAT.S (NAT.S (NAT.S NAT.Z))) (NAT.S (NAT.S (NAT.S (NAT.S (NAT.S (NAT.S (NAT.S (NAT.S NAT.Z))))))))))
-  := @The.val NAT.Z
diff --git a/bench/nat_exp.v b/bench/nat_exp.v
deleted file mode 100644
index 41561462..00000000
--- a/bench/nat_exp.v
+++ /dev/null
@@ -1,36 +0,0 @@
-Inductive Nat : Type :=
-  | Z
-  | S : Nat -> Nat.
-
-(* Inductive The : Nat -> Type :=
-   | val : forall (x : Nat), The x. *)
-
-Inductive The : Nat -> Prop :=
-  | val (x : Nat) : The x.
-
-Fixpoint add (m : Nat) (n : Nat) : Nat :=
-  match m, n with
-  | m, Z     => m
-  | m, (S n) => S (add m n)
-  end.
-
-Fixpoint mul (m : Nat) (n : Nat) : Nat :=
-  match m, n with
-  | m, Z     => Z
-  | m, (S n) => (add m (mul m n))
-  end.
-
-Fixpoint exp (m : Nat) (n : Nat) : Nat :=
-  match m, n with
-  | m, Z     => (S Z)
-  | m, (S n) => (mul m (exp m n))
-  end.
-
-Fixpoint nul (n : Nat) : Nat :=
-  match n with
-  | Z     => Z
-  | (S n) => nul n
-  end.
-
-Definition work : The (nul (exp (S (S (S Z))) (S (S (S (S (S (S (S (S Z)))))))))) :=
-   val Z.