diff --git a/encodings/pair_equality.lp b/encodings/pair_equality.lp
index 976d5b312b43a527d12d3074ce9c51599f209ca2..3da34c121a28d5817611c2d8e0b720ed1162af9a 100644
--- a/encodings/pair_equality.lp
+++ b/encodings/pair_equality.lp
@@ -1,6 +1,7 @@
 require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
 require open personoj.encodings.pairs
 require open personoj.encodings.logical
 
-symbol peq {t: Set} (_: El (σ t t)): Bool
-definition pneq  {t: Set} (m: El (σ t t)) ≔ ¬ (@peq t m)
+symbol peq {t: Set} (_: El (σ (μ t) (μ t))): Bool
+definition pneq  {t} m ≔ ¬ (@peq t m)