diff --git a/encodings/dtuple.lp b/encodings/dtuple.lp
new file mode 100644
index 0000000000000000000000000000000000000000..1e4e9c12b07e7d565b9007cbb0de649f07301d17
--- /dev/null
+++ b/encodings/dtuple.lp
@@ -0,0 +1,9 @@
+// Dependent tuples
+require open personoj.encodings.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
diff --git a/encodings/equality_tup.lp b/encodings/equality_tup.lp
new file mode 100644
index 0000000000000000000000000000000000000000..dbfae48986e17310c9ea6f6227b442315be73316
--- /dev/null
+++ b/encodings/equality_tup.lp
@@ -0,0 +1,7 @@
+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+require personoj.encodings.tuple as T
+require open personoj.encodings.logical
+
+symbol peq {t: Set} (_: El (T.t (μ t) (μ t))): Bool
+definition pneq {t} m ≔ ¬ (@peq t m)
diff --git a/encodings/logical.lp b/encodings/logical.lp
index 161a017a81886b0bec1cfa664b49bda8609d4ad4..3bfae83ac9b4691774f397c68fce81ee13e6ad93 100644
--- a/encodings/logical.lp
+++ b/encodings/logical.lp
@@ -1,6 +1,5 @@
 // Definition based on implication
 require open personoj.encodings.lhol
-require open personoj.encodings.pairs
 
 definition false ≔ ∀ {bool} (λx, x)
 definition true ≔ impd {false} (λ_, false)
@@ -23,7 +22,7 @@ set builtin "imp" ≔ imp
 set builtin "and" ≔ and
 set builtin "or"  ≔ or
 
-symbol if {s: Set} p: (Prf p → El s) → (Prf (¬ p) → El s) → El s
+symbol if {s: Set} (p: Bool): (Prf p → El s) → (Prf (¬ p) → El s) → El s
 rule if {bool} $p $then $else ↪ ($p ⊃ $then) ⊃ (λ_, (¬ $p) ⊃ $else)
 
 definition iff P Q ≔ (P ⊃ (λ_, Q)) ∧ ((λ_, Q ⊃ (λ_, P)))
diff --git a/encodings/pair_equality.lp b/encodings/pair_equality.lp
deleted file mode 100644
index 3da34c121a28d5817611c2d8e0b720ed1162af9a..0000000000000000000000000000000000000000
--- a/encodings/pair_equality.lp
+++ /dev/null
@@ -1,7 +0,0 @@
-require open personoj.encodings.lhol
-require open personoj.encodings.pvs_cert
-require open personoj.encodings.pairs
-require open personoj.encodings.logical
-
-symbol peq {t: Set} (_: El (σ (μ t) (μ t))): Bool
-definition pneq  {t} m ≔ ¬ (@peq t m)
diff --git a/encodings/pairs.lp b/encodings/pairs.lp
deleted file mode 100644
index 4b852f2e49188bed4f438f3d7faca14033f24c41..0000000000000000000000000000000000000000
--- a/encodings/pairs.lp
+++ /dev/null
@@ -1,23 +0,0 @@
-require open personoj.encodings.lhol
-
-set declared "Σ" // Dependent pairs
-set declared "σ" // Non dependent pairs
-set declared "σcons"
-set declared "σfst"
-set declared "σsnd"
-
-constant symbol σ: Set → Set → Set
-symbol σcons {t} {u}: El t → El u → El (σ t u)
-symbol σfst {t} {u}: El (σ t u) → El t
-rule σfst (σcons $x _) ↪ $x
-symbol σsnd {t} {u}: El (σ t u) → El u
-rule σsnd (σcons _ $y) ↪ $y
-
-constant symbol Σ (t: Set): (El t → Set) → Set
-symbol pair_ss {t: Set} {u: El t → Set} (m: El t): El (u m) → El (Σ t u)
-
-symbol fst_ss {t: Set} {u: El t → Set}: El (Σ t u) → El t
-symbol snd_ss {t: Set} {u: El t → Set} (m: El (Σ t u)): El (u (fst_ss m))
-
-rule fst_ss (pair_ss $m _) ↪ $m
-rule snd_ss (pair_ss _ $n) ↪ $n
diff --git a/encodings/tuple.lp b/encodings/tuple.lp
index e24bd8d8c2df16e33a76ae7e3a135a6ff043cd93..708980026cb17adafd487d0c73be7ba0491510e6 100644
--- a/encodings/tuple.lp
+++ b/encodings/tuple.lp
@@ -1,34 +1,9 @@
-/// WIP
-require open personoj.encodings.lhol
-require open personoj.encodings.pvs_cert
-
 // Non dependent tuples
-constant symbol tuple_t: Set → Set → Set
-constant symbol tuple {t} {u}: El t → El u → El (tuple_t t u)
-symbol p1 {t} {u}: El (tuple_t t u) → El t
-symbol p2 {t} {u}: El (tuple_t t u) → El u
-rule p1 (tuple $m _) ↪ $m
-rule p2 (tuple _ $n) ↪ $n
-
-constant symbol set_t: Set
-constant symbol set_nil: El set_t
-constant symbol set_cons: Set → El set_t → El set_t
-// TODO rewrite rules that transform (t, u, v) ~> w in t ~> u ~> v ~> w
-
-constant symbol TypeList: TYPE
-constant symbol type_nil: TypeList
-constant symbol type_cons: Set → TypeList → TypeList
-symbol type_cdr: TypeList → TypeList
-rule type_cdr (type_cons _ $tl) ↪ $tl
-symbol type_car: TypeList → Set
-rule type_car (type_cons $hd _) ↪ $hd
-
-constant symbol Tuple: TypeList → TYPE
-constant symbol tuple_nil: Tuple type_nil
-constant symbol tuple_cons (t: Set) (_: El t) (tl: TypeList) (_: Tuple tl):
-  Tuple (type_cons t tl)
+require open personoj.encodings.lhol
 
-symbol tuple_car (tl: TypeList): Tuple tl → El (type_car tl)
-rule tuple_car (type_cons $t _) (tuple_cons $t $x _) ↪ $x
-symbol tuple_cdr (tl: TypeList): Tuple tl → Tuple (type_cdr tl)
-rule tuple_cdr _ (tuple_cons _ _ _ $tup) ↪ $tup
+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
+rule car (cons $x _) ↪ $x
+rule cdr (cons _ $y) ↪ $y