diff --git a/syntax.sig b/syntax.sig
index 4549f7f..d2354e2 100644
--- a/syntax.sig
+++ b/syntax.sig
@@ -2,6 +2,7 @@ nat  : Type
 Tm(VarTm) : Type
 PTag : Type
 TTag : Type
+bool : Type
 
 TPi : TTag
 TSig : TTag
@@ -14,3 +15,6 @@ Proj : PTag -> Tm -> Tm
 TBind : TTag -> Tm -> (bind Tm in Tm) -> Tm
 Bot : Tm
 Univ : nat -> Tm
+Bool : Tm
+BVal : bool -> Tm
+If : Tm -> Tm -> Tm -> Tm
\ No newline at end of file
diff --git a/theories/Autosubst2/syntax.v b/theories/Autosubst2/syntax.v
index b972476..ffb7c7c 100644
--- a/theories/Autosubst2/syntax.v
+++ b/theories/Autosubst2/syntax.v
@@ -41,7 +41,10 @@ Inductive Tm (n_Tm : nat) : Type :=
   | Proj : PTag -> Tm n_Tm -> Tm n_Tm
   | TBind : TTag -> Tm n_Tm -> Tm (S n_Tm) -> Tm n_Tm
   | Bot : Tm n_Tm
-  | Univ : nat -> Tm n_Tm.
+  | Univ : nat -> Tm n_Tm
+  | Bool : Tm n_Tm
+  | BVal : bool -> Tm n_Tm
+  | If : Tm n_Tm -> Tm n_Tm -> 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.
@@ -94,6 +97,27 @@ Proof.
 exact (eq_trans eq_refl (ap (fun x => Univ m_Tm x) H0)).
 Qed.
 
+Lemma congr_Bool {m_Tm : nat} : Bool m_Tm = Bool m_Tm.
+Proof.
+exact (eq_refl).
+Qed.
+
+Lemma congr_BVal {m_Tm : nat} {s0 : bool} {t0 : bool} (H0 : s0 = t0) :
+  BVal m_Tm s0 = BVal m_Tm t0.
+Proof.
+exact (eq_trans eq_refl (ap (fun x => BVal m_Tm x) H0)).
+Qed.
+
+Lemma congr_If {m_Tm : nat} {s0 : Tm m_Tm} {s1 : Tm m_Tm} {s2 : Tm m_Tm}
+  {t0 : Tm m_Tm} {t1 : Tm m_Tm} {t2 : Tm m_Tm} (H0 : s0 = t0) (H1 : s1 = t1)
+  (H2 : s2 = t2) : If m_Tm s0 s1 s2 = If m_Tm t0 t1 t2.
+Proof.
+exact (eq_trans
+         (eq_trans (eq_trans eq_refl (ap (fun x => If m_Tm x s1 s2) H0))
+            (ap (fun x => If m_Tm t0 x s2) H1))
+         (ap (fun x => If m_Tm t0 t1 x) H2)).
+Qed.
+
 Lemma upRen_Tm_Tm {m : nat} {n : nat} (xi : fin m -> fin n) :
   fin (S m) -> fin (S n).
 Proof.
@@ -118,6 +142,10 @@ Fixpoint ren_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm)
       TBind n_Tm s0 (ren_Tm xi_Tm s1) (ren_Tm (upRen_Tm_Tm xi_Tm) s2)
   | Bot _ => Bot n_Tm
   | Univ _ s0 => Univ n_Tm s0
+  | Bool _ => Bool n_Tm
+  | BVal _ s0 => BVal n_Tm s0
+  | If _ s0 s1 s2 =>
+      If n_Tm (ren_Tm xi_Tm s0) (ren_Tm xi_Tm s1) (ren_Tm xi_Tm s2)
   end.
 
 Lemma up_Tm_Tm {m : nat} {n_Tm : nat} (sigma : fin m -> Tm n_Tm) :
@@ -145,6 +173,11 @@ Fixpoint subst_Tm {m_Tm : nat} {n_Tm : nat} (sigma_Tm : fin m_Tm -> Tm n_Tm)
       TBind n_Tm s0 (subst_Tm sigma_Tm s1) (subst_Tm (up_Tm_Tm sigma_Tm) s2)
   | Bot _ => Bot n_Tm
   | Univ _ s0 => Univ n_Tm s0
+  | Bool _ => Bool n_Tm
+  | BVal _ s0 => BVal n_Tm s0
+  | If _ s0 s1 s2 =>
+      If n_Tm (subst_Tm sigma_Tm s0) (subst_Tm sigma_Tm s1)
+        (subst_Tm sigma_Tm s2)
   end.
 
 Lemma upId_Tm_Tm {m_Tm : nat} (sigma : fin m_Tm -> Tm m_Tm)
@@ -185,6 +218,11 @@ subst_Tm sigma_Tm s = s :=
         (idSubst_Tm (up_Tm_Tm sigma_Tm) (upId_Tm_Tm _ Eq_Tm) s2)
   | Bot _ => congr_Bot
   | Univ _ s0 => congr_Univ (eq_refl s0)
+  | Bool _ => congr_Bool
+  | BVal _ s0 => congr_BVal (eq_refl s0)
+  | If _ s0 s1 s2 =>
+      congr_If (idSubst_Tm sigma_Tm Eq_Tm s0) (idSubst_Tm sigma_Tm Eq_Tm s1)
+        (idSubst_Tm sigma_Tm Eq_Tm s2)
   end.
 
 Lemma upExtRen_Tm_Tm {m : nat} {n : nat} (xi : fin m -> fin n)
@@ -229,6 +267,11 @@ Fixpoint extRen_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm)
            (upExtRen_Tm_Tm _ _ Eq_Tm) s2)
   | Bot _ => congr_Bot
   | Univ _ s0 => congr_Univ (eq_refl s0)
+  | Bool _ => congr_Bool
+  | BVal _ s0 => congr_BVal (eq_refl s0)
+  | If _ s0 s1 s2 =>
+      congr_If (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0)
+        (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1) (extRen_Tm xi_Tm zeta_Tm Eq_Tm s2)
   end.
 
 Lemma upExt_Tm_Tm {m : nat} {n_Tm : nat} (sigma : fin m -> Tm n_Tm)
@@ -274,6 +317,11 @@ Fixpoint ext_Tm {m_Tm : nat} {n_Tm : nat} (sigma_Tm : fin m_Tm -> Tm n_Tm)
            s2)
   | Bot _ => congr_Bot
   | Univ _ s0 => congr_Univ (eq_refl s0)
+  | Bool _ => congr_Bool
+  | BVal _ s0 => congr_BVal (eq_refl s0)
+  | If _ s0 s1 s2 =>
+      congr_If (ext_Tm sigma_Tm tau_Tm Eq_Tm s0)
+        (ext_Tm sigma_Tm tau_Tm Eq_Tm s1) (ext_Tm sigma_Tm tau_Tm Eq_Tm s2)
   end.
 
 Lemma up_ren_ren_Tm_Tm {k : nat} {l : nat} {m : nat} (xi : fin k -> fin l)
@@ -319,6 +367,12 @@ Fixpoint compRenRen_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
            (upRen_Tm_Tm rho_Tm) (up_ren_ren _ _ _ Eq_Tm) s2)
   | Bot _ => congr_Bot
   | Univ _ s0 => congr_Univ (eq_refl s0)
+  | Bool _ => congr_Bool
+  | BVal _ s0 => congr_BVal (eq_refl s0)
+  | If _ s0 s1 s2 =>
+      congr_If (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0)
+        (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1)
+        (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s2)
   end.
 
 Lemma up_ren_subst_Tm_Tm {k : nat} {l : nat} {m_Tm : nat}
@@ -375,6 +429,12 @@ Fixpoint compRenSubst_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
            (up_Tm_Tm theta_Tm) (up_ren_subst_Tm_Tm _ _ _ Eq_Tm) s2)
   | Bot _ => congr_Bot
   | Univ _ s0 => congr_Univ (eq_refl s0)
+  | Bool _ => congr_Bool
+  | BVal _ s0 => congr_BVal (eq_refl s0)
+  | If _ s0 s1 s2 =>
+      congr_If (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0)
+        (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s1)
+        (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s2)
   end.
 
 Lemma up_subst_ren_Tm_Tm {k : nat} {l_Tm : nat} {m_Tm : nat}
@@ -452,6 +512,12 @@ ren_Tm zeta_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s :=
            (up_Tm_Tm theta_Tm) (up_subst_ren_Tm_Tm _ _ _ Eq_Tm) s2)
   | Bot _ => congr_Bot
   | Univ _ s0 => congr_Univ (eq_refl s0)
+  | Bool _ => congr_Bool
+  | BVal _ s0 => congr_BVal (eq_refl s0)
+  | If _ s0 s1 s2 =>
+      congr_If (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0)
+        (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s1)
+        (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s2)
   end.
 
 Lemma up_subst_subst_Tm_Tm {k : nat} {l_Tm : nat} {m_Tm : nat}
@@ -530,6 +596,12 @@ subst_Tm tau_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s :=
            (up_Tm_Tm theta_Tm) (up_subst_subst_Tm_Tm _ _ _ Eq_Tm) s2)
   | Bot _ => congr_Bot
   | Univ _ s0 => congr_Univ (eq_refl s0)
+  | Bool _ => congr_Bool
+  | BVal _ s0 => congr_BVal (eq_refl s0)
+  | If _ s0 s1 s2 =>
+      congr_If (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0)
+        (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s1)
+        (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s2)
   end.
 
 Lemma renRen_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat}
@@ -646,6 +718,12 @@ Fixpoint rinst_inst_Tm {m_Tm : nat} {n_Tm : nat}
            (rinstInst_up_Tm_Tm _ _ Eq_Tm) s2)
   | Bot _ => congr_Bot
   | Univ _ s0 => congr_Univ (eq_refl s0)
+  | Bool _ => congr_Bool
+  | BVal _ s0 => congr_BVal (eq_refl s0)
+  | If _ s0 s1 s2 =>
+      congr_If (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0)
+        (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1)
+        (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s2)
   end.
 
 Lemma rinstInst'_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm)
@@ -844,6 +922,12 @@ Core.
 
 Arguments VarTm {n_Tm}.
 
+Arguments If {n_Tm}.
+
+Arguments BVal {n_Tm}.
+
+Arguments Bool {n_Tm}.
+
 Arguments Univ {n_Tm}.
 
 Arguments Bot {n_Tm}.
diff --git a/theories/fp_red.v b/theories/fp_red.v
index d2fbdf6..30b96ef 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -8,6 +8,9 @@ Require Import Psatz.
 From stdpp Require Import relations (rtc (..), rtc_once, rtc_r).
 From Hammer Require Import Tactics.
 Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax.
+Import Relation_Operators (clos_refl(..)).
+Arguments clos_refl {A}.
+
 
 Ltac2 spec_refl () :=
   List.iter
@@ -40,7 +43,21 @@ Module Par.
     R a0 a1 ->
     R b0 b1 ->
     R (Proj p (Pair a0 b0)) (if p is PL then a1 else b1)
-
+  | IfAbs (a0 a1 : Tm (S n)) b0 b1 c0 c1 :
+    R a0 a1 ->
+    R b0 b1 ->
+    R c0 c1 ->
+    R (If (Abs a0) b0 c0) (Abs (If a1 (ren_Tm shift b1) (ren_Tm shift c1)))
+  | IfPair a0 a1 b0 b1 c0 c1 d0 d1 :
+    R a0 a1 ->
+    R b0 b1 ->
+    R c0 c1 ->
+    R d0 d1 ->
+    R (If (Pair a0 b0) c0 d0) (Pair (If a1 c1 d1) (If b1 c1 d1))
+  | IfBool a b0 b1 c0 c1 :
+    R b0 b1 ->
+    R c0 c1 ->
+    R (If (BVal a) b0 c0) (if a then b1 else c1)
   (****************** Eta ***********************)
   | AppEta a0 a1 :
     R a0 a1 ->
@@ -73,7 +90,27 @@ Module Par.
   | BotCong :
     R Bot Bot
   | UnivCong i :
-    R (Univ i) (Univ i).
+    R (Univ i) (Univ i)
+  | BoolCong :
+    R Bool Bool
+  | BValCong b :
+    R (BVal b) (BVal b)
+  | IfCong a0 a1 b0 b1 c0 c1 :
+    R a0 a1 ->
+    R b0 b1 ->
+    R c0 c1 ->
+    R (If a0 b0 c0) (If a1 b1 c1)
+  | IfApp a0 a1 b0 b1 c0 c1 d0 d1 :
+    R a0 a1 ->
+    R b0 b1 ->
+    R c0 c1 ->
+    R d0 d1 ->
+    R (If (App a0 b0) c0 d0) (App (If a1 c1 d1) b1)
+  | IfProj p a0 a1 b0 b1 c0 c1 :
+    R a0 a1 ->
+    R b0 b1 ->
+    R c0 c1 ->
+    R (If (Proj p a0) b0 c0) (Proj p (If a1 b1 c1)).
 
   Lemma refl n (a : Tm n) : R a a.
     elim : n /a; hauto ctrs:R.
@@ -93,12 +130,27 @@ Module Par.
     R (Proj p (Pair a0 b0)) t.
   Proof.  move => > ->. apply ProjPair. Qed.
 
+  Lemma IfBool' n a b0 b1 c0 c1 u :
+    u = (if a then (b1 : Tm n) else c1) ->
+    R b0 b1 ->
+    R c0 c1 ->
+    R (If (BVal a) b0 c0) u.
+  Proof. move => ->. apply IfBool. Qed.
+
   Lemma AppEta' n (a0 a1 b : Tm n) :
     b = (Abs (App (ren_Tm shift a1) (VarTm var_zero))) ->
     R a0 a1 ->
     R a0 b.
   Proof. move => ->; apply AppEta. Qed.
 
+  Lemma IfAbs' n (a0 a1  : Tm (S n)) (b0 b1 c0 c1 : Tm n)  u :
+    u = (Abs (If a1 (ren_Tm shift b1) (ren_Tm shift c1))) ->
+    @R (S n) a0 a1 ->
+    R b0 b1 ->
+    R c0 c1 ->
+    R (If (Abs a0) b0 c0) u.
+  Proof. move => ->. apply IfAbs. Qed.
+
   Lemma renaming n m (a b : Tm n) (ξ : fin n -> fin m) :
     R a b -> R (ren_Tm ξ a) (ren_Tm ξ b).
   Proof.
@@ -107,11 +159,11 @@ Module Par.
     move => *; apply : AppAbs'; eauto; by asimpl.
     all : match goal with
           | [ |- context[var_zero]] => move => *; apply : AppEta'; eauto; by asimpl
-          | _ => qauto ctrs:R use:ProjPair'
+          | [ |- context[ren_Tm]] => move => * /=; apply : IfAbs'; eauto; by asimpl
+          | _ => qauto ctrs:R use:ProjPair', IfBool'
           end.
   Qed.
 
