diff --git a/syntax.sig b/syntax.sig
index 9c83c4f..68be421 100644
--- a/syntax.sig
+++ b/syntax.sig
@@ -1,8 +1,9 @@
 Tm(VarTm) : Type
--- nat : Type
+PTag : Type
 
+PL : PTag
+PR : PTag
 Abs : (bind Tm in Tm) -> Tm
 App : Tm -> Tm -> Tm
 Pair : Tm -> Tm -> Tm
-Proj1 : Tm -> Tm
-Proj2 : Tm -> Tm
+Proj : PTag -> Tm -> Tm
diff --git a/theories/Autosubst2/syntax.v b/theories/Autosubst2/syntax.v
index 79e4f87..ed66e97 100644
--- a/theories/Autosubst2/syntax.v
+++ b/theories/Autosubst2/syntax.v
@@ -5,13 +5,26 @@ Require Import Setoid Morphisms Relation_Definitions.
 
 Module Core.
 
+Inductive PTag : Type :=
+  | PL : PTag
+  | PR : PTag.
+
+Lemma congr_PL : PL = PL.
+Proof.
+exact (eq_refl).
+Qed.
+
+Lemma congr_PR : PR = PR.
+Proof.
+exact (eq_refl).
+Qed.
+
 Inductive Tm (n_Tm : nat) : Type :=
   | VarTm : fin n_Tm -> Tm n_Tm
   | Abs : Tm (S n_Tm) -> Tm n_Tm
   | App : Tm n_Tm -> Tm n_Tm -> Tm n_Tm
   | Pair : Tm n_Tm -> Tm n_Tm -> Tm n_Tm
-  | Proj1 : Tm n_Tm -> Tm n_Tm
-  | Proj2 : Tm n_Tm -> Tm n_Tm.
+  | Proj : PTag -> Tm n_Tm -> Tm n_Tm.
 
 Lemma congr_Abs {m_Tm : nat} {s0 : Tm (S m_Tm)} {t0 : Tm (S m_Tm)}
   (H0 : s0 = t0) : Abs m_Tm s0 = Abs m_Tm t0.
@@ -35,16 +48,12 @@ exact (eq_trans (eq_trans eq_refl (ap (fun x => Pair m_Tm x s1) H0))
          (ap (fun x => Pair m_Tm t0 x) H1)).
 Qed.
 
-Lemma congr_Proj1 {m_Tm : nat} {s0 : Tm m_Tm} {t0 : Tm m_Tm} (H0 : s0 = t0) :
-  Proj1 m_Tm s0 = Proj1 m_Tm t0.
+Lemma congr_Proj {m_Tm : nat} {s0 : PTag} {s1 : Tm m_Tm} {t0 : PTag}
+  {t1 : Tm m_Tm} (H0 : s0 = t0) (H1 : s1 = t1) :
+  Proj m_Tm s0 s1 = Proj m_Tm t0 t1.
 Proof.
-exact (eq_trans eq_refl (ap (fun x => Proj1 m_Tm x) H0)).
-Qed.
-
-Lemma congr_Proj2 {m_Tm : nat} {s0 : Tm m_Tm} {t0 : Tm m_Tm} (H0 : s0 = t0) :
-  Proj2 m_Tm s0 = Proj2 m_Tm t0.
-Proof.
-exact (eq_trans eq_refl (ap (fun x => Proj2 m_Tm x) H0)).
+exact (eq_trans (eq_trans eq_refl (ap (fun x => Proj m_Tm x s1) H0))
+         (ap (fun x => Proj m_Tm t0 x) H1)).
 Qed.
 
 Lemma upRen_Tm_Tm {m : nat} {n : nat} (xi : fin m -> fin n) :
@@ -66,8 +75,7 @@ Fixpoint ren_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm)
   | Abs _ s0 => Abs n_Tm (ren_Tm (upRen_Tm_Tm xi_Tm) s0)
   | App _ s0 s1 => App n_Tm (ren_Tm xi_Tm s0) (ren_Tm xi_Tm s1)
   | Pair _ s0 s1 => Pair n_Tm (ren_Tm xi_Tm s0) (ren_Tm xi_Tm s1)
