diff --git a/encoding/README.adoc b/encoding/README.adoc
index c6b4cbf5f0dc36e4560d110056963d590a490e9a..d54f46bd3c8fc703674b6139171d7bf00baf85b9 100644
--- a/encoding/README.adoc
+++ b/encoding/README.adoc
@@ -1,6 +1,5 @@
 = Encodings =
 Gabriel Hondet <gabriel.hondet@inria.fr>
-v1.0, October 2021
 
 The encoding is a set of lambdapi files in +encoding/+ that define
 axioms allowing to type check PVS terms and propositions.
@@ -15,8 +14,8 @@ tuple ::
   Bruijn telescopes].
 logical ::
   Locical connectives
-eqtup ::
-  Uncurried equality and disequality, latexmath:[$eq (t, u)$]
+eq ::
+  Equality latexmath:[$=\, t\, u$] with elimination principle
 coercions ::
   Define coercions to implement implicit predicate subtyping
 extra ::
diff --git a/encoding/eqtup.lp b/encoding/eqtup.lp
deleted file mode 100644
index 4f043f0e880cb3d9d3919a635e0c9b00131ccc4e..0000000000000000000000000000000000000000
--- a/encoding/eqtup.lp
+++ /dev/null
@@ -1,11 +0,0 @@
-// 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 & &nil))): 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) ($x ^ $y ^ ^nil)
-   ↪ @eq $t ((@fst $t $p $x) ^ (@fst $t $p $y) ^ ^nil);
-symbol neq {t} m ≔ ¬ (@eq t m);
diff --git a/encoding/examples/proof_irr.lp b/encoding/examples/proof_irr.lp
index 00c7ead0a38fb60d759dc4314058cede9e78a216..c5917d7006ff915b1660eed608ae1f51d2b2c457 100644
--- a/encoding/examples/proof_irr.lp
+++ b/encoding/examples/proof_irr.lp
@@ -1,6 +1,7 @@
-require open personoj.lhol personoj.pvs_cert personoj.logical personoj.eqtup; 
+require open personoj.lhol personoj.pvs_cert personoj.logical personoj.eq; 
+
+notation = infix 2;
 
-require open personoj.extra.equality; // Friendlier equality
 constant symbol â„•: Set;
 constant symbol z: El â„•;
 constant symbol s (_: El â„•): El â„•;
@@ -21,7 +22,7 @@ constant symbol scons {bound: El â„•} (head: El (bounded bound))
 symbol l₁: El (slist (s z)) ≔ scons (pair z p1) (snil z);
 symbol l₂: El (slist (s z)) ≔ scons (pair z p2) (snil z);
 
-opaque symbol listeq: Prf (l₁ = l₂) ≔ eq_refl l₁;
+opaque symbol listeq: Prf (l₁ = l₂) ≔ refl l₁;
 // begin
 //   refine eq_refl l₁
 // end
diff --git a/encoding/examples/stack.lp b/encoding/examples/stack.lp
index 6acb169b75b228020660bb7f10ffd5dd32adcfeb..761f30f03d0565873df2915fec039355086bf74f 100644
--- a/encoding/examples/stack.lp
+++ b/encoding/examples/stack.lp
@@ -1,13 +1,13 @@
-require open personoj.lhol personoj.pvs_cert personoj.logical personoj.eqtup;
+require open personoj.lhol personoj.pvs_cert personoj.logical personoj.eq;
 require open personoj.coercions;
 
-// Get currified infix equality
-require open personoj.extra.equality;
+notation = infix 2;
+notation != infix 2;
 
 constant symbol stack {_: Set}: Set;
 constant symbol empty {t: Set}: El (stack {t});
 
-symbol nonempty_stack? {t: Set} (s: El (stack {t})) ≔ s ≠ empty {t};
+symbol nonempty_stack? {t: Set} (s: El (stack {t})) ≔ s != empty {t};
 symbol nonempty_stack {t: Set} ≔ psub (nonempty_stack? {t});
 
 constant symbol push {t: Set}: El t → El (stack {t}) → El (nonempty_stack {t});
diff --git a/encoding/examples/transitivity.lp b/encoding/examples/transitivity.lp
index 46cd683391ce19ce278ac4982b0086afeca2cc74..ab6650b19b1d4e1c27a0dda2d323248efd1772a0 100644
--- a/encoding/examples/transitivity.lp
+++ b/encoding/examples/transitivity.lp
@@ -12,11 +12,9 @@
 //
 // And we coerce an element (in [foox]) from [real*] to [numfield*].
 require open
-  personoj.lhol personoj.pvs_cert personoj.tuple personoj.logical personoj.eqtup;
+  personoj.lhol personoj.pvs_cert personoj.tuple personoj.logical personoj.eq;
 require open personoj.coercions;
 
-require open personoj.extra.equality;
-
 constant symbol numfield: Set;
 constant symbol nz_numfield : El numfield → Prop;
 symbol numfield* ≔ psub {numfield} nz_numfield;
diff --git a/encoding/extra/bool_plus.lp b/encoding/extra/bool_plus.lp
index 1e94967ca6e8c0435e66658a77113b589385b9f6..8435eebb241b10c986ca09fb30192db4c5f5038b 100644
--- a/encoding/extra/bool_plus.lp
+++ b/encoding/extra/bool_plus.lp
@@ -1,4 +1,4 @@
-require open personoj.lhol personoj.tuple personoj.logical personoj.eqtup;
+require open personoj.lhol personoj.tuple personoj.logical personoj.eq;
 
 // It may be generalisable to dependent propositions
 opaque
@@ -19,4 +19,4 @@ admitted;
 
 symbol propositional_extensionality:
   Prf (∀ (λ p: El prop,
-          (∀ (λ q: El prop, (iff p q) ⇒ (λ _, eq (p ^ q ^ ^nil))))));
+          (∀ (λ q: El prop, (iff p q) ⇒ (λ _, = p q)))));
diff --git a/encoding/extra/equality.lp b/encoding/extra/equality.lp
deleted file mode 100644
index c0004f97851869b4f336b69ff15f6a741ce00d2b..0000000000000000000000000000000000000000
--- a/encoding/extra/equality.lp
+++ /dev/null
@@ -1,34 +0,0 @@
-// Usual prenex polymorphic equaltiy, with two arguments
-require open
-  personoj.lhol
-  personoj.pvs_cert
-  personoj.logical;
-
-// We don't use prenex encoding to have implicit arguments.
-symbol = {s: Set}: El s → El s → Prop;
-notation = infix 2;
-builtin "eq" ≔ =;
-
-rule @= (@psub $t $p) $x $y ↪ @= $t (@fst $t $p $x) (@fst $t $p $y);
-
-symbol ≠ {s: Set} (x y: El s) ≔ ¬ (x = y);
-notation ≠ infix 2;
-
-// Leibniz equality
-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 λ _ x p (h: Prf (p x)), h;
-end;
-builtin "refl" ≔ eq_refl;
-
-opaque
-symbol eq_trans {a: Set} (x y z: El a) (_: Prf (x = y)) (_: Prf (y = z))
-      : Prf (x = z) ≔
-begin
-  refine λ _ x y z (hxy: Prf (x = y)) (hyz: Prf (y = z)) p (px: Prf (p x)),
-         hyz p (hxy p px);
-end;