syntax.sig

@@ -1,18 +1,15 @@
 PTm(VarPTm) : Type
 PTag : Type
-BTag : Type
+Ty : Type
 
-nat : Type
+Fun : Ty -> Ty -> Ty
+Prod : Ty -> Ty -> Ty
+Void : Ty
 
 PL : PTag
 PR : PTag
 
-PPi : BTag
-PSig : BTag
-
 PAbs : (bind PTm in PTm) -> PTm
 PApp : PTm -> PTm -> PTm
 PPair : PTm -> PTm -> PTm
 PProj : PTag -> PTm -> PTm
-PBind : BTag -> PTm -> (bind PTm in PTm) -> PTm
-PUniv : nat -> PTm

theories/Autosubst2/syntax.v

@@ -5,20 +5,6 @@ Require Import Setoid Morphisms Relation_Definitions.
 
 Module Core.
 
-Inductive BTag : Type :=
-  | PPi : BTag
-  | PSig : BTag.
-
-Lemma congr_PPi : PPi = PPi.
-Proof.
-exact (eq_refl).
-Qed.
-
-Lemma congr_PSig : PSig = PSig.
-Proof.
-exact (eq_refl).
-Qed.
-
 Inductive PTag : Type :=
   | PL : PTag
   | PR : PTag.
@@ -38,9 +24,7 @@ Inductive PTm (n_PTm : nat) : Type :=
   | PAbs : PTm (S n_PTm) -> PTm n_PTm
   | PApp : PTm n_PTm -> PTm n_PTm -> PTm n_PTm
   | PPair : PTm n_PTm -> PTm n_PTm -> PTm n_PTm
-  | PProj : PTag -> PTm n_PTm -> PTm n_PTm
+  | PProj : PTag -> PTm n_PTm -> PTm n_PTm.
-  | PBind : BTag -> PTm n_PTm -> PTm (S n_PTm) -> PTm n_PTm
-  | PUniv : nat -> PTm n_PTm.
 
 Lemma congr_PAbs {m_PTm : nat} {s0 : PTm (S m_PTm)} {t0 : PTm (S m_PTm)}
   (H0 : s0 = t0) : PAbs m_PTm s0 = PAbs m_PTm t0.
@@ -72,23 +56,6 @@ exact (eq_trans (eq_trans eq_refl (ap (fun x => PProj m_PTm x s1) H0))
          (ap (fun x => PProj m_PTm t0 x) H1)).
 Qed.
 
-Lemma congr_PBind {m_PTm : nat} {s0 : BTag} {s1 : PTm m_PTm}
-  {s2 : PTm (S m_PTm)} {t0 : BTag} {t1 : PTm m_PTm} {t2 : PTm (S m_PTm)}
-  (H0 : s0 = t0) (H1 : s1 = t1) (H2 : s2 = t2) :
-  PBind m_PTm s0 s1 s2 = PBind m_PTm t0 t1 t2.
-Proof.
-exact (eq_trans
-         (eq_trans (eq_trans eq_refl (ap (fun x => PBind m_PTm x s1 s2) H0))
-            (ap (fun x => PBind m_PTm t0 x s2) H1))
-         (ap (fun x => PBind m_PTm t0 t1 x) H2)).
-Qed.
-
-Lemma congr_PUniv {m_PTm : nat} {s0 : nat} {t0 : nat} (H0 : s0 = t0) :
-  PUniv m_PTm s0 = PUniv m_PTm t0.
-Proof.
-exact (eq_trans eq_refl (ap (fun x => PUniv m_PTm x) H0)).
-Qed.
-
 Lemma upRen_PTm_PTm {m : nat} {n : nat} (xi : fin m -> fin n) :
   fin (S m) -> fin (S n).
 Proof.
@@ -109,9 +76,6 @@ Fixpoint ren_PTm {m_PTm : nat} {n_PTm : nat}
   | PApp _ s0 s1 => PApp n_PTm (ren_PTm xi_PTm s0) (ren_PTm xi_PTm s1)
   | PPair _ s0 s1 => PPair n_PTm (ren_PTm xi_PTm s0) (ren_PTm xi_PTm s1)
   | PProj _ s0 s1 => PProj n_PTm s0 (ren_PTm xi_PTm s1)
-  | PBind _ s0 s1 s2 =>
-      PBind n_PTm s0 (ren_PTm xi_PTm s1) (ren_PTm (upRen_PTm_PTm xi_PTm) s2)
-  | PUniv _ s0 => PUniv n_PTm s0
   end.
 
 Lemma up_PTm_PTm {m : nat} {n_PTm : nat} (sigma : fin m -> PTm n_PTm) :
@@ -138,10 +102,6 @@ Fixpoint subst_PTm {m_PTm : nat} {n_PTm : nat}
   | PPair _ s0 s1 =>
       PPair n_PTm (subst_PTm sigma_PTm s0) (subst_PTm sigma_PTm s1)
   | PProj _ s0 s1 => PProj n_PTm s0 (subst_PTm sigma_PTm s1)
-  | PBind _ s0 s1 s2 =>
-      PBind n_PTm s0 (subst_PTm sigma_PTm s1)
-        (subst_PTm (up_PTm_PTm sigma_PTm) s2)
-  | PUniv _ s0 => PUniv n_PTm s0
   end.
 
 Lemma upId_PTm_PTm {m_PTm : nat} (sigma : fin m_PTm -> PTm m_PTm)
@@ -180,10 +140,6 @@ Fixpoint idSubst_PTm {m_PTm : nat} (sigma_PTm : fin m_PTm -> PTm m_PTm)
         (idSubst_PTm sigma_PTm Eq_PTm s1)
   | PProj _ s0 s1 =>
       congr_PProj (eq_refl s0) (idSubst_PTm sigma_PTm Eq_PTm s1)
-  | PBind _ s0 s1 s2 =>
-      congr_PBind (eq_refl s0) (idSubst_PTm sigma_PTm Eq_PTm s1)
-        (idSubst_PTm (up_PTm_PTm sigma_PTm) (upId_PTm_PTm _ Eq_PTm) s2)
-  | PUniv _ s0 => congr_PUniv (eq_refl s0)
   end.
 
 Lemma upExtRen_PTm_PTm {m : nat} {n : nat} (xi : fin m -> fin n)
