From 3a3769facbfd02a9930cffd2f5155afe7c0dc1c4 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Mon, 23 Mar 2020 12:41:48 +0100
Subject: [PATCH] reduction of fst on opair

---
 encodings/cert_f.lp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/encodings/cert_f.lp b/encodings/cert_f.lp
index b612efb..6558d9f 100644
--- a/encodings/cert_f.lp
+++ b/encodings/cert_f.lp
@@ -60,8 +60,6 @@ constant symbol snd {T: Univ Type} {P: Term T ⇒ Univ Prop}
 symbol pair {T: Univ Type} (P: Term T ⇒ Univ Prop) (M: Term T):
   Term (P M) ⇒ Term (Psub P)
 
-rule fst (pair _ &M _) → &M
-
 // opair is a pair forgetting its snd argument
 protected symbol opair (T: Univ Type) (P: Term T ⇒ Univ Prop) (M: Term T):
   Term (Psub P)
@@ -69,6 +67,8 @@ protected symbol opair (T: Univ Type) (P: Term T ⇒ Univ Prop) (M: Term T):
 // Two pairs are convertible if their first element is
 rule pair {&T} &P &M _ → opair &T &P &M
 
+rule fst (opair _ _ &M) → &M
+
 // The subtype relation
 symbol subtype: Term uType ⇒ Term uType ⇒ Term uProp
 set infix left 6 "⊑" ≔ subtype
-- 
GitLab