diff --git a/syntax.sig b/syntax.sig
index 6b7e4df..e2bafac 100644
--- a/syntax.sig
+++ b/syntax.sig
@@ -1,19 +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
-PBot : PTm
\ No newline at end of file
diff --git a/theories/Autosubst2/syntax.v b/theories/Autosubst2/syntax.v
index ff9ec18..78c4fec 100644
--- a/theories/Autosubst2/syntax.v
+++ b/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,10 +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
-  | PBind : BTag -> PTm n_PTm -> PTm (S n_PTm) -> PTm n_PTm
-  | PUniv : nat -> PTm n_PTm
-  | PBot : PTm n_PTm.
+  | PProj : PTag -> PTm n_PTm -> 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.
@@ -73,28 +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 congr_PBot {m_PTm : nat} : PBot m_PTm = PBot m_PTm.
-Proof.
-exact (eq_refl).
-Qed.
-
 Lemma upRen_PTm_PTm {m : nat} {n : nat} (xi : fin m -> fin n) :
   fin (S m) -> fin (S n).
 Proof.
@@ -115,10 +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
-  | PBot _ => PBot n_PTm
   end.
 
 Lemma up_PTm_PTm {m : nat} {n_PTm : nat} (sigma : fin m -> PTm n_PTm) :
@@ -145,11 +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
-  | PBot _ => PBot n_PTm
   end.
 
 Lemma upId_PTm_PTm {m_PTm : nat} (sigma : fin m_PTm -> PTm m_PTm)
@@ -188,11 +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)
-  | PBot _ => congr_PBot
   end.
 
 Lemma upExtRen_PTm_PTm {m : nat} {n : nat} (xi : fin m -> fin n)
@@ -233,12 +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)
-  | PBot _ => congr_PBot
   end.
 
 Lemma upExt_PTm_PTm {m : nat} {n_PTm : nat} (sigma : fin m -> PTm n_PTm)
@@ -280,12 +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)
-  | PBot _ => congr_PBot
   end.
 
 Lemma up_ren_ren_PTm_PTm {k : nat} {l : nat} {m : nat} (xi : fin k -> fin l)
@@ -327,13 +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)
-  | PBot _ => congr_PBot
   end.
 
 Lemma up_ren_subst_PTm_PTm {k : nat} {l : nat} {m_PTm : nat}
@@ -384,13 +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)
-  | PBot _ => congr_PBot
   end.
 
 Lemma up_subst_ren_PTm_PTm {k : nat} {l_PTm : nat} {m_PTm : nat}
@@ -461,13 +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)
-  | PBot _ => congr_PBot
   end.
 
 Lemma up_subst_subst_PTm_PTm {k : nat} {l_PTm : nat} {m_PTm : nat}
@@ -540,13 +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)
-  | PBot _ => congr_PBot
   end.
 
 Lemma renRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
@@ -659,12 +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)
-  | PBot _ => congr_PBot
   end.
 
 Lemma rinstInst'_PTm {m_PTm : nat} {n_PTm : nat}
@@ -736,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.
 
@@ -871,12 +796,6 @@ Core.
 
 Arguments VarPTm {n_PTm}.
 
-Arguments PBot {n_PTm}.
-
-Arguments PUniv {n_PTm}.
-
-Arguments PBind {n_PTm}.
-
 Arguments PProj {n_PTm}.
 
 Arguments PPair {n_PTm}.
diff --git a/theories/fp_red.v b/theories/fp_red.v
index e22e759..062f9a6 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -47,15 +47,7 @@ Module EPar.
     R a0 a1 ->
     R (PProj p a0) (PProj p a1)
   | VarTm 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)
-  | BotCong :
-    R PBot PBot.
+    R (VarPTm i) (VarPTm i).
 
   Lemma refl n (a : PTm n) : R a a.
   Proof.
@@ -107,10 +99,6 @@ Module EPar.
     all : hauto lq:on ctrs:R use:morphing_up.
   Qed.
 
-  Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) :
-    R a b -> R (subst_PTm ρ a) (subst_PTm ρ b).
-  Proof. hauto l:on use:morphing, refl. Qed.
-
 End EPar.
 
 Inductive SNe {n} : PTm n -> Prop :=
@@ -123,8 +111,6 @@ Inductive SNe {n} : PTm n -> Prop :=
 | N_Proj p a :
   SNe a ->
   SNe (PProj p a)
-| N_Bot :
-  SNe PBot
 with SN  {n} : PTm n -> Prop :=
 | N_Pair a b :
   SN a ->
@@ -140,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 ->
@@ -166,65 +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 isbind {n} (a : PTm n) := if a is PBind _ _ _ then true else false.
-
-Definition isuniv {n} (a : PTm n) := if a is PUniv _ then true else false.
-
-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.
@@ -235,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.
@@ -245,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.
@@ -278,9 +179,6 @@ Fixpoint ne {n} (a : PTm n) :=
   | PAbs a => false
   | PPair _ _ => false
   | PProj _ a => ne a
-  | PUniv _ => false
-  | PBind _ _ _ => false
-  | PBot => true
   end
 with nf {n} (a : PTm n) :=
   match a with
@@ -289,9 +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
-  | PBot => true
 end.
 
 Lemma ne_nf n a : @ne n a -> nf a.
@@ -439,7 +334,6 @@ Proof.
   - sauto lq:on.
   - sauto lq:on.
   - sauto lq:on.
-  - sauto lq:on.
   - move => a b ha iha hb ihb b0.
     inversion 1; subst.
     + have /iha : (EPar.R (PProj PL a0) (PProj PL b0)) by sauto lq:on.
@@ -456,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.
@@ -518,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)
-  | 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).
+    R (PProj p a0) (PProj p a1).
 
   Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop.
 
@@ -571,20 +457,6 @@ Module RRed.
     R a b -> False.
   Proof. move/[swap]. induction 1; hauto qb:on inv:PTm. Qed.
 
-  Lemma FromRedSN n (a b : PTm n) :
-    TRedSN a b ->
-    RRed.R a b.
-  Proof. induction 1; hauto lq:on ctrs:RRed.R. Qed.
-
-  Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) :
-    R a b -> R (subst_PTm ρ a) (subst_PTm ρ b).
-  Proof.
-    move => h. move : m ρ. elim : n a b / h => n.
-    move => a b m ρ /=.
-    eapply AppAbs'; eauto; cycle 1. by asimpl.
-    all : hauto lq:on ctrs:R.
-  Qed.
-
 End RRed.
 
 Module RPar.
@@ -616,15 +488,7 @@ Module RPar.
     R a0 a1 ->
     R (PProj p a0) (PProj p a1)
   | VarTm 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)
-  | BotCong :
-    R PBot PBot.
+    R (VarPTm i) (VarPTm i).
 
   Lemma refl n (a : PTm n) : R a a.
   Proof.
@@ -717,9 +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)
-    | PBot => PBot
     end.
 
   Lemma triangle n (a b : PTm n) :
@@ -748,9 +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.
-    - hauto lq:on ctrs:R inv:R.
   Qed.
 
   Lemma diamond n (a b c : PTm n) :
@@ -767,13 +625,10 @@ Proof.
   - hauto l:on inv:RPar.R.
   - qauto l:on inv:RPar.R,SNe,SN ctrs:SNe.
   - hauto lq:on inv:RPar.R, SNe ctrs:SNe.
-  - hauto lq:on inv:RPar.R, SNe ctrs:SNe.
   - qauto l:on ctrs:SN inv:RPar.R.
   - 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.
@@ -795,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 :=
@@ -826,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.
@@ -841,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.
@@ -863,11 +797,6 @@ Module RReds.
     rtc RRed.R a b -> nf a -> a = b.
   Proof. induction 1; sfirstorder use:RRed.nf_imp. Qed.
 
-  Lemma FromRedSNs n (a b : PTm n) :
-    rtc TRedSN a b ->
-    rtc RRed.R a b.
-  Proof. induction 1; hauto lq:on ctrs:rtc use:RRed.FromRedSN. Qed.
-
 End RReds.
 
 