@@ -224,11 +180,6 @@ ren_PTm xi_PTm s = ren_PTm zeta_PTm s :=
         (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1)
   | PProj _ s0 s1 =>
       congr_PProj (eq_refl s0) (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1)
-  | PBind _ s0 s1 s2 =>
-      congr_PBind (eq_refl s0) (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1)
-        (extRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm)
-           (upExtRen_PTm_PTm _ _ Eq_PTm) s2)
-  | PUniv _ s0 => congr_PUniv (eq_refl s0)
   end.
 
 Lemma upExt_PTm_PTm {m : nat} {n_PTm : nat} (sigma : fin m -> PTm n_PTm)
@@ -270,11 +221,6 @@ subst_PTm sigma_PTm s = subst_PTm tau_PTm s :=
         (ext_PTm sigma_PTm tau_PTm Eq_PTm s1)
   | PProj _ s0 s1 =>
       congr_PProj (eq_refl s0) (ext_PTm sigma_PTm tau_PTm Eq_PTm s1)
-  | PBind _ s0 s1 s2 =>
-      congr_PBind (eq_refl s0) (ext_PTm sigma_PTm tau_PTm Eq_PTm s1)
-        (ext_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm)
-           (upExt_PTm_PTm _ _ Eq_PTm) s2)
-  | PUniv _ s0 => congr_PUniv (eq_refl s0)
   end.
 
 Lemma up_ren_ren_PTm_PTm {k : nat} {l : nat} {m : nat} (xi : fin k -> fin l)
@@ -316,12 +262,6 @@ Fixpoint compRenRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
   | PProj _ s0 s1 =>
       congr_PProj (eq_refl s0)
         (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1)
-  | PBind _ s0 s1 s2 =>
-      congr_PBind (eq_refl s0)
-        (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1)
-        (compRenRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm)
-           (upRen_PTm_PTm rho_PTm) (up_ren_ren _ _ _ Eq_PTm) s2)
-  | PUniv _ s0 => congr_PUniv (eq_refl s0)
   end.
 
 Lemma up_ren_subst_PTm_PTm {k : nat} {l : nat} {m_PTm : nat}
@@ -372,12 +312,6 @@ Fixpoint compRenSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
   | PProj _ s0 s1 =>
       congr_PProj (eq_refl s0)
         (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1)
-  | PBind _ s0 s1 s2 =>
-      congr_PBind (eq_refl s0)
-        (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1)
-        (compRenSubst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm tau_PTm)
-           (up_PTm_PTm theta_PTm) (up_ren_subst_PTm_PTm _ _ _ Eq_PTm) s2)
-  | PUniv _ s0 => congr_PUniv (eq_refl s0)
   end.
 
 Lemma up_subst_ren_PTm_PTm {k : nat} {l_PTm : nat} {m_PTm : nat}
@@ -448,12 +382,6 @@ ren_PTm zeta_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s :=
   | PProj _ s0 s1 =>
       congr_PProj (eq_refl s0)
         (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1)
-  | PBind _ s0 s1 s2 =>
-      congr_PBind (eq_refl s0)
-        (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1)
-        (compSubstRen_PTm (up_PTm_PTm sigma_PTm) (upRen_PTm_PTm zeta_PTm)
-           (up_PTm_PTm theta_PTm) (up_subst_ren_PTm_PTm _ _ _ Eq_PTm) s2)
-  | PUniv _ s0 => congr_PUniv (eq_refl s0)
   end.
 
 Lemma up_subst_subst_PTm_PTm {k : nat} {l_PTm : nat} {m_PTm : nat}
@@ -526,12 +454,6 @@ subst_PTm tau_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s :=
   | PProj _ s0 s1 =>
       congr_PProj (eq_refl s0)
         (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1)
-  | PBind _ s0 s1 s2 =>
-      congr_PBind (eq_refl s0)
-        (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1)
-        (compSubstSubst_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm)
-           (up_PTm_PTm theta_PTm) (up_subst_subst_PTm_PTm _ _ _ Eq_PTm) s2)
-  | PUniv _ s0 => congr_PUniv (eq_refl s0)
   end.
 
 Lemma renRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
@@ -644,11 +566,6 @@ Fixpoint rinst_inst_PTm {m_PTm : nat} {n_PTm : nat}
         (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1)
   | PProj _ s0 s1 =>
       congr_PProj (eq_refl s0) (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1)
-  | PBind _ s0 s1 s2 =>
-      congr_PBind (eq_refl s0) (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1)
-        (rinst_inst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm sigma_PTm)
-           (rinstInst_up_PTm_PTm _ _ Eq_PTm) s2)
-  | PUniv _ s0 => congr_PUniv (eq_refl s0)
   end.
 
 Lemma rinstInst'_PTm {m_PTm : nat} {n_PTm : nat}
@@ -720,6 +637,30 @@ Proof.
 exact (fun x => eq_refl).
 Qed.
 
+Inductive Ty : Type :=
+  | Fun : Ty -> Ty -> Ty
+  | Prod : Ty -> Ty -> Ty
+  | Void : Ty.
+
+Lemma congr_Fun {s0 : Ty} {s1 : Ty} {t0 : Ty} {t1 : Ty} (H0 : s0 = t0)
+  (H1 : s1 = t1) : Fun s0 s1 = Fun t0 t1.
+Proof.
+exact (eq_trans (eq_trans eq_refl (ap (fun x => Fun x s1) H0))
+         (ap (fun x => Fun t0 x) H1)).
+Qed.
+
+Lemma congr_Prod {s0 : Ty} {s1 : Ty} {t0 : Ty} {t1 : Ty} (H0 : s0 = t0)
+  (H1 : s1 = t1) : Prod s0 s1 = Prod t0 t1.
+Proof.
+exact (eq_trans (eq_trans eq_refl (ap (fun x => Prod x s1) H0))
+         (ap (fun x => Prod t0 x) H1)).
+Qed.
+
+Lemma congr_Void : Void = Void.
+Proof.
+exact (eq_refl).
+Qed.
+
 Class Up_PTm X Y :=
     up_PTm : X -> Y.
 
@@ -855,10 +796,6 @@ Core.
 
 Arguments VarPTm {n_PTm}.
 
-Arguments PUniv {n_PTm}.
-
-Arguments PBind {n_PTm}.
-
 Arguments PProj {n_PTm}.
 
 Arguments PPair {n_PTm}.
