diff --git a/personoj/builtins.lp b/personoj/builtins.lp
index f25efac143ff1fb8d6e32f7cfeec857ba6696e70..360baa80568baf02304dc137d4951870951b1501 100644
--- a/personoj/builtins.lp
+++ b/personoj/builtins.lp
@@ -1,7 +1,5 @@
-require open personoj.lhol
-             personoj.pvs_cert
-             personoj.logical
-             personoj.equality;
+require open personoj.lhol personoj.tuple personoj.pvs_cert 
+  personoj.logical personoj.eqtup; 
 
 constant symbol {|!Number!|}: Set;
 
@@ -11,11 +9,11 @@ constant symbol succ: El ({|!Number!|} ~> {|!Number!|});
 builtin "0" ≔ zero;
 builtin "+1" ≔ succ;
 
-// In PVS, the axipms 1 ≠ 2, 1≠3, ... are built in
+// In PVS, the axioms 1 ≠ 2, 1≠3, ... are built in
 // Here we use the decidable equality
-rule Prf (succ $n = succ $m) ↪ Prf ($n = $m)
-with Prf (zero = succ _) ↪ Prf false
-with Prf (zero = zero) ↪ Prf true;
+rule Prf (eq (cons (succ $n) (succ $m))) ↪ Prf (eq (cons $n $m))
+with Prf (eq (cons zero (succ _))) ↪ Prf false
+with Prf (eq (cons zero zero)) ↪ Prf true;
 
 // Define strings as list of numbers
 constant symbol {|!String!|}: Set;
@@ -25,4 +23,4 @@ constant symbol str_cons: El {|!Number!|} → El {|!String!|} → El {|!String!|
 symbol ∃ {T: Set} (P: El T → El prop) ≔ ¬ (∀ (λ x, ¬ (P x)));
 
 symbol propositional_extensionality:
-  Prf (∀ {prop} (λ p, (∀ {prop} (λ q, (iff p q) ⊃ (λ _, eq {prop} p q)))));
+  Prf (∀ {prop} (λ p, (∀ {prop} (λ q, (iff p q) ⊃ (λ _, eq {prop} (cons p q))))));
diff --git a/personoj/coercions.lp b/personoj/coercions.lp
index 906e4444b5914883c9a22669194c303f1652d386..d405ee8b31c021cf6f84ff3269f19081575a93c0 100644
--- a/personoj/coercions.lp
+++ b/personoj/coercions.lp
@@ -1,7 +1,4 @@
-require open personoj.lhol
-             personoj.pvs_cert
-             personoj.logical;
-require personoj.tuple as T;
+require open personoj.lhol personoj.pvs_cert personoj.logical personoj.tuple;
 
 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;
@@ -26,9 +23,9 @@ coercion "psub-pair-tr"
 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)
+  λ (a0 b0 a1 b1: Set) (t: El (σ a0 b0)),
+    cons {a1} {b1} $c[car {a0} {b0} t] $d[cdr {a0} {b0} t]:
+  Π (a0 b0 a1 b1: Set) (_: El (σ a0 b0)), El (σ a1 b1)
   on 5
 with c : El a0 → El a1
 with d : El b0 → El b1;
