diff --git a/encodings/builtins.lp b/encodings/builtins.lp
new file mode 100644
index 0000000000000000000000000000000000000000..2d2c2992d741b4d56a449ebfbf03976006e153ef
--- /dev/null
+++ b/encodings/builtins.lp
@@ -0,0 +1,17 @@
+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+require open personoj.encodings.bool_hol
+
+constant symbol {|!Number!|}: θ {|set|}
+
+constant symbol zero: η {|!Number!|}
+constant symbol succ: η ({|!Number!|} ~> {|!Number!|})
+
+set builtin "0" ≔ zero
+set builtin "+1" ≔ succ
+
+// In PVS, the axipms 1 ≠ 2, 1≠3, ... are built in
+// Here we use the decidable equality
+rule ε (succ $n = succ $m) ↪ ε ($n = $m)
+with ε (zero = succ _) ↪ ε false
+with ε (zero = zero) ↪ ε true
diff --git a/prelude/logic.lp b/prelude/logic.lp
index 101208f76ada5039e23493e680247c58c8fd2aeb..12bd0ffc08ae7eba241ce1e8d7e9e6a2fa1efef9 100644
--- a/prelude/logic.lp
+++ b/prelude/logic.lp
@@ -49,9 +49,8 @@ theorem xor_def
 proof
 admit
 
-
 //
-// Quantifier props[t: TYPE]
+// Quantifier props[t: TYPE], built in
 //
 set declared "∃"
 definition ∃ {T: Set} (P: η T → η bool) ≔ ¬ (∀ (λx, ¬ (P x)))