@@ -867,9 +804,9 @@ Arguments PApp {n_PTm}.
 
 Arguments PAbs {n_PTm}.
 
-#[global]Hint Opaque subst_PTm: rewrite.
+#[global] Hint Opaque subst_PTm: rewrite.
 
-#[global]Hint Opaque ren_PTm: rewrite.
+#[global] Hint Opaque ren_PTm: rewrite.
 
 End Extra.
 

theories/fp_red.v

@@ -47,13 +47,7 @@ Module EPar.
     R a0 a1 ->
     R (PProj p a0) (PProj p a1)
   | VarTm i :
-    R (VarPTm i) (VarPTm i)
+    R (VarPTm i) (VarPTm i).
-  | Univ i :
-    R (PUniv i) (PUniv i)
-  | BindCong p A0 A1 B0 B1 :
-    R A0 A1 ->
-    R B0 B1 ->
-    R (PBind p A0 B0) (PBind p A1 B1).
 
   Lemma refl n (a : PTm n) : R a a.
   Proof.
@@ -132,12 +126,6 @@ with SN  {n} : PTm n -> Prop :=
   TRedSN a b ->
   SN b ->
   SN a
-| N_Bind p A B :
-  SN A ->
-  SN B ->
-  SN (PBind p A B)
-| N_Univ i :
-  SN (PUniv i)
 with TRedSN {n} : PTm n -> PTm n -> Prop :=
 | N_β a b :
   SN b ->
@@ -158,63 +146,6 @@ with TRedSN {n} : PTm n -> PTm n -> Prop :=
 
 Derive Dependent Inversion tred_inv with (forall n (a b : PTm n), TRedSN a b) Sort Prop.
 
-Definition ishf {n} (a : PTm n) :=
-  match a with
-  | PPair _ _ => true
-  | PAbs _ => true
-  | PUniv _ => true
-  | PBind _ _ _ => true
-  | _ => false
-  end.
-
-Definition ispair {n} (a : PTm n) :=
-  match a with
-  | PPair _ _ => true
-  | _ => false
-  end.
-
-Definition isabs {n} (a : PTm n) :=
-  match a with
-  | PAbs _ => true
-  | _ => false
-  end.
-
-Definition ishf_ren n m (a : PTm n)  (ξ : fin n -> fin m) :
-  ishf (ren_PTm ξ a) = ishf a.
-Proof. case : a => //=. Qed.
-
-Definition isabs_ren n m (a : PTm n)  (ξ : fin n -> fin m) :
-  isabs (ren_PTm ξ a) = isabs a.
-Proof. case : a => //=. Qed.
-
-Definition ispair_ren n m (a : PTm n)  (ξ : fin n -> fin m) :
-  ispair (ren_PTm ξ a) = ispair a.
-Proof. case : a => //=. Qed.
-
-
-Lemma PProj_imp n p a :
-  @ishf n a ->
-  ~~ ispair a ->
-  ~ SN (PProj p a).
-Proof.
-  move => + + h. move E  : (PProj p a) h => u h.
-  move : p a E.
-  elim : n u / h => //=.
-  hauto lq:on inv:SNe,PTm.
-  hauto lq:on inv:TRedSN.
-Qed.
-
-Lemma PAbs_imp n a b :
-  @ishf n a ->
-  ~~ isabs a ->
-  ~ SN (PApp a b).
-Proof.
-  move => + + h. move E : (PApp a b) h => u h.
-  move : a b E. elim  : n u /h=>//=.
-  hauto lq:on inv:SNe,PTm.
-  hauto lq:on inv:TRedSN.
-Qed.
-
 Lemma PProjAbs_imp n p (a : PTm (S n)) :
   ~ SN (PProj p (PAbs a)).
 Proof.
@@ -225,7 +156,7 @@ Proof.
   hauto lq:on inv:TRedSN.
 Qed.
 
-Lemma PAppPair_imp n (a b0 b1 : PTm n ) :
+Lemma PProjPair_imp n (a b0 b1 : PTm n ) :
   ~ SN (PApp (PPair b0 b1) a).
 Proof.
   move E : (PApp (PPair b0 b1) a) => u hu.
@@ -235,26 +166,6 @@ Proof.
   hauto lq:on inv:TRedSN.
 Qed.
 
