diff --git a/encodings/pvs_cert.lp b/encodings/pvs_cert.lp
index 02b798e0354731bf8b6faa91bdf6b4b7cc35cdf4..bedc42095184dc9b6d54f391bb051e561118ca40 100644
--- a/encodings/pvs_cert.lp
+++ b/encodings/pvs_cert.lp
@@ -2,18 +2,13 @@
 require open personoj.encodings.lhol
 
 constant symbol psub {x: Set}: (El x → Bool) → Set
-symbol pair: Π{t: Set} {p: El t → Bool} (m: El t), Prf (p m) → El (psub p)
+protected symbol pair': Π(t: Set) (p: El t → Bool), El t → El (psub p)
 symbol fst: Π{t: Set} {p: El t → Bool}, El (psub p) → El t
 
 symbol snd {t: Set}{p: El t → Bool} (m: El (psub p)): Prf (p (fst m))
 
 // Proof irrelevance
-protected symbol ppair: Π{t: Set} {p: El t → Bool}, El t → El (psub p)
+definition pair {t: Set} {p: El t → Bool} (m: El t) (_: Prf (p m))
+         ≔ pair' t p m
 
-// Reduction
-rule pair $X _ ↪ ppair $X
-rule fst (ppair $M) ↪ $M
-
-// Sub-typing relation
-symbol subtype : Set → Set → Bool
-set infix left 6 "⊑" ≔ subtype
+rule fst (pair' _ _ $M) ↪ $M