From 47473fd3cdc8c0a6619da3a144089e81e6b42eab Mon Sep 17 00:00:00 2001
From: Yiyun Liu <liuyiyun@seas.upenn.edu>
Date: Fri, 31 Jan 2025 16:30:06 -0500
Subject: [PATCH 1/2] Minor

---
 theories/fp_red.v | 229 ++++++++++++++++++++++++++++++----------------
 1 file changed, 152 insertions(+), 77 deletions(-)

diff --git a/theories/fp_red.v b/theories/fp_red.v
index a53a692..4cc344f 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -20,7 +20,7 @@ Ltac2 spec_refl () :=
 
 Ltac spec_refl := ltac2:(spec_refl ()).
 
-Module ERed.
+Module EPar.
   Inductive R {n} : PTm n -> PTm n ->  Prop :=
   (****************** Eta ***********************)
   | AppEta a0 a1 :
@@ -97,7 +97,7 @@ Module ERed.
     all : hauto lq:on ctrs:R use:morphing_up.
   Qed.
 
-End ERed.
+End EPar.
 
 Inductive SNe {n} : PTm n -> Prop :=
 | N_Var i :
@@ -333,10 +333,10 @@ Proof.
   hauto lq:on rew:off inv:TRedSN db:sn.
 Qed.
 