@@ -877,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 ***********************)
@@ -905,14 +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)
-  | BotCong :
-    R_nonelim PBot PBot
   with R_elim {n} : PTm n -> PTm n -> Prop :=
   | NAbsCong a0 a1 :
     R_nonelim a0 a1 ->
@@ -929,15 +863,7 @@ Module NeEPar.
     R_elim a0 a1 ->
     R_elim (PProj p a0) (PProj p a1)
   | NVarTm 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)
-  | NBotCong :
-    R_elim PBot PBot.
+    R_elim (VarPTm i) (VarPTm i).
 
   Scheme epar_elim_ind := Induction for R_elim Sort Prop
       with epar_nonelim_ind := Induction for R_nonelim Sort Prop.
@@ -952,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.
@@ -972,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) :
@@ -1003,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_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_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_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.
@@ -1052,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).
-    sfirstorder use:fp_red.PAbs_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_AppPair : forall n (a b c : PTm n), ~ P (PApp (PPair a b) c).
+  Proof. sfirstorder use:PProjPair_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.
@@ -1067,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.
@@ -1084,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 ->
@@ -1114,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.
@@ -1126,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.
-        have {}hP : P (PApp (ren_PTm shift b) (VarPTm var_zero))
-          by sfirstorder use:P_RReds, RReds.AppCong, @rtc_refl, RReds.renaming.
-        move => ? ?.
-        have ? : ~~ isabs (ren_PTm shift b) by scongruence use:isabs_ren.
-        have ? : ishf (ren_PTm shift b) by scongruence use:ishf_ren.
-        exfalso.
-        sfirstorder use:PAbs_imp.
+      + move => p p0 h. exfalso.
+        have : P (PApp (ren_PTm shift a0) (VarPTm var_zero))
+          by sfirstorder use:P_AbsInv.
+
+        have : rtc RRed.R (PApp (ren_PTm shift a0) (VarPTm var_zero))
+                 (PApp (ren_PTm shift (PPair p p0)) (VarPTm var_zero))
+          by hauto lq:on use:RReds.AppCong, RReds.renaming, rtc_refl.
+
+        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].
@@ -1142,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 => //=.
-        move => t0 t1 ih0 h1 _ _.
+
+      case : b ih0 ih1 => //=.
+      (* 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.
@@ -1152,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].
@@ -1166,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 => //= p h0 h1 _ _.
+      + case : a2 iha0 iha1 => //=.
+        * move => p h0 h1 _.
           inversion h1; subst.
           ** exists (PApp a2 b2).
              split.
@@ -1178,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.
-          have : P (PApp a2 b0) by sfirstorder use:RReds.AppCong, @rtc_refl, P_RReds.
-          sfirstorder use:PAbs_imp.
+        * move => u0 u1 h. exfalso.
+          have : rtc RRed.R (PApp a0 b0) (PApp (PPair u0 u1) b0)
+            by hauto lq:on ctrs:rtc use:RReds.AppCong.
+          move : P_RReds hP; repeat move/[apply].
+          sfirstorder use:P_AppPair.
     - hauto lq:on ctrs: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]].
@@ -1189,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)).
-      + move => *. exfalso.
-        have : rtc RRed.R (PProj p a0) (PProj p a2)
+      case : a2 iha0 iha1 => //=.
+      + move => u iha0. exfalso.
+        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.
-      + case : a2 iha0 iha1 => //= u0 u1 iha0 iha1 _ _.
+        sfirstorder use:P_ProjAbs.
+      + move => u0 u1 iha0 iha1 _.
         inversion iha1; subst.
         * exists (PProj p a2). split.
           apply : rtc_r.
@@ -1204,9 +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.
-    - hauto lq:on ctrs:NeEPar.R_nonelim, rtc use:RReds.BindCong, P_BindInv.
   Qed.
 
 
@@ -1260,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.
@@ -1287,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.
@@ -1312,9 +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.
-    - hauto lq:on inv:RRed.R ctrs:rtc.
   Qed.
 
   Lemma η_postponement_star n a b c :
@@ -1351,6 +1256,7 @@ End UniqueNF.
 
 Module SN_UniqueNF := UniqueNF SN_NoForbid NoForbid_FactSN.
 
+
 Module ERed.
   Inductive R {n} : PTm n -> PTm n ->  Prop :=
 
@@ -1378,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)
-  | 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).
+    R (PProj p a0) (PProj p a1).
 
   Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop.
 
@@ -1428,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 :
@@ -1487,22 +1380,8 @@ 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.
 
-  Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) :
-    R a b -> R (subst_PTm ρ a) (subst_PTm ρ b).
-  Proof.
-    move => h. move : m ρ. elim : n a b /h => n.
-    move => a m ρ /=.
-    eapply AppEta'; eauto. by asimpl.
-    all : hauto lq:on ctrs:R.
-  Qed.
 
 End ERed.
 
@@ -1537,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.
@@ -1552,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.
@@ -1563,17 +1435,6 @@ Module EReds.
       apply ERed.PairEta.
   Qed.
 
-  Lemma FromEPars n (a b : PTm n) :
-    rtc EPar.R a b ->
-    rtc ERed.R a b.
-  Proof. induction 1; hauto l:on use:FromEPar, @relations.rtc_transitive. Qed.
-
-  Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) :
-    rtc ERed.R a b -> rtc ERed.R (subst_PTm ρ a) (subst_PTm ρ b).
-  Proof.
-    induction 1; hauto lq:on ctrs:rtc use:ERed.substing.
-  Qed.
-
 End EReds.
 
 #[export]Hint Constructors ERed.R RRed.R EPar.R : red.
@@ -1612,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)
-  | 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).
+    R (PProj p a0) (PProj p a1).
 
   Lemma ToBetaEta n (a b : PTm n) :
     R a b ->
@@ -1646,26 +1501,6 @@ Module RERed.
     SN b.
   Proof. hauto q:on use:ToBetaEtaPar, epar_sn_preservation, red_sn_preservation, RPar.FromRRed. Qed.
 
-  Lemma bind_preservation n (a b : PTm n) :
-    R a b -> isbind a -> isbind b.
-  Proof. hauto q:on inv:R. Qed.
-
-  Lemma univ_preservation n (a b : PTm n) :
-    R a b -> isuniv a -> isuniv b.
-  Proof. hauto q:on inv:R. Qed.
-
-  Lemma sne_preservation n (a b : PTm n) :
-    R a b -> SNe a -> SNe b.
-  Proof.
-    hauto q:on use:ToBetaEtaPar, RPar.FromRRed use:red_sn_preservation, epar_sn_preservation.
-  Qed.
-
-  Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) :
-    RERed.R a b -> RERed.R (subst_PTm ρ a) (subst_PTm ρ b).
-  Proof.
-    hauto q:on use:ToBetaEta, FromBeta, FromEta, RRed.substing, ERed.substing.
-  Qed.
-
 End RERed.
 
 Module REReds.
@@ -1714,48 +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.
-
-  Lemma bind_preservation n (a b : PTm n) :
-    rtc RERed.R a b -> isbind a -> isbind b.
-  Proof. induction 1; qauto l:on ctrs:rtc use:RERed.bind_preservation. Qed.
-
-  Lemma univ_preservation n (a b : PTm n) :
-    rtc RERed.R a b -> isuniv a -> isuniv b.
-  Proof. induction 1; qauto l:on ctrs:rtc use:RERed.univ_preservation. Qed.
-
-  Lemma sne_preservation n (a b : PTm n) :
-    rtc RERed.R a b -> SNe a -> SNe b.
-  Proof. induction 1; qauto l:on ctrs:rtc use:RERed.sne_preservation. Qed.
-
-  Lemma bind_inv n p A B C :
-    rtc (@RERed.R n) (PBind p A B) C ->
-    exists A0 B0, C = PBind p A0 B0 /\ rtc RERed.R A A0 /\ rtc RERed.R B B0.
-  Proof.
-    move E : (PBind p A B) => u hu.
-    move : p A B E.
-    elim : u C / hu; sauto lq:on rew:off.
-  Qed.
-
-  Lemma univ_inv n i C :
-    rtc (@RERed.R n) (PUniv i) C  ->
-    C = PUniv i.
-  Proof.
-    move E : (PUniv i) => u hu.
-    move : i E. elim : u C / hu=>//=.
-    hauto lq:on rew:off ctrs:rtc inv:RERed.R.
-  Qed.
-
-  Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) :
-    rtc RERed.R a b -> rtc RERed.R (subst_PTm ρ a) (subst_PTm ρ b).
-  Proof.
-    induction 1; hauto lq:on ctrs:rtc use:RERed.substing.
-  Qed.
-
 End REReds.
 
 Module LoRed.
