diff --git a/theories/Autosubst2/syntax.v b/theories/Autosubst2/syntax.v
index 78c4fec..b5cbc66 100644
--- a/theories/Autosubst2/syntax.v
+++ b/theories/Autosubst2/syntax.v
@@ -804,9 +804,9 @@ Arguments PApp {n_PTm}.
 
 Arguments PAbs {n_PTm}.
 
-#[global] Hint Opaque subst_PTm: rewrite.
+#[global]Hint Opaque subst_PTm: rewrite.
 
-#[global] Hint Opaque ren_PTm: rewrite.
+#[global]Hint Opaque ren_PTm: rewrite.
 
 End Extra.
 
diff --git a/theories/fp_red.v b/theories/fp_red.v
index 670ce12..85a9512 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -229,7 +229,7 @@ Ltac2 rec solve_anti_ren () :=
   let x := Fresh.in_goal (Option.get (Ident.of_string "x")) in
   intro $x;
   lazy_match! Constr.type (Control.hyp x) with
-  | fin _ -> _ _ => (ltac1:(case;qauto depth:2 db:sn))
+  | fin ?x -> _ ?y => (ltac1:(case;qauto depth:2 db:sn))
   | _ => solve_anti_ren ()
   end.
 
@@ -431,32 +431,34 @@ Module RRed.
     all : qauto ctrs:R.
   Qed.
 
-  Ltac2 rec solve_anti_ren () :=
-    let x := Fresh.in_goal (Option.get (Ident.of_string "x")) in
-    intro $x;
-    lazy_match! Constr.type (Control.hyp x) with
-    | fin _ -> _ _ => (ltac1:(case;hauto q:on depth:2 ctrs:RRed.R))
-    | _ => solve_anti_ren ()
-    end.
-
-  Ltac solve_anti_ren := ltac2:(Control.enter solve_anti_ren).
 
   Lemma antirenaming n m (a : PTm n) (b : PTm m) (ξ : fin n -> fin m) :
     R (ren_PTm ξ a) b -> exists b0, R a b0 /\ ren_PTm ξ b0 = b.
   Proof.
     move E : (ren_PTm ξ a) => u h.
-    move : n ξ a E. elim : m u b/h; try solve_anti_ren.
+    move : n ξ a E. elim : m u b/h.
     - move => n a b m ξ []//=. move => []//= t t0 [*]. subst.
       eexists. split. apply AppAbs. by asimpl.
     - move => n p a b m ξ []//=.
       move => p0 []//=. hauto q:on ctrs:R.
+    - move => n a0 a1 ha iha m ξ []//=.
+      move => p [*]. subst.
+      spec_refl.
+      move : iha => [t [h0 h1]]. subst.
+      eexists. split. eauto using AbsCong.
+      by asimpl.
+    - move => n a0 a1 b ha iha m ξ []//=.
+      hauto lq:on ctrs:R.
+    - move => n a b0 b1 h ih m ξ []//=.
+      hauto lq:on ctrs:R.
+    - move => n a0 a1 b ha iha m ξ []//=.
+      hauto lq:on ctrs:R.
+    - move => n a b0 b1 h ih m ξ []//=.
+      hauto lq:on ctrs:R.
+    - move => n p a0 a1 ha iha m ξ []//=.
+      hauto lq:on ctrs:R.
   Qed.
 
-  Lemma nf_imp n (a b : PTm n) :
-    nf a ->
-    R a b -> False.
-  Proof. move/[swap]. induction 1; hauto qb:on inv:PTm. Qed.
-
 End RRed.
 
 Module RPar.
@@ -572,48 +574,6 @@ Module RPar.
     induction 1; qauto l:on use:RPar.refl ctrs:RPar.R.
   Qed.
 