-Lemma PAppBind_imp n p (A : PTm n) B b :
-  ~ SN (PApp (PBind p A B) b).
-Proof.
-  move E :(PApp (PBind p A B) b) => u hu.
-  move : p A B b E.
-  elim : n u /hu=> //=.
-  hauto lq:on inv:SNe.
-  hauto lq:on inv:TRedSN.
-Qed.
-
-Lemma PProjBind_imp n p p' (A : PTm n) B :
-  ~ SN (PProj p (PBind p' A B)).
-Proof.
-  move E :(PProj p (PBind p' A B)) => u hu.
-  move : p p' A B E.
-  elim : n u /hu=>//=.
-  hauto lq:on inv:SNe.
-  hauto lq:on inv:TRedSN.
-Qed.
-
 Scheme sne_ind := Induction for SNe Sort Prop
   with sn_ind := Induction for SN Sort Prop
   with sred_ind := Induction for TRedSN Sort Prop.
@@ -268,8 +179,6 @@ Fixpoint ne {n} (a : PTm n) :=
   | PAbs a => false
   | PPair _ _ => false
   | PProj _ a => ne a
-  | PUniv _ => false
-  | PBind _ _ _ => false
   end
 with nf {n} (a : PTm n) :=
   match a with
@@ -278,8 +187,6 @@ with nf {n} (a : PTm n) :=
   | PAbs a => nf a
   | PPair a b => nf a && nf b
   | PProj _ a => ne a
-  | PUniv _ => true
-  | PBind _ A B => nf A && nf B
 end.
 
 Lemma ne_nf n a : @ne n a -> nf a.
@@ -443,8 +350,6 @@ Proof.
     + sauto lq:on.
   - sauto lq:on.
   - sauto lq:on.
-  - sauto lq:on.
-  - sauto lq:on.
   - move => a b ha iha c h0.
     inversion h0; subst.
     inversion H1; subst.
@@ -505,13 +410,7 @@ Module RRed.
     R (PPair a b0) (PPair a b1)
   | ProjCong p a0 a1 :
     R a0 a1 ->
-    R (PProj p a0) (PProj p a1)
+    R (PProj p a0) (PProj p a1).
-  | BindCong0 p A0 A1 B :
-    R A0 A1 ->
-    R (PBind p A0 B) (PBind p A1 B)
-  | BindCong1 p A B0 B1 :
-    R B0 B1 ->
-    R (PBind p A B0) (PBind p A B1).
 
   Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop.
 
@@ -589,13 +488,7 @@ Module RPar.
     R a0 a1 ->
     R (PProj p a0) (PProj p a1)
   | VarTm i :
-    R (VarPTm i) (VarPTm i)
+    R (VarPTm i) (VarPTm i).
-  | Univ i :
-    R (PUniv i) (PUniv i)
-  | BindCong p A0 A1 B0 B1 :
-    R A0 A1 ->
-    R B0 B1 ->
-    R (PBind p A0 B0) (PBind p A1 B1).
 
   Lemma refl n (a : PTm n) : R a a.
   Proof.
@@ -688,8 +581,6 @@ Module RPar.
     | PPair a b => PPair (tstar a) (tstar b)
     | PProj p (PPair a b) => if p is PL then (tstar a) else (tstar b)
     | PProj p a => PProj p (tstar a)
-    | PUniv i => PUniv i
-    | PBind p A B => PBind p (tstar A) (tstar B)
     end.
 
   Lemma triangle n (a b : PTm n) :
@@ -718,8 +609,6 @@ Module RPar.
         elim /inv : ha => //=_ > ? ? [*]. subst.
         apply : ProjPair'; eauto using refl.
     - hauto lq:on ctrs:R inv:R.
-    - hauto lq:on ctrs:R inv:R.
-    - hauto lq:on ctrs:R inv:R.
   Qed.
 
   Lemma diamond n (a b c : PTm n) :
@@ -740,8 +629,6 @@ Proof.
   - hauto lq:on ctrs:SN inv:RPar.R.
   - hauto lq:on ctrs:SN.
   - hauto q:on ctrs:SN inv:SN, TRedSN'.
-  - hauto lq:on ctrs:SN inv:RPar.R.
-  - hauto lq:on ctrs:SN inv:RPar.R.
   - move => a b ha iha hb ihb.
     elim /RPar.inv : ihb => //=_.
     + move => a0 a1 b0 b1 ha0 hb0 [*]. subst.
@@ -763,6 +650,91 @@ Proof.
   - sauto.
 Qed.
 
+Module EPar'.
+  Inductive R {n} : PTm n -> PTm n ->  Prop :=
+  (****************** Eta ***********************)
+  | AppEta a :
+    R (PAbs (PApp (ren_PTm shift a) (VarPTm var_zero))) a
+  | PairEta a :
+    R (PPair (PProj PL a) (PProj PR a)) a
+  (*************** Congruence ********************)
+  | AbsCong a0 a1 :
+    R a0 a1 ->
+    R (PAbs a0) (PAbs a1)
+  | AppCong0 a0 a1 b :
+    R a0 a1 ->
+    R (PApp a0 b) (PApp a1 b)
+  | AppCong1 a b0 b1 :
+    R b0 b1 ->
+    R (PApp a b0) (PApp a b1)
+  | PairCong0 a0 a1 b :
+    R a0 a1 ->
+    R (PPair a0 b) (PPair a1 b)
+  | PairCong1 a b0 b1 :
+    R b0 b1 ->
+    R (PPair a b0) (PPair a b1)
+  | ProjCong p a0 a1 :
+    R a0 a1 ->
+    R (PProj p a0) (PProj p a1).
+
+  Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop.
+
+  Lemma AppEta' n a (u : PTm n) :
+    u = (PAbs (PApp (ren_PTm shift a) (VarPTm var_zero))) ->
+    R u a.
+  Proof. move => ->. apply AppEta. Qed.
+
+  Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) :
+    R a b -> R (ren_PTm ξ a) (ren_PTm ξ b).
+  Proof.
+    move => h. move : m ξ.
+    elim : n a b /h.
+
+    move => n a m ξ /=.
+    eapply AppEta'; eauto. by asimpl.
+    all : qauto ctrs:R.
+  Qed.
+
+  Lemma morphing_ren n m p (ρ0 ρ1 : fin n -> PTm m) (ξ : fin m -> fin p) :
+    (forall i, R (ρ0 i) (ρ1 i)) ->
+    (forall i, R ((funcomp (ren_PTm ξ) ρ0) i) ((funcomp (ren_PTm ξ) ρ1) i)).
+  Proof. eauto using renaming. Qed.
+
+End EPar'.
+
+Module EPars.
+
+  #[local]Ltac solve_s_rec :=
+  move => *; eapply rtc_l; eauto;
+         hauto lq:on ctrs:EPar'.R.
+
+  #[local]Ltac solve_s :=
+    repeat (induction 1; last by solve_s_rec); apply rtc_refl.
+
+  Lemma AbsCong n (a b : PTm (S n)) :
+    rtc EPar'.R a b ->
+    rtc EPar'.R (PAbs a) (PAbs b).
+  Proof. solve_s. Qed.
+
+  Lemma AppCong n (a0 a1 b0 b1 : PTm n) :
+    rtc EPar'.R a0 a1 ->
+    rtc EPar'.R b0 b1 ->
+    rtc EPar'.R (PApp a0 b0) (PApp a1 b1).
+  Proof. solve_s. Qed.
+
+  Lemma PairCong n (a0 a1 b0 b1 : PTm n) :
+    rtc EPar'.R a0 a1 ->
+    rtc EPar'.R b0 b1 ->
+    rtc EPar'.R (PPair a0 b0) (PPair a1 b1).
+  Proof. solve_s. Qed.
+
+  Lemma ProjCong n p (a0 a1  : PTm n) :
+    rtc EPar'.R a0 a1 ->
+    rtc EPar'.R (PProj p a0) (PProj p a1).
+  Proof. solve_s. Qed.
+
+End EPars.
+
 Module RReds.
 
   #[local]Ltac solve_s_rec :=
@@ -794,12 +766,6 @@ Module RReds.
     rtc RRed.R (PProj p a0) (PProj p a1).
   Proof. solve_s. Qed.
 
-  Lemma BindCong n p (A0 A1 : PTm n) B0 B1 :
-    rtc RRed.R A0 A1 ->
-    rtc RRed.R B0 B1 ->
-    rtc RRed.R (PBind p A0 B0) (PBind p A1 B1).
-  Proof. solve_s. Qed.
-
   Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) :
     rtc RRed.R a b -> rtc RRed.R (ren_PTm ξ a) (ren_PTm ξ b).
   Proof.
@@ -809,7 +775,7 @@ Module RReds.
   Lemma FromRPar n (a b : PTm n) (h : RPar.R a b) :
     rtc RRed.R a b.
   Proof.
-    elim : n a b /h; eauto using AbsCong, AppCong, PairCong, ProjCong, rtc_refl, BindCong.
+    elim : n a b /h; eauto using AbsCong, AppCong, PairCong, ProjCong, rtc_refl.
     move => n a0 a1 b0 b1 ha iha hb ihb.
     apply : rtc_r; last by apply RRed.AppAbs.
     by eauto using AppCong, AbsCong.
@@ -840,6 +806,19 @@ Proof.
   move : m ξ. elim : n / a => //=; solve [hauto b:on].
 Qed.
 
+Lemma ne_epar n (a b : PTm n) (h : EPar'.R a b ) :
+  (ne a -> ne b) /\ (nf a -> nf b).
+Proof.
+  elim : n a b /h=>//=; hauto qb:on use:ne_nf_ren, ne_nf.
+Qed.
+
+Definition ishf {n} (a : PTm n) :=
+  match a with
+  | PPair _ _ => true
+  | PAbs _ => true
+  | _ => false
+  end.
+
 Module NeEPar.
   Inductive R_nonelim {n} : PTm n -> PTm n ->  Prop :=
   (****************** Eta ***********************)
@@ -868,12 +847,6 @@ Module NeEPar.
     R_nonelim (PProj p a0) (PProj p a1)
   | VarTm i :
     R_nonelim (VarPTm i) (VarPTm i)
-  | Univ i :
-    R_nonelim (PUniv i) (PUniv i)
-  | BindCong p A0 A1 B0 B1 :
-    R_nonelim A0 A1 ->
-    R_nonelim B0 B1 ->
-    R_nonelim (PBind p A0 B0) (PBind p A1 B1)
   with R_elim {n} : PTm n -> PTm n -> Prop :=
   | NAbsCong a0 a1 :
     R_nonelim a0 a1 ->
@@ -890,13 +863,7 @@ Module NeEPar.
     R_elim a0 a1 ->
     R_elim (PProj p a0) (PProj p a1)
   | NVarTm i :
-    R_elim (VarPTm i) (VarPTm i)
+    R_elim (VarPTm i) (VarPTm i).
-  | NUniv i :
-    R_elim (PUniv i) (PUniv i)
-  | NBindCong p A0 A1 B0 B1 :
-    R_nonelim A0 A1 ->
-    R_nonelim B0 B1 ->
-    R_elim (PBind p A0 B0) (PBind p A1 B1).
 
   Scheme epar_elim_ind := Induction for R_elim Sort Prop
       with epar_nonelim_ind := Induction for R_nonelim Sort Prop.
@@ -911,10 +878,9 @@ Module NeEPar.
     - move => a0 a1 b0 b1 h ih h' ih' /andP [h0 h1].
       have hb0 : nf b0 by eauto.
       suff : ne a0 by qauto b:on.
-      hauto q:on inv:R_elim.
+      qauto l:on inv:R_elim.
     - hauto lb:on.
     - hauto lq:on inv:R_elim.
-    - hauto b:on.
     - move => a0 a1 /negP ha' ha ih ha1.
       have {ih} := ih ha1.
       move => ha0.
@@ -931,7 +897,6 @@ Module NeEPar.
       move : ha h0. hauto lq:on inv:R_elim.
     - hauto lb: on drew: off.
     - hauto lq:on rew:off inv:R_elim.
-    - sfirstorder b:on.
   Qed.
 
   Lemma R_nonelim_nothf n (a b : PTm n) :
@@ -962,17 +927,11 @@ Module Type NoForbid.
 
   Axiom P_EPar : forall n (a b : PTm n), EPar.R a b -> P a -> P b.
   Axiom P_RRed : forall n (a b : PTm n), RRed.R a b -> P a -> P b.
-  (* Axiom P_AppPair : forall n (a b c : PTm n), ~ P (PApp (PPair a b) c). *)
+  Axiom P_AppPair : forall n (a b c : PTm n), ~ P (PApp (PPair a b) c).
-  (* Axiom P_ProjAbs : forall n p (a : PTm (S n)), ~ P (PProj p (PAbs a)). *)
+  Axiom P_ProjAbs : forall n p (a : PTm (S n)), ~ P (PProj p (PAbs a)).
-  (* Axiom P_ProjBind : forall n p p' (A : PTm n) B, ~ P (PProj p (PBind p' A B)). *)
-  (* Axiom P_AppBind : forall n p (A : PTm n) B b, ~ P (PApp (PBind p A B) b). *)
-  Axiom PAbs_imp : forall n a b, @ishf n a -> ~~ isabs a -> ~ P (PApp a b).
-  Axiom PProj_imp : forall  n p a, @ishf n a -> ~~ ispair a -> ~ P (PProj p a).
 
   Axiom P_AppInv : forall n (a b : PTm n), P (PApp a b) -> P a /\ P b.
   Axiom P_AbsInv : forall n (a : PTm (S n)), P (PAbs a) -> P a.
-  Axiom P_BindInv : forall n p (A : PTm n) B, P (PBind p A B) -> P A /\ P B.
-
   Axiom P_PairInv : forall n (a b : PTm n), P (PPair a b) -> P a /\ P b.
   Axiom P_ProjInv : forall n p (a : PTm n), P (PProj p a) -> P a.
   Axiom P_renaming : forall n m (ξ : fin n -> fin m) a , P (ren_PTm ξ a) <-> P a.
@@ -1011,10 +970,11 @@ Module SN_NoForbid <: NoForbid.
   Lemma P_RRed : forall n (a b : PTm n), RRed.R a b -> P a -> P b.
   Proof. hauto q:on use:red_sn_preservation, RPar.FromRRed. Qed.
 
-  Lemma PAbs_imp : forall n a b, @ishf n a -> ~~ isabs a -> ~ P (PApp a b).
+  Lemma P_AppPair : forall n (a b c : PTm n), ~ P (PApp (PPair a b) c).
-    sfirstorder use:fp_red.PAbs_imp. Qed.
+  Proof. sfirstorder use:PProjPair_imp. Qed.
-  Lemma PProj_imp : forall  n p a, @ishf n a -> ~~ ispair a -> ~ P (PProj p a).
+
-    sfirstorder use:fp_red.PProj_imp. Qed.
+  Lemma P_ProjAbs : forall n p (a : PTm (S n)), ~ P (PProj p (PAbs a)).
+  Proof. sfirstorder use:PProjAbs_imp. Qed.
 
   Lemma P_AppInv : forall n (a b : PTm n), P (PApp a b) -> P a /\ P b.
   Proof. sfirstorder use:SN_AppInv. Qed.
@@ -1026,13 +986,6 @@ Module SN_NoForbid <: NoForbid.
   Lemma P_ProjInv : forall n p (a : PTm n), P (PProj p a) -> P a.
   Proof. sfirstorder use:SN_ProjInv. Qed.
 
-  Lemma P_BindInv : forall n p (A : PTm n) B, P (PBind p A B) -> P A /\ P B.
-  Proof.
-    move => n p A B.
-    move E : (PBind p A B) => u hu.
-    move : p A B E. elim : n u /hu=>//=;sauto lq:on rew:off.
-  Qed.
-
   Lemma P_AbsInv : forall n (a : PTm (S n)), P (PAbs a) -> P a.
   Proof.
     move => n a. move E : (PAbs a) => u h.
@@ -1043,19 +996,13 @@ Module SN_NoForbid <: NoForbid.
   Lemma P_renaming : forall n m (ξ : fin n -> fin m) a , P (ren_PTm ξ a) <-> P  a.
   Proof. hauto lq:on use:sn_antirenaming, sn_renaming. Qed.
 
-  Lemma P_ProjBind : forall n p p' (A : PTm n) B, ~ P (PProj p (PBind p' A B)).
-  Proof. sfirstorder use:PProjBind_imp. Qed.
-
-  Lemma P_AppBind : forall n p (A : PTm n) B b, ~ P (PApp (PBind p A B) b).
-  Proof. sfirstorder use:PAppBind_imp. Qed.
-
 End SN_NoForbid.
 
 Module NoForbid_FactSN := NoForbid_Fact SN_NoForbid.
 
 Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
   Import M MFacts.
