From fbe0bc4acce09e507a76de730f8bf3987e257742 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <yliu8e5f7@protonmail.com>
Date: Sun, 22 Dec 2024 15:08:01 -0500
Subject: [PATCH] Finish Pair EPar

---
 theories/fp_red.v | 25 +++++++++++++++++++++++--
 1 file changed, 23 insertions(+), 2 deletions(-)

diff --git a/theories/fp_red.v b/theories/fp_red.v
index 4ee8bdb..02c7c0b 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -393,8 +393,29 @@ Proof.
   - move => n a0 a1 ha iha a b ?. subst. specialize iha with (1 := eq_refl).
     split => [p|].
     + move : iha => [/(_ p) [d [ih0 ih1]] _].
-
-
+      exists d. split=>//.
+      apply : rtc_l. apply RPar.ProjPair; eauto using RPar.refl.
+      set q := (X in rtc RPar.R X d).
+      by have -> : q = Proj p a1 by hauto lq:on.
+    + move  :iha => [iha _].
+      move : (iha PL) => [d0 [ih0 ih0']].
+      move : (iha PR) => [d1 [ih1 ih1']] {iha}.
+      exists d0, d1.
+      apply RPars.weakening in ih0, ih1.
+      repeat split => //=.
+      apply : rtc_l. apply RPar.AppPair; eauto using RPar.refl.
+      apply RPars.PairCong; apply RPars.AppCong; eauto using rtc_refl.
+  - move => n a0 a1 b0 b1 ha _ hb _ a b [*]. subst.
+    split.
+    + move => p.
+      exists (if p is PL then a1 else b1).
+      split.
+      * apply rtc_once. apply : RPar.ProjPair'; eauto using RPar.refl.
+      * hauto lq:on rew:off.
+    + exists a1, b1.
+      split. apply rtc_once. apply RPar.AppPair; eauto using RPar.refl.
+      split => //.
+Qed.
 
 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.