diff --git a/encoding/lhol.lp b/encoding/lhol.lp
index d834dced6918df1d6095448901ba9f41529b3c83..0b9353d87aeb9d03a5833486fe38dddc528c5e31 100644
--- a/encoding/lhol.lp
+++ b/encoding/lhol.lp
@@ -2,6 +2,7 @@
 constant symbol Set: TYPE;
 constant symbol Prop: TYPE;
 
+// WARNING: El and Prf are not injective.
 injective symbol El: Set → TYPE;
 injective symbol Prf: Prop → TYPE;
 
@@ -16,6 +17,8 @@ rule Prf ($P ⇒ $Q) ↪ Π h: Prf $P, Prf ($Q h);
 
 constant symbol arrd (x: Set): (El x → Set) → Set;
 rule El (arrd $X $T) ↪ Π x: El $X, El ($T x);
+// To have injectivity wrt. El, the above rule may be replaced by
+// rule El (arrd $X (\x, $T[x])) ↪ Π y: El $X, El ($T[y]);
 
 constant symbol arr: Set → Set → Set;
 rule El (arr $X $Y) ↪ (El $X) → (El $Y);
diff --git a/encoding/pvs_cert.lp b/encoding/pvs_cert.lp
index 601d23a5231b0852e773f1afa7202ed98161c37a..d6fef9e6588e932b98bb8a24ea67100e77fbce0d 100644
--- a/encoding/pvs_cert.lp
+++ b/encoding/pvs_cert.lp
@@ -2,13 +2,13 @@
 require open personoj.lhol;
 
 constant symbol psub {x: Set}: (El x → Prop) → Set;
-protected symbol pair': Π(t: Set) (p: El t → Prop), El t → El (psub p);
-symbol fst: Π{t: Set} {p: El t → Prop}, El (psub p) → El t;
+protected constant symbol pair': Π(a: Set) (p: El a → Prop), El a → El (@psub a p);
+symbol fst: Π{a: Set} {p: El a → Prop}, El (@psub a p) → El a;
 
-symbol snd {t: Set} {p: El t → Prop} (m: El (psub p)): Prf (p (fst m));
+symbol snd {a: Set} {p: El a → Prop} (m: El (@psub a p)): Prf (p (@fst a p m));
 
 // Proof irrelevance
-symbol pair {t: Set} {p: El t → Prop} (m: El t) (_: Prf (p m))
-     ≔ pair' t p m;
+symbol pair {a: Set} {p: El a → Prop} (m: El a) (_: Prf (p m))
+     ≔ pair' a p m;
 
-rule fst (pair' _ _ $M) ↪ $M;
+rule @fst _ _ (pair' _ _ $M) ↪ $M;