-  #[local]Hint Resolve P_EPar P_RRed PAbs_imp PProj_imp : forbid.
+  #[local]Hint Resolve P_EPar P_RRed P_AppPair P_ProjAbs : forbid.
 
   Lemma η_split n (a0 a1 : PTm n) :
     EPar.R a0 a1 ->
@@ -1073,8 +1020,9 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
       by eauto using RReds.renaming.
       apply NeEPar.AppEta=>//.
       sfirstorder use:NeEPar.R_nonelim_nothf.
-      case /orP : (orbN (isabs b)).
+
-      + case : b ih0 ih1 => //= p ih0 ih1 _ _.
+      case : b ih0 ih1 => //=.
+      + move => p ih0 ih1 _.
         set q := PAbs _.
         suff : rtc RRed.R q (PAbs p) by sfirstorder.
         subst q.
@@ -1085,14 +1033,16 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
         apply : RRed.AbsCong => /=.
         apply RRed.AppAbs'. by asimpl.
       (* violates SN *)
-      + move /P_AbsInv in hP.
+      + move => p p0 h. exfalso.
-        have {}hP : P (PApp (ren_PTm shift b) (VarPTm var_zero))
+        have : P (PApp (ren_PTm shift a0) (VarPTm var_zero))
-          by sfirstorder use:P_RReds, RReds.AppCong, @rtc_refl, RReds.renaming.
+          by sfirstorder use:P_AbsInv.
-        move => ? ?.
+
-        have ? : ~~ isabs (ren_PTm shift b) by scongruence use:isabs_ren.
+        have : rtc RRed.R (PApp (ren_PTm shift a0) (VarPTm var_zero))
-        have ? : ishf (ren_PTm shift b) by scongruence use:ishf_ren.
+                 (PApp (ren_PTm shift (PPair p p0)) (VarPTm var_zero))
-        exfalso.
+          by hauto lq:on use:RReds.AppCong, RReds.renaming, rtc_refl.
-        sfirstorder use:PAbs_imp.
+
+        move : P_RReds. repeat move/[apply] => /=.
+        hauto l:on use:P_AppPair.
     - move => n a0 a1 h ih /[dup] hP.
       move /P_PairInv => [/P_ProjInv + _].
       move : ih => /[apply].