-  | Proj1 _ s0 => Proj1 n_Tm (ren_Tm xi_Tm s0)
-  | Proj2 _ s0 => Proj2 n_Tm (ren_Tm xi_Tm s0)
+  | Proj _ s0 s1 => Proj n_Tm s0 (ren_Tm xi_Tm s1)
   end.
 
 Lemma up_Tm_Tm {m : nat} {n_Tm : nat} (sigma : fin m -> Tm n_Tm) :
@@ -90,8 +98,7 @@ Fixpoint subst_Tm {m_Tm : nat} {n_Tm : nat} (sigma_Tm : fin m_Tm -> Tm n_Tm)
   | Abs _ s0 => Abs n_Tm (subst_Tm (up_Tm_Tm sigma_Tm) s0)
   | App _ s0 s1 => App n_Tm (subst_Tm sigma_Tm s0) (subst_Tm sigma_Tm s1)
   | Pair _ s0 s1 => Pair n_Tm (subst_Tm sigma_Tm s0) (subst_Tm sigma_Tm s1)
-  | Proj1 _ s0 => Proj1 n_Tm (subst_Tm sigma_Tm s0)
-  | Proj2 _ s0 => Proj2 n_Tm (subst_Tm sigma_Tm s0)
+  | Proj _ s0 s1 => Proj n_Tm s0 (subst_Tm sigma_Tm s1)
   end.
 
 Lemma upId_Tm_Tm {m_Tm : nat} (sigma : fin m_Tm -> Tm m_Tm)
@@ -126,8 +133,7 @@ subst_Tm sigma_Tm s = s :=
   | Pair _ s0 s1 =>
       congr_Pair (idSubst_Tm sigma_Tm Eq_Tm s0)
         (idSubst_Tm sigma_Tm Eq_Tm s1)
-  | Proj1 _ s0 => congr_Proj1 (idSubst_Tm sigma_Tm Eq_Tm s0)
-  | Proj2 _ s0 => congr_Proj2 (idSubst_Tm sigma_Tm Eq_Tm s0)
+  | Proj _ s0 s1 => congr_Proj (eq_refl s0) (idSubst_Tm sigma_Tm Eq_Tm s1)
   end.
 
 Lemma upExtRen_Tm_Tm {m : nat} {n : nat} (xi : fin m -> fin n)
@@ -164,8 +170,8 @@ Fixpoint extRen_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm)
   | Pair _ s0 s1 =>
       congr_Pair (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0)
         (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1)
-  | Proj1 _ s0 => congr_Proj1 (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0)
-  | Proj2 _ s0 => congr_Proj2 (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0)
+  | Proj _ s0 s1 =>
+      congr_Proj (eq_refl s0) (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1)
   end.
 
 Lemma upExt_Tm_Tm {m : nat} {n_Tm : nat} (sigma : fin m -> Tm n_Tm)
@@ -204,8 +210,7 @@ Fixpoint ext_Tm {m_Tm : nat} {n_Tm : nat} (sigma_Tm : fin m_Tm -> Tm n_Tm)
   | Pair _ s0 s1 =>
       congr_Pair (ext_Tm sigma_Tm tau_Tm Eq_Tm s0)
         (ext_Tm sigma_Tm tau_Tm Eq_Tm s1)
-  | Proj1 _ s0 => congr_Proj1 (ext_Tm sigma_Tm tau_Tm Eq_Tm s0)
-  | Proj2 _ s0 => congr_Proj2 (ext_Tm sigma_Tm tau_Tm Eq_Tm s0)
+  | Proj _ s0 s1 => congr_Proj (eq_refl s0) (ext_Tm sigma_Tm tau_Tm Eq_Tm s1)
   end.
 
 Lemma up_ren_ren_Tm_Tm {k : nat} {l : nat} {m : nat} (xi : fin k -> fin l)
@@ -243,8 +248,8 @@ Fixpoint compRenRen_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
   | Pair _ s0 s1 =>
       congr_Pair (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0)
         (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1)
-  | Proj1 _ s0 => congr_Proj1 (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0)
-  | Proj2 _ s0 => congr_Proj2 (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0)
+  | Proj _ s0 s1 =>
+      congr_Proj (eq_refl s0) (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1)
   end.
 
 Lemma up_ren_subst_Tm_Tm {k : nat} {l : nat} {m_Tm : nat}
@@ -291,10 +296,9 @@ Fixpoint compRenSubst_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
   | Pair _ s0 s1 =>
       congr_Pair (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0)
         (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s1)