diff --git a/personoj/eqtup.lp b/personoj/eqtup.lp
new file mode 100644
index 0000000000000000000000000000000000000000..f834cf22e9a390c4e87d41d6d58c71641e080ace
--- /dev/null
+++ b/personoj/eqtup.lp
@@ -0,0 +1,11 @@
+// Equality
+// The equality of PVS is an operation from a 2-uple to bool, so we do the same
+// thing here.
+require open personoj.lhol personoj.pvs_cert personoj.tuple personoj.logical;
+
+symbol eq {t: Set} (_: El (σ t t)): Prop;
+// Equality operates on the maximal supertype. It allows to profit
+// from predicate subtyping for free in the propositional equality.
+rule @eq (@psub $t $p) (cons $x $y)
+   ↪ @eq $t (cons (@fst $t $p $x) (@fst $t $p $y));
+symbol neq {t} m ≔ ¬ (@eq t m);
diff --git a/personoj/equality_tup.lp b/personoj/equality_tup.lp
deleted file mode 100644
index 31bedc9217bce02621aa7e5dea187102a99d70b7..0000000000000000000000000000000000000000
--- a/personoj/equality_tup.lp
+++ /dev/null
@@ -1,12 +0,0 @@
-// Equality defined on tuple of arguments
-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.
-symbol eq {t: Set} (_: El (T.t t t)): Prop;
-symbol neq {t} m ≔ ¬ (@eq t m);
-rule @eq (@psub $t $p) (T.cons $x $y)
-   ↪ @eq $t (T.cons (@fst $t $p $x) (@fst $t $p $y));
diff --git a/personoj/examples/proof_irr.lp b/personoj/examples/proof_irr.lp
index 84fb85f03343a768d5765d154656d6d3456bdbbe..00c7ead0a38fb60d759dc4314058cede9e78a216 100644
--- a/personoj/examples/proof_irr.lp
+++ b/personoj/examples/proof_irr.lp
@@ -1,9 +1,6 @@
-require open personoj.lhol
-             personoj.pvs_cert
-             personoj.logical
-             personoj.equality;
-
+require open personoj.lhol personoj.pvs_cert personoj.logical personoj.eqtup; 
 
+require open personoj.extra.equality; // Friendlier equality
 constant symbol â„•: Set;
 constant symbol z: El â„•;
 constant symbol s (_: El â„•): El â„•;
diff --git a/personoj/examples/rat.lp b/personoj/examples/rat.lp
index 1a4fb623a02bd7265d0ed5c5ef0faf4d5e73b4b7..885c5b5eda1d47bf915fe543627dc36ebac71e5c 100644
--- a/personoj/examples/rat.lp
+++ b/personoj/examples/rat.lp
@@ -1,5 +1,5 @@
-require open personoj.encodings.lhol;
-require open personoj.encodings.pvs_cert;
+require open personoj.lhol;
+require open personoj.pvs_cert;
 
 // Prelude with some logics operator
 symbol ⇒ P Q ≔ impd {P} (λ _, Q);
diff --git a/personoj/examples/stack.lp b/personoj/examples/stack.lp
index ddae3b9d363f0df51f26f7c7fb1a1cea0d579c10..2218f4532ac203c633f9915c9261e6e0db69dcca 100644
--- a/personoj/examples/stack.lp
+++ b/personoj/examples/stack.lp
@@ -1,7 +1,10 @@
-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.eqtup;
+
+// Get currified infix equality
+require open personoj.extra.equality;
 
 constant symbol stack: Set;
 constant symbol empty: El stack;
diff --git a/personoj/deptype.lp b/personoj/extra/deptype.lp
similarity index 100%
rename from personoj/deptype.lp
rename to personoj/extra/deptype.lp
diff --git a/personoj/equality.lp b/personoj/extra/equality.lp
similarity index 53%
rename from personoj/equality.lp
rename to personoj/extra/equality.lp
index 8cbcf36159fbaa05f01a27b0c9b2f10930c4324f..c0004f97851869b4f336b69ff15f6a741ce00d2b 100644
--- a/personoj/equality.lp
+++ b/personoj/extra/equality.lp
@@ -5,25 +5,23 @@ require open
   personoj.logical;
 
 // We don't use prenex encoding to have implicit arguments.
-symbol eq {s: Set}: El s → El s → Prop;
-symbol = {s} ≔ @eq s;
+symbol = {s: Set}: El s → El s → Prop;
 notation = infix 2;
-builtin "eq" ≔ eq;
+builtin "eq" ≔ =;
 
-rule @eq (@psub $t $p) $x $y ↪ @eq $t (@fst $t $p $x) (@fst $t $p $y);
+rule @= (@psub $t $p) $x $y ↪ @= $t (@fst $t $p $x) (@fst $t $p $y);
 