@@ -1101,9 +1051,16 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
       exists (PPair (PProj PL b) (PProj PR b)).
       split. sfirstorder use:RReds.PairCong,RReds.ProjCong.
       hauto lq:on ctrs:NeEPar.R_nonelim use:NeEPar.R_nonelim_nothf.
-      case /orP : (orbN (ispair b)).
+
-      + case : b ih0 ih1 => //=.
+      case : b ih0 ih1 => //=.
-        move => t0 t1 ih0 h1 _ _.
+      (* violates SN *)
+      + move => p ?. exfalso.
+        have {}hP : P (PProj PL a0) by sfirstorder use:P_PairInv.
+        have : rtc RRed.R (PProj PL a0) (PProj PL (PAbs p))
+          by eauto using RReds.ProjCong.
+        move : P_RReds hP. repeat move/[apply] => /=.
+        sfirstorder use:P_ProjAbs.
+      + move => t0 t1 ih0 h1 _.
         exists (PPair t0 t1).
         split => //=.
         apply RReds.PairCong.
@@ -1111,12 +1068,6 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
         apply RRed.ProjPair.
         apply : rtc_r; eauto using RReds.ProjCong.
         apply RRed.ProjPair.
-      + move => ? ?. exfalso.
-        move/P_PairInv : hP=>[hP _].
-        have : rtc RRed.R (PProj PL a0) (PProj PL b)
-          by eauto using RReds.ProjCong.
-        move : P_RReds hP. repeat move/[apply] => /=.
-        sfirstorder use:PProj_imp.
     - hauto lq:on ctrs:NeEPar.R_nonelim use:RReds.AbsCong, P_AbsInv.
     - move => n a0 a1 b0 b1 ha iha hb ihb.
       move => /[dup] hP /P_AppInv [hP0 hP1].