-  | Proj1 _ s0 =>
-      congr_Proj1 (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0)
-  | Proj2 _ s0 =>
-      congr_Proj2 (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0)
+  | Proj _ s0 s1 =>
+      congr_Proj (eq_refl s0)
+        (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s1)
   end.
 
 Lemma up_subst_ren_Tm_Tm {k : nat} {l_Tm : nat} {m_Tm : nat}
@@ -362,10 +366,9 @@ ren_Tm zeta_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s :=
   | Pair _ s0 s1 =>
       congr_Pair (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0)
         (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s1)
-  | Proj1 _ s0 =>
-      congr_Proj1 (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0)
-  | Proj2 _ s0 =>
-      congr_Proj2 (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0)
+  | Proj _ s0 s1 =>
+      congr_Proj (eq_refl s0)
+        (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s1)
   end.
 
 Lemma up_subst_subst_Tm_Tm {k : nat} {l_Tm : nat} {m_Tm : nat}
@@ -434,10 +437,9 @@ subst_Tm tau_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s :=
   | Pair _ s0 s1 =>
       congr_Pair (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0)
         (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s1)
-  | Proj1 _ s0 =>
-      congr_Proj1 (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0)
-  | Proj2 _ s0 =>
-      congr_Proj2 (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0)
+  | Proj _ s0 s1 =>
+      congr_Proj (eq_refl s0)
+        (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s1)
   end.
 
 Lemma renRen_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
@@ -546,8 +548,8 @@ Fixpoint rinst_inst_Tm {m_Tm : nat} {n_Tm : nat}
   | Pair _ s0 s1 =>
       congr_Pair (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0)
         (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1)
-  | Proj1 _ s0 => congr_Proj1 (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0)
-  | Proj2 _ s0 => congr_Proj2 (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0)
+  | Proj _ s0 s1 =>
+      congr_Proj (eq_refl s0) (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1)
   end.
 
 Lemma rinstInst'_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm)
@@ -746,9 +748,7 @@ Core.
 
 Arguments VarTm {n_Tm}.
 
-Arguments Proj2 {n_Tm}.
-
-Arguments Proj1 {n_Tm}.
+Arguments Proj {n_Tm}.
 
 Arguments Pair {n_Tm}.
 
diff --git a/theories/fp_red.v b/theories/fp_red.v
index 7c90cab..32a17b4 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -17,18 +17,13 @@ Module Par.
     R b0 b1 ->
     R c0 c1 ->
     R (App (Pair a0 b0) c0) (Pair (App a1 c1) (App b1 c1))
-  | Proj1Abs a0 a1 :
+  | ProjAbs p a0 a1 :
     R a0 a1 ->
-    R (Proj1 (Abs a0)) (Abs (Proj1 a0))
-  | Proj1Pair a0 a1 b :
+    R (Proj p (Abs a0)) (Abs (Proj p a1))
+  | ProjPair p a0 a1 b0 b1 :
     R a0 a1 ->
-    R (Proj1 (Pair a0 b)) a1
-  | Proj2Abs a0 a1 :
-    R a0 a1 ->
-    R (Proj2 (Abs a0)) (Abs (Proj2 a0))
-  | Proj2Pair a0 a1 b :
-    R a0 a1 ->
-    R (Proj2 (Pair b a0)) a1
+    R b0 b1 ->
+    R (Proj p (Pair a0 b0)) (if p is PL then a1 else b1)
 
   (****************** Eta ***********************)
   | AppEta a0 a1 :
@@ -36,7 +31,7 @@ Module Par.
     R a0 (Abs (App (ren_Tm shift a1) (VarTm var_zero)))
   | PairEta a0 a1 :
     R a0 a1 ->
-    R a0 (Pair (Proj1 a1) (Proj2 a1))
+    R a0 (Pair (Proj PL a1) (Proj PR a1))
 
   (*************** Congruence ********************)
   | Var i : R (VarTm i) (VarTm i)
@@ -51,12 +46,9 @@ Module Par.
     R a0 a1 ->
     R b0 b1 ->
     R (Pair a0 b0) (Pair a1 b1)
-  | Proj1Cong a0 a1 :
+  | ProjCong p a0 a1 :
     R a0 a1 ->
-    R (Proj1 a0) (Proj1 a1)
-  | Proj2Cong a0 a1 :
-    R a0 a1 ->
-    R (Proj2 a0) (Proj2 a1).
+    R (Proj p a0) (Proj p a1).
 End Par.
 
 (***************** Beta rules only ***********************)