-
   Lemma morphing n m (a b : Tm n) (ρ0 ρ1 : fin n -> Tm m) :
     (forall i, R (ρ0 i) (ρ1 i)) ->
     R a b -> R (subst_Tm ρ0 a) (subst_Tm ρ1 b).
@@ -124,6 +176,11 @@ Module Par.
     - hauto lq:on rew:off ctrs:R.
     - hauto l:on inv:option use:renaming ctrs:R.
     - hauto lq:on use:ProjPair'.
+    - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ρ0 ρ1 hρ /=.
+      eapply IfAbs' with (a1 := (subst_Tm (up_Tm_Tm ρ1) a1)); eauto. by asimpl.
+      hauto l:on use:renaming inv:option.
+    - qauto l:on ctrs:R.
+    - hauto q:on use:IfBool'.
     - move => n a0 a1 ha iha m ρ0 ρ1 hρ /=.
       apply : AppEta'; eauto. by asimpl.
     - hauto lq:on ctrs:R.
@@ -135,6 +192,11 @@ Module Par.
     - hauto l:on inv:option ctrs:R use:renaming.
     - sfirstorder.
     - sfirstorder.
+    - sfirstorder.
+    - sfirstorder.
+    - hauto lq:on ctrs:R.
+    - hauto lq:on ctrs:R.
+    - qauto l:on ctrs:R.
   Qed.
 
   Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) :
@@ -174,6 +236,26 @@ Module Par.
       move : ihb => [c0 [? ?]]. subst.
       eexists. split. by eauto using ProjPair.
       hauto q:on.
+    - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ξ []//= t t0 t1 [h *]. subst.
+      case : t h => // t [*]. subst.
+      spec_refl.
+      move : iha => [a2 [iha ?]]. subst.
+      move : ihb => [b2 [ihb ?]]. subst.
+      move : ihc => [c2 [ihc ?]]. subst.
+      exists (Abs (If a2 (ren_Tm shift b2) (ren_Tm shift c2))).
+      split; last by asimpl.
+      hauto lq:on ctrs:R.
+    - move => n a0 a1 b0 b1 c0 c1 d0 d1 ha iha hb ihb hc ihc hd ihd m ξ []//=.
+      move => a2 b2 c2 [h *]. subst.
+      case : a2 h => //= a3 b3 [*]. subst.
+      spec_refl.
+      hauto lq:on ctrs:R.
+    - move => n a b0 b1 c0 c1 hb ihb hc ihc m ξ []//= p0 p1 p2 [h *]. subst.
+      spec_refl.
+      move : ihb => [b0 [? ?]].
+      move : ihc => [c0 [? ?]]. subst.
+      case : p0 h => //=.
+      hauto q:on use:IfBool'.
     - move => n a0 a1 ha iha m ξ a ?. subst.
       spec_refl. move : iha => [a0 [? ?]]. subst.
       eexists. split. apply AppEta; eauto.
@@ -214,6 +296,16 @@ Module Par.
       by asimpl.
     - move => n n0 ξ []//=. hauto l:on.
     - move => n i n0 ξ []//=. hauto l:on.
+    - move => n m ξ []//=. hauto l:on.
+    - move => n b m ξ []//=. hauto l:on.
+    - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ξ []//= t t0 t1[*]. subst.
+      spec_refl.
+      qauto l:on ctrs:R.
+    - move => n a0 a1 b0 b1 c0 c1 d0 d1 ha iha hb ihb hc ihc hd ihd m ξ []//= t0 t1 t2 [h *]. subst.
+      case : t0 h => //= t t0 [*]. subst.
+      qauto l:on ctrs:R.
+    - move => n p a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ξ []//= t0 t1 t [h *]. subst.
+      case : t0 h => //=. qauto l:on ctrs:R.
   Qed.
 
 End Par.
@@ -282,6 +374,127 @@ Definition var_or_bot {n} (a : Tm n) :=
   | _ => false
   end.
 
+(* *********** Commutativity rules only ********************** *)
+Module CRed.
+  Inductive R {n} : Tm n -> Tm n ->  Prop :=
+  (****************** Eta ***********************)
+  | IfApp a0 a1 b0 b1 c0 c1 d0 d1 :
+    R a0 a1 ->
+    R b0 b1 ->
+    R c0 c1 ->
+    R d0 d1 ->
+    R (If (App a0 b0) c0 d0) (App (If a1 c1 d1) b1)
+  | IfProj p a0 a1 b0 b1 c0 c1 :
+    R a0 a1 ->
+    R b0 b1 ->
+    R c0 c1 ->
+    R (If (Proj p a0) b0 c0) (Proj p (If a1 b1 c1))
+  (*************** Congruence ********************)
+  | Var i : R (VarTm i) (VarTm i)
+  | AbsCong a0 a1 :
+    R a0 a1 ->
+    R (Abs a0) (Abs a1)
+  | AppCong a0 a1 b0 b1 :
+    R a0 a1 ->
+    R b0 b1 ->
+    R (App a0 b0) (App a1 b1)
+  | PairCong a0 a1 b0 b1 :
+    R a0 a1 ->
+    R b0 b1 ->
+    R (Pair a0 b0) (Pair a1 b1)
+  | ProjCong p a0 a1 :
+    R a0 a1 ->
+    R (Proj p a0) (Proj p a1)
+  | BindCong p A0 A1 B0 B1:
+    R A0 A1 ->
+    R B0 B1 ->
+    R (TBind p A0 B0) (TBind p A1 B1)
+  | BotCong :
+    R Bot Bot
+  | UnivCong i :
+    R (Univ i) (Univ i)
+  | BoolCong :
+    R Bool Bool
+  | BValCong b :
+    R (BVal b) (BVal b)
+  | IfCong a0 a1 b0 b1 c0 c1 :
+    R a0 a1 ->
+    R b0 b1 ->
+    R c0 c1 ->
+    R (If a0 b0 c0) (If a1 b1 c1).
+
+  Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop.
+
+  Lemma refl n (a : Tm n) : R a a.
+  Proof. elim : n / a; hauto lq:on ctrs:R. 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; hauto lq:on ctrs:R.
+  Qed.
+
+  Lemma morphing n m (a b : Tm n) (ρ0 ρ1 : fin n -> Tm m) :
+    (forall i, R (ρ0 i) (ρ1 i)) ->
+    R a b -> R (subst_Tm ρ0 a) (subst_Tm ρ1 b).
+  Proof.
+    move => + h. move : m ρ0 ρ1. elim : a b /h; hauto l:on ctrs:R inv:option use:renaming.
+  Qed.
+
+  Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) :
+    R a b ->
+    R (subst_Tm ρ a) (subst_Tm ρ b).
+  Proof. hauto l:on use:morphing, refl. Qed.
+
+  Lemma cong n (a b : Tm (S n)) c d :
+    R a b ->
+    R c d ->
+    R (subst_Tm (scons c VarTm) a) (subst_Tm (scons d VarTm) b).
+  Proof.
+    move => h0 h1. apply morphing => //=.
+    qauto l:on ctrs:R inv:option.
+  Qed.
+
+  Function tstar {n} (a : Tm n) :=
+    match a with
+    | VarTm i => a
+    | Abs a => Abs (tstar a)
+    | App a b => App (tstar a) (tstar b)
+    | Pair a b => Pair (tstar a) (tstar b)
+    | Proj p a => Proj p (tstar a)
+    | TBind p a b => TBind p (tstar a) (tstar b)
+    | Bot => Bot
+    | Univ i => Univ i
+    | Bool => Bool
+    | If (Proj p a) b c => Proj p (If (tstar a) (tstar b) (tstar c))
+    | If (App a d) b c => App (If (tstar a) (tstar b) (tstar c)) (tstar d)
+    | If a b c => If (tstar a) (tstar b) (tstar c)
+    | BVal v => BVal v
+    end.
+
+  Lemma triangle n (a : Tm n) : forall b, R a b -> R b (tstar a).
+  Proof.
+    apply tstar_ind => {n a}.
+    - hauto lq:on inv:R ctrs:R.
+    - hauto lq:on inv:R ctrs:R.
+    - hauto lq:on rew:off ctrs:R inv:R.
+    - hauto lq:on rew:off inv:R ctrs:R.
+    - hauto lq:on rew:off inv:R ctrs:R.
+    - hauto lq:on inv:R ctrs:R.
+    - hauto lq:on inv:R ctrs:R.
+    - hauto lq:on inv:R ctrs:R.
+    - hauto lq:on inv:R ctrs:R.
+    - hauto lq:on inv:R ctrs:R.
+    - hauto lq:on ctrs:R inv:R.
+    - hauto lq:on drew:off ctrs:R inv:R.
+    - hauto lq:on drew:off ctrs:R inv:R.
+  Qed.
+
+  Lemma diamond n (a b c : Tm n) : R a b -> R a c -> exists d, R b d /\ R c d.
+  Proof. sfirstorder use:triangle. Qed.
+End CRed.
+
 (***************** Beta rules only ***********************)
 Module RPar.
   Inductive R {n} : Tm n -> Tm n ->  Prop :=
@@ -302,6 +515,21 @@ Module RPar.
     R a0 a1 ->
     R b0 b1 ->
     R (Proj p (Pair a0 b0)) (if p is PL then a1 else b1)
+  | IfAbs (a0 a1 : Tm (S n)) b0 b1 c0 c1 :
+    R a0 a1 ->
+    R b0 b1 ->
+    R c0 c1 ->
+    R (If (Abs a0) b0 c0) (Abs (If a1 (ren_Tm shift b1) (ren_Tm shift c1)))
+  | IfPair a0 a1 b0 b1 c0 c1 d0 d1 :
+    R a0 a1 ->
+    R b0 b1 ->
+    R c0 c1 ->
+    R d0 d1 ->
+    R (If (Pair a0 b0) c0 d0) (Pair (If a1 c1 d1) (If b1 c1 d1))
+  | IfBool a b0 b1 c0 c1 :
+    R b0 b1 ->
+    R c0 c1 ->
+    R (If (BVal a) b0 c0) (if a then b1 else c1)
 
 
   (*************** Congruence ********************)
@@ -327,7 +555,16 @@ Module RPar.
   | BotCong :
     R Bot Bot
   | UnivCong i :
-    R (Univ i) (Univ i).
+    R (Univ i) (Univ i)
+  | BoolCong :
+    R Bool Bool
+  | BValCong b :
+    R (BVal b) (BVal b)
+  | IfCong a0 a1 b0 b1 c0 c1 :
+    R a0 a1 ->
+    R b0 b1 ->
+    R c0 c1 ->
+    R (If a0 b0 c0) (If a1 b1 c1).
 
   Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop.
 
@@ -350,13 +587,28 @@ Module RPar.
     R (Proj p (Pair a0 b0)) t.
   Proof.  move => > ->. apply ProjPair. Qed.
 
+  Lemma IfBool' n a b0 b1 c0 c1 u :
+    u = (if a then (b1 : Tm n) else c1) ->
+    R b0 b1 ->
+    R c0 c1 ->
+    R (If (BVal a) b0 c0) u.
+  Proof. move => ->. apply IfBool. Qed.
+
+
+  Lemma IfAbs' n (a0 a1  : Tm (S n)) (b0 b1 c0 c1 : Tm n)  u :
+    u = (Abs (If a1 (ren_Tm shift b1) (ren_Tm shift c1))) ->
+    @R (S n) a0 a1 ->
+    R b0 b1 ->
+    R c0 c1 ->
+    R (If (Abs a0) b0 c0) u.
+  Proof. move => ->. apply IfAbs. 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 use:ProjPair'.
+    elim : n a b /h; try solve [(move => *; apply : AppAbs'; eauto; by asimpl) | (move => *; apply : IfAbs'; eauto; by asimpl)].
+    all : try qauto ctrs:R use:ProjPair', IfBool'.
   Qed.
 
   Lemma morphing_ren n m p (ρ0 ρ1 : fin n -> Tm m) (ξ : fin m -> fin p) :
@@ -387,6 +639,11 @@ Module RPar.
     - hauto lq:on ctrs:R.
     - hauto lq:on ctrs:R use:morphing_up.
     - hauto lq:on ctrs:R use:ProjPair' use:morphing_up.
+    - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ρ0 ρ1 hρ /=.
+      apply : IfAbs'; eauto using morphing_up.
+      by asimpl.
+    - hauto lq:on ctrs:R.
+    - hauto lq:on ctrs:R use:IfBool' 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.
@@ -395,6 +652,9 @@ Module RPar.
     - 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.
+    - hauto lq:on ctrs:R.
   Qed.
 
   Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) :
@@ -415,7 +675,7 @@ Module RPar.
     var_or_bot a ->
     a = b -> ~~ var_or_bot b -> False.
   Proof.
-    hauto lq:on inv:Tm.
+    hauto l:on inv:Tm.
   Qed.
 
   Lemma var_or_bot_up n m (ρ : fin n -> Tm m) :
@@ -485,231 +745,36 @@ Module RPar.
       move : ihb => [c0 [? ?]]. subst.
       eexists. split. by eauto using ProjPair.
       hauto q:on.