@@ -1125,9 +1076,8 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
       case /orP : (orNb (ishf a2)) => [h|].
       + exists (PApp a2 b2). split; first by eauto using RReds.AppCong.
         hauto lq:on ctrs:NeEPar.R_nonelim use:NeEPar.R_nonelim_nothf.
-      + case /orP : (orbN (isabs a2)).
+      + case : a2 iha0 iha1 => //=.
-        (* case : a2 iha0 iha1 => //=. *)
+        * move => p h0 h1 _.
-        * case : a2 iha0 iha1 => //= p h0 h1 _ _.
           inversion h1; subst.
           ** exists (PApp a2 b2).
              split.
@@ -1137,9 +1087,11 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
              hauto lq:on ctrs:NeEPar.R_nonelim.
           ** hauto lq:on ctrs:NeEPar.R_nonelim,NeEPar.R_elim use:RReds.AppCong.
         (* Impossible *)
-        * move =>*. exfalso.
+        * move => u0 u1 h. exfalso.
-          have : P (PApp a2 b0) by sfirstorder use:RReds.AppCong, @rtc_refl, P_RReds.
+          have : rtc RRed.R (PApp a0 b0) (PApp (PPair u0 u1) b0)
-          sfirstorder use:PAbs_imp.
+            by hauto lq:on ctrs:rtc use:RReds.AppCong.
+          move : P_RReds hP; repeat move/[apply].
+          sfirstorder use:P_AppPair.
     - hauto lq:on ctrs:NeEPar.R_nonelim use:RReds.PairCong, P_PairInv.
     - move => n p a0 a1 ha ih /[dup] hP /P_ProjInv.
       move : ih => /[apply]. move => [a2 [iha0 iha1]].
@@ -1148,13 +1100,13 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
       split.  eauto using RReds.ProjCong.
       qauto l:on ctrs:NeEPar.R_nonelim, NeEPar.R_elim use:NeEPar.R_nonelim_nothf.
 
-      case /orP : (orNb (ispair a2)).
+      case : a2 iha0 iha1 => //=.
-      + move => *. exfalso.
+      + move => u iha0. exfalso.
-        have : rtc RRed.R (PProj p a0) (PProj p a2)
+        have : rtc RRed.R (PProj p a0) (PProj p (PAbs u))
           by sfirstorder use:RReds.ProjCong ctrs:rtc.
         move : P_RReds hP. repeat move/[apply].
-        sfirstorder use:PProj_imp.
+        sfirstorder use:P_ProjAbs.
-      + case : a2 iha0 iha1 => //= u0 u1 iha0 iha1 _ _.
+      + move => u0 u1 iha0 iha1 _.
         inversion iha1; subst.
         * exists (PProj p a2). split.
           apply : rtc_r.
@@ -1163,8 +1115,6 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
           hauto lq:on ctrs:NeEPar.R_nonelim.
         * hauto lq:on ctrs:NeEPar.R_nonelim,NeEPar.R_elim use:RReds.ProjCong.
     - hauto lq:on ctrs:rtc, NeEPar.R_nonelim.
-    - hauto l:on.
-    - hauto lq:on ctrs:NeEPar.R_nonelim, rtc use:RReds.BindCong, P_BindInv.
   Qed.
 
 
@@ -1218,7 +1168,7 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
           have : rtc RRed.R (PApp a0 b0) (PApp (PPair (PProj PL a1) (PProj PR a1)) b0)
             by qauto l:on ctrs:rtc use:RReds.AppCong.
           move : P_RReds hP. repeat move/[apply].
-          sfirstorder use:PAbs_imp.
+          sfirstorder use:P_AppPair.
         * exists (subst_PTm (scons b0 VarPTm) a1).
           split.
           apply : rtc_r; last by apply RRed.AppAbs.
@@ -1245,7 +1195,7 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
         move : η_split hP'  ha; repeat move/[apply].
         move => [a1 [h0 h1]].
         inversion h1; subst.
-        * sauto q:on ctrs:rtc use:RReds.ProjCong, PProj_imp, P_RReds.
+        * qauto l:on ctrs:rtc use:RReds.ProjCong, P_ProjAbs, P_RReds.
         * inversion H0; subst.
           exists (if p is PL then a1 else b1).
           split; last by scongruence use:NeEPar.ToEPar.
@@ -1270,8 +1220,6 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
         move : iha hP' h0;repeat move/[apply].
         hauto lq:on ctrs:rtc, EPar.R use:RReds.ProjCong.
     - hauto lq:on inv:RRed.R.
-    - hauto lq:on inv:RRed.R ctrs:rtc.
-    - sauto lq:on ctrs:EPar.R, rtc use:RReds.BindCong, P_BindInv, @relations.rtc_transitive.
   Qed.
 
   Lemma η_postponement_star n a b c :
@@ -1308,6 +1256,7 @@ End UniqueNF.
 
 Module SN_UniqueNF := UniqueNF SN_NoForbid NoForbid_FactSN.
 
+
 Module ERed.
   Inductive R {n} : PTm n -> PTm n ->  Prop :=
 
@@ -1335,13 +1284,7 @@ Module ERed.
     R (PPair a b0) (PPair a b1)
   | ProjCong p a0 a1 :
     R a0 a1 ->
-    R (PProj p a0) (PProj p a1)
+    R (PProj p a0) (PProj p a1).
-  | BindCong0 p A0 A1 B :
-    R A0 A1 ->
-    R (PBind p A0 B) (PBind p A1 B)
-  | BindCong1 p A B0 B1 :
-    R B0 B1 ->
-    R (PBind p A B0) (PBind p A B1).
 
   Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop.
 
@@ -1385,13 +1328,6 @@ Module ERed.
     apply iha in h. by subst.
     destruct i, j=>//=.
     hauto l:on.
-
-    move => n p A ihA B ihB m ξ []//=.
-    move => b A0 B0  hξ [?]. subst.
-    move => ?. have ? : A0 = A by firstorder. subst.
-    move => ?. have : B = B0. apply : ihB; eauto.
-    sauto.
-    congruence.
   Qed.
 
   Lemma AppEta' n a u :
@@ -1444,14 +1380,9 @@ Module ERed.
       hauto l:on.
     - move => n a0 a1 ha iha m ξ []//= p hξ [?]. subst.
       sauto lq:on use:up_injective.
-    - move => n p A B0 B1 hB ihB m ξ + hξ.
-      case => //= p' A2 B2 [*]. subst.
-      have : (forall i j, (upRen_PTm_PTm ξ) i = (upRen_PTm_PTm ξ) j -> i = j) by sauto.
-      move => {}/ihB => ihB.
-      spec_refl.
-      sauto lq:on.
   Admitted.
 
+
 End ERed.
 
 Module EReds.
@@ -1485,13 +1416,6 @@ Module EReds.
     rtc ERed.R (PProj p a0) (PProj p a1).
   Proof. solve_s. Qed.
 
-  Lemma BindCong n p (A0 A1 : PTm n) B0 B1 :
-    rtc ERed.R A0 A1 ->
-    rtc ERed.R B0 B1 ->
-    rtc ERed.R (PBind p A0 B0) (PBind p A1 B1).
-  Proof. solve_s. Qed.
-
-
   Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) :
     rtc ERed.R a b -> rtc ERed.R (ren_PTm ξ a) (ren_PTm ξ b).
   Proof. induction 1; hauto l:on use:ERed.renaming ctrs:rtc. Qed.
