From 5a7f46a8a19e48b5ac3b322c38c49418348eefa2 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <yliu8e5f7@protonmail.com>
Date: Thu, 30 Jan 2025 23:29:25 -0500
Subject: [PATCH] Finish the enhanced eta postponement

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

diff --git a/theories/fp_red.v b/theories/fp_red.v
index bc8ec58..20929e1 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -1192,6 +1192,36 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
     - hauto lq:on inv:RRed.R.
   Qed.
 
+  Lemma η_postponement_star n a b c :
+    @P n a ->
+    ERed.R a b ->
+    rtc RRed.R b c ->
+    exists d, rtc RRed.R a d /\ ERed.R d c.
+  Proof.
+    move => + + h. move : a.
+    elim : b c / h.
+    - sfirstorder.
+    - move => a0 a1 a2 ha ha' iha u hu hu'.
+      move : eta_postponement (hu) ha hu'; repeat move/[apply].
+      move => [d [h0 h1]].
+      have : P d by sfirstorder use:P_RReds.
+      move : iha h1; repeat move/[apply].
+      sfirstorder use:@relations.rtc_transitive.
+  Qed.
+
+  Lemma η_postponement_star' n a b c :
+    @P n a ->
+    ERed.R a b ->
+    rtc RRed.R b c ->
+    exists d, rtc RRed.R a d /\ NeERed.R_nonelim d c.
+  Proof.
+    move => h0 h1 h2.
+    have : exists d, rtc RRed.R a d /\ ERed.R d c by eauto using η_postponement_star.
+    move => [d [h3 /η_split]].
+    move /(_ ltac:(eauto using P_RReds)).
+    sfirstorder use:@relations.rtc_transitive.
+  Qed.
+
 End UniqueNF.
 
 Lemma η_nf_to_ne n (a0 a1 : PTm n) :