-    - move => n i m ρ hρ []//=.
-      hauto l:on.
-    - move => n a0 a1 ha iha m ρ hρ []//=; first by antiimp.
-      move => t [*]. subst.
-      have /var_or_bot_up {}/iha := hρ => iha.
-      spec_refl.
-      move  :iha => [b0 [? ?]]. subst.
-      eexists. split. by apply AbsCong; eauto.
-      by asimpl.
-    - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=;
-               first by antiimp.
-      move => t t0 [*]. subst.
-      have {}/iha := (hρ) => iha.
-      have {}/ihb := (hρ) => ihb.
-      spec_refl.
-      move : iha => [b0 [? ?]]. subst.
-      move : ihb => [c0 [? ?]]. subst.
-      eexists. split. by apply AppCong; eauto.
-      done.
-    - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=;
-               first by antiimp.
-      move => t t0[*]. subst.
-      have {}/iha := (hρ) => iha.
-      have {}/ihb := (hρ) => ihb.
-      spec_refl.
-      move : iha => [b0 [? ?]]. subst.
-      move : ihb => [c0 [? ?]]. subst.
-      eexists. split. by apply PairCong; eauto.
-      by asimpl.
-    - move => n p a0 a1 ha iha m ρ hρ []//=;
-               first by antiimp.
-      move => p0 t [*]. subst.
-      have {}/iha := (hρ) => iha.
-      spec_refl.
-      move : iha => [b0 [? ?]]. subst.
-      eexists. split. apply ProjCong; eauto. reflexivity.
-    - move => n p A0 A1 B0 B1 ha iha hB ihB m ρ hρ []//=;
-               first by antiimp.
-      move => ? t t0 [*]. subst.
-      have {}/iha := (hρ) => iha.
-      have /var_or_bot_up {}/ihB := (hρ) => ihB.
-      spec_refl.
-      move : iha => [b0 [? ?]].
-      move : ihB => [c0 [? ?]]. subst.
-      eexists. split. by apply BindCong; eauto.
-      by asimpl.
-    - hauto q:on ctrs:R inv:Tm.
-    - move => n i n0 ρ hρ []//=; first by antiimp.
-      hauto l:on.
-  Qed.
-End RPar.
-
-(***************** Beta rules only ***********************)
-Module RPar'.
-  Inductive R {n} : Tm n -> Tm n ->  Prop :=
-  (***************** Beta ***********************)
-  | AppAbs a0 a1 b0 b1 :
-    R a0 a1 ->
-    R b0 b1 ->
-    R (App (Abs a0) b0)  (subst_Tm (scons b1 VarTm) a1)
-  | ProjPair p a0 a1 b0 b1 :
-    R 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)
-  | AbsCong a0 a1 :
-    R a0 a1 ->
-    R (Abs a0) (Abs a1)
-  | AppCong a0 a1 b0 b1 :
-    R a0 a1 ->
-    R b0 b1 ->
-    R (App a0 b0) (App a1 b1)
-  | PairCong a0 a1 b0 b1 :
-    R a0 a1 ->
-    R b0 b1 ->
-    R (Pair a0 b0) (Pair a1 b1)
-  | ProjCong p a0 a1 :
-    R a0 a1 ->
-    R (Proj p a0) (Proj p a1)
-  | BindCong p A0 A1 B0 B1:
-    R A0 A1 ->
-    R B0 B1 ->
-    R (TBind p A0 B0) (TBind p A1 B1)
-  | BotCong :
-    R Bot Bot
-  | UnivCong i :
-    R (Univ i) (Univ i).
-
-  Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop.
-
-  Lemma refl n (a : Tm n) : R a a.
-  Proof.
-    induction a; hauto lq:on ctrs:R.
-  Qed.
-
-  Lemma AppAbs' n a0 a1 (b0 b1 t : Tm n) :
-    t = subst_Tm (scons b1 VarTm) a1 ->
-    R a0 a1 ->
-    R b0 b1 ->
-    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 use:ProjPair'.
-  Qed.
-
-  Lemma morphing_ren n m p (ρ0 ρ1 : fin n -> Tm m) (ξ : fin m -> fin p) :
-    (forall i, R (ρ0 i) (ρ1 i)) ->
-    (forall i, R ((funcomp (ren_Tm ξ) ρ0) i) ((funcomp (ren_Tm ξ) ρ1) i)).
-  Proof. eauto using renaming. Qed.
-
-  Lemma morphing_ext n m (ρ0 ρ1 : fin n -> Tm m) a b  :
-    R a b ->
-    (forall i, R (ρ0 i) (ρ1 i)) ->
-    (forall i, R ((scons a ρ0) i) ((scons b ρ1) i)).
-  Proof. hauto q:on inv:option. Qed.
-
-  Lemma morphing_up n m (ρ0 ρ1 : fin n -> Tm m) :
-    (forall i, R (ρ0 i) (ρ1 i)) ->
-    (forall i, R (up_Tm_Tm ρ0 i) (up_Tm_Tm ρ1 i)).
-  Proof. hauto l:on ctrs:R use:morphing_ext, morphing_ren unfold:up_Tm_Tm. Qed.
-
-  Lemma morphing n m (a b : Tm n) (ρ0 ρ1 : fin n -> Tm m) :
-    (forall i, R (ρ0 i) (ρ1 i)) ->
-    R a b -> R (subst_Tm ρ0 a) (subst_Tm ρ1 b).
-  Proof.
-    move => + h. move : m ρ0 ρ1.
-    elim : n a b /h.
-    - move => *.
-      apply : AppAbs'; eauto using morphing_up.
-      by asimpl.
-    - 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.
-    - hauto lq:on ctrs:R.
-    - hauto lq:on ctrs:R.
-    - hauto lq:on ctrs:R use:morphing_up.
-    - hauto lq:on ctrs:R.
-    - hauto lq:on ctrs:R.
-  Qed.
-
-  Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) :
-    R a b ->
-    R (subst_Tm ρ a) (subst_Tm ρ b).
-  Proof. hauto l:on use:morphing, refl. Qed.
-
-  Lemma cong n (a b : Tm (S n)) c d :
-    R a b ->
-    R c d ->
-    R (subst_Tm (scons c VarTm) a) (subst_Tm (scons d VarTm) b).
-  Proof.
-    move => h0 h1. apply morphing => //=.
-    qauto l:on ctrs:R inv:option.
-  Qed.
-
-  Lemma var_or_bot_imp {n} (a b : Tm n) :
-    var_or_bot a ->
-    a = b -> ~~ var_or_bot b -> False.
-  Proof.
-    hauto lq:on inv:Tm.
-  Qed.
-
-  Lemma var_or_bot_up n m (ρ : fin n -> Tm m) :
-    (forall i, var_or_bot (ρ i)) ->
-    (forall i, var_or_bot (up_Tm_Tm ρ i)).
-  Proof.
-    move => h /= [i|].
-    - asimpl.
-      move /(_ i) in h.
-      rewrite /funcomp.
-      move : (ρ i) h.
-      case => //=.
-    - sfirstorder.
-  Qed.
-
-  Local Ltac antiimp := qauto l:on use:var_or_bot_imp.
-
-  Lemma antirenaming n m (a : Tm n) (b : Tm m) (ρ : fin n -> Tm m) :
-    (forall i, var_or_bot (ρ i)) ->
-    R (subst_Tm ρ a) b -> exists b0, R a b0 /\ subst_Tm ρ b0 = b.
-  Proof.
-    move E : (subst_Tm ρ a) => u hρ h.
-    move : n ρ hρ a E. elim : m u b/h.
-    - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=;
-               first by antiimp.
-      move => c c0 [+ ?]. subst.
-      case : c => //=; first by antiimp.
-      move => c [?]. subst.
-      spec_refl.
+    - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ρ hρ []//=; first by antiimp.
+      move => + b2 c2 [+ *]. subst. case => //=; first by antiimp.
+      move => a [*]. subst.
       have /var_or_bot_up hρ' := hρ.
       move : iha hρ' => /[apply] iha.
-      move : ihb hρ => /[apply] ihb.
+      move : ihb (hρ) => /[apply] ihb.
+      move : ihc hρ => /[apply] ihc.
       spec_refl.
-      move : iha => [c1][ih0]?. subst.
-      move : ihb => [c2][ih1]?. subst.
-      eexists. split.
-      apply AppAbs; eauto.
+      move : iha => [a0 [ha0 ?]]. subst.
+      move : ihb => [b0 [hb0 ?]]. subst.
+      move : ihc => [c0 [hc0 ?]]. subst.
+      exists (Abs (If a0 (ren_Tm shift b0) (ren_Tm shift c0))). split.
+      hauto lq:on ctrs:R.
       by asimpl.
-    - move => n p a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=;
-               first by antiimp.
-      move => p0 []//=; first by antiimp. move => t t0[*].
-      subst.
+    - move => n a0 a1 b0 b1 c0 c1 d0 d1 ha iha hb ihb hc ihc hd ihd m ρ hρ []//=; first by antiimp.
+      move => a2 b2 c2 [+ *]. subst. case : a2 => //=; first by antiimp.
+      move => a3 b3 [*]. subst.
       have {}/iha := (hρ) => iha.
       have {}/ihb := (hρ) => ihb.
+      have {}/ihc := (hρ) => ihc.
       spec_refl.
-      move : iha => [b0 [? ?]].
-      move : ihb => [c0 [? ?]]. subst.
-      eexists. split. by eauto using ProjPair.
-      hauto q:on.
+      hauto lq:on ctrs:R.
+    - move => n a b0 b1 c0 c1 hb ihb hc ihc m ρ hρ []//=; first by antiimp.
+      move => t t0 t1 [h *]. subst.
+      case : t h => //=; first by antiimp.
+      move => b [*]. subst.
+      have {}/ihb := (hρ) => ihb.
+      have {}/ihc := (hρ) => ihc.
+      spec_refl.
+      hauto q:on use:IfBool.
     - move => n i m ρ hρ []//=.
       hauto l:on.
     - move => n a0 a1 ha iha m ρ hρ []//=; first by antiimp.
@@ -759,16 +824,87 @@ Module RPar'.
     - hauto q:on ctrs:R inv:Tm.
     - move => n i n0 ρ hρ []//=; first by antiimp.
       hauto l:on.
+    - move => n m ρ hρ []//=; first by antiimp.
+      hauto lq:on ctrs:R.
+    - move => n b m ρ hρ []//; first by antiimp.
+      hauto lq:on ctrs:R.
+    - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ρ hρ []//=; first by antiimp.
+      move => t t0 t1 [*]. subst.
+      have {}/iha := (hρ) => iha.
+      have {}/ihb := (hρ) => ihb.
+      have {}/ihc := (hρ) => ihc.
+      spec_refl.
+      hauto lq:on ctrs:R.
   Qed.
-End RPar'.
 
-Module ERed.
+  Function tstar {n} (a : Tm n) :=
+    match a with
+    | VarTm i => a
+    | Abs a => Abs (tstar a)
+    | App (Abs a) b => subst_Tm (scons (tstar b) VarTm) (tstar a)
+    | App (Pair a b) c =>
+        Pair (App (tstar a) (tstar c)) (App (tstar b) (tstar c))
+    | App a b => App (tstar a) (tstar b)
+    | Pair a b => Pair (tstar a) (tstar b)
+    | Proj p (Pair a b) => if p is PL then (tstar a) else (tstar b)
+    | Proj p (Abs a) => (Abs (Proj p (tstar a)))
+    | Proj p a => Proj p (tstar a)
+    | TBind p a b => TBind p (tstar a) (tstar b)
+    | Bot => Bot
+    | Univ i => Univ i
+    | Bool => Bool
+    | If (BVal v) b c => if v then (tstar b) else (tstar c)
+    | If (Abs a) b c => Abs (If (tstar a) (ren_Tm shift (tstar b)) (ren_Tm shift (tstar c)))
+    | If (Pair a0 a1) b c => Pair (If (tstar a0) (tstar b) (tstar c)) (If (tstar a1) (tstar b) (tstar c))
+    | If a b c => If (tstar a) (tstar b) (tstar c)
+    | BVal v => BVal v
+    end.
+
+  Lemma RPar_triangle n (a : Tm n) : forall b, RPar.R a b -> RPar.R b (tstar a).
+  Proof.
+    apply tstar_ind => {n a}.
+    - hauto lq:on inv:RPar.R ctrs:RPar.R.
+    - hauto lq:on inv:RPar.R ctrs:RPar.R.
+    - hauto lq:on use:RPar.cong, RPar.refl ctrs:RPar.R inv:RPar.R.
+    - hauto lq:on rew:off ctrs:RPar.R inv:RPar.R.
+    - hauto lq:on rew:off inv:RPar.R ctrs:RPar.R.
+    - hauto lq:on rew:off inv:RPar.R ctrs:RPar.R.
+    - hauto drew:off inv:RPar.R use:RPar.refl, RPar.ProjPair'.
+    - hauto drew:off inv:RPar.R use:RPar.refl, RPar.ProjPair'.
+    - hauto lq:on inv:RPar.R ctrs:RPar.R.
+    - hauto lq:on inv:RPar.R ctrs:RPar.R.
+    - hauto lq:on inv:RPar.R ctrs:RPar.R.
+    - hauto lq:on inv:RPar.R ctrs:RPar.R.
+    - hauto lq:on inv:RPar.R ctrs:RPar.R.
+    - hauto lq:on ctrs:R inv:R.
+    - qauto l:on use:refl, IfBool' inv:R.
+    - hauto drew:off use:refl, IfBool' inv:R.
+    - hauto lq:on ctrs:RPar.R inv:RPar.R use:renaming.
+    - hauto lq:on drew:off ctrs:R inv:R.
+    - hauto lq:on drew:off ctrs:R inv:R.
+    - hauto lq:on drew:off ctrs:R inv:R.
+  Qed.
+
+End RPar.
+
+
+Module RRed.
   Inductive R {n} : Tm n -> Tm n ->  Prop :=
-  (****************** Eta ***********************)
-  | AppEta a :
-    R a (Abs (App (ren_Tm shift a) (VarTm var_zero)))
-  | PairEta a :
-    R a (Pair (Proj PL a) (Proj PR a))
+  (****************** Beta ***********************)
+  | AppAbs a b :
+    R (App (Abs a) b)  (subst_Tm (scons b VarTm) a)
+  | AppPair a b c:
+    R (App (Pair a b) c) (Pair (App a c) (App b c))
+  | ProjAbs p a :
+    R (Proj p (Abs a)) (Abs (Proj p a))
+  | ProjPair p a b :
+    R (Proj p (Pair a b)) (if p is PL then a else b)
+  | IfAbs (a : Tm (S n)) b c :
+    R (If (Abs a) b c) (Abs (If a (ren_Tm shift b) (ren_Tm shift c)))
+  | IfPair a b c d :
+    R (If (Pair a b) c d) (Pair (If a c d) (If b c d))
+  | IfBool a b c :
+    R (If (BVal a) b c) (if a then b else c)
 
   (*************** Congruence ********************)
   | AbsCong a0 a1 :
@@ -798,71 +934,626 @@ Module ERed.
 
   Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop.
 
-  Lemma AppEta' n a (u : Tm n) :
-    u = (Abs (App (ren_Tm shift a) (VarTm var_zero))) ->
-    R a u.
-  Proof. move => ->. apply AppEta. Qed.
+End RRed.
 
-  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 => n a m ξ.
-    apply AppEta'. by asimpl.
-    all : qauto ctrs:R.
-  Qed.
-
-  Lemma substing n m (a : Tm n) b (ρ : fin n -> Tm m) :
-    R a b ->
-    R (subst_Tm ρ a) (subst_Tm ρ b).
-  Proof.
-    move => h. move : m ρ. elim : n a b / h => n.
-    move => a m ρ /=.
-    apply : AppEta'; eauto. by asimpl.
-    all : hauto ctrs:R inv:option use:renaming.
-  Qed.
-
-End ERed.
-
-Module EReds.
+Module RReds.
 
   #[local]Ltac solve_s_rec :=
   move => *; eapply rtc_l; eauto;
-         hauto lq:on ctrs:ERed.R.
+         hauto lq:on ctrs:RRed.R.
 
   #[local]Ltac solve_s :=
     repeat (induction 1; last by solve_s_rec); apply rtc_refl.
 
   Lemma AbsCong n (a b : Tm (S n)) :
-    rtc ERed.R a b ->
-    rtc ERed.R (Abs a) (Abs b).
+    rtc RRed.R a b ->
+    rtc RRed.R (Abs a) (Abs b).
   Proof. solve_s. Qed.
 
   Lemma AppCong n (a0 a1 b0 b1 : Tm n) :