@@ -1789,14 +1582,7 @@ Module LoRed.
   | ProjCong p a0 a1 :
     ~~ ishf a0 ->
     R a0 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).
+    R (PProj p a0) (PProj p a1).
 
   Lemma hf_preservation n (a b : PTm n) :
     LoRed.R a b ->
@@ -1863,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,
@@ -1881,13 +1660,10 @@ Module LoReds.
     - hauto lq:on ctrs:rtc.
     - hauto lq:on rew:off use:LoReds.AppCong solve+:triv.
     - hauto l:on use:LoReds.ProjCong solve+:triv.
-    - hauto lq:on ctrs:rtc.
     - hauto q:on use:LoReds.PairCong solve+:triv.
     - 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.
@@ -1911,13 +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)
-  | PUniv _ => 3
-  | PBind p A B => 3 + Nat.add (size_PTm A) (size_PTm B)
-  | PBot => 1
+  | PPair a b => 1 + 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.
@@ -2002,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) :
@@ -2106,36 +1873,7 @@ Proof.
   move /REReds.FromRReds : hc0. move /REReds.FromEReds : hv'. eauto using relations.rtc_transitive.
 Qed.
 
-(* Beta joinability *)
-Module BJoin.
-  Definition R {n} (a b : PTm n) := exists c, rtc RRed.R a c /\ rtc RRed.R b c.
-  Lemma refl n (a : PTm n) : R a a.
-  Proof. sfirstorder use:@rtc_refl unfold:R. Qed.
-
-  Lemma symmetric n (a b : PTm n) : R a b -> R b a.
-  Proof. sfirstorder unfold:R. Qed.
-
-  Lemma transitive n (a b c : PTm n) : R a b -> R b c -> R a c.
-  Proof.
-    rewrite /R.
-    move => [ab [ha +]] [bc [+ hc]].
-    move : red_confluence; repeat move/[apply].
-    move => [v [h0 h1]].
-    exists v. sfirstorder use:@relations.rtc_transitive.
-  Qed.
-
-  Lemma AbsCong n (a b : PTm (S n)) :
-    R a b ->
-    R (PAbs a) (PAbs b).
-  Proof. hauto lq:on use:RReds.AbsCong unfold:R. Qed.
-
-  Lemma AppCong n (a0 a1 b0 b1 : PTm n) :
-    R a0 a1 ->
-    R b0 b1 ->
-    R (PApp a0 b0) (PApp a1 b1).
-  Proof. hauto lq:on use:RReds.AppCong unfold:R. Qed.
-End BJoin.
-
+(* "Declarative" Joinability *)
 Module DJoin.
   Definition R {n} (a b : PTm n) := exists c, rtc RERed.R a c /\ rtc RERed.R b c.
 
@@ -2176,81 +1914,4 @@ Module DJoin.
     R (PProj p a0) (PProj p a1).
   Proof. hauto q:on use:REReds.ProjCong. Qed.
 
-  Lemma FromRedSNs n (a b : PTm n) :
-    rtc TRedSN a b ->
-    R a b.
-  Proof.
-    move /RReds.FromRedSNs /REReds.FromRReds.
-    sfirstorder use:@rtc_refl unfold:R.
-  Qed.
-
-  Lemma sne_bind_noconf n (a b : PTm n) :
-    R a b -> SNe a -> isbind b -> False.
-  Proof.
-    move => [c [? ?]] *.
-    have : SNe c /\ isbind c by sfirstorder use:REReds.sne_preservation, REReds.bind_preservation.
-    qauto l:on inv:SNe.
-  Qed.
-
-  Lemma sne_univ_noconf n (a b : PTm n) :
-    R a b -> SNe a -> isuniv b -> False.
-  Proof.
-    hauto q:on use:REReds.sne_preservation,
-          REReds.univ_preservation inv:SNe.
-  Qed.
-
-  Lemma bind_univ_noconf n (a b : PTm n) :
-    R a b -> isbind a -> isuniv b -> False.
-  Proof.
-    move => [c [h0 h1]] h2 h3.
-    have {h0 h1 h2 h3} : isbind c /\ isuniv c by
-      hauto l:on use:REReds.bind_preservation,
-          REReds.univ_preservation.
-    case : c => //=; itauto.
-  Qed.
-
-  Lemma bind_inj n p0 p1 (A0 A1 : PTm n) B0 B1 :
-    DJoin.R (PBind p0 A0 B0) (PBind p1 A1 B1) ->
-    p0 = p1 /\ DJoin.R A0 A1 /\ DJoin.R B0 B1.
-  Proof.
-    rewrite /R.
-    hauto lq:on rew:off use:REReds.bind_inv.
-  Qed.
-
-  Lemma univ_inj n i j :
-    @R n (PUniv i) (PUniv j)  -> i = j.
-  Proof.
-    sauto lq:on rew:off use:REReds.univ_inv.
-  Qed.
-
-  Lemma FromRRed0 n (a b : PTm n) :
-    RRed.R a b -> R a b.
-  Proof.
-    hauto lq:on ctrs:rtc use:RERed.FromBeta unfold:R.
-  Qed.
-
-  Lemma FromRRed1 n (a b : PTm n) :
-    RRed.R b a -> R a b.
-  Proof.
-    hauto lq:on ctrs:rtc use:RERed.FromBeta unfold:R.
-  Qed.
-
-  Lemma FromRReds n (a b : PTm n) :
-    rtc RRed.R b a -> R a b.
-  Proof.
-    hauto lq:on ctrs:rtc use:REReds.FromRReds unfold:R.
-  Qed.
-
-  Lemma FromBJoin n (a b : PTm n) :
-    BJoin.R a b -> R a b.
-  Proof.
-    hauto lq:on ctrs:rtc use:REReds.FromRReds unfold:R.
-  Qed.
-
-  Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) :
-    R a b -> R (subst_PTm ρ a) (subst_PTm ρ b).
-  Proof.
-    hauto lq:on rew:off ctrs:rtc unfold:R use:REReds.substing.
-  Qed.
-
 End DJoin.
