From df9c91dad54432e64a7b9e8c5f980d60db59c1e1 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <yliu8e5f7@protonmail.com>
Date: Sun, 22 Dec 2024 16:06:36 -0500
Subject: [PATCH] Start EPar_diamond

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

diff --git a/theories/fp_red.v b/theories/fp_red.v
index d74e169..f1735fa 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -501,6 +501,21 @@ Lemma commutativity n (a b0 b1 : Tm n) :
     hauto q:on ctrs:rtc.
 Qed.
 
+Lemma EPar_diamond n (c a1 b1 : Tm n) :
+  EPar.R c a1 ->
+  EPar.R c b1 ->
+  exists d2, EPar.R a1 d2 /\ EPar.R b1 d2.
+Proof.
+  move => h. move : b1. elim : n c a1 / h.
+  - move => n c a1 ha iha b1 /iha [d2 [hd0 hd1]].
+    exists(Abs (App (ren_Tm shift d2) (VarTm var_zero))).
+    hauto lq:on ctrs:EPar.R use:EPar.renaming.
+  - hauto lq:on rew:off ctrs:EPar.R.
+  - hauto lq:on use:EPar.refl.
+  - move => n a0 a1 ha iha a2 ha2.
+
+
+
 
 Lemma EPar_Par n (a b : Tm n) : EPar.R a b -> Par.R a b.
 Proof. induction 1; hauto lq:on ctrs:Par.R. Qed.