diff --git a/encodings/cert_f.lp b/encodings/cert_f.lp
index bde178ad280c849a32f509e1daf83c324e2e9d12..ef6370d515759b70822c6ce29b68ed9b27adb718 100644
--- a/encodings/cert_f.lp
+++ b/encodings/cert_f.lp
@@ -60,3 +60,10 @@ symbol pair {T: Univ Type} (U: Term T ⇒ Univ Prop) (M: Term T):
 
 rule fst &U (pair &U &M _) → &M
 rule snd &U (pair &U _ &P) → &P
+
+// opair is a pair forgetting its snd argument
+protected symbol opair (T: Univ Type) (U: Term T ⇒ Univ Prop) (M: Term T):
+  Term (psub T U)
+
+// Two pairs are convertible if their first element is
+rule @pair &T &U &M _ → opair &T &U &M