diff --git a/theories/logrel.v b/theories/logrel.v
deleted file mode 100644
index 5377dfb..0000000
--- a/theories/logrel.v
+++ /dev/null
@@ -1,752 +0,0 @@
-Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax.
-Require Import fp_red.
-From Hammer Require Import Tactics.
-From Equations Require Import Equations.
-Require Import ssreflect ssrbool.
-Require Import Logic.PropExtensionality (propositional_extensionality).
-From stdpp Require Import relations (rtc(..), rtc_subrel).
-Import Psatz.
-Require Import Cdcl.Itauto.
-
-Definition ProdSpace {n} (PA : PTm n -> Prop)
-  (PF : PTm n -> (PTm n -> Prop) -> Prop) b : Prop :=
-  forall a PB, PA a -> PF a PB -> PB (PApp b a).
-
-Definition SumSpace {n} (PA : PTm n -> Prop)
-  (PF : PTm n -> (PTm n -> Prop) -> Prop) t : Prop :=
-  (exists v, rtc TRedSN t v /\ SNe v) \/ exists a b, rtc TRedSN t (PPair a b) /\ PA a /\ (forall PB, PF a PB -> PB b).
-
-Definition BindSpace {n} p := if p is PPi then @ProdSpace n else SumSpace.
-
-Reserved Notation "⟦ A ⟧ i ;; I ↘ S" (at level 70).
-
-Inductive InterpExt {n} i (I : nat -> PTm n -> Prop) : PTm n -> (PTm n -> Prop) -> Prop :=
-| InterpExt_Ne A :
-  SNe A ->
-  ⟦ A ⟧ i ;; I ↘ (fun a => exists v, rtc TRedSN a v /\ SNe v)
-| InterpExt_Bind p A B PA PF :
-  ⟦ A ⟧ i ;; I ↘ PA ->
-  (forall a, PA a -> exists PB, PF a PB) ->
-  (forall a PB, PF a PB -> ⟦ subst_PTm (scons a VarPTm) B ⟧ i ;; I ↘ PB) ->
-  ⟦ PBind p A B ⟧ i ;; I ↘ BindSpace p PA PF
-
-| InterpExt_Univ j :
-  j < i ->
-  ⟦ PUniv j ⟧ i ;; I ↘ (I j)
-
-| InterpExt_Step A A0 PA :
-  TRedSN A A0 ->
-  ⟦ A0 ⟧ i ;; I ↘ PA ->
-  ⟦ A ⟧ i ;; I ↘ PA
-where "⟦ A ⟧ i ;; I ↘ S" := (InterpExt i I A S).
-
-
-Lemma InterpExt_Univ' n i  I j (PF : PTm n -> Prop) :
-  PF = I j ->
-  j < i ->
-  ⟦ PUniv j ⟧ i ;; I ↘ PF.
-Proof. hauto lq:on ctrs:InterpExt. Qed.
-
-Infix "<?" := Compare_dec.lt_dec (at level 60).
-
-Equations InterpUnivN n (i : nat) : PTm n -> (PTm n -> Prop) -> Prop by wf i lt :=
-  InterpUnivN n i := @InterpExt n i
-                     (fun j A =>
-                        match j <? i  with
-                        | left _ => exists PA, InterpUnivN n j A PA
-                        | right _ => False
-                        end).
-Arguments InterpUnivN {n}.
-
-Lemma InterpExt_lt_impl n i I I' A (PA : PTm n -> Prop) :
-  (forall j, j < i -> I j = I' j) ->
-  ⟦ A ⟧ i ;; I ↘ PA ->
-  ⟦ A ⟧ i ;; I' ↘ PA.
-Proof.
-  move => hI h.
-  elim : A PA /h.
-  - hauto q:on ctrs:InterpExt.
-  - hauto lq:on rew:off ctrs:InterpExt.
-  - hauto q:on ctrs:InterpExt.
-  - hauto lq:on ctrs:InterpExt.
-Qed.
-
-Lemma InterpExt_lt_eq n i I I' A (PA : PTm n -> Prop) :
-  (forall j, j < i -> I j = I' j) ->
-  ⟦ A ⟧ i ;; I ↘ PA =
-  ⟦ A ⟧ i ;; I' ↘ PA.
-Proof.
-  move => hI. apply propositional_extensionality.
-  have : forall j, j < i -> I' j = I j by sfirstorder.
-  firstorder using InterpExt_lt_impl.
-Qed.
-
-Notation "⟦ A ⟧ i ↘ S" := (InterpUnivN i A S) (at level 70).
-
-Lemma InterpUnivN_nolt n i :
-  @InterpUnivN n i = @InterpExt n i (fun j (A : PTm n) => exists PA, ⟦ A ⟧ j ↘ PA).
-Proof.
-  simp InterpUnivN.
-  extensionality A. extensionality PA.
-  set I0 := (fun _ => _).
-  set I1 := (fun _ => _).
-  apply InterpExt_lt_eq.
-  hauto q:on.
-Qed.
-
-#[export]Hint Rewrite @InterpUnivN_nolt : InterpUniv.
-
-Lemma InterpUniv_ind
-  : forall n (P : nat -> PTm n -> (PTm n -> Prop) -> Prop),
-       (forall i (A : PTm n), SNe A -> P i A (fun a : PTm n => exists v : PTm n, rtc TRedSN a v /\ SNe v)) ->
-       (forall i (p : BTag) (A : PTm n) (B : PTm (S n)) (PA : PTm n -> Prop)
-          (PF : PTm n -> (PTm n -> Prop) -> Prop),
-        ⟦ A ⟧ i ↘ PA ->
-        P i A PA ->
-        (forall a : PTm n, PA a -> exists PB : PTm n -> Prop, PF a PB) ->
-        (forall (a : PTm n) (PB : PTm n -> Prop), PF a PB -> ⟦ subst_PTm (scons a VarPTm) B ⟧ i ↘ PB) ->
-        (forall (a : PTm n) (PB : PTm n -> Prop), PF a PB -> P i (subst_PTm (scons a VarPTm) B) PB) ->
-        P i (PBind p A B) (BindSpace p PA PF)) ->
-       (forall i j : nat, j < i ->  (forall A PA, ⟦ A ⟧ j ↘ PA -> P j A PA) -> P i (PUniv j) (fun A => exists PA, ⟦ A ⟧ j ↘ PA)) ->
-       (forall i (A A0 : PTm n) (PA : PTm n -> Prop), TRedSN A A0 -> ⟦ A0 ⟧ i ↘ PA -> P i A0 PA -> P i A PA) ->
-       forall i (p : PTm n) (P0 : PTm n -> Prop), ⟦ p ⟧ i ↘ P0 -> P i p P0.
-Proof.
-  move => n P  hSN hBind hUniv hRed.
-  elim /Wf_nat.lt_wf_ind => i ih . simp InterpUniv.
-  move => A PA. move => h. set I := fun _ => _ in h.
-  elim : A PA / h; rewrite -?InterpUnivN_nolt; eauto.
-Qed.
-
-Derive Dependent Inversion iinv with (forall n i I (A : PTm n) PA, InterpExt i I A PA) Sort Prop.
-
-Lemma InterpUniv_Ne n i (A : PTm n) :
-  SNe A ->
-  ⟦ A ⟧ i ↘ (fun a => exists v, rtc TRedSN a v /\ SNe v).
-Proof. simp InterpUniv. apply InterpExt_Ne. Qed.
-
-Lemma InterpUniv_Bind n i p A B PA PF :
-  ⟦ A : PTm n ⟧ i ↘ PA ->
-  (forall a, PA a -> exists PB, PF a PB) ->
-  (forall a PB, PF a PB -> ⟦ subst_PTm (scons a VarPTm) B ⟧ i ↘ PB) ->
-  ⟦ PBind p A B ⟧ i ↘ BindSpace p PA PF.
-Proof. simp InterpUniv. apply InterpExt_Bind. Qed.
-
-Lemma InterpUniv_Univ n i j :
-  j < i -> ⟦ PUniv j : PTm n ⟧ i ↘ (fun A => exists PA, ⟦ A ⟧ j ↘ PA).
-Proof.
-  simp InterpUniv. simpl.
-  apply InterpExt_Univ'. by simp InterpUniv.
-Qed.
-
-Lemma InterpUniv_Step i n A A0 PA :
-  TRedSN A A0 ->
-  ⟦ A0 : PTm n ⟧ i ↘ PA ->
-  ⟦ A ⟧ i ↘ PA.
-Proof. simp InterpUniv. apply InterpExt_Step. Qed.
-
-
-#[export]Hint Resolve InterpUniv_Bind InterpUniv_Step InterpUniv_Ne InterpUniv_Univ : InterpUniv.
-
-Lemma InterpExt_cumulative n i j I (A : PTm n) PA :
-  i <= j ->
-   ⟦ A ⟧ i ;; I ↘ PA ->
-   ⟦ A ⟧ j ;; I ↘ PA.
-Proof.
-  move => h h0.
-  elim : A PA /h0;
-    hauto l:on ctrs:InterpExt solve+:(by lia).
-Qed.
-
-Lemma InterpUniv_cumulative n i (A : PTm n) PA :
-   ⟦ A ⟧ i ↘ PA -> forall j, i <= j ->
-   ⟦ A ⟧ j ↘ PA.
-Proof.
-  hauto l:on rew:db:InterpUniv use:InterpExt_cumulative.
-Qed.
-
-Definition CR {n} (P : PTm n -> Prop) :=
-  (forall a, P a -> SN a) /\
-    (forall a, SNe a -> P a).
-
-Lemma N_Exps n (a b : PTm n) :
-  rtc TRedSN a b ->
-  SN b ->
-  SN a.
-Proof.
-  induction 1; eauto using N_Exp.
-Qed.
-
-Lemma adequacy : forall i n A PA,
-   ⟦ A : PTm n ⟧ i ↘ PA ->
-  CR PA /\ SN A.
-Proof.
-  move => + n. apply : InterpUniv_ind.
-  - hauto l:on use:N_Exps ctrs:SN,SNe.
-  - move => i p A B PA PF hPA [ihA0 ihA1] hTot hRes ihPF.
-    have hb : PA PBot by hauto q:on ctrs:SNe.
-    have hb' : SN PBot by hauto q:on ctrs:SN, SNe.
-    rewrite /CR.
-    repeat split.
-    + case : p =>//=.
-      * rewrite /ProdSpace.
-        qauto use:SN_AppInv unfold:CR.
-      * hauto q:on unfold:SumSpace use:N_SNe, N_Pair,N_Exps.
-    + move => a ha.
-      case : p=>/=.
-      * rewrite /ProdSpace => a0 *.
-        suff : SNe (PApp a a0) by sfirstorder.
-        hauto q:on use:N_App.
-      * sfirstorder.
-    + apply N_Bind=>//=.
-      have : SN (PApp (PAbs B) PBot).
-      apply : N_Exp; eauto using N_β.
-      hauto lq:on.
-      qauto l:on use:SN_AppInv, SN_NoForbid.P_AbsInv.
-  - hauto l:on ctrs:InterpExt rew:db:InterpUniv.
-  - hauto l:on ctrs:SN unfold:CR.
-Qed.
-
-Lemma InterpUniv_Steps i n A A0 PA :
-  rtc TRedSN A A0 ->
-  ⟦ A0 : PTm n ⟧ i ↘ PA ->
-  ⟦ A ⟧ i ↘ PA.
-Proof. induction 1; hauto l:on use:InterpUniv_Step. Qed.
-
-Lemma InterpUniv_back_clos n i (A : PTm n) PA :
-    ⟦ A ⟧ i ↘ PA ->
-    forall a b, TRedSN a b ->
-           PA b -> PA a.
-Proof.
-  move : i A PA . apply : InterpUniv_ind; eauto.
-  - hauto q:on ctrs:rtc.
-  - move => i p A B PA PF hPA ihPA hTot hRes ihPF a b hr.
-    case : p => //=.
-    + rewrite /ProdSpace.
-    move => hba a0 PB ha hPB.
-    suff : TRedSN  (PApp a a0) (PApp b a0) by hauto lq:on.
-    apply N_AppL => //=.
-    hauto q:on use:adequacy.
-    + hauto lq:on ctrs:rtc unfold:SumSpace.
-  - hauto l:on use:InterpUniv_Step.
-Qed.
-
-Lemma InterpUniv_back_closs n i (A : PTm n) PA :
-    ⟦ A ⟧ i ↘ PA ->
-    forall a b, rtc TRedSN a b ->
-           PA b -> PA a.
-Proof.
-  induction 2; hauto lq:on ctrs:rtc use:InterpUniv_back_clos.
-Qed.
-
-
-Lemma InterpUniv_case n i (A : PTm n) PA :
-  ⟦ A ⟧ i ↘ PA ->
-  exists H, rtc TRedSN A H /\  ⟦ H ⟧ i ↘ PA /\ (SNe H \/ isbind H \/ isuniv H).
-Proof.
-  move : i A PA. apply InterpUniv_ind => //=.
-  hauto lq:on ctrs:rtc use:InterpUniv_Ne.
-  hauto l:on use:InterpUniv_Bind.
-  hauto l:on use:InterpUniv_Univ.
-  hauto lq:on ctrs:rtc.
-Qed.
-
-Lemma redsn_preservation_mutual n :
-  (forall (a : PTm n) (s : SNe a), forall b, TRedSN a b -> False) /\
-    (forall (a : PTm n) (s : SN a), forall b, TRedSN a b -> SN b) /\
-  (forall (a b : PTm n) (_ : TRedSN a b), forall c, TRedSN a c -> b = c).
-Proof.
-  move : n. apply sn_mutual; sauto lq:on rew:off.
-Qed.
-
-Lemma redsns_preservation : forall n a b, @SN n a -> rtc TRedSN a b -> SN b.
-Proof. induction 2; sfirstorder use:redsn_preservation_mutual ctrs:rtc. Qed.
-
-#[export]Hint Resolve DJoin.sne_bind_noconf DJoin.sne_univ_noconf DJoin.bind_univ_noconf : noconf.
-
-Lemma InterpUniv_SNe_inv n i (A : PTm n) PA :
-  SNe A ->
-  ⟦ A ⟧ i ↘ PA ->
-  PA = (fun a => exists v, rtc TRedSN a v /\ SNe v).
-Proof.
-  simp InterpUniv.
-  hauto lq:on rew:off inv:InterpExt,SNe use:redsn_preservation_mutual.
-Qed.
-
-Lemma InterpUniv_Bind_inv n i p A B S :
-  ⟦ PBind p A B ⟧ i ↘ S -> exists PA PF,
-  ⟦ A : PTm n ⟧ i ↘ PA /\
-  (forall a, PA a -> exists PB, PF a PB) /\
-  (forall a PB, PF a PB -> ⟦ subst_PTm (scons a VarPTm) B ⟧ i ↘ PB) /\
-  S = BindSpace p PA PF.
-Proof. simp InterpUniv.
-       inversion 1; try hauto inv:SNe q:on use:redsn_preservation_mutual.
-       rewrite -!InterpUnivN_nolt.
-       sauto lq:on.
-Qed.
-
-Lemma InterpUniv_Univ_inv n i j S :
-  ⟦ PUniv j : PTm n ⟧ i ↘ S ->
-  S = (fun A => exists PA, ⟦ A ⟧ j ↘ PA) /\ j < i.
-Proof.
-  simp InterpUniv. inversion 1;
-    try hauto inv:SNe use:redsn_preservation_mutual.
-  rewrite -!InterpUnivN_nolt. sfirstorder.
-  subst. hauto lq:on inv:TRedSN.
-Qed.
-
-Lemma bindspace_iff n p (PA : PTm n -> Prop) PF PF0 b  :
-  (forall (a : PTm n) (PB PB0 : PTm n -> Prop), PA a -> PF a PB -> PF0 a PB0 -> PB = PB0) ->
-  (forall a, PA a -> exists PB, PF a PB) ->
-  (forall a, PA a -> exists PB0, PF0 a PB0) ->
-  (BindSpace p PA PF b <-> BindSpace p PA PF0 b).
-Proof.
-  rewrite /BindSpace => h hPF hPF0.
-  case : p => /=.
-  - rewrite /ProdSpace.
-    split.
-    move => h1 a PB ha hPF'.
-    specialize hPF with (1 := ha).
-    specialize hPF0 with (1 := ha).
-    sblast.
-    move => ? a PB ha.
-    specialize hPF with (1 := ha).
-    specialize hPF0 with (1 := ha).
-    sblast.
-  - rewrite /SumSpace.
-    hauto lq:on rew:off.
-Qed.
-
-Lemma InterpUniv_Join n i (A B : PTm n) PA PB :
-  ⟦ A ⟧ i ↘ PA ->
-  ⟦ B ⟧ i ↘ PB ->
-  DJoin.R A B ->
-  PA = PB.
-Proof.
-  move => hA.
-  move : i A PA hA B PB.
-  apply : InterpUniv_ind.
-  - move => i A hA B PB hPB hAB.
-    have [*] : SN B /\ SN A by hauto l:on use:adequacy.
-    move /InterpUniv_case : hPB.
-    move => [H [/DJoin.FromRedSNs h [h1 h0]]].
-    have {hAB} {}h : DJoin.R A H by eauto using DJoin.transitive.
-    have {}h0 : SNe H.
-    suff : ~ isbind H /\ ~ isuniv H by itauto.
-    move : h hA. clear. hauto lq:on db:noconf.
-    hauto lq:on use:InterpUniv_SNe_inv.
-  - move => i p A B PA PF hPA ihPA hTot hRes ihPF U PU hU.
-    have hU' : SN U by hauto l:on use:adequacy.
-    move /InterpUniv_case : hU => [H [/DJoin.FromRedSNs h [h1 h0]]] hU.
-    have {hU} {}h : DJoin.R (PBind p A B) H by eauto using DJoin.transitive.
-    have{h0} : isbind H.
-    suff : ~ SNe H /\ ~ isuniv H by itauto.
-    have : isbind (PBind p A B) by scongruence.
-    hauto l:on use: DJoin.sne_bind_noconf, DJoin.bind_univ_noconf, DJoin.symmetric.
-    case : H h1 h => //=.
-    move => p0 A0 B0 h0 /DJoin.bind_inj.
-    move => [? [hA hB]] _. subst.
-    move /InterpUniv_Bind_inv : h0.
-    move => [PA0][PF0][hPA0][hTot0][hRes0 ?]. subst.
-    have ? : PA0 = PA by qauto l:on. subst.
-    have : forall a PB PB', PA a -> PF a PB -> PF0 a PB' -> PB = PB'.
-    move => a PB PB' ha hPB hPB'. apply : ihPF; eauto.
-    have hj0 : DJoin.R (PAbs B) (PAbs B0) by eauto using DJoin.AbsCong.
-    have {}hj0 : DJoin.R (PApp (PAbs B) a) (PApp (PAbs B0) a) by eauto using DJoin.AppCong, DJoin.refl.
-    have [? ?] : SN (PApp (PAbs B) a) /\ SN (PApp (PAbs B0) a) by
-      hauto lq:on rew:off use:N_Exp, N_β, adequacy.
-    have [? ?] : DJoin.R (PApp (PAbs B0) a) (subst_PTm (scons a VarPTm) B0) /\
-           DJoin.R (subst_PTm (scons a VarPTm) B) (PApp (PAbs B) a)
-      by hauto lq:on ctrs:RRed.R use:DJoin.FromRRed0, DJoin.FromRRed1.
-    eauto using DJoin.transitive.
-    move => h. extensionality b. apply propositional_extensionality.
-    hauto l:on use:bindspace_iff.
-  - move => i j jlti ih B PB hPB.
-    have ? : SN B by hauto l:on use:adequacy.
-    move /InterpUniv_case : hPB => [H [/DJoin.FromRedSNs h [h1 h0]]].
-    move => hj.
-    have {hj}{}h : DJoin.R (PUniv j) H by eauto using DJoin.transitive.
-    have {h0} : isuniv H.
-    suff : ~ SNe H /\ ~ isbind H by tauto.
-    hauto l:on use: DJoin.sne_univ_noconf, DJoin.bind_univ_noconf, DJoin.symmetric.
-    case : H h1 h => //=.
-    move => j' hPB h _.
-    have {}h : j' = j by hauto lq:on use: DJoin.univ_inj. subst.
-    hauto lq:on use:InterpUniv_Univ_inv.
-  - move => i A A0 PA hr hPA ihPA B PB hPB hAB.
-    have /DJoin.symmetric ? : DJoin.R A A0 by hauto lq:on rew:off ctrs:rtc use:DJoin.FromRedSNs.
-    have ? : SN A0 by hauto l:on use:adequacy.
-    have ? : SN A by eauto using N_Exp.
-    have : DJoin.R A0 B by eauto using DJoin.transitive.
-    eauto.
-Qed.
-
-Lemma InterpUniv_Functional n i  (A : PTm n) PA PB :
-  ⟦ A ⟧ i ↘ PA ->
-  ⟦ A ⟧ i ↘ PB ->
-  PA = PB.
-Proof. hauto use:InterpUniv_Join, DJoin.refl. Qed.
-
-Lemma InterpUniv_Join' n i j (A B : PTm n) PA PB :
-  ⟦ A ⟧ i ↘ PA ->
-  ⟦ B ⟧ j ↘ PB ->
-  DJoin.R A B ->
-  PA = PB.
-Proof.
-  have [? ?] : i <= max i j /\ j <= max i j by lia.
-  move => hPA hPB.
-  have : ⟦ A ⟧ (max i j) ↘ PA by eauto using InterpUniv_cumulative.
-  have : ⟦ B ⟧ (max i j) ↘ PB by eauto using InterpUniv_cumulative.
-  eauto using InterpUniv_Join.
-Qed.
-
-Lemma InterpUniv_Functional' n i j A PA PB :
-  ⟦ A : PTm n ⟧ i ↘ PA ->
-  ⟦ A ⟧ j ↘ PB ->
-  PA = PB.
-Proof.
-  hauto l:on use:InterpUniv_Join', DJoin.refl.
-Qed.
-
-Lemma InterpUniv_Bind_inv_nopf n i p A B P (h :  ⟦PBind p A B ⟧ i ↘ P) :
-  exists (PA : PTm n -> Prop),
-     ⟦ A ⟧ i ↘ PA /\
-    (forall a, PA a -> exists PB, ⟦ subst_PTm (scons a VarPTm) B ⟧ i ↘ PB) /\
-      P = BindSpace p PA (fun a PB => ⟦ subst_PTm (scons a VarPTm) B ⟧ i ↘ PB).
-Proof.
-  move /InterpUniv_Bind_inv : h.
-  move => [PA][PF][hPA][hPF][hPF']?. subst.
-  exists PA. repeat split => //.
-  - sfirstorder.
-  - extensionality b.
-    case : p => /=.
-    + extensionality a.
-      extensionality PB.
-      extensionality ha.
-      apply propositional_extensionality.
-      split.
-      * move => h hPB.  apply h.
-        have {}/hPF := ha.
-        move => [PB0 hPB0].
-        have {}/hPF' := hPB0 => ?.
-        have : PB = PB0 by hauto l:on use:InterpUniv_Functional.
-        congruence.
-      * sfirstorder.
-    + rewrite /SumSpace. apply propositional_extensionality.
-      split; hauto q:on use:InterpUniv_Functional.
-Qed.
-
-Definition ρ_ok {n} (Γ : fin n -> PTm n) (ρ : fin n -> PTm 0) := forall i k PA,
-    ⟦ subst_PTm ρ (Γ i) ⟧ k ↘ PA -> PA (ρ i).
-
-Definition SemWt {n} Γ (a A : PTm n) := forall ρ, ρ_ok Γ ρ -> exists k PA, ⟦ subst_PTm ρ A ⟧ k ↘ PA /\ PA (subst_PTm ρ a).
-Notation "Γ ⊨ a ∈ A" := (SemWt Γ a A) (at level 70).
-
-(* Semantic context wellformedness *)
-Definition SemWff {n} Γ := forall (i : fin n), exists j, Γ ⊨ Γ i ∈ PUniv j.
-Notation "⊨ Γ" := (SemWff Γ) (at level 70).
-
-Lemma ρ_ok_bot n (Γ : fin n -> PTm n)  :
-  ρ_ok Γ (fun _ => PBot).
-Proof.
-  rewrite /ρ_ok.
-  hauto q:on use:adequacy ctrs:SNe.
-Qed.
-
-Lemma ρ_ok_cons n i (Γ : fin n -> PTm n) ρ a PA A :
-  ⟦ subst_PTm ρ A ⟧ i ↘ PA -> PA a ->
-  ρ_ok Γ ρ ->
-  ρ_ok (funcomp (ren_PTm shift) (scons A Γ)) (scons a ρ).
-Proof.
-  move => h0 h1 h2.
-  rewrite /ρ_ok.
-  move => j.
-  destruct j as [j|].
-  - move => m PA0. asimpl => ?.
-    asimpl.
-    firstorder.
-  - move => m PA0. asimpl => h3.
-    have ? : PA0 = PA by eauto using InterpUniv_Functional'.
-    by subst.
-Qed.
-
-Definition renaming_ok {n m} (Γ : fin n -> PTm n) (Δ : fin m -> PTm m) (ξ : fin m -> fin n) :=
-  forall (i : fin m), ren_PTm ξ (Δ i) = Γ (ξ i).
-
-Lemma ρ_ok_renaming n m (Γ : fin n -> PTm n) ρ :
-  forall (Δ : fin m -> PTm m) ξ,
-    renaming_ok Γ Δ ξ ->
-    ρ_ok Γ ρ ->
-    ρ_ok Δ (funcomp ρ ξ).
-Proof.
-  move => Δ ξ hξ hρ.
-  rewrite /ρ_ok => i m' PA.
-  rewrite /renaming_ok in hξ.
-  rewrite /ρ_ok in hρ.
-  move => h.
-  rewrite /funcomp.
-  apply hρ with (k := m').
-  move : h. rewrite -hξ.
-  by asimpl.
-Qed.
-
-Lemma renaming_SemWt {n} Γ a A :
-  Γ ⊨ a ∈ A ->
-  forall {m} Δ (ξ : fin n -> fin m),
-    renaming_ok Δ Γ ξ ->
-    Δ ⊨ ren_PTm ξ a ∈ ren_PTm ξ A.
-Proof.
-  rewrite /SemWt => h m Δ ξ hξ ρ hρ.
-  have /h hρ' : (ρ_ok Γ (funcomp ρ ξ)) by eauto using ρ_ok_renaming.
-  hauto q:on solve+:(by asimpl).
-Qed.
-
-Lemma weakening_Sem n Γ (a : PTm n) A B i
-  (h0 : Γ ⊨ B ∈ PUniv i)
-  (h1 : Γ ⊨ a ∈ A) :
-   funcomp (ren_PTm shift) (scons B Γ) ⊨ ren_PTm shift a ∈ ren_PTm shift A.
-Proof.
-  apply : renaming_SemWt; eauto.
-  hauto lq:on inv:option unfold:renaming_ok.
-Qed.
-
-Lemma SemWt_SN n Γ (a : PTm n) A :
-  Γ ⊨ a ∈ A ->
-  SN a /\ SN A.
-Proof.
-  move => h.
-  have {}/h := ρ_ok_bot _ Γ => h.
-  have h0 : SN (subst_PTm (fun _ : fin n => (PBot : PTm 0)) A) by hauto l:on use:adequacy.
-  have h1 : SN (subst_PTm (fun _ : fin n => (PBot : PTm 0)) a)by hauto l:on use:adequacy.
-  move {h}. hauto l:on use:sn_unmorphing.
-Qed.
-
-Lemma SemWt_Univ n Γ (A : PTm n) i  :
-  Γ ⊨ A ∈ PUniv i <->
-  forall ρ, ρ_ok Γ ρ -> exists S, ⟦ subst_PTm ρ A ⟧ i ↘ S.
-Proof.
-  rewrite /SemWt.
-  split.
-  - hauto lq:on rew:off use:InterpUniv_Univ_inv.
-  - move => /[swap] ρ /[apply].
-    move => [PA hPA].
-    exists (S i). eexists.
-    split.
-    + simp InterpUniv. apply InterpExt_Univ. lia.
-    + simpl. eauto.
-Qed.
-
-(* Structural laws for Semantic context wellformedness *)
-Lemma SemWff_nil : SemWff null.
-Proof. case. Qed.
-
-Lemma SemWff_cons n Γ (A : PTm n) i :
-    ⊨ Γ ->
-    Γ ⊨ A ∈ PUniv i ->
-    (* -------------- *)
-    ⊨ funcomp (ren_PTm shift) (scons A Γ).
-Proof.
-  move => h h0.
-  move => j. destruct j as [j|].
-  - move /(_ j) : h => [k hk].
-    exists k. change (PUniv k) with (ren_PTm shift (PUniv k : PTm n)).
-    eauto using weakening_Sem.
-  - hauto q:on use:weakening_Sem.
-Qed.
-
-(* Semantic typing rules *)
-Lemma ST_Var n Γ (i : fin n) :
-  ⊨ Γ ->
-  Γ ⊨ VarPTm i ∈ Γ i.
-Proof.
-  move /(_ i) => [j /SemWt_Univ h].
-  rewrite /SemWt => ρ /[dup] hρ {}/h [S hS].
-  exists j, S.
-  asimpl. firstorder.
-Qed.
-
-Lemma InterpUniv_Bind_nopf n p i (A : PTm n) B PA :
-  ⟦ A ⟧ i ↘ PA ->
-  (forall a, PA a -> exists PB, ⟦ subst_PTm (scons a VarPTm) B ⟧ i ↘ PB) ->
-  ⟦ PBind p A B ⟧ i ↘ (BindSpace p PA (fun a PB => ⟦ subst_PTm (scons a VarPTm) B ⟧ i ↘ PB)).
-Proof.
-  move => h0 h1. apply InterpUniv_Bind => //=.
-Qed.
-
-
-Lemma ST_Bind n Γ i j p (A : PTm n) (B : PTm (S n)) :
-  Γ ⊨ A ∈ PUniv i ->
-  funcomp (ren_PTm shift) (scons A Γ) ⊨ B ∈ PUniv j ->
-  Γ ⊨ PBind p A B ∈ PUniv (max i j).
-Proof.
-  move => /SemWt_Univ h0 /SemWt_Univ h1.
-  apply SemWt_Univ => ρ hρ.
-  move /h0 : (hρ){h0} => [S hS].
-  eexists => /=.
-  have ? : i <= Nat.max i j by lia.
-  apply InterpUniv_Bind_nopf; eauto.
-  - eauto using InterpUniv_cumulative.
-  - move => *. asimpl. hauto l:on use:InterpUniv_cumulative, ρ_ok_cons.
-Qed.
-
-Lemma ST_Abs n Γ (a : PTm (S n)) A B i :
-  Γ ⊨ PBind PPi A B ∈ (PUniv i) ->
-  funcomp (ren_PTm shift) (scons A Γ) ⊨ a ∈ B ->
-  Γ ⊨ PAbs a ∈ PBind PPi A B.
-Proof.
-  rename a into b.
-  move /SemWt_Univ => + hb ρ hρ.
-  move /(_ _ hρ) => [PPi hPPi].
-  exists i, PPi. split => //.
-  simpl in hPPi.
-  move /InterpUniv_Bind_inv_nopf : hPPi.
-  move => [PA [hPA [hTot ?]]]. subst=>/=.
-  move => a PB ha. asimpl => hPB.
-  move : ρ_ok_cons (hPA) (hρ) (ha). repeat move/[apply].
-  move /hb.
-  intros (m & PB0 & hPB0 & hPB0').
-  replace PB0 with PB in * by hauto l:on use:InterpUniv_Functional'.
-  apply : InterpUniv_back_clos; eauto.
-  apply N_β'. by asimpl.
-  move : ha hPA. clear. hauto q:on use:adequacy.
-Qed.
-
-Lemma ST_App n Γ (b a : PTm n) A B :
-  Γ ⊨ b ∈ PBind PPi A B ->
-  Γ ⊨ a ∈ A ->
-  Γ ⊨ PApp b a ∈ subst_PTm (scons a VarPTm) B.
-Proof.
-  move => hf hb ρ hρ.
-  move /(_ ρ hρ) : hf; intros (i & PPi & hPi & hf).
-  move /(_ ρ hρ) : hb; intros (j & PA & hPA & hb).
-  simpl in hPi.
-  move /InterpUniv_Bind_inv_nopf : hPi. intros (PA0 & hPA0 & hTot & ?). subst.
-  have ? : PA0 = PA by eauto using InterpUniv_Functional'. subst.
-  move  : hf (hb). move/[apply].
-  move : hTot hb. move/[apply].
-  asimpl. hauto lq:on.
-Qed.
-
-Lemma ST_Pair n Γ (a b : PTm n) A B i :
-  Γ ⊨ PBind PSig A B ∈ (PUniv i) ->
-  Γ ⊨ a ∈ A ->
-  Γ ⊨ b ∈ subst_PTm (scons a VarPTm) B ->
-  Γ ⊨ PPair a b ∈ PBind PSig A B.
-Proof.
-  move /SemWt_Univ => + ha hb ρ hρ.
-  move /(_ _ hρ) => [PPi hPPi].
-  exists i, PPi. split => //.
-  simpl in hPPi.
-  move /InterpUniv_Bind_inv_nopf : hPPi.
-  move => [PA [hPA [hTot ?]]]. subst=>/=.
-  rewrite /SumSpace. right.
-  exists (subst_PTm ρ a), (subst_PTm ρ b).
-  split.
-  - apply rtc_refl.
-  - move /ha : (hρ){ha}.
-    move => [m][PA0][h0]h1.
-    move /hb : (hρ){hb}.
-    move => [k][PB][h2]h3.
-    have ? : PA0 = PA by eauto using InterpUniv_Functional'. subst.
-    split => // PB0.
-    move : h2. asimpl => *.
-    have ? : PB0 = PB by eauto using InterpUniv_Functional'. by subst.
-Qed.
-
-Lemma N_Projs n p (a b : PTm n) :
-  rtc TRedSN a b ->
-  rtc TRedSN (PProj p a) (PProj p b).
-Proof. induction 1; hauto lq:on ctrs:rtc, TRedSN. Qed.
-
-Lemma ST_Proj1 n Γ (a : PTm n) A B :
-  Γ ⊨ a ∈ PBind PSig A B ->
-  Γ ⊨ PProj PL a ∈ A.
-Proof.
-  move => h ρ /[dup]hρ {}/h [m][PA][/= /InterpUniv_Bind_inv_nopf h0]h1.
-  move : h0 => [S][h2][h3]?. subst.
-  move : h1 => /=.
-  rewrite /SumSpace.
-  case.
-  - move => [v [h0 h1]].
-    have {}h0 : rtc TRedSN (PProj PL (subst_PTm ρ a)) (PProj PL v) by hauto lq:on use:N_Projs.
-    have {}h1 : SNe (PProj PL v) by hauto lq:on ctrs:SNe.
-    hauto q:on use:InterpUniv_back_closs,adequacy.
-  - move => [a0 [b0 [h4 [h5 h6]]]].
-    exists m, S. split => //=.
-    have {}h4 : rtc TRedSN (PProj PL (subst_PTm ρ a)) (PProj PL (PPair a0 b0)) by eauto using N_Projs.
-    have ? : rtc TRedSN (PProj PL (PPair a0 b0)) a0 by hauto q:on ctrs:rtc, TRedSN use:adequacy.
-    have : rtc TRedSN (PProj PL (subst_PTm ρ a)) a0 by hauto q:on ctrs:rtc use:@relations.rtc_r.
-    move => h.
-    apply : InterpUniv_back_closs; eauto.
-Qed.
-
-Lemma ST_Proj2 n Γ (a : PTm n) A B :
-  Γ ⊨ a ∈ PBind PSig A B ->
-  Γ ⊨ PProj PR a ∈ subst_PTm (scons (PProj PL a) VarPTm) B.
-Proof.
-  move => h ρ hρ.
-  move : (hρ) => {}/h [m][PA][/= /InterpUniv_Bind_inv_nopf h0]h1.
-  move : h0 => [S][h2][h3]?. subst.
-  move : h1 => /=.
-  rewrite /SumSpace.
-  case.
-  - move => h.
-    move : h => [v [h0 h1]].
-    have hp : forall p, SNe (PProj p v) by hauto lq:on ctrs:SNe.
-    have hp' : forall p, rtc TRedSN (PProj p(subst_PTm ρ a)) (PProj p v) by eauto using N_Projs.
-    have hp0 := hp PL. have hp1 := hp PR => {hp}.
-    have hp0' := hp' PL. have hp1' := hp' PR => {hp'}.
-    have : S (PProj PL (subst_PTm ρ a)). apply : InterpUniv_back_closs; eauto. hauto q:on use:adequacy.
-    move /h3 => [PB]. asimpl => hPB.
-    do 2 eexists. split; eauto.
-    apply : InterpUniv_back_closs; eauto. hauto q:on use:adequacy.
-  - move => [a0 [b0 [h4 [h5 h6]]]].
-    have h3_dup := h3.
-    specialize h3 with (1 := h5).
-    move : h3 => [PB hPB].
-    have hr : forall p, rtc TRedSN (PProj p (subst_PTm ρ a)) (PProj p (PPair a0 b0)) by hauto l:on use: N_Projs.
-    have hSN : SN a0 by move : h5 h2; clear; hauto q:on use:adequacy.
-    have hSN' : SN b0 by hauto q:on use:adequacy.
-    have hrl : TRedSN (PProj PL (PPair a0 b0)) a0 by hauto lq:on ctrs:TRedSN.
-    have hrr : TRedSN (PProj PR (PPair a0 b0)) b0 by hauto lq:on ctrs:TRedSN.
-    exists m, PB.
-    asimpl. split.
-    + have hr' : rtc TRedSN (PProj PL (subst_PTm ρ a)) a0 by hauto l:on use:@relations.rtc_r.
-      have : S (PProj PL (subst_PTm ρ a)) by hauto lq:on use:InterpUniv_back_closs.
-      move => {}/h3_dup.
-      move => [PB0]. asimpl => hPB0.
-      suff : PB = PB0 by congruence.
-      move : hPB. asimpl => hPB.
-      suff : DJoin.R (subst_PTm (scons (PProj PL (subst_PTm ρ a)) ρ) B) (subst_PTm (scons a0 ρ) B).
-      move : InterpUniv_Join hPB0 hPB; repeat move/[apply]. done.
-      suff : BJoin.R (subst_PTm (scons (PProj PL (subst_PTm ρ a)) ρ) B) (subst_PTm (scons a0 ρ) B)
-        by hauto q:on use:DJoin.FromBJoin.
-      have : BJoin.R (PApp (PAbs (subst_PTm (up_PTm_PTm ρ) B)) (PProj PL (subst_PTm ρ a)))
-               (subst_PTm (scons (PProj PL (subst_PTm ρ a)) ρ) B).
-      eexists. split. apply relations.rtc_once. apply RRed.AppAbs.
-      asimpl. apply rtc_refl.
-      have /BJoin.symmetric : BJoin.R (PApp (PAbs (subst_PTm (up_PTm_PTm ρ)B)) a0)
-                                (subst_PTm (scons a0 ρ) B).
-      eexists. split. apply relations.rtc_once. apply RRed.AppAbs.
-      asimpl. apply rtc_refl.
-      suff : BJoin.R (PApp (PAbs (subst_PTm (up_PTm_PTm ρ) B)) (PProj PL (subst_PTm ρ a)))
-               (PApp (PAbs (subst_PTm (up_PTm_PTm ρ)B)) a0) by eauto using BJoin.transitive, BJoin.symmetric.
-      apply BJoin.AppCong. apply BJoin.refl.
-      move /RReds.FromRedSNs : hr'.
-      hauto lq:on ctrs:rtc unfold:BJoin.R.
-    + hauto lq:on use:@relations.rtc_r, InterpUniv_back_closs.
-Qed.
-
-Lemma ST_Conv n Γ (a : PTm n) A B i :
-  Γ ⊨ a ∈ A ->
-  Γ ⊨ B ∈ PUniv i ->
-  DJoin.R A B ->
-  Γ ⊨ a ∈ B.
-Proof.
-  move => ha /SemWt_Univ h h0.
-  move => ρ hρ.
-  have {}h0 : DJoin.R (subst_PTm ρ A) (subst_PTm ρ B) by eauto using DJoin.substing.
-  move /ha : (hρ){ha} => [m [PA [h1 h2]]].
-  move /h : (hρ){h} => [S hS].
-  have ? : PA = S by eauto using InterpUniv_Join'. subst.
-  eauto.
-Qed.