From df62e3691ce6f2bf6f974724b84525fc40ed5965 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <yliu8e5f7@protonmail.com>
Date: Sat, 25 Jan 2025 16:53:48 -0700
Subject: [PATCH] Need to parallelize eta

---
 theories/fp_red.v | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/theories/fp_red.v b/theories/fp_red.v
index 74af932..e105262 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -109,6 +109,12 @@ Module RRed.
   Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop.
 End RRed.
 
+Module ERedM.
+  Inductive R {n} (a : PTm n) : PTm n ->  Prop :=
+  | refl : R a a
+  | step b : ERed.R a b -> R a b.
+End ERedM.
+
 Inductive Wt {n} (Γ : fin n -> Ty) : PTm n -> Ty -> Prop :=
 | T_Var i :
   Wt Γ (VarPTm i) (Γ i)
@@ -229,7 +235,7 @@ Lemma eta_postponement n Γ a b c A :
   @Wt n Γ a A ->
   ERed.R a b ->
   RRed.R b c ->
-  exists d, rtc RRed.R a d /\ ERed.R d c.
+  exists d, rtc RRed.R a d /\  ERed.R d c.
 Proof.
   move => + h.
   move : Γ c A.
@@ -284,6 +290,10 @@ Proof.
   - move => n a b0 b1 hb ihb Γ c A hu hu'.
     elim /RRed.inv : hu' => //=_.
     + move => A0 a0 b2 [*]. subst.
+      move {ihb}.
+      eexists.
+      split. apply rtc_once.
+      apply RRed.AppAbs.
       admit.
     + sauto lq:on.
     + move => a0 b2 b3 hb0 [*]. subst.