From b56541e33c8567eee750f73c8727b90c67e1f9d8 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Sun, 2 Feb 2020 13:13:42 +0100
Subject: [PATCH] oblivious pair

---
 encodings/cert_f.lp | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/encodings/cert_f.lp b/encodings/cert_f.lp
index bde178a..ef6370d 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
-- 
GitLab