@@ -72,18 +64,14 @@ Module RPar.
     R b0 b1 ->
     R c0 c1 ->
     R (App (Pair a0 b0) c0) (Pair (App a1 c1) (App b1 c1))
-  | Proj1Abs a0 a1 :
+  | ProjAbs p a0 a1 :
     R a0 a1 ->
-    R (Proj1 (Abs a0)) (Abs (Proj1 a1))
-  | Proj1Pair a0 a1 b :
+    R (Proj p (Abs a0)) (Abs (Proj p a1))
+  | ProjPair p a0 a1 b0 b1 :
     R a0 a1 ->
-    R (Proj1 (Pair a0 b)) a1
-  | Proj2Abs a0 a1 :
-    R a0 a1 ->
-    R (Proj2 (Abs a0)) (Abs (Proj2 a1))
-  | Proj2Pair a0 a1 b :
-    R a0 a1 ->
-    R (Proj2 (Pair b a0)) a1
+    R b0 b1 ->
+    R (Proj p (Pair a0 b0)) (if p is PL then a1 else b1)
+
 
   (*************** Congruence ********************)
   | Var i : R (VarTm i) (VarTm i)
@@ -98,12 +86,9 @@ Module RPar.
     R a0 a1 ->
     R b0 b1 ->
     R (Pair a0 b0) (Pair a1 b1)
-  | Proj1Cong a0 a1 :
+  | ProjCong p a0 a1 :
     R a0 a1 ->
-    R (Proj1 a0) (Proj1 a1)
-  | Proj2Cong a0 a1 :
-    R a0 a1 ->
-    R (Proj2 a0) (Proj2 a1).
+    R (Proj p a0) (Proj p a1).
 
   Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop.
 
@@ -119,13 +104,20 @@ Module RPar.
     R (App (Abs a0) b0) t.
   Proof. move => ->. apply AppAbs. Qed.
 
+  Lemma ProjPair' n p (a0 a1 b0 b1 : Tm n) t :
+    t = (if p is PL then a1 else b1) ->
+    R a0 a1 ->
+    R b0 b1 ->
+    R (Proj p (Pair a0 b0)) t.
+  Proof.  move => > ->. apply ProjPair. Qed.
+
   Lemma renaming n m (a b : Tm n) (ξ : fin n -> fin m) :
     R a b -> R (ren_Tm ξ a) (ren_Tm ξ b).
   Proof.
     move => h. move : m ξ.
     elim : n a b /h.
     move => *; apply : AppAbs'; eauto; by asimpl.
-    all : qauto ctrs:R.
+    all : qauto ctrs:R use:ProjPair'.
   Qed.
 
   Lemma morphing_ren n m p (ρ0 ρ1 : fin n -> Tm m) (ξ : fin m -> fin p) :
@@ -155,13 +147,10 @@ Module RPar.
       by asimpl.
     - hauto lq:on ctrs:R.
     - hauto lq:on ctrs:R use:morphing_up.
+    - hauto lq:on ctrs:R use:ProjPair' use:morphing_up.
     - hauto lq:on ctrs:R use:morphing_up.
     - hauto lq:on ctrs:R use:morphing_up.
     - hauto lq:on ctrs:R use:morphing_up.
-    - qauto.
-    - hauto lq:on ctrs:R use:morphing_up.
-    - hauto lq:on ctrs:R.
-    - hauto lq:on ctrs:R.
     - hauto lq:on ctrs:R.
     - hauto lq:on ctrs:R.
   Qed.
@@ -180,7 +169,7 @@ Module EPar.
     R a0 (Abs (App (ren_Tm shift a1) (VarTm var_zero)))
   | PairEta a0 a1 :
     R a0 a1 ->
-    R a0 (Pair (Proj1 a1) (Proj2 a1))
+    R a0 (Pair (Proj PL a1) (Proj PR a1))
 
   (*************** Congruence ********************)
   | Var i : R (VarTm i) (VarTm i)
@@ -195,12 +184,9 @@ Module EPar.
     R a0 a1 ->
     R b0 b1 ->
     R (Pair a0 b0) (Pair a1 b1)
-  | Proj1Cong a0 a1 :
+  | ProjCong p a0 a1 :
     R a0 a1 ->