-  Function tstar {n} (a : PTm n) :=
-    match a with
-    | VarPTm i => a
-    | PAbs a => PAbs (tstar a)
-    | PApp (PAbs a) b => subst_PTm (scons (tstar b) VarPTm) (tstar a)
-    | PApp a b => PApp (tstar a) (tstar b)
-    | PPair a b => PPair (tstar a) (tstar b)
-    | PProj p (PPair a b) => if p is PL then (tstar a) else (tstar b)
-    | PProj p a => PProj p (tstar a)
-    end.
-
-  Lemma triangle n (a b : PTm n) :
-    RPar.R a b -> RPar.R b (tstar a).
-  Proof.
-    move : b.
-    apply tstar_ind => {}n{}a.
-    - hauto lq:on ctrs:R inv:R.
-    - hauto lq:on ctrs:R inv:R.
-    - hauto lq:on rew:off inv:R use:cong ctrs:R.
-    - hauto lq:on ctrs:R inv:R.
-    - hauto lq:on ctrs:R inv:R.
-    - move => p a0 b ? ? ih b0. subst.
-      elim /inv => //=_.
-      + move => p a1 a2 b1 b2 h0 h1[*]. subst.
-        by apply ih.
-      + move => p a1 a2 ha [*]. subst.
-        elim /inv : ha => //=_.
-        move => a1 a3 b0 b1 h0 h1 [*]. subst.
-        apply : ProjPair'; eauto using refl.
-    - move => p a0 b ? p0 ?. subst.
-      case : p0 => //= _.
-      move => ih b0. elim /inv => //=_.
-      + hauto l:on.
-      + move => p a1 a2 ha [*]. subst.
-        elim /inv : ha => //=_ > ? ? [*]. subst.
-        apply : ProjPair'; eauto using refl.
-    - hauto lq:on ctrs:R inv:R.
-  Qed.
-
-  Lemma diamond n (a b c : PTm n) :
-    R a b -> R a c -> exists d, R b d /\ R c d.
-  Proof. eauto using triangle. Qed.
 End RPar.
 
 Lemma red_sn_preservation n :
@@ -650,6 +610,46 @@ Proof.
   - sauto.
 Qed.
 
+Function tstar {n} (a : PTm n) :=
+  match a with
+  | VarPTm i => a
+  | PAbs a => PAbs (tstar a)
+  | PApp (PAbs a) b => subst_PTm (scons (tstar b) VarPTm) (tstar a)
+  | PApp a b => PApp (tstar a) (tstar b)
+  | PPair a b => PPair (tstar a) (tstar b)
+  | PProj p (PPair a b) => if p is PL then (tstar a) else (tstar b)
+  | PProj p a => PProj p (tstar a)
+  end.
+
+Module TStar.
+  Lemma renaming n m (ξ : fin n -> fin m) (a : PTm n) :
+    tstar (ren_PTm ξ a) = ren_PTm ξ (tstar a).
+  Proof.
+    move : m ξ.
+    apply tstar_ind => {}n {}a => //=.
+    - hauto lq:on.
+    - scongruence.
+    - move => a0 b ? h ih m ξ.
+      rewrite ih.
+      asimpl; congruence.
+    - qauto l:on.
+    - scongruence.
+    - hauto q:on.
+    - qauto l:on.
+  Qed.
+
+  Lemma pair n (a b : PTm n) :
+    tstar (PPair a b) = PPair (tstar a) (tstar b).
+    reflexivity. Qed.
+End TStar.
+
+Definition isPair {n} (a : PTm n) := if a is PPair _ _ then true else false.
+
+Lemma tstar_proj n (a : PTm n) :
+  ((~~ isPair a) /\ forall p, tstar (PProj p a) = PProj p (tstar a)) \/
+    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 EPar'.
   Inductive R {n} : PTm n -> PTm n ->  Prop :=
   (****************** Eta ***********************)
@@ -732,7 +732,6 @@ Module EPars.
     rtc EPar'.R a0 a1 ->
     rtc EPar'.R (PProj p a0) (PProj p a1).
   Proof. solve_s. Qed.
-
 End EPars.
 
 Module RReds.
@@ -772,31 +771,6 @@ Module RReds.
     move => h. move : m ξ. elim : a b /h; hauto lq:on ctrs:rtc use:RRed.renaming.
   Qed.
 
