diff --git a/personoj/builtins.lp b/personoj/builtins.lp
deleted file mode 100644
index ddda077c38fb0b88ca98259a6abc86265f4ff676..0000000000000000000000000000000000000000
--- a/personoj/builtins.lp
+++ /dev/null
@@ -1,27 +0,0 @@
-require open personoj.lhol personoj.tuple personoj.pvs_cert 
-  personoj.logical personoj.eqtup; 
-
-constant symbol {|!Number!|}: Set;
-
-constant symbol zero: El {|!Number!|};
-constant symbol succ: El ({|!Number!|} ~> {|!Number!|});
-
-builtin "0" ≔ zero;
-builtin "+1" ≔ succ;
-
-// In PVS, the axioms 1 ≠ 2, 1≠3, ... are built in
-// Here we use the decidable equality
-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;
-constant symbol str_empty: El {|!String!|};
-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 (∀ (λ p: El prop,
-          (∀ (λ q: El prop, (iff p q) ⇒ (λ _, eq {prop} (cons p q))))));
diff --git a/personoj/extra/bool_plus.lp b/personoj/extra/bool_plus.lp
index 1eb48fb52c1c3c31ea5cae70cc594ef4cde168b8..a466a0f5b40bb9574b5af4c8ef8a854234346af0 100644
--- a/personoj/extra/bool_plus.lp
+++ b/personoj/extra/bool_plus.lp
@@ -1,5 +1,4 @@
-require open personoj.lhol
-             personoj.logical;
+require open personoj.lhol personoj.tuple personoj.logical personoj.eqtup;
 
 // It may be generalisable to dependent propositions
 opaque
@@ -17,3 +16,7 @@ opaque
 symbol and_elim_1 a b (_: Prf (a ∧ (λ _, b))): Prf a ≔
 begin
 admitted;
+
+symbol propositional_extensionality:
+  Prf (∀ (λ p: El prop,
+          (∀ (λ q: El prop, (iff p q) ⇒ (λ _, eq (cons p q))))));
diff --git a/personoj/logical.lp b/personoj/logical.lp
index cf7f528b644eb87e1b125fb6f53ccb29d9ac4ebc..c3db436deb183092082dc99eb2266abf0badefd7 100644
--- a/personoj/logical.lp
+++ b/personoj/logical.lp
@@ -12,3 +12,6 @@ symbol if {s: Set} (p: Prop): (Prf p → El s) → (Prf (¬ p) → El s) → El
 rule if {prop} $p $then $else ↪ ($p ⇒ $then) ⇒ (λ _, (¬ $p) ⇒ $else);
 
 symbol iff P Q ≔ (P ⇒ (λ _, Q)) ∧ (λ _, Q ⇒ (λ _, P));
+
+symbol ∃ {T: Set} (P: El T → El prop) ≔ ¬ (∀ (λ x, ¬ (P x)));
+
diff --git a/personoj/nat.lp b/personoj/nat.lp
new file mode 100644
index 0000000000000000000000000000000000000000..7af7eb040d15e1ed74abfbfbfd6e1b7fd9448bf3
--- /dev/null
+++ b/personoj/nat.lp
@@ -0,0 +1,11 @@
+require open personoj.lhol personoj.logical;
+constant symbol Nat: TYPE;
+
+constant symbol zero: Nat;       builtin "0" ≔ zero;
+constant symbol succ: Nat → Nat; builtin "+1" ≔ succ;
+
+symbol eqnat: Nat → Nat → Prop;
+rule eqnat (succ $n) (succ $m) ↪ eqnat $n $m
+with eqnat zero (succ _) ↪ false
+with eqnat (succ _) zero ↪ false
+with eqnat zero zero ↪ true;
diff --git a/personoj/unif_rules.lp b/personoj/unif_rules.lp
deleted file mode 100644
index 2645004516ecf7a838a8652b1a6aca2b42a47aaf..0000000000000000000000000000000000000000
--- a/personoj/unif_rules.lp
+++ /dev/null
@@ -1,3 +0,0 @@
-require open personoj.lhol;
-
-unif_rule El $t ≡ Prop ↪ [$t ≡ prop];