-    R (Proj1 a0) (Proj1 a1)
-  | Proj2Cong a0 a1 :
-    R a0 a1 ->
-    R (Proj2 a0) (Proj2 a1).
+    R (Proj p a0) (Proj p a1).
 
   Lemma refl n (a : Tm n) : EPar.R a a.
   Proof.
@@ -242,7 +228,6 @@ Module EPar.
     - hauto q:on ctrs:R.
     - hauto q:on ctrs:R.
     - hauto q:on ctrs:R.
-    - hauto q:on ctrs:R.
   Qed.
 
   Lemma substing n a0 a1 (b0 b1 : Tm n) :
@@ -287,14 +272,9 @@ Module RPars.
     rtc RPar.R (Pair a0 b0) (Pair a1 b1).
   Proof. solve_s. Qed.
 
-  Lemma Proj1Cong n (a0 a1  : Tm n) :
+  Lemma ProjCong n p (a0 a1  : Tm n) :
     rtc RPar.R a0 a1 ->
-    rtc RPar.R (Proj1 a0) (Proj1 a1).
-  Proof. solve_s. Qed.
-
-  Lemma Proj2Cong n (a0 a1  : Tm n) :
-    rtc RPar.R a0 a1 ->
-    rtc RPar.R (Proj2 a0) (Proj2 a1).
+    rtc RPar.R (Proj p a0) (Proj p a1).
   Proof. solve_s. Qed.
 
   Lemma renaming n (a0 a1 : Tm n) m (ξ : fin n -> fin m) :
@@ -337,9 +317,8 @@ Lemma Abs_EPar n a (b : Tm n) :
   (exists d, EPar.R a d /\
      rtc RPar.R (App (ren_Tm shift b) (VarTm var_zero)) d) /\
          (exists d,
-         EPar.R a d /\
-         rtc RPar.R (Proj1 b) (Abs (Proj1 d)) /\
-         rtc RPar.R (Proj2 b) (Abs (Proj2 d))).
+         EPar.R a d /\ forall p,
+         rtc RPar.R (Proj p b) (Abs (Proj p d))).
 Proof.
   move E : (Abs a) => u h.
   move : a E.
@@ -354,47 +333,35 @@ Proof.
       apply RPar.refl.
       by apply RPar.refl.
       move :ih1; substify; by asimpl.
-    + repeat split => //.
-      * apply : rtc_l.
-        apply : RPar.Proj1Abs.
-        by apply RPar.refl.
-        eauto using RPars.Proj1Cong, RPars.AbsCong.
-      * apply : rtc_l.
-        apply : RPar.Proj2Abs.
-        by apply RPar.refl.
-        eauto using RPars.Proj2Cong, RPars.AbsCong.
+    + split => // p.
+      apply : rtc_l.
+      apply : RPar.ProjAbs.
+      by apply RPar.refl.
+      eauto using RPars.ProjCong, RPars.AbsCong.
   - move => n ? a1 ha iha a0 ?. subst. specialize iha with (1 := eq_refl).
-    move : iha => [_ [d [ih0 [ih1 ih2]]]].
+    move : iha => [_ [d [ih0 ih1]]].
     split.
-    + apply RPars.weakening in ih1, ih2.
-      exists (Pair (Proj1 d) (Proj2 d)).
-      split; first by by by apply EPar.PairEta.
+    + exists (Pair (Proj PL d) (Proj PR d)).
+      split; first by apply EPar.PairEta.
       apply : rtc_l.
       apply RPar.AppPair; eauto using RPar.refl.