-  Lemma FromRPar n (a b : PTm n) (h : RPar.R a b) :
-    rtc RRed.R a b.
-  Proof.
-    elim : n a b /h; eauto using AbsCong, AppCong, PairCong, ProjCong, rtc_refl.
-    move => n a0 a1 b0 b1 ha iha hb ihb.
-    apply : rtc_r; last by apply RRed.AppAbs.
-    by eauto using AppCong, AbsCong.
-
-    move => n p a0 a1 b0 b1 ha iha hb ihb.
-    apply : rtc_r; last by apply RRed.ProjPair.
-    by eauto using PairCong, ProjCong.
-  Qed.
-
-  Lemma RParIff n (a b : PTm n) :
-    rtc RRed.R a b <-> rtc RPar.R a b.
-  Proof.
-    split.
-    induction 1; hauto l:on ctrs:rtc use:RPar.FromRRed, @relations.rtc_transitive.
-    induction 1; hauto l:on ctrs:rtc use:FromRPar, @relations.rtc_transitive.
-  Qed.
-
-  Lemma nf_refl n (a b : PTm n) :
-    rtc RRed.R a b -> nf a -> a = b.
-  Proof. induction 1; sfirstorder use:RRed.nf_imp. Qed.
-
 End RReds.
 
 
@@ -1298,7 +1272,7 @@ Module ERed.
     let x := Fresh.in_goal (Option.get (Ident.of_string "x")) in
     intro $x;
     lazy_match! Constr.type (Control.hyp x) with
-    | fin _ -> _ _ => (ltac1:(case;hauto q:on depth:2 ctrs:ERed.R))
+    | fin ?x -> _ ?y => (ltac1:(case;qauto depth:2 ctrs:ERed.R))
     | _ => solve_anti_ren ()
     end.
 
@@ -1308,134 +1282,36 @@ Module ERed.
   (*   destruct a. *)
   (*   exact (ξ f). *)
 
-  Lemma up_injective n m (ξ : fin n -> fin m) :
-    (forall i j, ξ i = ξ j -> i = j) ->
-    forall i j, (upRen_PTm_PTm ξ)  i = (upRen_PTm_PTm ξ) j -> i = j.
-  Proof.
-    sblast inv:option.
-  Qed.
-
-  Lemma ren_injective n m (a b : PTm n) (ξ : fin n -> fin m) :
-    (forall i j, ξ i = ξ j -> i = j) ->
-    ren_PTm ξ a = ren_PTm ξ b ->
-    a = b.
-  Proof.
-    move : m ξ b.
-    elim : n / a => //; try solve_anti_ren.
-
-    move => n a iha m ξ []//=.
-    move => u hξ [h].
-    apply iha in h. by subst.
-    destruct i, j=>//=.
-    hauto l:on.
-  Qed.
-
-  Lemma AppEta' n a u :
-    u = (@PApp (S n) (ren_PTm shift a) (VarPTm var_zero)) ->
-    R (PAbs u) a.
-  Proof. move => ->. apply AppEta. Qed.
-
-  Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) :
-    R a b -> R (ren_PTm ξ a) (ren_PTm ξ b).
-  Proof.
-    move => h. move : m ξ.
-    elim : n a b /h.
-
-    move => n a m ξ /=.
-    apply AppEta'; eauto. by asimpl.
-    all : qauto ctrs:R.
-  Qed.
-
   (* Need to generalize to injective renaming *)
   Lemma antirenaming n m (a : PTm n) (b : PTm m) (ξ : fin n -> fin m) :
-    (forall i j, ξ i = ξ j -> i = j) ->
     R (ren_PTm ξ a) b -> exists b0, R a b0 /\ ren_PTm ξ b0 = b.
   Proof.
-    move => hξ.
     move E : (ren_PTm ξ a) => u hu.
-    move : n ξ a hξ E.
+    move : n ξ a E.
     elim : m u b / hu; try solve_anti_ren.
     - move => n a m ξ []//=.
-      move => u hξ [].
+      move => u [].
       case : u => //=.
       move => u0 u1 [].
       case : u1 => //=.
       move => i /[swap] [].
       case : i => //= _ h.
-      have : exists p, ren_PTm shift p = u0 by admit.
-      move => [p ?]. subst.
-      move : h. asimpl.
-      replace (ren_PTm (funcomp shift ξ) p) with
-        (ren_PTm shift (ren_PTm ξ p)); last by asimpl.
-      move /ren_injective.
-      move /(_ ltac:(hauto l:on)).
-      move => ?. subst.
-      exists p. split=>//. apply AppEta.
-    - move => n a m ξ [] //=.
-      move => u u0 hξ [].
+      apply f_equal with (f := subst_PTm (scons (PAbs (VarPTm var_zero)) VarPTm)) in h.
+      move : h. asimpl. move => ?. subst.
+      admit.
+    - move => n a m ξ []//=.
+      move => u u0 [].
       case : u => //=.
       case : u0 => //=.