-    rtc ERed.R a0 a1 ->
-    rtc ERed.R b0 b1 ->
-    rtc ERed.R (App a0 b0) (App a1 b1).
+    rtc RRed.R a0 a1 ->
+    rtc RRed.R b0 b1 ->
+    rtc RRed.R (App a0 b0) (App a1 b1).
   Proof. solve_s. Qed.
 
   Lemma BindCong n p (a0 a1 : Tm n) b0 b1 :
-    rtc ERed.R a0 a1 ->
-    rtc ERed.R b0 b1 ->
-    rtc ERed.R (TBind p a0 b0) (TBind p a1 b1).
+    rtc RRed.R a0 a1 ->
+    rtc RRed.R b0 b1 ->
+    rtc RRed.R (TBind p a0 b0) (TBind p a1 b1).
   Proof. solve_s. Qed.
 
   Lemma PairCong n (a0 a1 b0 b1 : Tm n) :
-    rtc ERed.R a0 a1 ->
-    rtc ERed.R b0 b1 ->
-    rtc ERed.R (Pair a0 b0) (Pair a1 b1).
+    rtc RRed.R a0 a1 ->
+    rtc RRed.R b0 b1 ->
+    rtc RRed.R (Pair a0 b0) (Pair a1 b1).
   Proof. solve_s. Qed.
 
   Lemma ProjCong n p (a0 a1  : Tm n) :
-    rtc ERed.R a0 a1 ->
-    rtc ERed.R (Proj p a0) (Proj p a1).
+    rtc RRed.R a0 a1 ->
+    rtc RRed.R (Proj p a0) (Proj p a1).
   Proof. solve_s. Qed.