-      suff : rtc RPar.R (App (Proj1 (ren_Tm shift a1)) (VarTm var_zero)) (Proj1 d) /\
-               rtc RPar.R (App (Proj2 (ren_Tm shift a1)) (VarTm var_zero)) (Proj2 d)
-        by firstorder using RPars.PairCong.
-      split.
-      * apply relations.rtc_transitive with (y := App (ren_Tm shift (Abs (Proj1 d))) (VarTm var_zero)).
-        by eauto using RPars.AppCong, rtc_refl.
-        apply relations.rtc_once => /=.
-        apply : RPar.AppAbs'; eauto using RPar.refl.
-        by asimpl.
-      * apply relations.rtc_transitive with (y := App (ren_Tm shift (Abs (Proj2 d))) (VarTm var_zero)).
-        by eauto using RPars.AppCong, rtc_refl.
-        apply relations.rtc_once => /=.
-        apply : RPar.AppAbs'; eauto using RPar.refl.
-        by asimpl.
-    + exists d. repeat split => //.
-      apply : rtc_l;eauto. apply RPar.Proj1Pair. eauto using RPar.refl.
-      apply : rtc_l;eauto. apply RPar.Proj2Pair. eauto using RPar.refl.
+      suff h : forall p, rtc RPar.R (App (Proj p (ren_Tm shift a1)) (VarTm var_zero)) (Proj p d) by
+          sfirstorder use:RPars.PairCong.
+      move => p. move /(_ p) /RPars.weakening in ih1.
+      apply relations.rtc_transitive with (y := App (ren_Tm shift (Abs (Proj p d))) (VarTm var_zero)).
+      by eauto using RPars.AppCong, rtc_refl.
+      apply relations.rtc_once => /=.
+      apply : RPar.AppAbs'; eauto using RPar.refl.
+      by asimpl.
+    + exists d. repeat split => //. move => p.
+      apply : rtc_l; eauto.
+      hauto q:on use:RPar.ProjPair', RPar.refl.
   - move => n a0 a1 ha _ ? [*]. subst.
     split.
     + exists a1. split => //.
       apply rtc_once. apply : RPar.AppAbs'; eauto using RPar.refl. by asimpl.
-    + exists a1. repeat split => //=.
-      apply rtc_once. apply : RPar.Proj1Abs; eauto using RPar.refl.
-      apply rtc_once. apply : RPar.Proj2Abs; eauto using RPar.refl.
+    + exists a1. split => // p.
+      apply rtc_once. apply : RPar.ProjAbs; eauto using RPar.refl.
 Qed.
 
 Lemma commutativity n (a b0 b1 : Tm n) :
@@ -411,10 +378,9 @@ Proof.
     + hauto lq:on ctrs:EPar.R use:EPar.refl, EPar.renaming.
   - move => n a b0 hb0 ihb0 b1 /[dup] hb1 {}/ihb0.
     move => [c [ih0 ih1]].
-    exists (Pair (Proj1 c) (Proj2 c)). split.
-    + apply RPars.PairCong.
-      by apply RPars.Proj1Cong.
-      by apply RPars.Proj2Cong.
+    exists (Pair (Proj PL c) (Proj PR c)). split.
+    + apply RPars.PairCong;
+      by apply RPars.ProjCong.
     + hauto lq:on ctrs:EPar.R use:EPar.refl, EPar.renaming.
   - hauto l:on ctrs:rtc inv:RPar.R.
   - move => n a0 a1 h ih b1.
@@ -440,20 +406,17 @@ Proof.
       admit.
     + hauto lq:on ctrs:EPar.R use:RPars.AppCong.
   - hauto lq:on ctrs:EPar.R inv:RPar.R use:RPars.PairCong.
-  - move => n a b0 h0 ih0 b1.
+  - move => n p a b0 h0 ih0 b1.
     elim /RPar.inv => //= _.
-    + move => a0 a1 h [*]. subst.
+    + move => ? a0 a1 h [*]. subst.
+      move /(_ _ ltac:(by eauto using RPar.AbsCong)) : ih0 => [c [ih0 ih1]].
+      move /Abs_EPar : ih1 => [_ [d [ih1 ih2]]].
+      exists (Abs (Proj p d)).
+      qauto l:on ctrs:EPar.R use:RPars.ProjCong, @relations.rtc_transitive.
+    + move => p0 a0 a1 b2 b3 h1 h2 [*]. subst.
+      move /(_ _ ltac:(by eauto using RPar.PairCong)) : ih0 => [c [ih0 ih1]].
       admit.
-    + move => a0 ? a1 h1 [*]. subst.
-      admit.
-    + hauto lq:on ctrs:RPar.R, EPar.R.
-  - move => n a b0 h0 ih0 b1.
-    elim /RPar.inv => //= _.
-    + move => a0 a1 ha [*]. subst.
-      admit.
-    + move => a0 a1 b2 h [*]. subst.
-      admit.
-    + hauto lq:on ctrs:RPar.R, EPar.R.
+    + hauto lq:on ctrs:EPar.R use:RPars.ProjCong.
 Admitted.
 
 Lemma EPar_Par n (a b : Tm n) : EPar.R a b -> Par.R a b.