-      move => p p0 p1 p2 [? ?] [? h]. subst.
-      have ? : p0 = p2 by eauto using ren_injective. subst.
-      hauto l:on.
-    - move => n a0 a1 ha iha m ξ []//= p hξ [?]. subst.
-      sauto lq:on use:up_injective.
-  Admitted.
+      move => p p0 p1 p2 [? ?] [? ?]. subst.
+
+
+
+
 
 
 End ERed.
 
-Module EReds.
-
-  #[local]Ltac solve_s_rec :=
-  move => *; eapply rtc_l; eauto;
-         hauto lq:on ctrs:ERed.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).
-  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).
-  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).
-  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).
-  Proof. solve_s. Qed.
-
-  Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) :
-    rtc ERed.R a b -> rtc ERed.R (ren_PTm ξ a) (ren_PTm ξ b).
-  Proof. induction 1; hauto l:on use:ERed.renaming ctrs:rtc. Qed.
-
-  Lemma FromEPar n (a b : PTm n) :
-    EPar.R a b ->
-    rtc ERed.R a b.
-  Proof.
-    move => h. elim : n a b /h; eauto using AbsCong, AppCong, PairCong, ProjCong, rtc_refl.
-    - move => n a0 a1 _ h.
-      have {}h : rtc ERed.R (ren_PTm shift a0) (ren_PTm shift a1) by apply renaming.
-      apply : rtc_r. apply AbsCong. apply AppCong; eauto. apply rtc_refl.
-      apply ERed.AppEta.
-    - move => n a0 a1 _ h.
-      apply : rtc_r.
-      apply PairCong; eauto using ProjCong.
-      apply ERed.PairEta.
-  Qed.
-End EReds.
-
 #[export]Hint Constructors ERed.R RRed.R EPar.R : red.
 
 
@@ -1479,14 +1355,6 @@ Module RERed.
     ERed.R a b \/ RRed.R a b.
   Proof. induction 1; hauto lq:on db:red. Qed.
 
-  Lemma FromBeta n (a b : PTm n) :
-    RRed.R a b -> RERed.R a b.
-  Proof. induction 1; qauto l:on ctrs:R. Qed.
-
-  Lemma FromEta n (a b : PTm n) :
-    ERed.R a b -> RERed.R a b.
-  Proof. induction 1; qauto l:on ctrs:R. Qed.
-
   Lemma ToBetaEtaPar n (a b : PTm n) :
     R a b ->
     EPar.R a b \/ RRed.R a b.
@@ -1494,33 +1362,8 @@ Module RERed.
     hauto q:on use:ERed.ToEPar, ToBetaEta.
   Qed.
 
-  Lemma sn_preservation n (a b : PTm n) :
-    R a b ->
-    SN a ->
-    SN b.
-  Proof. hauto q:on use:ToBetaEtaPar, epar_sn_preservation, red_sn_preservation, RPar.FromRRed. Qed.
-
 End RERed.
 
-Module REReds.
-  Lemma sn_preservation n (a b : PTm n) :
-    rtc RERed.R a b ->
-    SN a ->
-    SN b.
-  Proof. induction 1; eauto using RERed.sn_preservation. Qed.
-
-  Lemma FromRReds n (a b : PTm n) :
-    rtc RRed.R a b ->
-    rtc RERed.R a b.
-  Proof. induction 1; hauto lq:on ctrs:rtc use:RERed.FromBeta. Qed.
-
-  Lemma FromEReds n (a b : PTm n) :
-    rtc ERed.R a b ->
-    rtc RERed.R a b.
-  Proof. induction 1; hauto lq:on ctrs:rtc use:RERed.FromEta. Qed.
-
-End REReds.
-
 Module LoRed.
   Inductive R {n} : PTm n -> PTm n ->  Prop :=
   (****************** Beta ***********************)
@@ -1562,11 +1405,6 @@ Module LoRed.
     move => h. elim : n a b /h=>//=.
   Qed.
 
-  Lemma ToRRed n (a b : PTm n) :
-    LoRed.R a b ->
-    RRed.R a b.
-  Proof. induction 1; hauto lq:on ctrs:RRed.R. Qed.
-
 End LoRed.
 
 Module LoReds.