-Lemma ered_sn_preservation n :
-  (forall (a : PTm n) (s : SNe a), forall b, ERed.R a b -> SNe b) /\
-  (forall (a : PTm n) (s : SN a), forall b, ERed.R a b -> SN b) /\
-  (forall (a b : PTm n) (_ : TRedSN a b), forall c, ERed.R a c -> exists d, TRedSN' c d /\ ERed.R b d).
+Lemma epar_sn_preservation n :
+  (forall (a : PTm n) (s : SNe a), forall b, EPar.R a b -> SNe b) /\
+  (forall (a : PTm n) (s : SN a), forall b, EPar.R a b -> SN b) /\
+  (forall (a b : PTm n) (_ : TRedSN a b), forall c, EPar.R a c -> exists d, TRedSN' c d /\ EPar.R b d).
 Proof.
   move : n. apply sn_mutual => n.
   - sauto lq:on.
@@ -344,14 +344,14 @@ Proof.
   - sauto lq:on.
   - move => a b ha iha hb ihb b0.
     inversion 1; subst.
-    + have /iha : (ERed.R (PProj PL a0) (PProj PL b0)) by sauto lq:on.
+    + have /iha : (EPar.R (PProj PL a0) (PProj PL b0)) by sauto lq:on.
       sfirstorder use:SN_Proj.
     + sauto lq:on.
   - move => a ha iha b.
     inversion 1; subst.
-    + have : ERed.R (PApp (ren_PTm shift a0) (VarPTm var_zero))  (PApp (ren_PTm shift b) (VarPTm var_zero)).
-      apply ERed.AppCong; eauto using ERed.refl.
-      sfirstorder use:ERed.renaming.
+    + have : EPar.R (PApp (ren_PTm shift a0) (VarPTm var_zero))  (PApp (ren_PTm shift b) (VarPTm var_zero)).
+      apply EPar.AppCong; eauto using EPar.refl.
+      sfirstorder use:EPar.renaming.
       move /iha.
       move /SN_AppInv => [+ _].
       hauto l:on use:sn_antirenaming.
@@ -368,21 +368,21 @@ Proof.
       exists (subst_PTm (scons b1 VarPTm) a2).
       split.
       sauto lq:on.
-      hauto lq:on use:ERed.morphing, ERed.refl inv:option.
+      hauto lq:on use:EPar.morphing, EPar.refl inv:option.
   - sauto.
   - move => a b hb ihb c.
-    elim /ERed.inv => //= _.
+    elim /EPar.inv => //= _.
     move => p a0 a1 ha [*]. subst.
-    elim  /ERed.inv :  ha => //= _.
+    elim  /EPar.inv :  ha => //= _.
     + move => a0 a2 ha' [*]. subst.
       exists (PProj PL a1).
       split. sauto.
       sauto lq:on.
     + sauto lq:on rew:off.
   - move => a b ha iha c.
-    elim /ERed.inv => //=_.
+    elim /EPar.inv => //=_.
     move => p a0 a1 + [*]. subst.
-    elim /ERed.inv => //=_.
+    elim /EPar.inv => //=_.
     + move => a0  a2 h1 [*]. subst.
       exists (PProj PR a1).
       split. sauto.
@@ -658,7 +658,7 @@ Lemma tstar_proj n (a : PTm n) :
     exists a0 b0, a = PPair a0 b0 /\ forall p, tstar (PProj p a) = (if p is PL then (tstar a0) else (tstar b0)).
 Proof. sauto lq:on. Qed.
 
-Module ERed'.
+Module EPar'.
   Inductive R {n} : PTm n -> PTm n ->  Prop :=
   (****************** Eta ***********************)
   | AppEta a :
@@ -708,39 +708,39 @@ Module ERed'.
     (forall i, R ((funcomp (ren_PTm ξ) ρ0) i) ((funcomp (ren_PTm ξ) ρ1) i)).
   Proof. eauto using renaming. Qed.
 
-End ERed'.
+End EPar'.
 
-Module EReds.
+Module EPars.
 
   #[local]Ltac solve_s_rec :=
   move => *; eapply rtc_l; eauto;
-         hauto lq:on ctrs:ERed'.R.
+         hauto lq:on ctrs:EPar'.R.
 
   #[local]Ltac solve_s :=
     repeat (induction 1; last by solve_s_rec); apply rtc_refl.
 
   Lemma AbsCong n (a b : PTm (S n)) :
-    rtc ERed'.R a b ->
-    rtc ERed'.R (PAbs a) (PAbs b).
+    rtc EPar'.R a b ->
+    rtc EPar'.R (PAbs a) (PAbs b).
   Proof. solve_s. Qed.
 
   Lemma AppCong n (a0 a1 b0 b1 : PTm n) :
-    rtc ERed'.R a0 a1 ->
-    rtc ERed'.R b0 b1 ->
-    rtc ERed'.R (PApp a0 b0) (PApp a1 b1).
+    rtc EPar'.R a0 a1 ->
+    rtc EPar'.R b0 b1 ->
+    rtc EPar'.R (PApp a0 b0) (PApp a1 b1).
   Proof. solve_s. Qed.
 
   Lemma PairCong n (a0 a1 b0 b1 : PTm n) :
-    rtc ERed'.R a0 a1 ->
-    rtc ERed'.R b0 b1 ->
-    rtc ERed'.R (PPair a0 b0) (PPair a1 b1).
+    rtc EPar'.R a0 a1 ->
+    rtc EPar'.R b0 b1 ->
+    rtc EPar'.R (PPair a0 b0) (PPair a1 b1).
   Proof. solve_s. Qed.
 
   Lemma ProjCong n p (a0 a1  : PTm n) :
-    rtc ERed'.R a0 a1 ->
-    rtc ERed'.R (PProj p a0) (PProj p a1).
+    rtc EPar'.R a0 a1 ->
+    rtc EPar'.R (PProj p a0) (PProj p a1).
   Proof. solve_s. Qed.
-End EReds.
+End EPars.
 
 Module RReds.
 
@@ -788,7 +788,7 @@ Proof.
   move : m ξ. elim : n / a => //=; solve [hauto b:on].
 Qed.
 
-Lemma ne_ered n (a b : PTm n) (h : ERed'.R a b ) :
+Lemma ne_epar n (a b : PTm n) (h : EPar'.R a b ) :
   (ne a -> ne b) /\ (nf a -> nf b).
 Proof.
   elim : n a b /h=>//=; hauto qb:on use:ne_nf_ren, ne_nf.
@@ -801,7 +801,7 @@ Definition ishf {n} (a : PTm n) :=
   | _ => false
   end.
 
-Module NeERed.
+Module NeEPar.
   Inductive R_nonelim {n} : PTm n -> PTm n ->  Prop :=
   (****************** Eta ***********************)
   | AppEta a0 a1 :
@@ -847,16 +847,16 @@ Module NeERed.
   | NVarTm i :
     R_elim (VarPTm i) (VarPTm i).
 
-  Scheme ered_elim_ind := Induction for R_elim Sort Prop
-      with ered_nonelim_ind := Induction for R_nonelim Sort Prop.
+  Scheme epar_elim_ind := Induction for R_elim Sort Prop
+      with epar_nonelim_ind := Induction for R_nonelim Sort Prop.
 
-  Combined Scheme ered_mutual from ered_elim_ind, ered_nonelim_ind.
+  Combined Scheme epar_mutual from epar_elim_ind, epar_nonelim_ind.
 
   Lemma R_elim_nf n :
     (forall (a b : PTm n), R_elim a b -> nf b -> nf a) /\
       (forall (a b : PTm n), R_nonelim a b -> nf b -> nf a).
   Proof.
-    move : n. apply ered_mutual => n //=.
+    move : n. apply epar_mutual => n //=.
     - move => a0 a1 b0 b1 h ih h' ih' /andP [h0 h1].
       have hb0 : nf b0 by eauto.
       suff : ne a0 by qauto b:on.
@@ -895,13 +895,13 @@ Module NeERed.
     move => h. elim : n a b /h=>//=; hauto lq:on ctrs:R_nonelim.
   Qed.
 
-End NeERed.
+End NeEPar.
 
 Module Type NoForbid.
   Parameter P : forall n, PTm n -> Prop.
   Arguments P {n}.
 
-  Axiom P_ERed : forall n (a b : PTm n), ERed.R a b -> P a -> P b.
+  Axiom P_EPar : forall n (a b : PTm n), EPar.R a b -> P a -> P b.
   Axiom P_RRed : forall n (a b : PTm n), RRed.R a b -> P a -> P b.
   Axiom P_AppPair : forall n (a b c : PTm n), ~ P (PApp (PPair a b) c).
   Axiom P_ProjAbs : forall n p (a : PTm (S n)), ~ P (PProj p (PAbs a)).
@@ -916,7 +916,7 @@ End NoForbid.
 
 Module Type NoForbid_FactSig (M : NoForbid).
 
-  Axiom P_EReds : forall n (a b : PTm n), rtc ERed.R a b -> M.P a -> M.P b.
+  Axiom P_EPars : forall n (a b : PTm n), rtc EPar.R a b -> M.P a -> M.P b.
 
   Axiom P_RReds : forall n (a b : PTm n), rtc RRed.R a b -> M.P a -> M.P b.
 
@@ -925,9 +925,9 @@ End NoForbid_FactSig.
 Module NoForbid_Fact (M : NoForbid) : NoForbid_FactSig M.
   Import M.
 
-  Lemma P_EReds : forall n (a b : PTm n), rtc ERed.R a b -> P a -> P b.
+  Lemma P_EPars : forall n (a b : PTm n), rtc EPar.R a b -> P a -> P b.
   Proof.
-    induction 1; eauto using P_ERed, rtc_l, rtc_refl.
+    induction 1; eauto using P_EPar, rtc_l, rtc_refl.
   Qed.
 
   Lemma P_RReds : forall n (a b : PTm n), rtc RRed.R a b -> P a -> P b.
@@ -936,12 +936,12 @@ Module NoForbid_Fact (M : NoForbid) : NoForbid_FactSig M.
   Qed.
 End NoForbid_Fact.
 
-Module SN_NoForbid : NoForbid.
+Module SN_NoForbid <: NoForbid.
   Definition P := @SN.
   Arguments P {n}.
 
-  Lemma P_ERed : forall n (a b : PTm n), ERed.R a b -> P a -> P b.
-  Proof. sfirstorder use:ered_sn_preservation. Qed.
+  Lemma P_EPar : forall n (a b : PTm n), EPar.R a b -> P a -> P b.
+  Proof. sfirstorder use:epar_sn_preservation. Qed.
 
   Lemma P_RRed : forall n (a b : PTm n), RRed.R a b -> P a -> P b.
   Proof. hauto q:on use:red_sn_preservation, RPar.FromRRed. Qed.
@@ -974,14 +974,16 @@ Module SN_NoForbid : NoForbid.
 
 End SN_NoForbid.
 
+Module NoForbid_FactSN := NoForbid_Fact SN_NoForbid.
+
 Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
   Import M MFacts.
-  #[local]Hint Resolve P_ERed P_RRed P_AppPair P_ProjAbs : forbid.
+  #[local]Hint Resolve P_EPar P_RRed P_AppPair P_ProjAbs : forbid.
 
   Lemma η_split n (a0 a1 : PTm n) :
-    ERed.R a0 a1 ->
+    EPar.R a0 a1 ->
     P a0 ->
-    exists b, rtc RRed.R a0 b /\ NeERed.R_nonelim b a1.
+    exists b, rtc RRed.R a0 b /\ NeEPar.R_nonelim b a1.
   Proof.
     move => h. elim : n a0 a1 /h .
     - move => n a0 a1 ha ih /[dup] hP.
@@ -992,8 +994,8 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
       exists (PAbs (PApp (ren_PTm shift b) (VarPTm var_zero))).
       split. apply RReds.AbsCong. apply RReds.AppCong; auto using rtc_refl.
       by eauto using RReds.renaming.
-      apply NeERed.AppEta=>//.
-      sfirstorder use:NeERed.R_nonelim_nothf.
+      apply NeEPar.AppEta=>//.
+      sfirstorder use:NeEPar.R_nonelim_nothf.
 
       case : b ih0 ih1 => //=.
       + move => p ih0 ih1 _.
@@ -1024,7 +1026,7 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
       case /orP : (orNb (ishf b)).
       exists (PPair (PProj PL b) (PProj PR b)).
       split. sfirstorder use:RReds.PairCong,RReds.ProjCong.
-      hauto lq:on ctrs:NeERed.R_nonelim use:NeERed.R_nonelim_nothf.
+      hauto lq:on ctrs:NeEPar.R_nonelim use:NeEPar.R_nonelim_nothf.
 
       case : b ih0 ih1 => //=.
       (* violates SN *)
@@ -1042,14 +1044,14 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
         apply RRed.ProjPair.
         apply : rtc_r; eauto using RReds.ProjCong.
         apply RRed.ProjPair.
-    - hauto lq:on ctrs:NeERed.R_nonelim use:RReds.AbsCong, P_AbsInv.
+    - hauto lq:on ctrs:NeEPar.R_nonelim use:RReds.AbsCong, P_AbsInv.
     - move => n a0 a1 b0 b1 ha iha hb ihb.
       move => /[dup] hP /P_AppInv [hP0 hP1].
       have {iha} [a2 [iha0 iha1]]  := iha hP0.
       have {ihb} [b2 [ihb0 ihb1]]  := ihb hP1.
       case /orP : (orNb (ishf a2)) => [h|].
       + exists (PApp a2 b2). split; first by eauto using RReds.AppCong.
-        hauto lq:on ctrs:NeERed.R_nonelim use:NeERed.R_nonelim_nothf.
+        hauto lq:on ctrs:NeEPar.R_nonelim use:NeEPar.R_nonelim_nothf.
       + case : a2 iha0 iha1 => //=.
         * move => p h0 h1 _.
           inversion h1; subst.
@@ -1058,21 +1060,21 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
              apply : rtc_r.
              apply RReds.AppCong; eauto.
              apply RRed.AppAbs'. by asimpl.
-             hauto lq:on ctrs:NeERed.R_nonelim.
-          ** hauto lq:on ctrs:NeERed.R_nonelim,NeERed.R_elim use:RReds.AppCong.
+             hauto lq:on ctrs:NeEPar.R_nonelim.
+          ** hauto lq:on ctrs:NeEPar.R_nonelim,NeEPar.R_elim use:RReds.AppCong.
         (* Impossible *)
         * move => u0 u1 h. exfalso.
           have : rtc RRed.R (PApp a0 b0) (PApp (PPair u0 u1) b0)
             by hauto lq:on ctrs:rtc use:RReds.AppCong.
           move : P_RReds hP; repeat move/[apply].
           sfirstorder use:P_AppPair.
-    - hauto lq:on ctrs:NeERed.R_nonelim use:RReds.PairCong, P_PairInv.
+    - hauto lq:on ctrs:NeEPar.R_nonelim use:RReds.PairCong, P_PairInv.
     - move => n p a0 a1 ha ih /[dup] hP /P_ProjInv.
       move : ih => /[apply]. move => [a2 [iha0 iha1]].
       case /orP : (orNb (ishf a2)) => [h|].
       exists (PProj p a2).
       split.  eauto using RReds.ProjCong.
-      qauto l:on ctrs:NeERed.R_nonelim, NeERed.R_elim use:NeERed.R_nonelim_nothf.
+      qauto l:on ctrs:NeEPar.R_nonelim, NeEPar.R_elim use:NeEPar.R_nonelim_nothf.
 
       case : a2 iha0 iha1 => //=.
       + move => u iha0. exfalso.
@@ -1086,28 +1088,101 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
           apply : rtc_r.
           apply RReds.ProjCong; eauto.
           clear. hauto l:on inv:PTag.
-          hauto lq:on ctrs:NeERed.R_nonelim.
-        * hauto lq:on ctrs:NeERed.R_nonelim,NeERed.R_elim use:RReds.ProjCong.
-    - hauto lq:on ctrs:rtc, NeERed.R_nonelim.
+          hauto lq:on ctrs:NeEPar.R_nonelim.
+        * hauto lq:on ctrs:NeEPar.R_nonelim,NeEPar.R_elim use:RReds.ProjCong.
+    - hauto lq:on ctrs:rtc, NeEPar.R_nonelim.
   Qed.
 
 End UniqueNF.
 
-Lemma η_nf_to_ne n (a0 a1 : PTm n) :
-  ERed'.R a0 a1 -> nf a0 -> ~~ ne a0 -> ne a1 ->
-  (a0 = PAbs (PApp (ren_PTm shift a1) (VarPTm var_zero))) \/
-    (a0 = PPair (PProj PL a1) (PProj PR a1)).
-Proof.
-  move => h.
-  elim : n a0 a1 /h => n /=.
-  - sfirstorder use:ne_ered.
-  - hauto l:on use:ne_ered.
-  - scongruence use:ne_ered.
-  - hauto qb:on use:ne_ered, ne_nf.
-  - move => a b0 b1 h0 ih0 /andP [h1 h2] h3 /andP [h4 h5].
-    have {h3} : ~~ ne a by sfirstorder b:on.
-    by move /negP.
-  - hauto lqb:on.
-  - sfirstorder b:on.
-  - scongruence b:on.
-Qed.
+Module SN_UniqueNF := UniqueNF SN_NoForbid NoForbid_FactSN.
+
+
+Module ERed.
+  Inductive R {n} : PTm n -> PTm n ->  Prop :=
+
+  (****************** Eta ***********************)
+  | AppEta a :
+    R (PAbs (PApp (ren_PTm shift a) (VarPTm var_zero))) a
+  | PairEta a :
+    R (PPair (PProj PL a) (PProj PR a)) a
+
+  (*************** Congruence ********************)
+  | AbsCong a0 a1 :
+    R a0 a1 ->
+    R (PAbs a0) (PAbs a1)
+  | AppCong0 a0 a1 b :
+    R a0 a1 ->
+    R (PApp a0 b) (PApp a1 b)
+  | AppCong1 a b0 b1 :
+    R b0 b1 ->
+    R (PApp a b0) (PApp a b1)
+  | PairCong0 a0 a1 b :
+    R a0 a1 ->
+    R (PPair a0 b) (PPair a1 b)
+  | PairCong1 a b0 b1 :
+    R b0 b1 ->
+    R (PPair a b0) (PPair a b1)
+  | ProjCong p a0 a1 :
+    R a0 a1 ->
+    R (PProj p a0) (PProj p a1).
+
+  Lemma ToEPar n (a b : PTm n) :
+    ERed.R a b -> EPar.R a b.
+  Proof.
+    induction 1; hauto lq:on use:EPar.refl ctrs:EPar.R.
+  Qed.
+
+End ERed.
+
+#[export]Hint Constructors ERed.R RRed.R EPar.R : red.
+
+
+Module RERed.
+  Inductive R {n} : PTm n -> PTm n ->  Prop :=
+  (****************** Beta ***********************)
+  | AppAbs a b :
+    R (PApp (PAbs a) b)  (subst_PTm (scons b VarPTm) a)
+
+  | ProjPair p a b :
+    R (PProj p (PPair a b)) (if p is PL then a else b)
+
+  (****************** Eta ***********************)
+  | AppEta a :
+    R (PAbs (PApp (ren_PTm shift a) (VarPTm var_zero))) a
+  | PairEta a :
+    R (PPair (PProj PL a) (PProj PR a)) a
+
+  (*************** Congruence ********************)
+  | AbsCong a0 a1 :
+    R a0 a1 ->
+    R (PAbs a0) (PAbs a1)
+  | AppCong0 a0 a1 b :
+    R a0 a1 ->
+    R (PApp a0 b) (PApp a1 b)
+  | AppCong1 a b0 b1 :
+    R b0 b1 ->
+    R (PApp a b0) (PApp a b1)
+  | PairCong0 a0 a1 b :
+    R a0 a1 ->
+    R (PPair a0 b) (PPair a1 b)
+  | PairCong1 a b0 b1 :
+    R b0 b1 ->
+    R (PPair a b0) (PPair a b1)
+  | ProjCong p a0 a1 :
+    R a0 a1 ->
+    R (PProj p a0) (PProj p a1).
+
+  Lemma ToBetaEta n (a b : PTm n) :
+    R a b ->
+    ERed.R a b \/ RRed.R a b.
+  Proof. induction 1; hauto lq:on db:red. Qed.
+
+  Lemma ToBetaEtaPar n (a b : PTm n) :
+    R a b ->
+    EPar.R a b \/ RRed.R a b.
+  Proof.
+    hauto q:on use:ERed.ToEPar, ToBetaEta.
+  Qed.
+
+End RERed.

From 571779a4dd323ff254197ae2e456b004b3721ec0 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <yliu8e5f7@protonmail.com>
Date: Fri, 31 Jan 2025 17:32:35 -0500
Subject: [PATCH 2/2] Fix name change errors for EPar

---
 theories/fp_red.v | 38 +++++++++++++++++++-------------------
 1 file changed, 19 insertions(+), 19 deletions(-)

diff --git a/theories/fp_red.v b/theories/fp_red.v
index a7624e2..2317fe2 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -888,7 +888,7 @@ Module NeEPar.
   Lemma ToEPar : forall n, (forall (a b : PTm n), R_elim a b -> EPar.R a b) /\
                  (forall (a b : PTm n), R_nonelim a b -> EPar.R a b).
   Proof.
-    apply ered_mutual; qauto l:on ctrs:EPar.R.
+    apply epar_mutual; qauto l:on ctrs:EPar.R.
   Qed.
 
 End NeEPar.
@@ -1092,9 +1092,9 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
 
   Lemma eta_postponement n a b c :
     @P n a ->
-    ERed.R a b ->
+    EPar.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 /\ EPar.R d c.
   Proof.
     move => + h.
     move : c.
@@ -1104,17 +1104,17 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
       move => [d [h0 h1]].
       exists  (PAbs (PApp (ren_PTm shift d) (VarPTm var_zero))).
       split. hauto lq:on rew:off ctrs:rtc use:RReds.AbsCong, RReds.AppCong, RReds.renaming.
-      hauto lq:on ctrs:ERed.R.
+      hauto lq:on ctrs:EPar.R.
     - move => n a0 a1 ha iha c /P_PairInv [/P_ProjInv + _].
       move /iha => /[apply].
       move => [d [h0 h1]].
       exists (PPair (PProj PL d) (PProj PR d)).
-      hauto lq:on ctrs:ERed.R use:RReds.PairCong, RReds.ProjCong.
+      hauto lq:on ctrs:EPar.R use:RReds.PairCong, RReds.ProjCong.
     - move => n a0 a1 ha iha c  /P_AbsInv /[swap].
       elim /RRed.inv => //=_.
       move => a2 a3 + [? ?]. subst.
       move : iha; repeat move/[apply].
-      hauto lq:on use:RReds.AbsCong ctrs:ERed.R.
+      hauto lq:on use:RReds.AbsCong ctrs:EPar.R.
     - move => n a0 a1 b0 b1 ha iha hb ihb c hP.
       elim /RRed.inv => //= _.
       + move => a2 b2 [*]. subst.
@@ -1125,7 +1125,7 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
         inversion h1; subst.
         * inversion H0; subst.
           exists (subst_PTm (scons b0 VarPTm) a3).
-          split; last by scongruence use:ERed.morphing.
+          split; last by scongruence use:EPar.morphing.
           apply : relations.rtc_transitive.
           apply RReds.AppCong.
           eassumption.
@@ -1145,22 +1145,22 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
           split.
           apply : rtc_r; last by apply RRed.AppAbs.
           hauto lq:on ctrs:rtc use:RReds.AppCong.
-          hauto l:on inv:option use:ERed.morphing,NeERed.ToERed.
+          hauto l:on inv:option use:EPar.morphing,NeEPar.ToEPar.
       + move => a2 a3 b2 ha2 [*]. subst.
         move : iha (ha2) {ihb} => /[apply].
         have : P a0 by sfirstorder use:P_AppInv.
         move /[swap]/[apply].
         move => [d [h0 h1]].
         exists (PApp d b0).
-        hauto lq:on ctrs:ERed.R, rtc use:RReds.AppCong.
+        hauto lq:on ctrs:EPar.R, rtc use:RReds.AppCong.
       + move => a2 b2 b3 hb2 [*]. subst.
         move {iha}.
         have : P b0 by sfirstorder use:P_AppInv.
         move : ihb hb2; repeat move /[apply].
-        hauto lq:on rew:off ctrs:ERed.R, rtc use:RReds.AppCong.
+        hauto lq:on rew:off ctrs:EPar.R, rtc use:RReds.AppCong.
     - move => n a0 a1 b0 b1 ha iha hb ihb c /P_PairInv [hP hP'].
       elim /RRed.inv => //=_;
-        hauto lq:on rew:off ctrs:ERed.R, rtc use:RReds.PairCong.
+        hauto lq:on rew:off ctrs:EPar.R, rtc use:RReds.PairCong.
     - move => n p a0 a1 ha iha c /[dup] hP /P_ProjInv hP'.
       elim / RRed.inv => //= _.
       + move => p0 a2 b0 [*]. subst.
@@ -1170,7 +1170,7 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
         * qauto l:on ctrs:rtc use:RReds.ProjCong, P_ProjAbs, P_RReds.
         * inversion H0; subst.
           exists (if p is PL then a1 else b1).
-          split; last by scongruence use:NeERed.ToERed.
+          split; last by scongruence use:NeEPar.ToEPar.
           apply : relations.rtc_transitive.
           apply RReds.ProjCong; eauto.
           apply : rtc_l.
@@ -1183,22 +1183,22 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
           apply RRed.ProjPair.
           apply rtc_once. apply RRed.ProjPair.
         * exists (if p is PL then a3 else b1).
-          split; last by hauto lq:on use:NeERed.ToERed.
+          split; last by hauto lq:on use:NeEPar.ToEPar.
           apply : relations.rtc_transitive.
           eauto using RReds.ProjCong.
           apply rtc_once.
           apply RRed.ProjPair.
       + move => p0 a2 a3 h0 [*]. subst.
         move : iha hP' h0;repeat move/[apply].
-        hauto lq:on ctrs:rtc, ERed.R use:RReds.ProjCong.
+        hauto lq:on ctrs:rtc, EPar.R use:RReds.ProjCong.
     - hauto lq:on inv:RRed.R.
   Qed.
 
   Lemma η_postponement_star n a b c :
     @P n a ->
-    ERed.R a b ->
+    EPar.R a b ->
     rtc RRed.R b c ->
-    exists d, rtc RRed.R a d /\ ERed.R d c.
+    exists d, rtc RRed.R a d /\ EPar.R d c.
   Proof.
     move => + + h. move : a.
     elim : b c / h.
@@ -1213,12 +1213,12 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
 
   Lemma η_postponement_star' n a b c :
     @P n a ->
-    ERed.R a b ->
+    EPar.R a b ->
     rtc RRed.R b c ->
-    exists d, rtc RRed.R a d /\ NeERed.R_nonelim d c.
+    exists d, rtc RRed.R a d /\ NeEPar.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.
+    have : exists d, rtc RRed.R a d /\ EPar.R d c by eauto using η_postponement_star.
     move => [d [h3 /η_split]].
     move /(_ ltac:(eauto using P_RReds)).
     sfirstorder use:@relations.rtc_transitive.