diff --git a/explicit/booleans.lp b/explicit/booleans.lp
deleted file mode 100644
index 2d023db167dc8e9499e103268de5e675be08505e..0000000000000000000000000000000000000000
--- a/explicit/booleans.lp
+++ /dev/null
@@ -1,8 +0,0 @@
-require open pvs_cert explicit.pts_bindings
-
-definition bool ≔ Prop
-
-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
deleted file mode 100644
index ad267c7f1efeab3c8fff38708a91861419e851d4..0000000000000000000000000000000000000000
--- a/explicit/equalities.lp
+++ /dev/null
@@ -1,3 +0,0 @@
-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
deleted file mode 100644
index dd2e3bc9af391702afda76c7b6eb5354ab43b642..0000000000000000000000000000000000000000
--- a/explicit/nat.lp
+++ /dev/null
@@ -1,8 +0,0 @@
-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
deleted file mode 100644
index 9ac3516064e3e708ea1cdd679f0ad1d68d0818a1..0000000000000000000000000000000000000000
--- a/explicit/nat_ops.lp
+++ /dev/null
@@ -1,12 +0,0 @@
-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
deleted file mode 100644
index 24df8b5b75b504d7e134c925bb24eb624776c101..0000000000000000000000000000000000000000
--- a/explicit/notequal.lp
+++ /dev/null
@@ -1,4 +0,0 @@
-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
deleted file mode 100644
index 9d4351a1114a7989d3d84ce21157aee1df44f592..0000000000000000000000000000000000000000
--- a/explicit/pts_bindings.lp
+++ /dev/null
@@ -1,7 +0,0 @@
-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
deleted file mode 100644
index 6088674832c96ad11dff1f49724ecef1224654a8..0000000000000000000000000000000000000000
--- a/explicit/rat.lp
+++ /dev/null
@@ -1,17 +0,0 @@
-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))