@@ -1621,7 +1459,7 @@ Module LoReds.
 
   Local Ltac triv := simpl in *; itauto.
 
-  Lemma FromSN_mutual : forall n,
+  Lemma FromSN : forall n,
     (forall (a : PTm n) (_ : SNe a), exists v, rtc LoRed.R a v /\ ne v) /\
     (forall (a : PTm n) (_ : SN a), exists v, rtc LoRed.R a v /\ nf v) /\
     (forall (a b : PTm n) (_ : TRedSN a b), LoRed.R a b).
@@ -1645,12 +1483,6 @@ Module LoReds.
       hauto lq:on ctrs:LoRed.R.
   Qed.
 
-  Lemma FromSN : forall n a, @SN n a -> exists v, rtc LoRed.R a v /\ nf v.
-  Proof. firstorder using FromSN_mutual. Qed.
-
-  Lemma ToRReds : forall n (a b : PTm n), rtc LoRed.R a b -> rtc RRed.R a b.
-  Proof. induction 1; hauto lq:on ctrs:rtc use:LoRed.ToRRed. Qed.
-
 End LoReds.
 
 
@@ -1699,166 +1531,74 @@ Proof.
     + move => a0 a1 ha [*]. subst.
       elim /ERed.inv : ha => //= _.
       * move => a0 a2 b0 ha [*]. subst. rename a2 into a1.
