From ecee278d04c5520e0ef02ab303c8014f8c66e3b1 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <liuyiyun@seas.upenn.edu>
Date: Sun, 22 Dec 2024 12:12:25 -0500
Subject: [PATCH] Write down the statement of pair_epar

---
 theories/fp_red.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/theories/fp_red.v b/theories/fp_red.v
index 32a17b4..898b7e8 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -364,6 +364,16 @@ Proof.
       apply rtc_once. apply : RPar.ProjAbs; eauto using RPar.refl.
 Qed.
 
+Lemma Pair_EPar n (a b c : Tm n) :
+  EPar.R (Pair a b) c ->
+  (forall p, exists d, rtc RPar.R (Proj p c) d /\ EPar.R (if p is PL then a else b) d) /\
+    (exists d0 d1, rtc RPar.R (App (ren_Tm shift c) (VarTm var_zero))
+                (Pair (App (ren_Tm shift d0) (VarTm var_zero))(App (ren_Tm shift d1) (VarTm var_zero))) /\
+    EPar.R a d0 /\ EPar.R b d1).
+Proof.
+Admitted.
+
+
 Lemma commutativity n (a b0 b1 : Tm n) :
   EPar.R a b0 -> RPar.R a b1 -> exists c, rtc RPar.R b0 c /\ EPar.R b1 c.
 Proof.