diff --git a/README.md b/README.md
new file mode 100644
index 0000000000000000000000000000000000000000..df8b4a6cf928905dcb4756af856fe4a69b8e9902
--- /dev/null
+++ b/README.md
@@ -0,0 +1,9 @@
+# PVS proofs
+
+Encodings of PVS and manual translations of PVS prelude. Use with `lambdapi`.
+
+## TODO
+- simplify PVS cert encoding:
+  - no `Rule` since PTS is functional,
+  - no `Type Prop Type` rule since it does not concern products but only
+    predicate subtyping.
diff --git a/explicit/booleans.lp b/explicit/booleans.lp
index bab760c4a22d7771b80c18382f59b8855c0764cb..2d023db167dc8e9499e103268de5e675be08505e 100644
--- a/explicit/booleans.lp
+++ b/explicit/booleans.lp
@@ -1,14 +1,8 @@
-require open pvs_cert
+require open pvs_cert explicit.pts_bindings
 
 definition bool ≔ Prop
 
-symbol r : Rule Type Prop Prop
-symbol a : Axiom Prop Type
-
-definition uProp ≔ univ Prop Type I
-
-compute Term Type uProp
-type uProp
-
 definition false ≔ prod Type Prop Prop uProp r (λ x : Term Type uProp, x)
 definition true ≔ Term Prop false ⇒ Term Prop false
+
+definition bnot (P : Term Type uProp) ≔ Term Prop P ⇒ Term Prop false
diff --git a/explicit/equalities.lp b/explicit/equalities.lp
new file mode 100644
index 0000000000000000000000000000000000000000..ad267c7f1efeab3c8fff38708a91861419e851d4
--- /dev/null
+++ b/explicit/equalities.lp
@@ -0,0 +1,3 @@
+require open pvs_cert explicit.pts_bindings explicit.booleans
+
+symbol eq (T : Term Kind uType) : Term Type T ⇒ Term Type T ⇒ Term Type uProp
diff --git a/explicit/nat.lp b/explicit/nat.lp
new file mode 100644
index 0000000000000000000000000000000000000000..dd2e3bc9af391702afda76c7b6eb5354ab43b642
--- /dev/null
+++ b/explicit/nat.lp
@@ -0,0 +1,8 @@
+require open pvs_cert explicit.pts_bindings
+
+constant symbol int : Term Kind uType
+symbol zero : Term Type int
+injective symbol succ : Term Type int ⇒ Term Type int
+
+set builtin "0" ≔ zero
+set builtin "+1" ≔ succ
diff --git a/explicit/nat_ops.lp b/explicit/nat_ops.lp
new file mode 100644
index 0000000000000000000000000000000000000000..9ac3516064e3e708ea1cdd679f0ad1d68d0818a1
--- /dev/null
+++ b/explicit/nat_ops.lp
@@ -0,0 +1,12 @@
+require open pvs_cert explicit.pts_bindings explicit.nat explicit.notequal
+
+symbol times : Term Type int ⇒ Term Type int ⇒ Term Type int
+rule times &n 1 → &n
+
+set infix left 6 "*" ≔ times
+
+type λ x : Term Type int, neq int x 0
+
+symbol prod_not_zero (x y : Term Type int) :
+  Term Prop (neq int x 0) ⇒ Term Prop (neq int y 0) ⇒
+  Term Prop (neq int (x * y) 0)
diff --git a/explicit/notequal.lp b/explicit/notequal.lp
new file mode 100644
index 0000000000000000000000000000000000000000..24df8b5b75b504d7e134c925bb24eb624776c101
--- /dev/null
+++ b/explicit/notequal.lp
@@ -0,0 +1,4 @@
+require open pvs_cert explicit.pts_bindings explicit.booleans
+require open explicit.equalities
+
+definition neq (T : Term Kind uType) (x y : Term Type T) ≔ bnot (eq T x y)
diff --git a/explicit/pts_bindings.lp b/explicit/pts_bindings.lp
new file mode 100644
index 0000000000000000000000000000000000000000..9d4351a1114a7989d3d84ce21157aee1df44f592
--- /dev/null
+++ b/explicit/pts_bindings.lp
@@ -0,0 +1,7 @@
+require open pvs_cert
+
+symbol r : Rule Type Prop Prop
+symbol a : Axiom Prop Type
+
+definition uProp ≔ univ Prop Type I
+definition uType ≔ univ Type Kind I
diff --git a/explicit/rat.lp b/explicit/rat.lp
new file mode 100644
index 0000000000000000000000000000000000000000..6088674832c96ad11dff1f49724ecef1224654a8
--- /dev/null
+++ b/explicit/rat.lp
@@ -0,0 +1,17 @@
+require open pvs_cert explicit.pts_bindings explicit.booleans explicit.equalities explicit.notequal
+
+constant symbol Nat : Term Kind uType
+symbol Nz : Term Type Nat
+symbol Nsuc : Term Type Nat ⇒ Term Type Nat
+
+constant symbol rat : Term Kind uType
+constant symbol Qz : Term Type rat
+
+definition notzero ≔ psub uProp (λ x : Term Type uProp, x)
+
+symbol frac : Term Type Nat ⇒ ∀ m : Term Type notzero, Term Type rat
+
+symbol times : Term Type rat ⇒ Term Type rat ⇒ Term Type rat
+
+rule times (frac &A (pair &B &P)) (frac &C (pair &D &Q)) →
+  frac (Nat_times &A &C) (pair (Nat_times &B &D) (Nat_prod_not_zero &B &D &P &Q))
diff --git a/pvs_cert.lp b/pvs_cert.lp
index 0030dbfbde01af101a4e7885f8f4a43f1cb694ac..768c1568f541935236c453a00a192fc1dd6d7747 100644
--- a/pvs_cert.lp
+++ b/pvs_cert.lp
@@ -20,7 +20,7 @@ rule Rule Prop Prop Prop → True
  and Rule Type Prop Prop → True
  and Rule Type Prop Type → True  // Dependent pairs
 
-injective symbol Term (s : Sort): Univ s ⇒ TYPE
+symbol Term (s : Sort): Univ s ⇒ TYPE
 
 constant symbol univ (s1 s2 : Sort): (Axiom s1 s2) ⇒ Univ s2