diff --git a/Makefile b/Makefile
index ad536957d45d83a8dbfafa10f79814757470d0cd..50f2bfae2b59748b57ffac45ea20b5140c6827e6 100644
--- a/Makefile
+++ b/Makefile
@@ -1,23 +1,11 @@
-LP = lambdapi
-LP_FLAGS = -v0 -w
-LP_SRC  != find encodings paper -type f -name "*.lp"
-LP_OBJ = ${LP_SRC:S/.lp$/.lpo/}
+.PHONY: encoding
+encoding:
+	${MAKE} -C personoj
 
-.SUFFIXES: .lpo .lp
-
-all: ${LP_OBJ}
-
-.lp.lpo:
-	${LP} check ${LP_FLAGS} --gen-obj $<
-
-.PHONY: install
-install: lambdapi.pkg
-	${LP} install lambdapi.pkg ${LP_SRC}
-
-.PHONY: uninstall
-uninstall:
-	${LP} uninstall lambdapi.pkg
+.PHONY: tests
+tests:
+	${MAKE} -C tests
 
 .PHONY: clean
 clean:
-	rm -f ${LP_OBJ}
+	find . -type f -name "*.lpo" -exec rm -f {} +
diff --git a/README.md b/README.md
index c3d6f599da5aed574f04e187786829ea90e50734..081da03ea743be295d3da8e1a8011aaa17bcdc59 100644
--- a/README.md
+++ b/README.md
@@ -14,22 +14,22 @@ library, also known as _Prelude_. The prelude is available
 
 ## Requirements
 