-        move /ERed.antirenaming : ha.
-        move /(_ ltac:(hauto lq:on)) => [a' [h0 h1]]. subst.
-        hauto lq:on ctrs:rtc, ERed.R.
+        have [a2 [h0 h1]] : exists a2, ERed.R a2 a /\ a1 = ren_PTm shift a2 by admit. subst.
+        eexists. split; cycle 1.
+        apply : relations.rtc_r; cycle 1.
+        apply ERed.AppEta.
+        apply rtc_refl.
+        eauto using relations.rtc_once.
       * hauto q:on ctrs:rtc, ERed.R inv:ERed.R.
   - move => a c ha.
     elim /ERed.inv : ha => //= _.
     + hauto l:on.
-    + move => a0 a1 b0 ha [*]. subst.
+    + move => a0 a1 b0 ha ? [*]. subst.
       elim /ERed.inv : ha => //= _.
-      move => p a0 a2 ha [*]. subst.
-      hauto q:on ctrs:rtc, ERed.R.
-    + move => a0 b0 b1 ha [*]. subst.
-      elim /ERed.inv : ha => //= _.
-      move => p a0 a2 ha [*]. subst.
-      hauto q:on ctrs:rtc, ERed.R.
+      move => p a1 a2 ha ? [*]. subst.
+      exists a1. split. by apply relations.rtc_once.
+      apply : rtc_l. apply ERed.PairEta.
+      apply : rtc_l. apply ERed.PairCong1. eauto using ERed.ProjCong.
+      apply rtc_refl.
+    + move => a0 b0 b1 ha ? [*]. subst.
+      elim /ERed.inv : ha => //= _ p a0 a1 h ? [*]. subst.
+      exists a0. split; first by apply relations.rtc_once.
+      apply : rtc_l; first by apply ERed.PairEta.
+      apply relations.rtc_once.
+      hauto lq:on ctrs:ERed.R.
   - move => a0 a1 ha iha c.
     elim /ERed.inv => //= _.
-    + move => a2 [*]. subst.
+    + move => a2 ? [*]. subst.
       elim /ERed.inv : ha => //=_.
-      * move => a0 a2 b0 ha [*] {iha}. subst.
-        have [a0 [h0 h1]] : exists a0, ERed.R c a0 /\ a2 = ren_PTm shift a0 by hauto lq:on use:ERed.antirenaming. subst.
+      * move => a1 a2 b0 ha ? [*] {iha}. subst.
+        have [a0 [h0 h1]] : exists a0, ERed.R a0 c /\ a1 = ren_Tm shift a0 by admit. subst.
         exists a0. split; last by apply relations.rtc_once.
         apply relations.rtc_once. apply ERed.AppEta.
       * hauto q:on inv:ERed.R.
-    + hauto lq:on use:EReds.AbsCong.
+    + hauto l:on use:EReds.AbsCong.
   - move => a0 a1 b ha iha c.
     elim /ERed.inv => //= _.
     + hauto lq:on ctrs:rtc use:EReds.AppCong.
     + hauto lq:on use:@relations.rtc_once ctrs:ERed.R.
   - move => a b0 b1 hb ihb c.
     elim /ERed.inv => //=_.
-    + move => a0 a1 a2 ha [*]. subst.
-      move {ihb}. exists (PApp a1 b1).
+    + move => a0 a1 a2 ha ? [*]. subst.
+      move {ihb}. exists (App a0 b0).
       hauto lq:on use:@relations.rtc_once ctrs:ERed.R.
     + hauto lq:on ctrs:rtc use:EReds.AppCong.
   - move => a0 a1 b ha iha c.
     elim /ERed.inv => //= _.
-    + sauto lq:on.
+    + move => ? ?[*]. subst.
+      elim /ERed.inv : ha => //= _ p a1 a2 h ? [*]. subst.
+      exists a1. split; last by apply relations.rtc_once.
+      apply : rtc_l. apply ERed.PairEta.
+      apply relations.rtc_once. hauto lq:on ctrs:ERed.R.
     + hauto lq:on ctrs:rtc use:EReds.PairCong.
     + hauto lq:on ctrs:ERed.R use:@relations.rtc_once.
   - move => a b0 b1 hb hc c. elim /ERed.inv => //= _.
-    + move => ? [*]. subst.
-      sauto lq:on.
+    + move => ? ? [*]. subst.
+      elim /ERed.inv : hb => //= _ p a0 a1 ha ? [*]. subst.
+      move {hc}.
+      exists a0. split; last by apply relations.rtc_once.
+      apply : rtc_l; first by apply ERed.PairEta.
+      hauto lq:on ctrs:ERed.R use:@relations.rtc_once.
     + hauto lq:on ctrs:ERed.R use:@relations.rtc_once.
     + hauto lq:on ctrs:rtc use:EReds.PairCong.
   - qauto l:on inv:ERed.R use:EReds.ProjCong.
-Qed.
-
-Lemma ered_confluence n (a b c : PTm n) :
-  rtc ERed.R a b ->
-  rtc ERed.R a c ->
-  exists d, rtc ERed.R b d  /\ rtc ERed.R c d.
-Proof.
-  sfirstorder use:relations.locally_confluent_confluent, ered_sn, ered_local_confluence.
-Qed.
-
-Lemma red_confluence n (a b c : PTm n) :
-  rtc RRed.R a b ->
-  rtc RRed.R a c ->
-  exists d, rtc RRed.R b d  /\ rtc RRed.R c d.
-  suff : rtc RPar.R a b -> rtc RPar.R a c -> exists d : PTm n, rtc RPar.R b d /\ rtc RPar.R c d
-             by hauto lq:on use:RReds.RParIff.
-  apply relations.diamond_confluent.
-  rewrite /relations.diamond.
-  eauto using RPar.diamond.
-Qed.
-
-Lemma red_uniquenf n (a b c : PTm n) :
-  rtc RRed.R a b ->
-  rtc RRed.R a c ->
-  nf b ->
-  nf c ->
-  b = c.
-Proof.
-  move : red_confluence; repeat move/[apply].
-  move => [d [h0 h1]].
-  move => *.
-  suff [] : b = d /\ c = d by congruence.
-  sfirstorder use:RReds.nf_refl.
-Qed.
-
-Module NeEPars.
-  Lemma R_nonelim_nf n (a b : PTm n) :
-    rtc NeEPar.R_nonelim a b ->
-    nf b ->
-    nf a.
-  Proof. induction 1; sfirstorder use:NeEPar.R_elim_nf. Qed.
-
-  Lemma ToEReds : forall n, (forall (a b : PTm n), rtc NeEPar.R_nonelim a b -> rtc ERed.R a b).
-  Proof.
-    induction 1; hauto l:on use:NeEPar.ToEPar, EReds.FromEPar, @relations.rtc_transitive.
-  Qed.
-End NeEPars.
-
-
-Lemma rered_standardization n (a c : PTm n) :
-  SN a ->
-  rtc RERed.R a c ->
-  exists b, rtc RRed.R a b /\ rtc NeEPar.R_nonelim b c.
-Proof.
-  move => + h. elim : a c /h.
-  by eauto using rtc_refl.
-  move => a b c.
-  move /RERed.ToBetaEtaPar.
-  case.
-  - move => h0 h1 ih hP.
-    have  : SN b by qauto use:epar_sn_preservation.
-    move => {}/ih [b' [ihb0 ihb1]].
-    hauto lq:on ctrs:rtc use:SN_UniqueNF.η_postponement_star'.
-  - hauto lq:on ctrs:rtc use:red_sn_preservation, RPar.FromRRed.
-Qed.
-
-Lemma rered_confluence n (a b c : PTm n) :
-  SN a ->
-  rtc RERed.R a b ->
-  rtc RERed.R a c ->
-  exists d, rtc RERed.R b d  /\ rtc RERed.R c d.
-Proof.
-  move => hP hb hc.
-  have [] : SN b /\ SN c by qauto use:REReds.sn_preservation.
-  move => /LoReds.FromSN [bv [/LoReds.ToRReds /REReds.FromRReds hbv  hbv']].
-  move => /LoReds.FromSN [cv [/LoReds.ToRReds /REReds.FromRReds hcv  hcv']].
-  have [] : SN b /\ SN c by sfirstorder use:REReds.sn_preservation.
-  move : rered_standardization hbv; repeat move/[apply]. move => [bv' [hb0 hb1]].
-  move : rered_standardization hcv; repeat move/[apply]. move => [cv' [hc0 hc1]].
-
-  have [] : rtc RERed.R a bv' /\ rtc RERed.R a cv'
-    by sfirstorder use:@relations.rtc_transitive, REReds.FromRReds.
-  move : rered_standardization (hP). repeat move/[apply]. move => [bv'' [hb3 hb4]].
-  move : rered_standardization (hP). repeat move/[apply]. move => [cv'' [hc3 hc4]].
-  have hb2 : rtc NeEPar.R_nonelim bv'' bv by hauto lq:on use:@relations.rtc_transitive.
-  have hc2 : rtc NeEPar.R_nonelim cv'' cv by hauto lq:on use:@relations.rtc_transitive.
-  have [hc5 hb5] : nf cv'' /\ nf bv'' by sfirstorder use:NeEPars.R_nonelim_nf.
-  have ? : bv'' = cv'' by sfirstorder use:red_uniquenf. subst.
-  apply NeEPars.ToEReds in hb2, hc2.
-  move : ered_confluence (hb2) (hc2); repeat move/[apply].
-  move => [v [hv hv']].
-  exists v. split.
-  move /NeEPars.ToEReds /REReds.FromEReds : hb1.
-  move /REReds.FromRReds : hb0. move /REReds.FromEReds : hv. eauto using relations.rtc_transitive.
-  move /NeEPars.ToEReds /REReds.FromEReds : hc1.
-  move /REReds.FromRReds : hc0. move /REReds.FromEReds : hv'. eauto using relations.rtc_transitive.
-Qed.
-
-(* "Declarative" Joinability *)
-Module DJoin.
-  Definition R {n} (a b : PTm n) := exists c, rtc RERed.R a c /\ rtc RERed.R b c.
-
-  Lemma refl n (a : PTm n) : R a a.
-  Proof. sfirstorder use:@rtc_refl unfold:R. Qed.
-
-  Lemma symmetric n (a b : PTm n) : R a b -> R b a.
-  Proof. sfirstorder unfold:R. Qed.
-
-  Lemma transitive n (a b c : PTm n) : SN b -> R a b -> R b c -> R a c.
-  Proof.
-    rewrite /R.
-    move => + [ab [ha +]] [bc [+ hc]].
-    move : rered_confluence; repeat move/[apply].
-    move => [v [h0 h1]].
-    exists v. sfirstorder use:@relations.rtc_transitive.
-  Qed.
-End DJoin.
+  - move => p A0 A1 B hA ihA.
+    move => c. elim/ERed.inv => //=.
+    + hauto lq:on ctrs:rtc use:EReds.BindCong.
+    + hauto lq:on ctrs:ERed.R use:@relations.rtc_once.
+  - move => p A B0 B1 hB ihB c.
+    elim /ERed.inv => //=.
+    + hauto lq:on ctrs:ERed.R use:@relations.rtc_once.
+    + hauto lq:on ctrs:rtc use:EReds.BindCong.
+Admitted.