-symbol neq {s: Set} (x y: El s) ≔ ¬ (x = y);
-symbol ≠ {s} ≔ @neq s;
+symbol ≠ {s: Set} (x y: El s) ≔ ¬ (x = y);
 notation ≠ infix 2;
 
 // Leibniz equality
-rule Prf (eq $x $y) ↪ Π p: El (_ ~> prop), Prf (p $x) → Prf (p $y);
+rule Prf ($x = $y) ↪ Π p: El (_ ~> prop), Prf (p $x) → Prf (p $y);
 
 // Some theorems for equality
 opaque
 symbol eq_refl {a: Set} (x: El a): Prf (x = x) ≔
 begin
-  refine λ a x p (h: Prf (p x)), h;
+  refine λ _ x p (h: Prf (p x)), h;
 end;
 builtin "refl" ≔ eq_refl;
 
@@ -31,8 +29,6 @@ opaque
 symbol eq_trans {a: Set} (x y z: El a) (_: Prf (x = y)) (_: Prf (y = z))
       : Prf (x = z) ≔
 begin
-  refine λ a x y z (hxy: Prf (x = y)) (hyz: Prf (y = z)) p (px: Prf (p x)),
+  refine λ _ 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/personoj/if.lp b/personoj/extra/if.lp
similarity index 100%
rename from personoj/if.lp
rename to personoj/extra/if.lp
diff --git a/personoj/extra/prenex/kind.lp b/personoj/extra/prenex/kind.lp
index d444e4139332a65a91afc12fec4c04d125687e9f..d3488372463b5cc69b5c3f0204d8aa106b931405 100644
--- a/personoj/extra/prenex/kind.lp
+++ b/personoj/extra/prenex/kind.lp
@@ -1,5 +1,5 @@
 require open personoj.lhol
-             personoj.deptype;
+             personoj.extra.deptype;
 
 constant symbol Scheme: TYPE;
 injective symbol El: Scheme → TYPE;
diff --git a/personoj/sum.lp b/personoj/sum.lp
index 3db4e9bda9fa353e53da7e56b8b61750d0583b72..96a37a5ec1d9f51e50d8fb8cbf2bd1e36e394719 100644
--- a/personoj/sum.lp
+++ b/personoj/sum.lp
@@ -1,9 +1,9 @@
 // Dependent sum type
 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);
-symbol car {a: Set} {b: El a → Set}: El (t a b) → El a;
-symbol cdr {a: Set} {b: El a → Set} (m: El (t a b)): El (b (car m));
-rule car (cons $m _) ↪ $m;
-rule cdr (cons _ $n) ↪ $n;
+constant symbol Σ (a: Set): (El a → Set) → Set;
+symbol consd {a: Set} {b: El a → Set} (m: El a): El (b m) → El (Σ a b);
+symbol card {a: Set} {b: El a → Set}: El (Σ a b) → El a;
+symbol cdrd {a: Set} {b: El a → Set} (m: El (Σ a b)): El (b (card m));
+rule card (consd $m _) ↪ $m;
+rule cdrd (consd _ $n) ↪ $n;
diff --git a/personoj/tuple.lp b/personoj/tuple.lp
index b6b5f00a7ec6c4cff7d4d03995a9290b4afe1f2e..36083080deca774dfd7ac2f21845411b8ec6de60 100644
--- a/personoj/tuple.lp
+++ b/personoj/tuple.lp
@@ -1,9 +1,9 @@
 // Non dependent tuples
 require open personoj.lhol;
 
-constant symbol t: Set → Set → Set;
-symbol cons {a: Set} {b: Set}: El a → El b → El (t a b);
-symbol car {a: Set} {b: Set}: El (t a b) → El a;
-symbol cdr {a: Set} {b: Set}: El (t a b) → El b;
+constant symbol σ: Set → Set → Set;
+symbol cons {a: Set} {b: Set}: El a → El b → El (σ a b);
+symbol car {a: Set} {b: Set}: El (σ a b) → El a;
+symbol cdr {a: Set} {b: Set}: El (σ a b) → El b;
 rule car (cons $x _) ↪ $x;
 rule cdr (cons _ $y) ↪ $y;