-[`lambdapi`](https://github.com/Deducteam/lambdapi.git) later than 
-3e5c7ee2388d233fdca05776009b5cb158e48d97,
+[`lambdapi`](https://github.com/Deducteam/lambdapi.git), but a development
+version,
 
 ``` sh
-git clone github.com/Deducteam/lambdapi.git
-git checkout 3e5c7ee2388d233fdca05776009b5cb158e48d97
+git clone github.com/gabrielhdt/lambdapi.git
+git checkout 3ac05539d019206ab191c21c8b487e9fb0750aee
 make
 make install
 ```
 
 ## Structure
 
-- `encodings`: encoding of PVS into Dedukti
-- `paper`: some specifications presented in papers
+- `personoj`: encoding of PVS into Dedukti
+- `personoj/extra`: encodings that are not needed for PVS
+- `personoj/examples`: examples of PVS development in Lambdapi
 - `sandbox`: miscellaneous experiments
-- `tools`: some additional scripts and utilities
 
 ## Dedukti coding conventions
 
diff --git a/encodings/prenex/kind.lp b/encodings/prenex/kind.lp
deleted file mode 100644
index c36b9e0def6bfb85691044911e01259a28bd290e..0000000000000000000000000000000000000000
--- a/encodings/prenex/kind.lp
+++ /dev/null
@@ -1,9 +0,0 @@
-require open personoj.encodings.lhol
-             personoj.encodings.deptype;
-
-constant symbol Scheme: TYPE;
-injective symbol Els: Scheme → TYPE;
-constant symbol lift: Kind → Scheme;
-rule Els (lift $X) ↪ Ty $X;
-constant symbol ∀: (Set → Scheme) → Scheme;
-rule Els (∀ $e) ↪ Π t: Set, Els ($e t);
diff --git a/lambdapi.mk b/lambdapi.mk
new file mode 100644
index 0000000000000000000000000000000000000000..30d760dd8f8213d8ce5c69c1e02ec48b86e58c73
--- /dev/null
+++ b/lambdapi.mk
@@ -0,0 +1,23 @@
+LP       ?= lambdapi
+LP_FLAGS ?= -v0 -w
+LP_SRC   ?=
+LP_OBJ   ?= ${LP_SRC:S/.lp$/.lpo/}
+
+.SUFFIXES: .lpo .lp
+
+all: ${LP_OBJ}
+
+.lp.lpo:
+	${LP} check ${LP_FLAGS} --gen-obj $<
+
+.PHONY: install
+install: lambdapi.pkg
+	${LP} install ${LP_SRC} ${LP_OBJ}
+
+.PHONY: uninstall
+uninstall:
+	${LP} uninstall
+
+.PHONY: clean
+clean:
+	rm -f ${LP_OBJ}
diff --git a/personoj/Makefile b/personoj/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..662be101673b8ba37faebd7cd9ff0ad3cd56462e
--- /dev/null
+++ b/personoj/Makefile
@@ -0,0 +1,3 @@
+LP_SRC != find . -type f -name "*.lp"
+
+.include "../lambdapi.mk"
diff --git a/encodings/builtins.lp b/personoj/builtins.lp
similarity index 83%
rename from encodings/builtins.lp
rename to personoj/builtins.lp
index 07edfb415da4f746ce934b40b59ef5e8d8c243db..f25efac143ff1fb8d6e32f7cfeec857ba6696e70 100644
--- a/encodings/builtins.lp
+++ b/personoj/builtins.lp
@@ -1,7 +1,7 @@
-require open personoj.encodings.lhol
-             personoj.encodings.pvs_cert
-             personoj.encodings.logical
-             personoj.encodings.equality;
+require open personoj.lhol
+             personoj.pvs_cert
+             personoj.logical
+             personoj.equality;
 
 constant symbol {|!Number!|}: Set;
 
diff --git a/personoj/coercions.lp b/personoj/coercions.lp
new file mode 100644
index 0000000000000000000000000000000000000000..906e4444b5914883c9a22669194c303f1652d386
--- /dev/null
+++ b/personoj/coercions.lp
@@ -0,0 +1,34 @@
+require open personoj.lhol
+             personoj.pvs_cert
+             personoj.logical;
+require personoj.tuple as T;
+
+coercion "set-pred" λ (t: Set) (_: El t), true : Π t : Set, (El (t ~> prop)) on 1;
+coercion "pred-set" @psub : Π (t: Set) (p: El (t ~> prop)), Set on 2;
+
+coercion "psub-fst" 
+  λ (t: Set) (p: El t → Prop) (m: El (@psub t p)), @fst t p m :
+  Π (t: Set) (p: El (t ~> prop)) (m : El (@psub t p)), El t
+on 3;
+coercion "psub-pair" 
+  λ (t: Set) (p: El t → Prop) (m: El t) (π: Prf (p m)), @pair t p m π :
+  Π (t: Set) (p: El (t ~> prop)) (m: El t) (_: Prf (p m) ), El (@psub t p)
+on 3;
+coercion "psub-fst-tr" 
+  λ (t: Set) (u: Set) (p: El t → Prop) (m: El (@psub t p)), $c[@fst t p m] :
+  Π (t: Set) (u: Set) (p: El t → Prop) (m: El (@psub t p)), El u
+  on 4
+with c : El t → El u;
+coercion "psub-pair-tr" 
+  λ (t: Set) (u: Set) (p: El u → Prop) (m: El t) (π: Prf (p _)), @pair u p ($c[m]) π :
+  Π (t: Set) (u: Set) (p: El u → Prop) (m: El t) (_: Prf (p _)), El (@psub u p)
+  on 4
+with c : El t → El u;
+
+coercion "tuple"
+  λ (a0 b0 a1 b1: Set) (t: El (T.t a0 b0)),
+    T.cons {a1} {b1} $c[T.car {a0} {b0} t] $d[T.cdr {a0} {b0} t]:
+  Π (a0 b0 a1 b1: Set) (_: El (T.t a0 b0)), El (T.t a1 b1)
+  on 5
+with c : El a0 → El a1
+with d : El b0 → El b1;
diff --git a/encodings/deptype.lp b/personoj/deptype.lp
similarity index 85%
rename from encodings/deptype.lp
rename to personoj/deptype.lp
index d6c57766c5e3cdfbfba79edb96278ad1295041a3..b50e720ff48da663ea0e1cb889ff314c247fadaa 100644
--- a/encodings/deptype.lp
+++ b/personoj/deptype.lp
@@ -5,8 +5,8 @@
 /// allows to define
 /// cons(n: nat, r: real, v: vector_real[n].vec): vector_real[n + 1].vec
 
-require open personoj.encodings.lhol
-             personoj.encodings.pvs_cert;
+require open personoj.lhol
+             personoj.pvs_cert;
 
 constant symbol Kind: TYPE;
 constant symbol set: Kind;
diff --git a/encodings/equality.lp b/personoj/equality.lp
similarity index 74%
rename from encodings/equality.lp
rename to personoj/equality.lp
index 29ca16f546e78da0c20fb8044724a7c4f1dc32a9..8cbcf36159fbaa05f01a27b0c9b2f10930c4324f 100644
--- a/encodings/equality.lp
+++ b/personoj/equality.lp
@@ -1,8 +1,8 @@
 // Usual prenex polymorphic equaltiy, with two arguments
 require open
-  personoj.encodings.lhol
-  personoj.encodings.pvs_cert
-  personoj.encodings.logical;
+  personoj.lhol
+  personoj.pvs_cert
+  personoj.logical;
 
 // We don't use prenex encoding to have implicit arguments.
 symbol eq {s: Set}: El s → El s → Prop;
@@ -23,8 +23,7 @@ rule Prf (eq $x $y) ↪ Π p: El (_ ~> prop), Prf (p $x) → Prf (p $y);
 opaque
 symbol eq_refl {a: Set} (x: El a): Prf (x = x) ≔
 begin
-  assume a x p h;
-  apply h;
+  refine λ a x p (h: Prf (p x)), h;
 end;
 builtin "refl" ≔ eq_refl;
 
@@ -32,6 +31,8 @@ opaque
 symbol eq_trans {a: Set} (x y z: El a) (_: Prf (x = y)) (_: Prf (y = z))
       : Prf (x = z) ≔
 begin
-  assume a x y z hxy hyz p px;
-  refine hyz p (hxy p px);
+  refine λ a x y z (hxy: Prf (x = y)) (hyz: Prf (y = z)) p (px: Prf (p x)),
+         hyz p (hxy p px);
+  // assume a x y z hxy hyz p px;
+  // refine hyz p (hxy p px);
 end;
diff --git a/encodings/equality_tup.lp b/personoj/equality_tup.lp
similarity index 68%
rename from encodings/equality_tup.lp
rename to personoj/equality_tup.lp
index e4a9b3cc181bcbcbadd1608a9d16baa75811f0db..31bedc9217bce02621aa7e5dea187102a99d70b7 100644
--- a/encodings/equality_tup.lp
+++ b/personoj/equality_tup.lp
@@ -1,8 +1,8 @@
 // Equality defined on tuple of arguments
-require open personoj.encodings.lhol
-             personoj.encodings.pvs_cert;
-require personoj.encodings.tuple as T;
-require open personoj.encodings.logical;
+require open personoj.lhol
+             personoj.pvs_cert;
+require personoj.tuple as T;
+require open personoj.logical;
 
 // Equality operates on the maximal supertype. It allows to profit
 // from predicate subtyping for free in the propositional equality.
diff --git a/paper/proof_irr.lp b/personoj/examples/proof_irr.lp
similarity index 89%
rename from paper/proof_irr.lp
rename to personoj/examples/proof_irr.lp
index 0ab530104014afefe180e0b231854fc578412adc..84fb85f03343a768d5765d154656d6d3456bdbbe 100644
--- a/paper/proof_irr.lp
+++ b/personoj/examples/proof_irr.lp
@@ -1,7 +1,7 @@
-require open personoj.encodings.lhol
-             personoj.encodings.pvs_cert
-             personoj.encodings.logical
-             personoj.encodings.equality;
+require open personoj.lhol
+             personoj.pvs_cert
+             personoj.logical
+             personoj.equality;
 
 
 constant symbol â„•: Set;
diff --git a/paper/rat.lp b/personoj/examples/rat.lp
similarity index 98%
rename from paper/rat.lp
rename to personoj/examples/rat.lp
index ac9a0b5914c00f692ea9d8f9b37d349758890c60..1a4fb623a02bd7265d0ed5c5ef0faf4d5e73b4b7 100644
--- a/paper/rat.lp
+++ b/personoj/examples/rat.lp
@@ -47,7 +47,7 @@ begin
   assume n;
   refine nat_ind (λ n, eqnat (z + n) n) _ _ n;
   refine λ x: Prf false, x;
-  assume n0 Hn;
+  assume _ Hn;
   apply Hn;
 end;
 
@@ -59,7 +59,7 @@ begin
   assume n;
   refine nat_ind (λ n, eqnat (z * n) z) _ _ n;
   refine λ x: Prf false, x;
-  assume n0 Hn;
+  assume _ Hn;
   refine Hn;
 end;
 
@@ -97,6 +97,6 @@ symbol right_cancel:
      ≔
 begin
   assume x y;
-  simpl;
+  simplify;
   apply times_comm x (fst y);
 end;
diff --git a/paper/stack.lp b/personoj/examples/stack.lp
similarity index 100%
rename from paper/stack.lp
rename to personoj/examples/stack.lp
diff --git a/encodings/bool_plus.lp b/personoj/extra/bool_plus.lp
similarity index 80%
rename from encodings/bool_plus.lp
rename to personoj/extra/bool_plus.lp
index a6cde4e6506ee08d13b51e9c2a78d582b3b44ce5..87ab607cd9f5df0a3d465755904ea7cd2c4b4f81 100644
--- a/encodings/bool_plus.lp
+++ b/personoj/extra/bool_plus.lp
@@ -1,5 +1,5 @@
-require open personoj.encodings.lhol
-             personoj.encodings.logical;
+require open personoj.lhol
+             personoj.logical;
 
 // It may be generalisable to dependent propositions
 opaque
diff --git a/encodings/prenex/README.md b/personoj/extra/prenex/README.md
similarity index 100%
rename from encodings/prenex/README.md
rename to personoj/extra/prenex/README.md
diff --git a/personoj/extra/prenex/kind.lp b/personoj/extra/prenex/kind.lp
new file mode 100644
index 0000000000000000000000000000000000000000..d444e4139332a65a91afc12fec4c04d125687e9f
--- /dev/null
+++ b/personoj/extra/prenex/kind.lp
@@ -0,0 +1,9 @@
+require open personoj.lhol
+             personoj.deptype;
+
+constant symbol Scheme: TYPE;
+injective symbol El: Scheme → TYPE;
+constant symbol lift: Kind → Scheme;
+rule El (lift $X) ↪ Ty $X;
+constant symbol ∀: (Set → Scheme) → Scheme;
+rule El (∀ $e) ↪ Π t: Set, El ($e t);
diff --git a/encodings/prenex/prop.lp b/personoj/extra/prenex/prop.lp
similarity index 79%
rename from encodings/prenex/prop.lp
rename to personoj/extra/prenex/prop.lp
index 71f3d982818e74dd961f6b114fccfa11732e134a..64f3353b4a7d62cf0e74ee502e51d5258f89bf3e 100644
--- a/encodings/prenex/prop.lp
+++ b/personoj/extra/prenex/prop.lp
@@ -1,6 +1,6 @@
 /// Prenex polymorphism in objects of type ‘Prop’
 
-require open personoj.encodings.lhol;
+require open personoj.lhol;
 
 constant symbol ∀: (Set → Prop) → Prop;
 rule Prf (∀ $P) ↪ Π x: Set, Prf ($P x);
diff --git a/encodings/prenex/set.lp b/personoj/extra/prenex/set.lp
similarity index 88%
rename from encodings/prenex/set.lp
rename to personoj/extra/prenex/set.lp
index 77e47501ff553db290c646a82f3ae57930ed7efd..eace248971ecf4cf4c907991b564da617db200f0 100644
--- a/encodings/prenex/set.lp
+++ b/personoj/extra/prenex/set.lp
@@ -1,5 +1,5 @@
 /// Prenex polymorphism in sorts of type ‘Set’
-require personoj.encodings.lhol as lhol;
+require personoj.lhol as lhol;
 
 constant symbol Scheme: TYPE;
 injective symbol El: Scheme → TYPE;
diff --git a/encodings/pvs_cert_minus.lp b/personoj/extra/pvs_cert_minus.lp
similarity index 91%
rename from encodings/pvs_cert_minus.lp
rename to personoj/extra/pvs_cert_minus.lp
index d796df4a32fe90c55edc1a06e6aa4aea1816aeb1..7c9f55555b06dcd60492a76568f48bda274d352e 100644
--- a/encodings/pvs_cert_minus.lp
+++ b/personoj/extra/pvs_cert_minus.lp
@@ -1,5 +1,5 @@
 // PVS-Cert-, or ECC with only one universe
-require open personoj.encodings.lhol;
+require open personoj.lhol;
 
 constant symbol Σ (T : Set): (El T → Set) → Set;
 constant symbol pair {T: Set} {U: El T → Set} (M: El T) (_: El (U M))
diff --git a/encodings/pvs_core.lp b/personoj/extra/pvs_core.lp
similarity index 100%
rename from encodings/pvs_core.lp
rename to personoj/extra/pvs_core.lp
diff --git a/encodings/if.lp b/personoj/if.lp
similarity index 92%
rename from encodings/if.lp
rename to personoj/if.lp
index a6fe959c958738162cd404618ad9216523512c57..2c770928d0ad5df32ef85beb94148239075a1b13 100644
--- a/encodings/if.lp
+++ b/personoj/if.lp
@@ -1,7 +1,7 @@
 // Close to PVS logic system: native equality,
 // true, false, and if
-require open personoj.encodings.lhol
-             personoj.encodings.pvs_cert;
+require open personoj.lhol
+             personoj.pvs_cert;
 
 symbol false ≔ ∀ {prop} (λ x, x);
 symbol true ≔ impd {false} (λ _, false);
diff --git a/lambdapi.pkg b/personoj/lambdapi.pkg
similarity index 100%
rename from lambdapi.pkg
rename to personoj/lambdapi.pkg
diff --git a/encodings/lhol.lp b/personoj/lhol.lp
similarity index 62%
rename from encodings/lhol.lp
rename to personoj/lhol.lp
index fb6484fad8d3d8c9e544df46afbf4e4ecfcf963b..c9af629f6a4b471913b710ae8d38b0dcba7722d5 100644
--- a/encodings/lhol.lp
+++ b/personoj/lhol.lp
@@ -1,21 +1,21 @@
 /// Encoding of λHOL
-symbol Set: TYPE;
-symbol Prop: TYPE;
+constant symbol Set: TYPE;
+constant symbol Prop: TYPE;
 
 injective symbol El: Set → TYPE;
 injective symbol Prf: Prop → TYPE;
 
 constant symbol prop: Set;
-
 rule El prop ↪ Prop;
 
 constant symbol ∀ {x: Set}: (El x → Prop) → Prop;
+rule Prf (∀ {$X} $P) ↪ Π x: El $X, Prf ($P x);
+
 constant symbol impd {x: Prop}: (Prf x → Prop) → Prop;
-constant symbol arrd {x: Set}: (El x → Set) → Set;
+rule Prf (impd {$H} $P) ↪ Π h: Prf $H, Prf ($P h);
 
-rule Prf (∀ {$X} $P) ↪ Π x: El $X, Prf ($P x)
-with Prf (impd {$H} $P) ↪ Π h: Prf $H, Prf ($P h)
-with El (arrd {$X} $T) ↪ Π x: El $X, El ($T x);
+constant symbol arrd (x: Set): (El x → Set) → Set;
+rule El (arrd $X $T) ↪ Π x: El $X, El ($T x);
 
 constant symbol arr: Set → Set → Set;
 rule El (arr $X $Y) ↪ (El $X) → (El $Y);
diff --git a/encodings/logical.lp b/personoj/logical.lp
similarity index 95%
rename from encodings/logical.lp
rename to personoj/logical.lp
index 49fc7375cb4d3d276ddd609b6b1150a15d825a0f..72014bcb8dd8afa38985b771e2e3e26bebac71c8 100644
--- a/encodings/logical.lp
+++ b/personoj/logical.lp
@@ -1,5 +1,5 @@
 // Definition based on implication
-require open personoj.encodings.lhol;
+require open personoj.lhol;
 
 symbol false ≔ ∀ {prop} (λ x, x);
 symbol true ≔ impd {false} (λ _, false);
diff --git a/encodings/pvs_cert.lp b/personoj/pvs_cert.lp
similarity index 91%
rename from encodings/pvs_cert.lp
rename to personoj/pvs_cert.lp
index 32918bf57ed256eb6630fd0fcbac47d994a836bc..601d23a5231b0852e773f1afa7202ed98161c37a 100644
--- a/encodings/pvs_cert.lp
+++ b/personoj/pvs_cert.lp
@@ -1,5 +1,5 @@
 // PVS-Cert
-require open personoj.encodings.lhol;
+require open personoj.lhol;
 
 constant symbol psub {x: Set}: (El x → Prop) → Set;
 protected symbol pair': Π(t: Set) (p: El t → Prop), El t → El (psub p);
diff --git a/encodings/sum.lp b/personoj/sum.lp
similarity index 89%
rename from encodings/sum.lp
rename to personoj/sum.lp
index 82f13ac1878aaa181b02a21a70b0cce4e9cad504..3db4e9bda9fa353e53da7e56b8b61750d0583b72 100644
--- a/encodings/sum.lp
+++ b/personoj/sum.lp
@@ -1,5 +1,5 @@
 // Dependent sum type
-require open personoj.encodings.lhol;
+require open personoj.lhol;
 
 constant symbol t (a: Set): (El a → Set) → Set;
 symbol cons {a: Set} {b: El a → Set} (m: El a): El (b m) → El (t a b);
diff --git a/encodings/tuple.lp b/personoj/tuple.lp
similarity index 88%
rename from encodings/tuple.lp
rename to personoj/tuple.lp
index ac98e504a81cf4c15bf8050448ae2295a3fd52e3..b6b5f00a7ec6c4cff7d4d03995a9290b4afe1f2e 100644
--- a/encodings/tuple.lp
+++ b/personoj/tuple.lp
@@ -1,5 +1,5 @@
 // Non dependent tuples
-require open personoj.encodings.lhol;
+require open personoj.lhol;
 
 constant symbol t: Set → Set → Set;
 symbol cons {a: Set} {b: Set}: El a → El b → El (t a b);
diff --git a/encodings/unif_rules.lp b/personoj/unif_rules.lp
similarity index 54%
rename from encodings/unif_rules.lp
rename to personoj/unif_rules.lp
index 93d2b39f56bf5d7ce62ebd47029bc66c934277e6..2645004516ecf7a838a8652b1a6aca2b42a47aaf 100644
--- a/encodings/unif_rules.lp
+++ b/personoj/unif_rules.lp
@@ -1,3 +1,3 @@
-require open personoj.encodings.lhol;
+require open personoj.lhol;
 
 unif_rule El $t ≡ Prop ↪ [$t ≡ prop];
diff --git a/tests/Makefile b/tests/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..662be101673b8ba37faebd7cd9ff0ad3cd56462e
--- /dev/null
+++ b/tests/Makefile
@@ -0,0 +1,3 @@
+LP_SRC != find . -type f -name "*.lp"
+
+.include "../lambdapi.mk"
diff --git a/tests/coercions.lp b/tests/coercions.lp
new file mode 100644
index 0000000000000000000000000000000000000000..c1494e4b534f9416b06a422d81d8968cb2a01c87
--- /dev/null
+++ b/tests/coercions.lp
@@ -0,0 +1,21 @@
+require open personoj.lhol
+             personoj.pvs_cert
+             personoj.logical
+             personoj.coercions;
+
+constant symbol nat : Set;
+constant symbol z : El nat;
+constant symbol even : El (nat ~> prop);
+constant symbol z_even : Prf (even z);
+
+// Coercion "pred-set"
+compute λ x : El even, x;
+
+// Coercion "set-pred"
+compute psub nat;
+
+// Coercion "psub-fst" (without transitivity)
+compute (λ x: El nat, x) (@pair nat even z z_even);
+
+// Coercion "psub-pair" (without transitivity)
+compute (λ x: El (psub even), x) z;
diff --git a/tests/lambdapi.pkg b/tests/lambdapi.pkg
new file mode 100644
index 0000000000000000000000000000000000000000..f9dcc3c4d5732c21d18fae1a42a53438b6b71ef7
--- /dev/null
+++ b/tests/lambdapi.pkg
@@ -0,0 +1,2 @@
+package_name = personoj_tests
+root_path = personoj.tests
diff --git a/tests/pairs.lp b/tests/pairs.lp
deleted file mode 100644
index 102cfce39ed5b4db0ee8d79bfc2e645c8b27a9b2..0000000000000000000000000000000000000000
--- a/tests/pairs.lp
+++ /dev/null
@@ -1,15 +0,0 @@
-require open personoj.encodings.lhol
-require open personoj.encodings.pvs_cert
-require open personoj.encodings.deptype
-require open personoj.encodings.prenex
-require open personoj.encodings.pairs
-
-symbol nat: Set
-symbol plus: El ((Σ nat (λ_, nat)) ~> nat)
-
-symbol z: El nat
-symbol s: El (nat ~> nat)
-set builtin "0" ≔ z
-set builtin "+1" ≔ s
-
-assert plus (pair_ss 3 4): El nat
diff --git a/tests/tuple.lp b/tests/tuple.lp
deleted file mode 100644
index 87b4280aef5622acea2fb360a7295ad746e0fa06..0000000000000000000000000000000000000000
--- a/tests/tuple.lp
+++ /dev/null
@@ -1,15 +0,0 @@
-require open personoj.encodings.lhol
-require open personoj.encodings.pvs_cert
-require open personoj.encodings.deptype
-require open personoj.encodings.prenex
-require open personoj.encodings.tuple
-
-constant symbol nat: Set
-constant symbol rat: Set
-
-
-set verbose 3
-constant symbol zn: El nat
-constant symbol zq: El rat
-definition tuple_zz ≔ tuple_cons _ zn _ (tuple_cons _ zq _ tuple_nil)
-// assert tuple_car (type_cons nat _) (tuple_cons _ zn _ (tuple_cons _ zq _ tuple_nil)) ≡ zn
diff --git a/tests/vect.lp b/tests/vect.lp
deleted file mode 100644
index cb234bfda28a89a4ac8ae0841a11cc99e0f23b77..0000000000000000000000000000000000000000
--- a/tests/vect.lp
+++ /dev/null
@@ -1,8 +0,0 @@
-require open personoj.encodings.lhol
-require open personoj.encodings.pvs_cert
-require open personoj.encodings.deptype
-require open personoj.encodings.prenex
-
-symbol nat: θ {|set|}
-symbol vect: ϕ (∀K (λ_, scheme_k (nat *> {|set|})))
-assert vect: Set → El nat → Set
diff --git a/tools/mk_top.sh b/tools/mk_top.sh
deleted file mode 100755
index 9a00cdfcb3a3765b054de2520a29e3f79f53c063..0000000000000000000000000000000000000000
--- a/tools/mk_top.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-#!/bin/bash
-
-## [./mk_top.sh d] creates a file [d/top.lp] importing all files in [d/]
-
-out="top.lp"
-
-( cd "$1" || exit
-  rm "${out}"
-  for f in *.lp; do
-      p=$(printf '%s/' "$1" | tr -s '/' '.')
-      printf 'require %s%s\n' "${p}" "${f%.lp}" >> "${out}"
-  done )