-End EReds.
+End RReds.
+
+
+Module CRedRRed.
+  Lemma commutativity0 n (a b0 b1 : Tm n) :
+    CRed.R a b0 -> RRed.R a b1 -> exists c, rtc RRed.R b0 c /\ CRed.R b1 c.
+  Proof.
+    move => h. move : b1. elim : n a b0/h => n.
+    - hauto lq:on inv:RRed.R.
+    - hauto q:on inv:RRed.R.
+    - hauto q:on inv:RRed.R.
+    - move => a0 a1 ha iha b.
+      elim /RRed.inv => //=_ a2 a3 h [*]. subst.
+      move /iha : h => [a [h0 h1]].
+      exists (Abs a). split. auto using RReds.AbsCong. hauto lq:on ctrs:CRed.R.
+    - move => a0 a1 b0 b1 ha iha hb ihb u.
+      elim /RRed.inv => //=_.
+      + move => a2 b2 [*]. subst.
+        elim /CRed.inv : ha => //= _ a0 a3 ha [*]. subst.
+        move {iha ihb}.
+        exists (subst_Tm (scons b1 VarTm) a3).
+        split. hauto lq:on ctrs:RRed.R use:@rtc_once.
+        hauto lq:on use:CRed.cong.
+      + sauto lq:on.
+      + move => a2 a3 b2 ha0 [*]. subst.
+        move /iha : ha0 => [a4 [h0 h1]].
+        exists (App a4 b1).
+        split. hauto lq:on ctrs:rtc use: RReds.AppCong.
+        sauto lq:on rew:off.
+      + move => a2 b2 b3 hb2 [*]. subst.
+        move /ihb : hb2 => [b4 [ih0 ih1]].
+        exists (App a1 b4).
+        split.
+        hauto lq:on ctrs:rtc use:RReds.AppCong.
+        hauto lq:on ctrs:CRed.R.
+    - move => a0 a1 b0 b1 ha iha hb ihb u.
+      elim /RRed.inv => //= _.
+      + move => a2 a3 b2 + [*]. subst.
+        move /iha => [a4 [ih0 ih1]].
+        exists (Pair a4 b1).
+        split. hauto lq:on ctrs:rtc use:RReds.PairCong.
+        sauto lq:on.
+      + move => a2 b2 b3 + [*]. subst.
+        move /ihb {ihb}.
+        move => [b4 [ih0 ih1]].
+        exists (Pair a1 b4). split. hauto lq:on ctrs:rtc use:RReds.PairCong.
+        sauto lq:on.
+    - move => p a0 a1 ha iha u.
+      elim /RRed.inv => //= _.
+      + sauto lq:on rew:off.
+      + sauto q:on.
+      + move => p0 a2 a3 ha2 [*]. subst.
+        move /iha : ha2 {iha} => [a4 [ih0 ih1]].
+        exists (Proj p a4).
+        split. sfirstorder ctrs:rtc use:RReds.ProjCong.
+        sauto lq:on.
+    - move => p A0 A1 B0 B1 hA ihA hB ihB u.
+      elim /RRed.inv => //=_.
+      + move => p0 A2 A3 B h [*]. subst.
+        apply ihA in h.
+        move : h => [A [h0 h1]].
+        exists (TBind p A B1).
+        split. hauto lq:on use:RReds.BindCong.
+        sauto lq:on.
+      + move => p0 A B2 B3 hB0 [*]. subst.
+        apply ihB in hB0.
+        move : hB0 => [B [ih0 ih1]].
+        exists (TBind p A1 B).
+        split. hauto ctrs:rtc lq:on use:RReds.BindCong.
+        sauto lq:on.
+    - sauto lq:on.
+    - sauto lq:on.
+    - sauto lq:on.
+    - sauto lq:on.
+    - move => a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc u.
+      elim /RRed.inv => //= _.
+      + move => a2 b2 c [*]. subst.
+        elim /CRed.inv : ha => //=_.
+        move => a0 a3 ha [*]. subst.
+        exists (Abs (If a3 (ren_Tm shift b1) (ren_Tm shift c1))).
+        split. sauto lq:on.
+        apply CRed.AbsCong.
+        apply CRed.IfCong; eauto using CRed.renaming.
+      + move => a2 b2 c d [*]. subst.
+        move {iha ihb ihc}.
+        elim /CRed.inv : ha => //=_.
+        move => a0 a3 b3 b4 h0 h1 [*]. subst.
+        exists (Pair (If a3 b1 c1) (If b4 b1 c1)).
+        split. sauto lq:on.
+        sauto lq:on.
+      + move {iha ihb ihc}.
+        move => a2 b2 c [*]. subst.
+        elim /CRed.inv : ha => //= _.
+        move => b2 [*]. subst.
+        sauto lq:on.
+  Qed.
+End CRedRRed.
+
+Module CRRed.
+  Inductive R {n} : Tm n -> Tm n ->  Prop :=
+  (****************** Beta ***********************)
+  | AppAbs a b :
+    R (App (Abs a) b)  (subst_Tm (scons b VarTm) a)
+  | AppPair a b c:
+    R (App (Pair a b) c) (Pair (App a c) (App b c))
+  | ProjAbs p a :
+    R (Proj p (Abs a)) (Abs (Proj p a))
+  | ProjPair p a b :
+    R (Proj p (Pair a b)) (if p is PL then a else b)
+  | IfAbs (a : Tm (S n)) b c :
+    R (If (Abs a) b c) (Abs (If a (ren_Tm shift b) (ren_Tm shift c)))
+  | IfPair a b c d :
+    R (If (Pair a b) c d) (Pair (If a c d) (If b c d))
+  | IfBool a b c :
+    R (If (BVal a) b c) (if a then b else c)
+  | IfApp a b c d :
+    R (If (App a b) c d) (App (If a c d) b)
+  | IfProj p a b c :
+    R (If (Proj p a) b c) (Proj p (If a b c))
+
+  (*************** Congruence ********************)
+  | AbsCong a0 a1 :
+    R a0 a1 ->
+    R (Abs a0) (Abs a1)
+  | AppCong0 a0 a1 b :
+    R a0 a1 ->
+    R (App a0 b) (App a1 b)
+  | AppCong1 a b0 b1 :
+    R b0 b1 ->
+    R (App a b0) (App a b1)
+  | PairCong0 a0 a1 b :
+    R a0 a1 ->
+    R (Pair a0 b) (Pair a1 b)
+  | PairCong1 a b0 b1 :
+    R b0 b1 ->
+    R (Pair a b0) (Pair a b1)
+  | ProjCong p a0 a1 :
+    R a0 a1 ->
+    R (Proj p a0) (Proj p a1)
+  | BindCong0 p A0 A1 B:
+    R A0 A1 ->
+    R (TBind p A0 B) (TBind p A1 B)
+  | BindCong1 p A B0 B1:
+    R B0 B1 ->
+    R (TBind p A B0) (TBind p A B1)
+  | IfCong0 a0 a1 b c :
+    R a0 a1 ->
+    R (If a0 b c) (If a1 b c)
+  | IfCong1 a b0 b1 c :
+    R b0 b1 ->
+    R (If a b0 c) (If a b1 c)
+  | IfCong2 a b c0 c1 :
+    R c0 c1 ->
+    R (If a b c0) (If a b c1).
+
+  Lemma AppAbs' n a (b t : Tm n) :
+    t = subst_Tm (scons b VarTm) a ->
+    R (App (Abs a) b) t.
+  Proof. move => ->. apply AppAbs. Qed.
+
+  Lemma IfAbs' n (a  : Tm (S n)) (b c : Tm n)  u :
+    u = (Abs (If a (ren_Tm shift b) (ren_Tm shift c))) ->
+    R (If (Abs a) b c) u.
+  Proof. move => ->. apply IfAbs. 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 => n;
+      lazymatch goal with
+      | [|- context[App (Abs _) _]] => move => * /=; apply AppAbs'; by asimpl
+      | [|- context[If (BVal _) _]] => hauto l:on use:IfBool
+      | [|- context[Proj _ (Pair _ _)]] => hauto l:on use:ProjPair
+      | [|- context[If (Abs _) _]] => move => * /=; apply IfAbs'; by asimpl
+      | _ => qauto ctrs:R
+      end.
+  Qed.
+
+  Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) :
+    R a b -> R (subst_Tm ρ a) (subst_Tm ρ b).
+  Proof.
+    move => h. move : m ρ.
+    elim : n a b /h => n /=;
+      lazymatch goal with
+      | [|- context[App (Abs _) _]] => move => * /=; apply AppAbs'; by asimpl
+      | [|- context[If (BVal _) _]] => hauto l:on use:IfBool
+      | [|- context[Proj _ (Pair _ _)]] => hauto l:on use:ProjPair
+      | [|- context[If (Abs _) _]] => move => * /=; apply IfAbs'; by asimpl
+      | _ => qauto ctrs:R
+      end.
+  Qed.
+
+  Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop.
+
+End CRRed.
+
+
+Module CRReds.
+
+  #[local]Ltac solve_s_rec :=
+  move => *; eapply rtc_l; eauto;
+         hauto lq:on ctrs:CRRed.R.
+
+  #[local]Ltac solve_s :=
+    repeat (induction 1; last by solve_s_rec); apply rtc_refl.
+
+  Lemma AbsCong n (a b : Tm (S n)) :
+    rtc CRRed.R a b ->
+    rtc CRRed.R (Abs a) (Abs b).
+  Proof. solve_s. Qed.
+
+  Lemma AppCong n (a0 a1 b0 b1 : Tm n) :
+    rtc CRRed.R a0 a1 ->
+    rtc CRRed.R b0 b1 ->
+    rtc CRRed.R (App a0 b0) (App a1 b1).
+  Proof. solve_s. Qed.
+
+  Lemma BindCong n p (a0 a1 : Tm n) b0 b1 :
+    rtc CRRed.R a0 a1 ->
+    rtc CRRed.R b0 b1 ->
+    rtc CRRed.R (TBind p a0 b0) (TBind p a1 b1).
+  Proof. solve_s. Qed.
+
+  Lemma PairCong n (a0 a1 b0 b1 : Tm n) :
+    rtc CRRed.R a0 a1 ->
+    rtc CRRed.R b0 b1 ->
+    rtc CRRed.R (Pair a0 b0) (Pair a1 b1).
+  Proof. solve_s. Qed.
+
+  Lemma ProjCong n p (a0 a1  : Tm n) :
+    rtc CRRed.R a0 a1 ->
+    rtc CRRed.R (Proj p a0) (Proj p a1).
+  Proof. solve_s. Qed.
+
+  Lemma IfCong n (a0 a1 b0 b1 c0 c1 : Tm n) :
+    rtc CRRed.R a0 a1 ->
+    rtc CRRed.R b0 b1 ->
+    rtc CRRed.R c0 c1 ->
+    rtc CRRed.R (If a0 b0 c0) (If a1 b1 c1).
+  Proof. solve_s. Qed.
+
+  Lemma renaming n m (a b : Tm n) (ξ : fin n -> fin m) :
+    rtc CRRed.R a b -> rtc CRRed.R (ren_Tm ξ a) (ren_Tm ξ b).
+  Proof.
+    move => h. move : m ξ.
+    induction h; hauto lq:on ctrs:rtc use:CRRed.renaming.
+  Qed.
+
+  Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) :
+    rtc CRRed.R a b -> rtc CRRed.R (subst_Tm ρ a) (subst_Tm ρ b).
+  Proof. induction 1; hauto lq:on ctrs:rtc use:CRRed.substing. Qed.
+
+End CRReds.
+
+
+(* (***************** Beta rules only ***********************) *)
+(* Module RPar'. *)
+(*   Inductive R {n} : Tm n -> Tm n ->  Prop := *)
+(*   (***************** Beta ***********************) *)
+(*   | AppAbs a0 a1 b0 b1 : *)
+(*     R a0 a1 -> *)
+(*     R b0 b1 -> *)
+(*     R (App (Abs a0) b0)  (subst_Tm (scons b1 VarTm) a1) *)
+(*   | ProjPair p a0 a1 b0 b1 : *)
+(*     R 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) *)
+(*   | AbsCong a0 a1 : *)
+(*     R a0 a1 -> *)
+(*     R (Abs a0) (Abs a1) *)
+(*   | AppCong a0 a1 b0 b1 : *)
+(*     R a0 a1 -> *)
+(*     R b0 b1 -> *)
+(*     R (App a0 b0) (App a1 b1) *)
+(*   | PairCong a0 a1 b0 b1 : *)
+(*     R a0 a1 -> *)
+(*     R b0 b1 -> *)
+(*     R (Pair a0 b0) (Pair a1 b1) *)
+(*   | ProjCong p a0 a1 : *)
+(*     R a0 a1 -> *)
+(*     R (Proj p a0) (Proj p a1) *)
+(*   | BindCong p A0 A1 B0 B1: *)
+(*     R A0 A1 -> *)
+(*     R B0 B1 -> *)
+(*     R (TBind p A0 B0) (TBind p A1 B1) *)
+(*   | BotCong : *)
+(*     R Bot Bot *)
+(*   | UnivCong i : *)
+(*     R (Univ i) (Univ i). *)
+
+(*   Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop. *)
+
+(*   Lemma refl n (a : Tm n) : R a a. *)
+(*   Proof. *)
+(*     induction a; hauto lq:on ctrs:R. *)
+(*   Qed. *)
+
+(*   Lemma AppAbs' n a0 a1 (b0 b1 t : Tm n) : *)
+(*     t = subst_Tm (scons b1 VarTm) a1 -> *)
+(*     R a0 a1 -> *)
+(*     R b0 b1 -> *)
+(*     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 use:ProjPair'. *)
+(*   Qed. *)
+
+(*   Lemma morphing_ren n m p (ρ0 ρ1 : fin n -> Tm m) (ξ : fin m -> fin p) : *)
+(*     (forall i, R (ρ0 i) (ρ1 i)) -> *)
+(*     (forall i, R ((funcomp (ren_Tm ξ) ρ0) i) ((funcomp (ren_Tm ξ) ρ1) i)). *)
+(*   Proof. eauto using renaming. Qed. *)
+
+(*   Lemma morphing_ext n m (ρ0 ρ1 : fin n -> Tm m) a b  : *)
+(*     R a b -> *)
+(*     (forall i, R (ρ0 i) (ρ1 i)) -> *)
+(*     (forall i, R ((scons a ρ0) i) ((scons b ρ1) i)). *)
+(*   Proof. hauto q:on inv:option. Qed. *)
+
+(*   Lemma morphing_up n m (ρ0 ρ1 : fin n -> Tm m) : *)
+(*     (forall i, R (ρ0 i) (ρ1 i)) -> *)
+(*     (forall i, R (up_Tm_Tm ρ0 i) (up_Tm_Tm ρ1 i)). *)
+(*   Proof. hauto l:on ctrs:R use:morphing_ext, morphing_ren unfold:up_Tm_Tm. Qed. *)
+
+(*   Lemma morphing n m (a b : Tm n) (ρ0 ρ1 : fin n -> Tm m) : *)
+(*     (forall i, R (ρ0 i) (ρ1 i)) -> *)
+(*     R a b -> R (subst_Tm ρ0 a) (subst_Tm ρ1 b). *)
+(*   Proof. *)
+(*     move => + h. move : m ρ0 ρ1. *)
+(*     elim : n a b /h. *)
+(*     - move => *. *)
+(*       apply : AppAbs'; eauto using morphing_up. *)
+(*       by asimpl. *)
+(*     - 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. *)
+(*     - hauto lq:on ctrs:R. *)
+(*     - hauto lq:on ctrs:R. *)
+(*     - hauto lq:on ctrs:R use:morphing_up. *)
+(*     - hauto lq:on ctrs:R. *)
+(*     - hauto lq:on ctrs:R. *)
+(*   Qed. *)
+
+(*   Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) : *)
+(*     R a b -> *)
+(*     R (subst_Tm ρ a) (subst_Tm ρ b). *)
+(*   Proof. hauto l:on use:morphing, refl. Qed. *)
+
+(*   Lemma cong n (a b : Tm (S n)) c d : *)
+(*     R a b -> *)
+(*     R c d -> *)
+(*     R (subst_Tm (scons c VarTm) a) (subst_Tm (scons d VarTm) b). *)
+(*   Proof. *)
+(*     move => h0 h1. apply morphing => //=. *)
+(*     qauto l:on ctrs:R inv:option. *)
+(*   Qed. *)
+
+(*   Lemma var_or_bot_imp {n} (a b : Tm n) : *)
+(*     var_or_bot a -> *)
+(*     a = b -> ~~ var_or_bot b -> False. *)
+(*   Proof. *)
+(*     hauto lq:on inv:Tm. *)
+(*   Qed. *)
+
+(*   Lemma var_or_bot_up n m (ρ : fin n -> Tm m) : *)
+(*     (forall i, var_or_bot (ρ i)) -> *)
+(*     (forall i, var_or_bot (up_Tm_Tm ρ i)). *)
+(*   Proof. *)
+(*     move => h /= [i|]. *)
+(*     - asimpl. *)
+(*       move /(_ i) in h. *)
+(*       rewrite /funcomp. *)
+(*       move : (ρ i) h. *)
+(*       case => //=. *)
+(*     - sfirstorder. *)
+(*   Qed. *)
+
+(*   Local Ltac antiimp := qauto l:on use:var_or_bot_imp. *)
+
+(*   Lemma antirenaming n m (a : Tm n) (b : Tm m) (ρ : fin n -> Tm m) : *)
+(*     (forall i, var_or_bot (ρ i)) -> *)
+(*     R (subst_Tm ρ a) b -> exists b0, R a b0 /\ subst_Tm ρ b0 = b. *)
+(*   Proof. *)
+(*     move E : (subst_Tm ρ a) => u hρ h. *)
+(*     move : n ρ hρ a E. elim : m u b/h. *)
+(*     - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; *)
+(*                first by antiimp. *)
+(*       move => c c0 [+ ?]. subst. *)
+(*       case : c => //=; first by antiimp. *)
+(*       move => c [?]. subst. *)
+(*       spec_refl. *)
+(*       have /var_or_bot_up hρ' := hρ. *)
+(*       move : iha hρ' => /[apply] iha. *)
+(*       move : ihb hρ => /[apply] ihb. *)
+(*       spec_refl. *)
+(*       move : iha => [c1][ih0]?. subst. *)
+(*       move : ihb => [c2][ih1]?. subst. *)
+(*       eexists. split. *)
+(*       apply AppAbs; eauto. *)
+(*       by asimpl. *)
+(*     - move => n p a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; *)
+(*                first by antiimp. *)
+(*       move => p0 []//=; first by antiimp. move => t t0[*]. *)
+(*       subst. *)
+(*       have {}/iha := (hρ) => iha. *)
+(*       have {}/ihb := (hρ) => ihb. *)
+(*       spec_refl. *)
+(*       move : iha => [b0 [? ?]]. *)
+(*       move : ihb => [c0 [? ?]]. subst. *)
+(*       eexists. split. by eauto using ProjPair. *)
+(*       hauto q:on. *)
+(*     - move => n i m ρ hρ []//=. *)
+(*       hauto l:on. *)
+(*     - move => n a0 a1 ha iha m ρ hρ []//=; first by antiimp. *)
+(*       move => t [*]. subst. *)
+(*       have /var_or_bot_up {}/iha := hρ => iha. *)
+(*       spec_refl. *)
+(*       move  :iha => [b0 [? ?]]. subst. *)
+(*       eexists. split. by apply AbsCong; eauto. *)
+(*       by asimpl. *)
+(*     - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; *)
+(*                first by antiimp. *)
+(*       move => t t0 [*]. subst. *)
+(*       have {}/iha := (hρ) => iha. *)
+(*       have {}/ihb := (hρ) => ihb. *)
+(*       spec_refl. *)
+(*       move : iha => [b0 [? ?]]. subst. *)
+(*       move : ihb => [c0 [? ?]]. subst. *)
+(*       eexists. split. by apply AppCong; eauto. *)
+(*       done. *)
+(*     - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=; *)
+(*                first by antiimp. *)
+(*       move => t t0[*]. subst. *)
+(*       have {}/iha := (hρ) => iha. *)
+(*       have {}/ihb := (hρ) => ihb. *)
+(*       spec_refl. *)
+(*       move : iha => [b0 [? ?]]. subst. *)
+(*       move : ihb => [c0 [? ?]]. subst. *)
+(*       eexists. split. by apply PairCong; eauto. *)
+(*       by asimpl. *)
+(*     - move => n p a0 a1 ha iha m ρ hρ []//=; *)
+(*                first by antiimp. *)
+(*       move => p0 t [*]. subst. *)
+(*       have {}/iha := (hρ) => iha. *)
+(*       spec_refl. *)
+(*       move : iha => [b0 [? ?]]. subst. *)
+(*       eexists. split. apply ProjCong; eauto. reflexivity. *)
+(*     - move => n p A0 A1 B0 B1 ha iha hB ihB m ρ hρ []//=; *)
+(*                first by antiimp. *)
+(*       move => ? t t0 [*]. subst. *)
+(*       have {}/iha := (hρ) => iha. *)
+(*       have /var_or_bot_up {}/ihB := (hρ) => ihB. *)
+(*       spec_refl. *)
+(*       move : iha => [b0 [? ?]]. *)
+(*       move : ihB => [c0 [? ?]]. subst. *)
+(*       eexists. split. by apply BindCong; eauto. *)
+(*       by asimpl. *)
+(*     - hauto q:on ctrs:R inv:Tm. *)
+(*     - move => n i n0 ρ hρ []//=; first by antiimp. *)
+(*       hauto l:on. *)
+(*   Qed. *)
+(* End RPar'. *)
+
+(* Module ERed. *)
+(*   Inductive R {n} : Tm n -> Tm n ->  Prop := *)
+(*   (****************** Eta ***********************) *)
+(*   | AppEta a : *)
+(*     R a (Abs (App (ren_Tm shift a) (VarTm var_zero))) *)
+(*   | PairEta a : *)
+(*     R a (Pair (Proj PL a) (Proj PR a)) *)
+
+(*   (*************** Congruence ********************) *)
+(*   | AbsCong a0 a1 : *)
+(*     R a0 a1 -> *)
+(*     R (Abs a0) (Abs a1) *)
+(*   | AppCong0 a0 a1 b : *)
+(*     R a0 a1 -> *)
+(*     R (App a0 b) (App a1 b) *)
+(*   | AppCong1 a b0 b1 : *)
+(*     R b0 b1 -> *)
+(*     R (App a b0) (App a b1) *)
+(*   | PairCong0 a0 a1 b : *)
+(*     R a0 a1 -> *)
+(*     R (Pair a0 b) (Pair a1 b) *)
+(*   | PairCong1 a b0 b1 : *)
+(*     R b0 b1 -> *)
+(*     R (Pair a b0) (Pair a b1) *)
+(*   | ProjCong p a0 a1 : *)
+(*     R a0 a1 -> *)
+(*     R (Proj p a0) (Proj p a1) *)
+(*   | BindCong0 p A0 A1 B: *)
+(*     R A0 A1 -> *)
+(*     R (TBind p A0 B) (TBind p A1 B) *)
+(*   | BindCong1 p A B0 B1: *)
+(*     R B0 B1 -> *)
+(*     R (TBind p A B0) (TBind p A B1). *)
+
+(*   Derive Dependent Inversion inv with (forall n (a b : Tm n), R a b) Sort Prop. *)
+
+(*   Lemma AppEta' n a (u : Tm n) : *)
+(*     u = (Abs (App (ren_Tm shift a) (VarTm var_zero))) -> *)
+(*     R a u. *)
+(*   Proof. move => ->. apply AppEta. 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 => n a m ξ. *)
+(*     apply AppEta'. by asimpl. *)
+(*     all : qauto ctrs:R. *)
+(*   Qed. *)
+
+(*   Lemma substing n m (a : Tm n) b (ρ : fin n -> Tm m) : *)
+(*     R a b -> *)
+(*     R (subst_Tm ρ a) (subst_Tm ρ b). *)
+(*   Proof. *)
+(*     move => h. move : m ρ. elim : n a b / h => n. *)
+(*     move => a m ρ /=. *)
+(*     apply : AppEta'; eauto. by asimpl. *)
+(*     all : hauto ctrs:R inv:option use:renaming. *)
+(*   Qed. *)
+
+(* 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 : Tm (S n)) : *)
+(*     rtc ERed.R a b -> *)
+(*     rtc ERed.R (Abs a) (Abs b). *)
+(*   Proof. solve_s. Qed. *)
+
+(*   Lemma AppCong n (a0 a1 b0 b1 : Tm n) : *)
+(*     rtc ERed.R a0 a1 -> *)
+(*     rtc ERed.R b0 b1 -> *)
+(*     rtc ERed.R (App a0 b0) (App a1 b1). *)
+(*   Proof. solve_s. Qed. *)
+
+(*   Lemma BindCong n p (a0 a1 : Tm n) b0 b1 : *)
+(*     rtc ERed.R a0 a1 -> *)
+(*     rtc ERed.R b0 b1 -> *)
+(*     rtc ERed.R (TBind p a0 b0) (TBind p a1 b1). *)
+(*   Proof. solve_s. Qed. *)
+
+(*   Lemma PairCong n (a0 a1 b0 b1 : Tm n) : *)
+(*     rtc ERed.R a0 a1 -> *)
+(*     rtc ERed.R b0 b1 -> *)
+(*     rtc ERed.R (Pair a0 b0) (Pair a1 b1). *)
+(*   Proof. solve_s. Qed. *)
+
+(*   Lemma ProjCong n p (a0 a1  : Tm n) : *)
+(*     rtc ERed.R a0 a1 -> *)
+(*     rtc ERed.R (Proj p a0) (Proj p a1). *)
+(*   Proof. solve_s. Qed. *)
+(* End EReds. *)
 
 Module EPar.
   Inductive R {n} : Tm n -> Tm n ->  Prop :=
@@ -897,7 +1588,16 @@ Module EPar.
   | BotCong :
     R Bot Bot
   | UnivCong i :
-    R (Univ i) (Univ i).
+    R (Univ i) (Univ i)
+  | BoolCong :
+    R Bool Bool
+  | BValCong b :
+    R (BVal b) (BVal b)
+  | IfCong a0 a1 b0 b1 c0 c1 :
+    R a0 a1 ->
+    R b0 b1 ->
+    R c0 c1 ->
+    R (If a0 b0 c0) (If a1 b1 c1).
 
   Lemma refl n (a : Tm n) : EPar.R a a.
   Proof.
@@ -942,6 +1642,9 @@ Module EPar.
     - hauto l:on ctrs:R use:renaming inv:option.
     - hauto lq:on ctrs:R.
     - hauto lq:on ctrs:R.
+    - hauto lq:on ctrs:R.
+    - hauto lq:on ctrs:R.
+    - hauto lq:on ctrs:R.
   Qed.
 
   Lemma substing n a0 a1 (b0 b1 : Tm n) :
@@ -1031,6 +1734,13 @@ Module RPars.
     rtc RPar.R (Pair a0 b0) (Pair a1 b1).
   Proof. solve_s. Qed.
 
+  Lemma IfCong n (a0 a1 b0 b1 c0 c1 : Tm n) :
+    rtc RPar.R a0 a1 ->
+    rtc RPar.R b0 b1 ->
+    rtc RPar.R c0 c1 ->
+    rtc RPar.R (If a0 b0 c0) (If a1 b1 c1).
+  Proof. solve_s. Qed.
+
   Lemma ProjCong n p (a0 a1  : Tm n) :
     rtc RPar.R a0 a1 ->
     rtc RPar.R (Proj p a0) (Proj p a1).
@@ -1086,100 +1796,105 @@ Module RPars.
 
 End RPars.
 
-Module RPars'.
+(* Module RPars'. *)
 
-  #[local]Ltac solve_s_rec :=
-  move => *; eapply rtc_l; eauto;
-         hauto lq:on ctrs:RPar'.R use:RPar'.refl.
+(*   #[local]Ltac solve_s_rec := *)
+(*   move => *; eapply rtc_l; eauto; *)
+(*          hauto lq:on ctrs:RPar'.R use:RPar'.refl. *)
 
-  #[local]Ltac solve_s :=
-    repeat (induction 1; last by solve_s_rec); apply rtc_refl.
+(*   #[local]Ltac solve_s := *)
+(*     repeat (induction 1; last by solve_s_rec); apply rtc_refl. *)
 
-  Lemma AbsCong n (a b : Tm (S n)) :
-    rtc RPar'.R a b ->
-    rtc RPar'.R (Abs a) (Abs b).
-  Proof. solve_s. Qed.
+(*   Lemma AbsCong n (a b : Tm (S n)) : *)
+(*     rtc RPar'.R a b -> *)
+(*     rtc RPar'.R (Abs a) (Abs b). *)
+(*   Proof. solve_s. Qed. *)
 
-  Lemma AppCong n (a0 a1 b0 b1 : Tm n) :
-    rtc RPar'.R a0 a1 ->
-    rtc RPar'.R b0 b1 ->
-    rtc RPar'.R (App a0 b0) (App a1 b1).
-  Proof. solve_s. Qed.
+(*   Lemma AppCong n (a0 a1 b0 b1 : Tm n) : *)
+(*     rtc RPar'.R a0 a1 -> *)
+(*     rtc RPar'.R b0 b1 -> *)
+(*     rtc RPar'.R (App a0 b0) (App a1 b1). *)
+(*   Proof. solve_s. Qed. *)
 
-  Lemma BindCong n p (a0 a1 : Tm n) b0 b1 :
-    rtc RPar'.R a0 a1 ->
-    rtc RPar'.R b0 b1 ->
-    rtc RPar'.R (TBind p a0 b0) (TBind p a1 b1).
-  Proof. solve_s. Qed.
+(*   Lemma BindCong n p (a0 a1 : Tm n) b0 b1 : *)
+(*     rtc RPar'.R a0 a1 -> *)
+(*     rtc RPar'.R b0 b1 -> *)
+(*     rtc RPar'.R (TBind p a0 b0) (TBind p a1 b1). *)
+(*   Proof. solve_s. Qed. *)
 
-  Lemma PairCong n (a0 a1 b0 b1 : Tm n) :
-    rtc RPar'.R a0 a1 ->
-    rtc RPar'.R b0 b1 ->
-    rtc RPar'.R (Pair a0 b0) (Pair a1 b1).
-  Proof. solve_s. Qed.
+(*   Lemma PairCong n (a0 a1 b0 b1 : Tm n) : *)
+(*     rtc RPar'.R a0 a1 -> *)
+(*     rtc RPar'.R b0 b1 -> *)
+(*     rtc RPar'.R (Pair a0 b0) (Pair a1 b1). *)
+(*   Proof. solve_s. Qed. *)
 
-  Lemma ProjCong n p (a0 a1  : Tm n) :
-    rtc RPar'.R a0 a1 ->
-    rtc RPar'.R (Proj p a0) (Proj p a1).
-  Proof. solve_s. Qed.
+(*   Lemma ProjCong n p (a0 a1  : Tm n) : *)
+(*     rtc RPar'.R a0 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) :
-    rtc RPar'.R a0 a1 ->
-    rtc RPar'.R (ren_Tm ξ a0) (ren_Tm ξ a1).
-  Proof.
-    induction 1.
-    - apply rtc_refl.
-    - eauto using RPar'.renaming, rtc_l.
-  Qed.
+(*   Lemma renaming n (a0 a1 : Tm n) m (ξ : fin n -> fin m) : *)
+(*     rtc RPar'.R a0 a1 -> *)
+(*     rtc RPar'.R (ren_Tm ξ a0) (ren_Tm ξ a1). *)
+(*   Proof. *)
+(*     induction 1. *)
+(*     - apply rtc_refl. *)
+(*     - eauto using RPar'.renaming, rtc_l. *)
+(*   Qed. *)
 
-  Lemma weakening n (a0 a1 : Tm n) :
-    rtc RPar'.R a0 a1 ->
-    rtc RPar'.R (ren_Tm shift a0) (ren_Tm shift a1).
-  Proof. apply renaming. Qed.
+(*   Lemma weakening n (a0 a1 : Tm n) : *)
+(*     rtc RPar'.R a0 a1 -> *)
+(*     rtc RPar'.R (ren_Tm shift a0) (ren_Tm shift a1). *)
+(*   Proof. apply renaming. Qed. *)
 
-  Lemma Abs_inv n (a : Tm (S n)) b :
-    rtc RPar'.R (Abs a) b -> exists a', b = Abs a' /\ rtc RPar'.R a a'.
-  Proof.
-    move E : (Abs a) => b0 h. move : a E.
-    elim : b0 b / h.
-    - hauto lq:on ctrs:rtc.
-    - hauto lq:on ctrs:rtc inv:RPar'.R, rtc.
-  Qed.
+(*   Lemma Abs_inv n (a : Tm (S n)) b : *)
+(*     rtc RPar'.R (Abs a) b -> exists a', b = Abs a' /\ rtc RPar'.R a a'. *)
+(*   Proof. *)
+(*     move E : (Abs a) => b0 h. move : a E. *)
+(*     elim : b0 b / h. *)
+(*     - hauto lq:on ctrs:rtc. *)
+(*     - hauto lq:on ctrs:rtc inv:RPar'.R, rtc. *)
+(*   Qed. *)
 
-  Lemma morphing n m (a b : Tm n) (ρ : fin n -> Tm m) :
-    rtc RPar'.R a b ->
-    rtc RPar'.R (subst_Tm ρ a) (subst_Tm ρ b).
-  Proof. induction 1; qauto l:on ctrs:rtc use:RPar'.substing. Qed.
+(*   Lemma morphing n m (a b : Tm n) (ρ : fin n -> Tm m) : *)
+(*     rtc RPar'.R a b -> *)
+(*     rtc RPar'.R (subst_Tm ρ a) (subst_Tm ρ b). *)
+(*   Proof. induction 1; qauto l:on ctrs:rtc use:RPar'.substing. Qed. *)
 
-  Lemma substing n (a b : Tm (S n)) c :
-    rtc RPar'.R a b ->
-    rtc RPar'.R (subst_Tm (scons c VarTm) a) (subst_Tm (scons c VarTm) b).
-  Proof. hauto lq:on use:morphing inv:option. Qed.
+(*   Lemma substing n (a b : Tm (S n)) c : *)
+(*     rtc RPar'.R a b -> *)
+(*     rtc RPar'.R (subst_Tm (scons c VarTm) a) (subst_Tm (scons c VarTm) b). *)
+(*   Proof. hauto lq:on use:morphing inv:option. Qed. *)
 
-  Lemma antirenaming n m (a : Tm n) (b : Tm m) (ρ : fin n -> Tm m) :
-    (forall i, var_or_bot (ρ i)) ->
-    rtc RPar'.R (subst_Tm ρ a) b -> exists b0, rtc RPar'.R a b0 /\ subst_Tm ρ b0 = b.
-  Proof.
-    move E  :(subst_Tm ρ a) => u hρ h.
-    move : a E.
-    elim : u b /h.
-    - sfirstorder.
-    - move => a b c h0 h1 ih1 a0 ?. subst.
-      move /RPar'.antirenaming : h0.
-      move /(_ hρ).
-      move => [b0 [h2 ?]]. subst.
-      hauto lq:on rew:off ctrs:rtc.
-  Qed.
+(*   Lemma antirenaming n m (a : Tm n) (b : Tm m) (ρ : fin n -> Tm m) : *)
+(*     (forall i, var_or_bot (ρ i)) -> *)
+(*     rtc RPar'.R (subst_Tm ρ a) b -> exists b0, rtc RPar'.R a b0 /\ subst_Tm ρ b0 = b. *)
+(*   Proof. *)
+(*     move E  :(subst_Tm ρ a) => u hρ h. *)
+(*     move : a E. *)
+(*     elim : u b /h. *)
+(*     - sfirstorder. *)
+(*     - move => a b c h0 h1 ih1 a0 ?. subst. *)
+(*       move /RPar'.antirenaming : h0. *)
+(*       move /(_ hρ). *)
+(*       move => [b0 [h2 ?]]. subst. *)
+(*       hauto lq:on rew:off ctrs:rtc. *)
+(*   Qed. *)
 
-End RPars'.
+(* End RPars'. *)
+
+(* (forall p, exists d, rtc RPar.R (Proj p c) d /\ EPar.R (if p is PL then a else b) d) *)
+(* (exists d0 d1, rtc RPar.R (App (ren_Tm shift c) (VarTm var_zero)) *)
+(*                 (Pair (App (ren_Tm shift d0) (VarTm var_zero))(App (ren_Tm shift d1) (VarTm var_zero))) /\ *)
+(*     EPar.R a d0 /\ EPar.R b d1) *)
 
 Lemma Abs_EPar n a (b : Tm n) :
   EPar.R (Abs a) b ->
   (exists d, EPar.R a d /\
-     rtc RPar.R (App (ren_Tm shift b) (VarTm var_zero)) d) /\
+     rtc CRRed.R (App (ren_Tm shift b) (VarTm var_zero)) d) /\
          (exists d,
          EPar.R a d /\ forall p,
-         rtc RPar.R (Proj p b) (Abs (Proj p d))).
+         rtc CRRed.R (Proj p b) (Abs (Proj p d))).
 Proof.
   move E : (Abs a) => u h.
   move : a E.
@@ -1190,45 +1905,227 @@ Proof.
     split; exists d.
     + split => //.
       apply : rtc_l.
-      apply RPar.AppAbs; eauto => //=.
-      apply RPar.refl.
-      by apply RPar.refl.
+      apply CRRed.AppAbs; eauto => //=.
       move :ih1; substify; by asimpl.
     + split => // p.
       apply : rtc_l.
-      apply : RPar.ProjAbs.
-      by apply RPar.refl.
-      eauto using RPars.ProjCong, RPars.AbsCong.
+      apply : CRRed.ProjAbs.
+      eauto using CRReds.ProjCong, CRReds.AbsCong.
   - move => n ? a1 ha iha a0 ?. subst. specialize iha with (1 := eq_refl).
     move : iha => [_ [d [ih0 ih1]]].
     split.
     + 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 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 CRRed.AppPair.
+      suff h : forall p, rtc CRRed.R (App (Proj p (ren_Tm shift a1)) (VarTm var_zero)) (Proj p d) by
+          sfirstorder use:CRReds.PairCong.
+      move => p. move /(_ p) /CRReds.renaming 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.
+      by eauto using CRReds.AppCong, rtc_refl.
       apply relations.rtc_once => /=.
-      apply : RPar.AppAbs'; eauto using RPar.refl.
-      by asimpl.
+      apply : CRRed.AppAbs'. by asimpl.
     + exists d. repeat split => //. move => p.
       apply : rtc_l; eauto.
-      hauto q:on use:RPar.ProjPair', RPar.refl.
+      case : p; sfirstorder use:CRRed.ProjPair.
   - move => n a0 a1 ha _ ? [*]. subst.
     split.
     + exists a1. split => //.
-      apply rtc_once. apply : RPar.AppAbs'; eauto using RPar.refl. by asimpl.
+      apply rtc_once. apply : CRRed.AppAbs'. by asimpl.
     + exists a1. split => // p.
-      apply rtc_once. apply : RPar.ProjAbs; eauto using RPar.refl.
+      apply rtc_once. apply : CRRed.ProjAbs.
+Qed.
+
+Lemma BVal_EPar_If n (v : bool) q :
+  EPar.R (BVal v : Tm n) q ->
+  forall b c, exists e, rtc CRRed.R (If q b c) e /\ rtc OExp.R (if v then b else c) e.
+Proof.
+  move E :(BVal v) => u h. move : v E.
+  elim : n u q /h => //=.
+  - move => n a0 a1 ha iha v ? b c. subst.
+    spec_refl.
+    move /(_ b c) : iha => [e [h0 h1]].
+    eexists. split; cycle 1.
+    apply : rtc_r; eauto. apply OExp.AppEta.
+    apply : rtc_l. apply CRRed.IfAbs.
+    apply CRReds.AbsCong.
+    apply : rtc_l. apply CRRed.IfApp.
+    apply CRReds.AppCong; auto using rtc_refl.
+    set (x := If _ _ _).
+    change x with (ren_Tm shift (If a1 b c)).
+    eauto using CRReds.renaming.
+  - move => n a0 a1 ha iha v ? b c. subst.
+    spec_refl.
+    move /(_ b c) : iha => [e [h0 h1]].
+    eexists; split; cycle 1.
+    apply : rtc_r; eauto. apply OExp.PairEta.
+    apply : rtc_l. apply CRRed.IfPair.
+    apply CRReds.PairCong; hauto lq:on ctrs:rtc use:CRRed.IfProj, CRReds.ProjCong.
+  - sauto lq:on.
+Qed.
+
+Lemma Proj_EPar_If n p (a : Tm n) q :
+  EPar.R (Proj p a) q ->
+  exists d, EPar.R a d /\
+         forall b c, exists e, rtc CRRed.R (If q b c) e /\ rtc OExp.R (Proj p (If d b c)) e.
+Proof.
+  move E :(Proj p a) => u h. move : p a E.
+  elim : n u q /h => //=.
+  - move => n a0 a1 ha iha p a ?. subst.
+    spec_refl.
+    move : iha => [d [ih0 ih1]].
+    exists d. split => // b c.
+    move /(_ b c) : ih1 => [e [ih1 ih2]].
+    eexists; split; cycle 1.
+    apply : rtc_r; eauto.
+    apply OExp.AppEta.
+    apply : rtc_l.
+    apply CRRed.IfAbs.
+    apply : rtc_l.
+    apply CRRed.AbsCong.
+    apply CRRed.IfApp.
+    apply CRReds.AbsCong.
+    apply CRReds.AppCong; eauto using rtc_refl.
+    set (x := If _ _ _).
+    change x with (ren_Tm shift (If a1 b c)).
+    eauto using CRReds.renaming.
+  - move => n a0 a1 ha ih p a ?. subst.
+    spec_refl. move : ih => [d [ih0 ih1]].
+    exists d. split => // b c.
+    move /(_ b c) : ih1 => [e [h0 h1]].
+    eexists; split; cycle 1.
+    apply : rtc_r; eauto.
+    apply OExp.PairEta.
+    apply : rtc_l.
+    apply CRRed.IfPair.
+    apply CRReds.PairCong; hauto lq:on ctrs:rtc use:CRRed.IfProj, CRReds.ProjCong.
+  - sauto lq:on rew:off.
+Qed.
+
+Lemma App_EPar_If n (r0 r1 : Tm n) q :
+  EPar.R (App r0 r1) q ->
+  exists d0 d1, EPar.R r0 d0 /\ EPar.R r1 d1 /\
+             forall b c, exists e, rtc CRRed.R (If q b c) e /\ rtc OExp.R (App (If d0 b c) d1) e.
+Proof.
+  move E : (App r0 r1) => u h.
+  move : r0 r1 E.
+  elim : n u q /h => //= n.
+  - move => a0 a1 ha iha r0 r1 ?. subst.
+    spec_refl.
+    move : iha => [d0 [d1 [ih0 [ih1 ih2]]]].
+    exists d0, d1. repeat split => //.
+    move => b c.
+    move /(_ b c) : ih2 => [e [h0 h1]].
+    eexists; split; cycle 1.
+    apply : rtc_r; eauto.
+    apply OExp.AppEta.
+    apply : rtc_l. apply CRRed.IfAbs.
+    apply CRReds.AbsCong.
+    apply : rtc_l. apply CRRed.IfApp.
+    apply CRReds.AppCong; auto using rtc_refl.
+    set (x := If _ _ _).
+    change x with (ren_Tm shift (If a1 b c)).
+    auto using CRReds.renaming.
+  - move => a0 a1 ha iha r0 r1 ?. subst.
+    spec_refl. move : iha => [d0 [d1 [ih0 [ih1 ih2]]]].
+    exists d0, d1. (repeat split) => // b c.
+    move /(_ b c) : ih2 => [d [h0 h1]].
+    eexists; split; cycle 1.
+    apply : rtc_r; eauto.
+    apply OExp.PairEta.
+    apply : rtc_l. apply CRRed.IfPair.
+    apply CRReds.PairCong;
+    hauto lq:on ctrs:rtc use:CRRed.IfProj, CRReds.ProjCong, CRReds.AppCong.
+  - sauto lq:on.
+Qed.
+
+Lemma Pair_EPar_If n (r0 r1 : Tm n) q :
+  EPar.R (Pair r0 r1) q ->
+  exists d0 d1, EPar.R r0 d0 /\ EPar.R r1 d1 /\
+             forall b c, exists e, rtc CRRed.R (If q b c) e /\ rtc OExp.R (Pair (If d0 b c) (If d1 b c)) e.
+Proof.
+  move E : (Pair r0 r1) => u h.
+  move : r0 r1 E.
+  elim : n u q /h => //= n.
+  - move => a0 a1 ha iha r0 r1 ?. subst.
+    spec_refl.
+    move : iha => [d0 [d1 [ih0 [ih1 ih2]]]].
+    exists d0, d1. repeat split => //.
+    move => b c.
+    move /(_ b c) : ih2 => [e [h0 h1]].
+    eexists; split; cycle 1.
+    apply : rtc_r; eauto.
+    apply OExp.AppEta.
+    apply : rtc_l. apply CRRed.IfAbs.
+    apply CRReds.AbsCong.
+    apply : rtc_l. apply CRRed.IfApp.
+    apply CRReds.AppCong; auto using rtc_refl.
+    set (x := If _ _ _).
+    change x with (ren_Tm shift (If a1 b c)).
+    auto using CRReds.renaming.
+  - move => a0 a1 ha iha r0 r1 ?. subst.
+    spec_refl. move : iha => [d0 [d1 [ih0 [ih1 ih2]]]].
+    exists d0, d1. (repeat split) => // b c.
+    move /(_ b c) : ih2 => [d [h0 h1]].
+    eexists; split; cycle 1.
+    apply : rtc_r; eauto.
+    apply OExp.PairEta.
+    apply : rtc_l. apply CRRed.IfPair.
+    hauto lq:on ctrs:rtc use:CRRed.IfProj, CRReds.ProjCong, CRReds.PairCong.
+  - sauto lq:on.
+Qed.
+
+Lemma Abs_EPar_If n (a : Tm (S n)) q :
+  EPar.R (Abs a) q ->
+  exists d, EPar.R a d /\
+         forall b c, exists e, rtc CRRed.R (If q b c) e /\ rtc OExp.R (Abs (If d (ren_Tm shift b) (ren_Tm shift c))) e.
+Proof.
+  move E : (Abs a) => u h.
+  move : a E.
+  elim : n u q /h => //= n.
+  - move => a0 a1 ha iha b ?. subst.
+    (* move /Abs_EPar : ha. *)
+    spec_refl.
+    move : iha => [d [hd h]].
+    exists d.
+    split => //.
+    move => b0 c0.
+    move /(_ b0 c0) : h.
+    move => [e [h0 h1]].
+    exists (Abs (App (ren_Tm shift e) (VarTm var_zero))).
+    split.
+    apply : rtc_l. apply CRRed.IfAbs.
+    apply : rtc_l. apply CRRed.AbsCong.
+    apply CRRed.IfApp.
+    apply CRReds.AbsCong. apply CRReds.AppCong; eauto using rtc_refl.
+    change (If (ren_Tm shift a1) (ren_Tm shift b0) (ren_Tm shift c0)) with (ren_Tm shift (If a1 b0 c0)).
+    hauto lq:on use:CRReds.renaming.
+    apply : rtc_r; eauto.
+    apply OExp.AppEta.
+  - move => a0 a1 ha iha a ?. subst.
+    spec_refl.
+    move : iha => [d [h0 h1]].
+    exists d. split => //.
+    move => b c. move/(_ b c ): h1 => [e [h1 h2]].
+    eexists; split; cycle 1.
+    apply : rtc_r; eauto.
+    apply OExp.PairEta.
+    apply : rtc_l.
+    apply CRRed.IfPair.
+    apply : rtc_l.
+    apply CRRed.PairCong0.
+    apply CRRed.IfProj.
+    apply : rtc_l.
+    apply CRRed.PairCong1.
+    apply CRRed.IfProj.
+    by apply CRReds.PairCong; apply CRReds.ProjCong.
+  - sauto lq: on.
 Qed.
 
 Lemma Pair_EPar n (a b c : Tm n) :
   EPar.R (Pair a b) c ->
-  (forall p, exists d, rtc RPar.R (Proj p c) d /\ EPar.R (if p is PL then a else b) d) /\
-    (exists d0 d1, rtc RPar.R (App (ren_Tm shift c) (VarTm var_zero))
+  (forall p, exists d, rtc CRRed.R (Proj p c) d /\ EPar.R (if p is PL then a else b) d) /\
+    (exists d0 d1, rtc CRRed.R (App (ren_Tm shift c) (VarTm var_zero))
                 (Pair (App (ren_Tm shift d0) (VarTm var_zero))(App (ren_Tm shift d1) (VarTm var_zero))) /\
     EPar.R a d0 /\ EPar.R b d1).
 Proof.
@@ -1242,44 +2139,44 @@ Proof.
       exists (Abs (App (ren_Tm shift (if p is PL then d0 else d1)) (VarTm var_zero))).
       split.
       * apply : relations.rtc_transitive.
-        ** apply RPars.ProjCong. apply RPars.AbsCong. eassumption.
-        ** apply : rtc_l. apply RPar.ProjAbs; eauto using RPar.refl. apply RPars.AbsCong.
-           apply : rtc_l. apply RPar.ProjPair; eauto using RPar.refl.
+        ** apply CRReds.ProjCong. apply CRReds.AbsCong. eassumption.
+        ** apply : rtc_l. apply CRRed.ProjAbs. apply CRReds.AbsCong.
+           apply : rtc_l. apply CRRed.ProjPair.
            hauto l:on.
       * hauto lq:on use:EPar.AppEta'.
     + exists d0, d1.
       repeat split => //.
-      apply : rtc_l. apply : RPar.AppAbs'; eauto using RPar.refl => //=.
+      apply : rtc_l. apply : CRRed.AppAbs' => //=.
       by asimpl; renamify.
   - move => n a0 a1 ha iha a b ?. subst. specialize iha with (1 := eq_refl).
     split => [p|].
     + move : iha => [/(_ p) [d [ih0 ih1]] _].
       exists d. split=>//.
-      apply : rtc_l. apply RPar.ProjPair; eauto using RPar.refl.
-      set q := (X in rtc RPar.R X d).
+      apply : rtc_l. apply CRRed.ProjPair.
+      set q := (X in rtc CRRed.R X d).
       by have -> : q = Proj p a1 by hauto lq:on.
     + move  :iha => [iha _].
       move : (iha PL) => [d0 [ih0 ih0']].
       move : (iha PR) => [d1 [ih1 ih1']] {iha}.
       exists d0, d1.
-      apply RPars.weakening in ih0, ih1.
+      apply CRReds.renaming with (ξ := shift) in ih0, ih1.
       repeat split => //=.
-      apply : rtc_l. apply RPar.AppPair; eauto using RPar.refl.
-      apply RPars.PairCong; apply RPars.AppCong; eauto using rtc_refl.
+      apply : rtc_l. apply CRRed.AppPair.
+      apply CRReds.PairCong; apply CRReds.AppCong; eauto using rtc_refl.
   - move => n a0 a1 b0 b1 ha _ hb _ a b [*]. subst.
     split.
     + move => p.
       exists (if p is PL then a1 else b1).
       split.
-      * apply rtc_once. apply : RPar.ProjPair'; eauto using RPar.refl.
+      * apply rtc_once. apply : CRRed.ProjPair.
       * hauto lq:on rew:off.
     + exists a1, b1.
-      split. apply rtc_once. apply RPar.AppPair; eauto using RPar.refl.
+      split. apply rtc_once. apply CRRed.AppPair.
       split => //.
 Qed.
 
 Lemma commutativity0 n (a b0 b1 : Tm n) :
-  EPar.R a b0 -> RPar.R a b1 -> exists c, rtc RPar.R b0 c /\ EPar.R b1 c.
+  EPar.R a b0 -> CRRed.R a b1 -> exists c, rtc CRRed.R b0 c /\ EPar.R b1 c.
 Proof.
   move => h. move : b1.
   elim : n a b0 / h.
@@ -1288,67 +2185,107 @@ Proof.
     move => [c [ih0 ih1]].
     exists (Abs (App (ren_Tm shift c) (VarTm var_zero))).
     split.
-    + hauto lq:on ctrs:rtc use:RPars.AbsCong, RPars.AppCong, RPars.renaming.
+    + hauto lq:on ctrs:rtc use:CRReds.AbsCong, CRReds.AppCong, CRReds.renaming.
     + 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 (Proj PL c) (Proj PR c)). split.
-    + apply RPars.PairCong;
-      by apply RPars.ProjCong.
+    + apply CRReds.PairCong;
+      by apply CRReds.ProjCong.
     + hauto lq:on ctrs:EPar.R use:EPar.refl, EPar.renaming.
-  - hauto l:on ctrs:rtc inv:RPar.R.
+  - hauto l:on ctrs:rtc inv:CRRed.R.
   - move => n a0 a1 h ih b1.
-    elim /RPar.inv => //= _.
+    elim /CRRed.inv => //= _.
     move => a2 a3 ? [*]. subst.
-    hauto lq:on ctrs:rtc, RPar.R, EPar.R use:RPars.AbsCong.
+    hauto lq:on ctrs:rtc, CRRed.R, EPar.R use:CRReds.AbsCong.
   - move => n a0 a1 b0 b1 ha iha hb ihb b2.
-    elim /RPar.inv => //= _.
-    + move =>  a2 a3 b3 b4 h0 h1 [*]. subst.
-      move /(_ _ ltac:(by eauto)) : ihb => [b [ihb0 ihb1]].
-      have {}/iha : RPar.R (Abs a2) (Abs a3) by hauto lq:on ctrs:RPar.R.
-      move => [c [ih0 /Abs_EPar [[d [ih1 ih2]] _]]].
-      exists (subst_Tm (scons b VarTm) d).
+    elim /CRRed.inv => //= _.
+    + move =>  a2 b3  [*]. subst. move {iha ihb}.
+      move /Abs_EPar : ha => [[d [ih1 ih2]] _].
+      exists (subst_Tm (scons b1 VarTm) d).
       split.
       (* By substitution *)
-      * move /RPars.substing  : ih2.
-        move /(_ b).
+      * move /CRReds.substing  : ih2.
+        move /(_ _ (scons b1 VarTm)).
         asimpl.
-        eauto using relations.rtc_transitive, RPars.AppCong.
+        eauto using relations.rtc_transitive, CRReds.AppCong.
       (* By EPar morphing *)
       * by apply EPar.substing.
-    + move => a2 a3 b3 b4 c0 c1 h0 h1 h2 [*]. subst.
-      move /(_ _ ltac:(by eauto using RPar.PairCong)) : iha
-           => [c [ihc0 ihc1]].
-      move /(_ _ ltac:(by eauto)) : ihb => [d [ihd0 ihd1]].
-      move /Pair_EPar  : ihc1 => [_ [d0 [d1 [ih0 [ih1 ih2]]]]].
-      move /RPars.substing : ih0. move /(_ d).
+    + move => a2 b3 c [*]. subst. move {iha ihb}.
+      move /Pair_EPar  : ha => [_ [d0 [d1 [ih0 [ih1 ih2]]]]].
+      move /CRReds.substing : ih0. move /(_ _ (scons b1 VarTm)).
       asimpl => h.
-      exists (Pair (App d0 d) (App d1 d)).
+      exists (Pair (App d0 b1) (App d1 b1)).
       split.
-      hauto lq:on use:relations.rtc_transitive, RPars.AppCong.
+      hauto lq:on use:@relations.rtc_transitive, CRReds.AppCong.
       apply EPar.PairCong; by apply EPar.AppCong.
-    + hauto lq:on ctrs:EPar.R use:RPars.AppCong.
-  - hauto lq:on ctrs:EPar.R inv:RPar.R use:RPars.PairCong.
+    + hauto lq:on ctrs:EPar.R, rtc use:CRReds.AppCong.
+    + move => a2 b3 b4 + [*]. subst.
+      move /ihb => [b [h0 h1]].
+      exists (App a1 b).
+      hauto q:on ctrs:EPar.R, rtc use:CRReds.AppCong.
+  - hauto lq:on ctrs:EPar.R, rtc inv:CRRed.R use:CRReds.PairCong.
   - move => n p a b0 h0 ih0 b1.
-    elim /RPar.inv => //= _.
-    + move => ? a0 a1 h [*]. subst.
-      move /(_ _ ltac:(by eauto using RPar.AbsCong)) : ih0 => [c [ih0 ih1]].
-      move /Abs_EPar : ih1 => [_ [d [ih1 ih2]]].
+    elim /CRRed.inv => //= _.
+    + move => ? a0 [*]. subst. move {ih0}.
+      move /Abs_EPar : h0 => [_ [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]].
-      move /Pair_EPar : ih1 => [/(_ p)[d [ihd ihd']] _].
+      qauto l:on ctrs:EPar.R use:CRReds.ProjCong, @relations.rtc_transitive.
+    + move => p0 a0 b2 [*]. subst.
+      move /Pair_EPar : h0 => [/(_ p)[d [ihd ihd']] _].
       exists d. split => //.
-      hauto lq:on use:RPars.ProjCong, relations.rtc_transitive.
-    + hauto lq:on ctrs:EPar.R use:RPars.ProjCong.
-  - hauto lq:on inv:RPar.R ctrs:EPar.R, rtc use:RPars.BindCong.
-  - hauto l:on ctrs:EPar.R inv:RPar.R.
-  - hauto l:on ctrs:EPar.R inv:RPar.R.
+    + hauto lq:on ctrs:EPar.R, rtc use:CRReds.ProjCong.
+  - hauto lq:on inv:CRRed.R ctrs:EPar.R, rtc use:CRReds.BindCong.
+  - hauto l:on ctrs:EPar.R inv:CRRed.R.
+  - hauto l:on ctrs:EPar.R inv:CRRed.R.
+  - hauto l:on ctrs:EPar.R inv:CRRed.R.
+  - hauto l:on ctrs:EPar.R inv:CRRed.R.
+  - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc u.
+    elim /CRRed.inv => //= _.
+    + move => a2 b2 c [*]{iha ihb ihc}. subst.
+      move /Abs_EPar_If : ha => [d [h0 h1]].
+      move /(_ b1 c1) : h1 => [e [h1 h2]].
+      exists e. split => //.
+      apply : OExp.merge; eauto.
+      hauto lq:on ctrs:EPar.R use:EPar.renaming.
+    + move => a2 b2 c d [*]. subst.
+      move {iha ihb ihc}.
+      move /Pair_EPar_If : ha => [r0 [r1 [h0 [h1 h2]]]].
+      move /(_ b1 c1) : h2 => [e [h3 h4]].
+      exists e. split => //.
+      hauto lq:on ctrs:EPar.R use:EPar.renaming, OExp.merge.
+    + move => a2 b2 c [*] {iha ihb ihc}. subst.
+      move /BVal_EPar_If : ha.
+      move /(_ b1 c1) => [e [h0 h1]].
+      exists e. split => //.
+      hauto lq:on ctrs:EPar.R use:EPar.renaming, OExp.merge.
+    + (* Need the rule that if commutes with abs *)
+      move => a2 b2 c d {iha ihb ihc} [*]. subst.
+      move /App_EPar_If : ha => [r0 [r1 [h0 [h1 h2]]]].
+      move /(_ b1 c1) : h2 => [e [h3 h4]].
+      exists e. split => //.
+      hauto lq:on ctrs:EPar.R use:EPar.renaming, OExp.merge.
+    + move => p a2 b2 c [*]. subst.
+      move {iha ihb ihc}.
+      move /Proj_EPar_If : ha => [d [h0 /(_ b1 c1) [e [h1 h2]]]].
+      hauto lq:on ctrs:EPar.R use:EPar.renaming, OExp.merge.
+    + move => a2 a3 b2 c h [*]. subst.
+      move /iha : h {iha} => [a [ha0 ha1]].
+      exists (If a b1 c1). split.
+      hauto lq:on ctrs:rtc use:CRReds.IfCong.
+      hauto lq:on ctrs:EPar.R.
+    + move => a2 b2 b3 c + [*]. subst.
+      move /ihb => [b [? ?]].
+      exists (If a1 b c1).
+      hauto lq:on ctrs:rtc,EPar.R use:CRReds.IfCong.
+    + move => a2 b2 c2 c3 + [*]. subst.
+      move /ihc => {ihc} [c [? ?]].
+      exists (If a1 b1 c).
+      hauto lq:on ctrs:rtc,EPar.R use:CRReds.IfCong.
 Qed.
 
 Lemma commutativity1 n (a b0 b1 : Tm n) :
-  EPar.R a b0 -> rtc RPar.R a b1 -> exists c, rtc RPar.R b0 c /\ EPar.R b1 c.
+  EPar.R a b0 -> rtc CRRed.R a b1 -> exists c, rtc CRRed.R b0 c /\ EPar.R b1 c.
 Proof.
   move => + h. move : b0.
   elim : a b1 / h.
@@ -1357,7 +2294,7 @@ Proof.
 Qed.
 
 Lemma commutativity n (a b0 b1 : Tm n) :
-  rtc EPar.R a b0 -> rtc RPar.R a b1 -> exists c, rtc RPar.R b0 c /\ rtc EPar.R b1 c.
+  rtc EPar.R a b0 -> rtc CRRed.R a b1 -> exists c, rtc CRRed.R b0 c /\ rtc EPar.R b1 c.
   move => h. move : b1. elim : a b0 /h.
   - sfirstorder.
   - move => a0 a1 a2 + ha1 ih b1 +.
@@ -1472,6 +2409,36 @@ Lemma Univ_EPar' n i (u : Tm n) :
   - hauto l:on ctrs:OExp.R.
 Qed.
 
+Lemma BVal_EPar' n i (u : Tm n) :
+  EPar.R (BVal i) u ->
+  rtc OExp.R (BVal i) u.
+  move E : (BVal i) => t h.
+  move : E. elim : n t u /h => //=.
+  - move => n a0 a1 h ih ?. subst.
+    specialize ih with (1 := eq_refl).
+    hauto lq:on ctrs:OExp.R use:rtc_r.
+  - move => n a0 a1 h ih ?. subst.
+    specialize ih with (1 := eq_refl).
+    hauto lq:on ctrs:OExp.R use:rtc_r.
+  - hauto l:on ctrs:OExp.R.
+Qed.
+
+Lemma If_EPar' n (a b c u : Tm n)  :
+  EPar.R (If a b c) u ->
+  (exists a0 b0 c0, EPar.R a a0 /\ EPar.R b b0 /\ EPar.R c c0 /\ rtc OExp.R (If a0 b0 c0) u).
+Proof.
+  move E : (If a b c) => t h.
+  move : a b c E. elim : n t u /h => //= n.
+  - move => a0 a1 ha iha a b c ?. subst.
+    specialize iha with (1 := eq_refl).
+    hauto lq:on ctrs:OExp.R use:rtc_r.
+  - move => a0 a1 ha iha a b c ?. subst.
+    specialize iha with (1 := eq_refl).
+    hauto lq:on ctrs:OExp.R use:rtc_r.
+  - hauto l:on ctrs:OExp.R.
+Qed.
+
+
 Lemma EPar_diamond n (c a1 b1 : Tm n) :
   EPar.R c a1 ->
   EPar.R c b1 ->
@@ -1519,94 +2486,63 @@ Proof.
     move : OExp.commutativity0 h2; repeat move/[apply].
     move => [d h].
     exists d. hauto lq:on rew:off ctrs:EPar.R use:OExp.merge.
-  - qauto use:Bot_EPar', EPar.refl.
-  - qauto use:Univ_EPar', EPar.refl.
+  - qauto use:EPar.refl.
+  - qauto use:EPar.refl.
+  - hauto lq:on use:EPar.refl.
+  - hauto lq:on use:EPar.refl.
+  - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc u.
+    move /If_EPar' => [a2 [b2 [c2 [h0 [h1 [h2 h3]]]]]].
+    have {}/iha := h0. have {}/ihb := h1. have {}/ihc := h2.
+    move => [c hc0]. move => [b hb0]. move => [a ha0].
+    have : EPar.R (If a2 b2 c2) (If a b c) by hauto lq:on ctrs:EPar.R.
+    move : OExp.commutativity0 h3. repeat move/[apply].
+    move => [d ?].
+    exists d. hauto lq:on rew:off ctrs:EPar.R use:OExp.merge.
 Qed.
 
-Function tstar {n} (a : Tm n) :=
-  match a with
-  | VarTm i => a
-  | Abs a => Abs (tstar a)
-  | App (Abs a) b => subst_Tm (scons (tstar b) VarTm) (tstar a)
-  | App (Pair a b) c =>
-      Pair (App (tstar a) (tstar c)) (App (tstar b) (tstar c))
-  | App a b => App (tstar a) (tstar b)
-  | Pair a b => Pair (tstar a) (tstar b)
-  | Proj p (Pair a b) => if p is PL then (tstar a) else (tstar b)
-  | Proj p (Abs a) => (Abs (Proj p (tstar a)))
-  | Proj p a => Proj p (tstar a)
-  | TBind p a b => TBind p (tstar a) (tstar b)
-  | Bot => Bot
-  | Univ i => Univ i
-  end.
+(* Function tstar' {n} (a : Tm n) := *)
+(*   match a with *)
+(*   | VarTm i => a *)
+(*   | Abs a => Abs (tstar' a) *)
+(*   | App (Abs a) b => subst_Tm (scons (tstar' b) VarTm) (tstar' a) *)
+(*   | App a b => App (tstar' a) (tstar' b) *)
+(*   | Pair a b => Pair (tstar' a) (tstar' b) *)
+(*   | Proj p (Pair a b) => if p is PL then (tstar' a) else (tstar' b) *)
+(*   | Proj p a => Proj p (tstar' a) *)
+(*   | TBind p a b => TBind p (tstar' a) (tstar' b) *)
+(*   | Bot => Bot *)
+(*   | Univ i => Univ i *)
+(*   end. *)
 
-Lemma RPar_triangle n (a : Tm n) : forall b, RPar.R a b -> RPar.R b (tstar a).
-Proof.
-  apply tstar_ind => {n a}.
-  - hauto lq:on inv:RPar.R ctrs:RPar.R.
-  - hauto lq:on inv:RPar.R ctrs:RPar.R.
-  - hauto lq:on use:RPar.cong, RPar.refl ctrs:RPar.R inv:RPar.R.
-  - hauto lq:on rew:off ctrs:RPar.R inv:RPar.R.
-  - hauto lq:on rew:off inv:RPar.R ctrs:RPar.R.
-  - hauto lq:on rew:off inv:RPar.R ctrs:RPar.R.
-  - hauto drew:off inv:RPar.R use:RPar.refl, RPar.ProjPair'.
-  - hauto drew:off inv:RPar.R use:RPar.refl, RPar.ProjPair'.
-  - hauto lq:on inv:RPar.R ctrs:RPar.R.
-  - hauto lq:on inv:RPar.R ctrs:RPar.R.
-  - hauto lq:on inv:RPar.R ctrs:RPar.R.
-  - hauto lq:on inv:RPar.R ctrs:RPar.R.
-  - hauto lq:on inv:RPar.R ctrs:RPar.R.
-Qed.
+(* Lemma RPar'_triangle n (a : Tm n) : forall b, RPar'.R a b -> RPar'.R b (tstar' a). *)
+(* Proof. *)
+(*   apply tstar'_ind => {n a}. *)
+(*   - hauto lq:on inv:RPar'.R ctrs:RPar'.R. *)
+(*   - hauto lq:on inv:RPar'.R ctrs:RPar'.R. *)
+(*   - hauto lq:on use:RPar'.cong, RPar'.refl ctrs:RPar'.R inv:RPar'.R. *)
+(*   - hauto lq:on rew:off ctrs:RPar'.R inv:RPar'.R. *)
+(*   - hauto lq:on rew:off inv:RPar'.R ctrs:RPar'.R. *)
+(*   - hauto drew:off inv:RPar'.R use:RPar'.refl, RPar'.ProjPair'. *)
+(*   - hauto drew:off inv:RPar'.R use:RPar'.refl, RPar'.ProjPair'. *)
+(*   - hauto lq:on inv:RPar'.R ctrs:RPar'.R. *)
+(*   - hauto lq:on inv:RPar'.R ctrs:RPar'.R. *)
+(*   - hauto lq:on inv:RPar'.R ctrs:RPar'.R. *)
+(*   - hauto lq:on inv:RPar'.R ctrs:RPar'.R. *)
+(* Qed. *)
 
-Function tstar' {n} (a : Tm n) :=
-  match a with
-  | VarTm i => a
-  | Abs a => Abs (tstar' a)
-  | App (Abs a) b => subst_Tm (scons (tstar' b) VarTm) (tstar' a)
-  | App a b => App (tstar' a) (tstar' b)
-  | Pair a b => Pair (tstar' a) (tstar' b)
-  | Proj p (Pair a b) => if p is PL then (tstar' a) else (tstar' b)
-  | Proj p a => Proj p (tstar' a)
-  | TBind p a b => TBind p (tstar' a) (tstar' b)
-  | Bot => Bot
-  | Univ i => Univ i
-  end.
+(* Lemma RPar'_diamond n (c a1 b1 : Tm n) : *)
+(*   RPar'.R c a1 -> *)
+(*   RPar'.R c b1 -> *)
+(*   exists d2, RPar'.R a1 d2 /\ RPar'.R b1 d2. *)
+(* Proof. hauto l:on use:RPar'_triangle. Qed. *)
 
-Lemma RPar'_triangle n (a : Tm n) : forall b, RPar'.R a b -> RPar'.R b (tstar' a).
-Proof.
-  apply tstar'_ind => {n a}.
-  - hauto lq:on inv:RPar'.R ctrs:RPar'.R.
-  - hauto lq:on inv:RPar'.R ctrs:RPar'.R.
-  - hauto lq:on use:RPar'.cong, RPar'.refl ctrs:RPar'.R inv:RPar'.R.
-  - hauto lq:on rew:off ctrs:RPar'.R inv:RPar'.R.
-  - hauto lq:on rew:off inv:RPar'.R ctrs:RPar'.R.
-  - hauto drew:off inv:RPar'.R use:RPar'.refl, RPar'.ProjPair'.
-  - hauto drew:off inv:RPar'.R use:RPar'.refl, RPar'.ProjPair'.
-  - hauto lq:on inv:RPar'.R ctrs:RPar'.R.
-  - hauto lq:on inv:RPar'.R ctrs:RPar'.R.
-  - hauto lq:on inv:RPar'.R ctrs:RPar'.R.
-  - hauto lq:on inv:RPar'.R ctrs:RPar'.R.
-Qed.
-
-Lemma RPar_diamond n (c a1 b1 : Tm n) :
-  RPar.R c a1 ->
-  RPar.R c b1 ->
-  exists d2, RPar.R a1 d2 /\ RPar.R b1 d2.
-Proof. hauto l:on use:RPar_triangle. Qed.
-
-Lemma RPar'_diamond n (c a1 b1 : Tm n) :
-  RPar'.R c a1 ->
-  RPar'.R c b1 ->
-  exists d2, RPar'.R a1 d2 /\ RPar'.R b1 d2.
-Proof. hauto l:on use:RPar'_triangle. Qed.
-
-Lemma RPar_confluent n (c a1 b1 : Tm n) :
-  rtc RPar.R c a1 ->
-  rtc RPar.R c b1 ->
-  exists d2, rtc RPar.R a1 d2 /\ rtc RPar.R b1 d2.
-Proof.
-  sfirstorder use:relations.diamond_confluent, RPar_diamond.
-Qed.
+(* Lemma RPar_confluent n (c a1 b1 : Tm n) : *)
+(*   rtc RPar.R c a1 -> *)
+(*   rtc RPar.R c b1 -> *)
+(*   exists d2, rtc RPar.R a1 d2 /\ rtc RPar.R b1 d2. *)
+(* Proof. *)
+(*   sfirstorder use:relations.diamond_confluent, RPar_diamond. *)
+(* Qed. *)
 
 Lemma EPar_confluent n (c a1 b1 : Tm n) :
   rtc EPar.R c a1 ->