diff --git a/encodings/builtins.lp b/encodings/builtins.lp
index ef313a8479ffa85ceef5e13dfb71544e7f0aa2c2..c7b18680c657bbdb9d9028e8f8bd0c9586f1629b 100644
--- a/encodings/builtins.lp
+++ b/encodings/builtins.lp
@@ -26,3 +26,7 @@ definition ∃ {T: Set} (P: η T → η bool) ≔ ¬ (∀ (λx, ¬ (P x)))
 
 symbol propositional_extensionality:
   ε (∀ {bool} (λp, (∀ {bool} (λq, (iff p q) ⊃ (λ_, eq {bool} p q)))))
+
+definition neq {t} x y ≔ ¬ (eq {t} x y)
+set infix left 2 "/=" ≔ neq
+set infix left 2 "≠" ≔ neq
diff --git a/prelude/logic.lp b/prelude/logic.lp
index 4e6a81d575bc0c5aea669fa41f1de6a898a1f04f..80c2ec4eda38fc7cf4e552c5c3fa5ef793fadd4a 100644
--- a/prelude/logic.lp
+++ b/prelude/logic.lp
@@ -2,6 +2,7 @@ require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 require open personoj.encodings.bool_hol
 require open personoj.encodings.prenex
+require open personoj.encodings.builtins
 //
 // Booleans
 // In [adlib.cert_f.bootstrap]
@@ -14,10 +15,11 @@ require open personoj.encodings.prenex
 // Notequal
 //
 // definition neq {T: Set} (x y: η T) ≔ ¬ (x = y)
-symbol neq: χ (∀S (λt, scheme (t ~> t ~> bool)))
-rule neq _ $x $y ↪ ¬ ($x = $y)
-set infix left 2 "/=" ≔ neq
-set infix left 2 "≠" ≔ neq
+// symbol neq: χ (∀S (λt, scheme (t ~> t ~> bool)))
+// rule neq _ $x $y ↪ ¬ ($x = $y)
+// set infix left 2 "/=" ≔ neq
+// set infix left 2 "≠" ≔ neq
+/// Defined in builtins
 
 //
 // if_def
@@ -26,7 +28,7 @@ set infix left 2 "≠" ≔ neq
 //
 // boolean_props
 // Slightly modified from the prelude
-constant symbol bool_exclusive: ε (neq bool false true)
+constant symbol bool_exclusive: ε (neq {bool} false true)
 constant
 symbol bool_inclusive
      : ε (∀ {bool} (λa, ((eq {bool} a false) ∨ (λ_, eq {bool} a true))))
@@ -40,7 +42,7 @@ qed
 //
 // xor_def
 //
-definition xor (a b: η bool) ≔ neq bool a b
+definition xor (a b: η bool) ≔ neq {bool} a b
 
 // PVS solves that kind of things thanks to the (bddsimp) tactic which uses an
 // external C program
diff --git a/prelude/numbers.lp b/prelude/numbers.lp
index 1978de675e97eb98915936edf596019234b6fe64..c3a159852246285a6d1bc9651f3a4500cf31bd54 100644
--- a/prelude/numbers.lp
+++ b/prelude/numbers.lp
@@ -58,7 +58,7 @@ symbol Num_real: ε (∀ (λx: η {|!Number!|}, real_pred (insertnum x)))
 definition nonzero_real ≔
   psub {real}
        (λx: η real,
-        neq _ x (cast {_} {real} (λx, x) (insertnum 0) _))
+        neq {_} x (cast {_} {real} (λx, x) (insertnum 0) _))
 
 // symbol closed_plus_real: Π(x y: Term real),
 //   let pr ≔ S.restr numfield real_pred in