@@ -1500,7 +1424,7 @@ Module EReds.
     EPar.R a b ->
     rtc ERed.R a b.
   Proof.
-    move => h. elim : n a b /h; eauto using AbsCong, AppCong, PairCong, ProjCong, rtc_refl, BindCong.
+    move => h. elim : n a b /h; eauto using AbsCong, AppCong, PairCong, ProjCong, rtc_refl.
     - move => n a0 a1 _ h.
       have {}h : rtc ERed.R (ren_PTm shift a0) (ren_PTm shift a1) by apply renaming.
       apply : rtc_r. apply AbsCong. apply AppCong; eauto. apply rtc_refl.
@@ -1549,13 +1473,7 @@ Module RERed.
     R (PPair a b0) (PPair a b1)
   | ProjCong p a0 a1 :
     R a0 a1 ->
-    R (PProj p a0) (PProj p a1)
+    R (PProj p a0) (PProj p a1).
-  | BindCong0 p A0 A1 B :
-    R A0 A1 ->
-    R (PBind p A0 B) (PBind p A1 B)
-  | BindCong1 p A B0 B1 :
-    R B0 B1 ->
-    R (PBind p A B0) (PBind p A B1).
 
   Lemma ToBetaEta n (a b : PTm n) :
     R a b ->
@@ -1631,12 +1549,6 @@ Module REReds.
     rtc RERed.R (PProj p a0) (PProj p a1).
   Proof. solve_s. Qed.
 
-  Lemma BindCong n p (A0 A1 : PTm n) B0 B1 :
-    rtc RERed.R A0 A1 ->
-    rtc RERed.R B0 B1 ->
-    rtc RERed.R (PBind p A0 B0) (PBind p A1 B1).
-  Proof. solve_s. Qed.
-
 End REReds.
 
 Module LoRed.
@@ -1670,14 +1582,7 @@ Module LoRed.
   | ProjCong p a0 a1 :
     ~~ ishf a0 ->
     R a0 a1 ->
-    R (PProj p a0) (PProj p a1)
+    R (PProj p a0) (PProj p a1).
-  | BindCong0 p A0 A1 B :
-    R A0 A1 ->
-    R (PBind p A0 B) (PBind p A1 B)
-  | BindCong1 p A B0 B1 :
-    nf A ->
-    R B0 B1 ->
-    R (PBind p A B0) (PBind p A B1).
 
   Lemma hf_preservation n (a b : PTm n) :
     LoRed.R a b ->
@@ -1744,13 +1649,6 @@ Module LoReds.
     rtc LoRed.R (PProj p a0) (PProj p a1).
   Proof. solve_s. Qed.
 
-  Lemma BindCong n p (A0 A1 : PTm n) B0 B1 :
-    rtc LoRed.R A0 A1 ->
-    rtc LoRed.R B0 B1 ->
-    nf A1 ->
-    rtc LoRed.R (PBind p A0 B0) (PBind p A1 B1).
-  Proof. solve_s. Qed.
-
   Local Ltac triv := simpl in *; itauto.
 
   Lemma FromSN_mutual : forall n,
@@ -1766,8 +1664,6 @@ Module LoReds.
     - hauto q:on use:LoReds.AbsCong solve+:triv.
     - sfirstorder use:ne_nf.
     - hauto lq:on ctrs:rtc.
-    - hauto lq:on use:LoReds.BindCong solve+:triv.
-    - hauto lq:on ctrs:rtc.
     - qauto ctrs:LoRed.R.
     - move => n a0 a1 b hb ihb h.
       have : ~~ ishf a0 by inversion h.
@@ -1791,12 +1687,10 @@ End LoReds.
 Fixpoint size_PTm {n} (a : PTm n) :=
   match a with
   | VarPTm _ => 1
-  | PAbs a => 3 + size_PTm a
+  | PAbs a => 1 + size_PTm a
   | PApp a b => 1 + Nat.add (size_PTm a) (size_PTm b)
   | PProj p a => 1 + size_PTm a
-  | PPair a b => 3 + Nat.add (size_PTm a) (size_PTm b)
+  | PPair a b => 1 + Nat.add (size_PTm a) (size_PTm b)
-  | PUniv _ => 3
-  | PBind p A B => 3 + Nat.add (size_PTm A) (size_PTm B)
   end.
 
 Lemma size_PTm_ren n m (ξ : fin n -> fin m) a : size_PTm (ren_PTm ξ a) = size_PTm a.
@@ -1881,12 +1775,6 @@ Proof.
     + hauto lq:on ctrs:ERed.R use:@relations.rtc_once.
     + hauto lq:on ctrs:rtc use:EReds.PairCong.
   - qauto l:on inv:ERed.R use:EReds.ProjCong.
-  - move => p A0 A1 B hA ihA u.
-    elim /ERed.inv => //=_;
-      hauto lq:on ctrs:rtc use:EReds.BindCong.
-  - move => p A B0 B1 hB ihB u.
-    elim /ERed.inv => //=_;
-      hauto lq:on ctrs:rtc use:EReds.BindCong.
 Qed.
 
 Lemma ered_confluence n (a b c : PTm n) :