diff --git a/syntax.sig b/syntax.sig
index e2bafac..6b7e4df 100644
--- a/syntax.sig
+++ b/syntax.sig
@@ -1,15 +1,19 @@
 PTm(VarPTm) : Type
 PTag : Type
-Ty : Type
+BTag : Type
 
-Fun : Ty -> Ty -> Ty
-Prod : Ty -> Ty -> Ty
-Void : Ty
+nat : Type
 
 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 78c4fec..ff9ec18 100644
--- a/theories/Autosubst2/syntax.v
+++ b/theories/Autosubst2/syntax.v
@@ -5,6 +5,20 @@ 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.
@@ -24,7 +38,10 @@ 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
+  | PBot : 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.
@@ -56,6 +73,28 @@ 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.
@@ -76,6 +115,10 @@ 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) :
@@ -102,6 +145,11 @@ 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)
@@ -140,6 +188,11 @@ 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)
@@ -180,6 +233,12 @@ 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)
@@ -221,6 +280,12 @@ 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)
@@ -262,6 +327,13 @@ 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}
@@ -312,6 +384,13 @@ 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}
@@ -382,6 +461,13 @@ 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}
@@ -454,6 +540,13 @@ 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}
@@ -566,6 +659,12 @@ 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}
@@ -637,30 +736,6 @@ 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.
 
@@ -796,6 +871,12 @@ 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 062f9a6..e22e759 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -47,7 +47,15 @@ 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)
+  | BotCong :
+    R PBot PBot.
 
   Lemma refl n (a : PTm n) : R a a.
   Proof.
@@ -99,6 +107,10 @@ 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 :=
@@ -111,6 +123,8 @@ 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 ->
@@ -126,6 +140,12 @@ 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 ->
@@ -146,6 +166,65 @@ 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.
@@ -156,7 +235,7 @@ Proof.
   hauto lq:on inv:TRedSN.
 Qed.
 
-Lemma PProjPair_imp n (a b0 b1 : PTm n ) :
+Lemma PAppPair_imp n (a b0 b1 : PTm n ) :
   ~ SN (PApp (PPair b0 b1) a).
 Proof.
   move E : (PApp (PPair b0 b1) a) => u hu.
@@ -166,6 +245,26 @@ 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.
@@ -179,6 +278,9 @@ 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
@@ -187,6 +289,9 @@ 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.
@@ -334,6 +439,7 @@ 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.
@@ -350,6 +456,8 @@ 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.
@@ -410,7 +518,13 @@ 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.
 
@@ -457,6 +571,20 @@ 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.
@@ -488,7 +616,15 @@ 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)
+  | BotCong :
+    R PBot PBot.
 
   Lemma refl n (a : PTm n) : R a a.
   Proof.
@@ -581,6 +717,9 @@ 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) :
@@ -609,6 +748,9 @@ 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) :
@@ -625,10 +767,13 @@ 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.
@@ -650,91 +795,6 @@ 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 :=
@@ -766,6 +826,12 @@ 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.
@@ -775,7 +841,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.
+    elim : n a b /h; eauto using AbsCong, AppCong, PairCong, ProjCong, rtc_refl, BindCong.
     move => n a0 a1 b0 b1 ha iha hb ihb.
     apply : rtc_r; last by apply RRed.AppAbs.
     by eauto using AppCong, AbsCong.
@@ -797,6 +863,11 @@ 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.
 
 
@@ -806,19 +877,6 @@ 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 ***********************)
@@ -847,6 +905,14 @@ 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 ->
@@ -863,7 +929,15 @@ 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)
+  | NBotCong :
+    R_elim PBot PBot.
 
   Scheme epar_elim_ind := Induction for R_elim Sort Prop
       with epar_nonelim_ind := Induction for R_nonelim Sort Prop.
@@ -878,9 +952,10 @@ 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.
-      qauto l:on inv:R_elim.
+      hauto q: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.
@@ -897,6 +972,7 @@ 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) :
@@ -927,11 +1003,17 @@ 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_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_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.
@@ -970,11 +1052,10 @@ 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 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 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_AppInv : forall n (a b : PTm n), P (PApp a b) -> P a /\ P b.
   Proof. sfirstorder use:SN_AppInv. Qed.
@@ -986,6 +1067,13 @@ 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.
@@ -996,13 +1084,19 @@ 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 P_AppPair P_ProjAbs : forbid.
+  #[local]Hint Resolve P_EPar P_RRed PAbs_imp PProj_imp : forbid.
 
   Lemma η_split n (a0 a1 : PTm n) :
     EPar.R a0 a1 ->
@@ -1020,9 +1114,8 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
       by eauto using RReds.renaming.
       apply NeEPar.AppEta=>//.
       sfirstorder use:NeEPar.R_nonelim_nothf.
-
-      case : b ih0 ih1 => //=.
-      + move => p ih0 ih1 _.
+      case /orP : (orbN (isabs b)).
+      + case : b ih0 ih1 => //= p ih0 ih1 _ _.
         set q := PAbs _.
         suff : rtc RRed.R q (PAbs p) by sfirstorder.
         subst q.
@@ -1033,16 +1126,14 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
         apply : RRed.AbsCong => /=.
         apply RRed.AppAbs'. by asimpl.
       (* violates SN *)
-      + 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 /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 => n a0 a1 h ih /[dup] hP.
       move /P_PairInv => [/P_ProjInv + _].
       move : ih => /[apply].
@@ -1051,16 +1142,9 @@ 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 : 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 _.
+      case /orP : (orbN (ispair b)).
+      + case : b ih0 ih1 => //=.
+        move => t0 t1 ih0 h1 _ _.
         exists (PPair t0 t1).
         split => //=.
         apply RReds.PairCong.
@@ -1068,6 +1152,12 @@ 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].
@@ -1076,8 +1166,9 @@ 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 : a2 iha0 iha1 => //=.
-        * move => p h0 h1 _.
+      + case /orP : (orbN (isabs a2)).
+        (* case : a2 iha0 iha1 => //=. *)
+        * case : a2 iha0 iha1 => //= p h0 h1 _ _.
           inversion h1; subst.
           ** exists (PApp a2 b2).
              split.
@@ -1087,11 +1178,9 @@ 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 => 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.
+        * move =>*. exfalso.
+          have : P (PApp a2 b0) by sfirstorder use:RReds.AppCong, @rtc_refl, P_RReds.
+          sfirstorder use:PAbs_imp.
     - 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]].
@@ -1100,13 +1189,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 : a2 iha0 iha1 => //=.
-      + move => u iha0. exfalso.
-        have : rtc RRed.R (PProj p a0) (PProj p (PAbs u))
+      case /orP : (orNb (ispair a2)).
+      + move => *. exfalso.
+        have : rtc RRed.R (PProj p a0) (PProj p a2)
           by sfirstorder use:RReds.ProjCong ctrs:rtc.
         move : P_RReds hP. repeat move/[apply].
-        sfirstorder use:P_ProjAbs.
-      + move => u0 u1 iha0 iha1 _.
+        sfirstorder use:PProj_imp.
+      + case : a2 iha0 iha1 => //= u0 u1 iha0 iha1 _ _.
         inversion iha1; subst.
         * exists (PProj p a2). split.
           apply : rtc_r.
@@ -1115,6 +1204,9 @@ 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.
 
 
@@ -1168,7 +1260,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:P_AppPair.
+          sfirstorder use:PAbs_imp.
         * exists (subst_PTm (scons b0 VarPTm) a1).
           split.
           apply : rtc_r; last by apply RRed.AppAbs.
@@ -1195,7 +1287,7 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
         move : η_split hP'  ha; repeat move/[apply].
         move => [a1 [h0 h1]].
         inversion h1; subst.
-        * qauto l:on ctrs:rtc use:RReds.ProjCong, P_ProjAbs, P_RReds.
+        * sauto q:on ctrs:rtc use:RReds.ProjCong, PProj_imp, P_RReds.
         * inversion H0; subst.
           exists (if p is PL then a1 else b1).
           split; last by scongruence use:NeEPar.ToEPar.
@@ -1220,6 +1312,9 @@ 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 :
@@ -1256,7 +1351,6 @@ End UniqueNF.
 
 Module SN_UniqueNF := UniqueNF SN_NoForbid NoForbid_FactSN.
 
-
 Module ERed.
   Inductive R {n} : PTm n -> PTm n ->  Prop :=
 
@@ -1284,7 +1378,13 @@ 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.
 
@@ -1328,6 +1428,13 @@ 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 :
@@ -1380,8 +1487,22 @@ 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.
 
@@ -1416,6 +1537,13 @@ 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.
@@ -1424,7 +1552,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.
+    move => h. elim : n a b /h; eauto using AbsCong, AppCong, PairCong, ProjCong, rtc_refl, BindCong.
     - 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.
@@ -1435,6 +1563,17 @@ 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.
@@ -1473,7 +1612,13 @@ 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 ->
@@ -1501,6 +1646,26 @@ 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.
@@ -1549,6 +1714,48 @@ 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.
@@ -1582,7 +1789,14 @@ 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 ->
@@ -1649,6 +1863,13 @@ 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,
@@ -1660,10 +1881,13 @@ 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.
@@ -1687,10 +1911,13 @@ End LoReds.
 Fixpoint size_PTm {n} (a : PTm n) :=
   match a with
   | VarPTm _ => 1
-  | PAbs a => 1 + size_PTm a
+  | PAbs a => 3 + 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 => 1 + Nat.add (size_PTm a) (size_PTm b)
+  | 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
   end.
 
 Lemma size_PTm_ren n m (ξ : fin n -> fin m) a : size_PTm (ren_PTm ξ a) = size_PTm a.
@@ -1775,6 +2002,12 @@ 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) :
@@ -1873,7 +2106,36 @@ Proof.
   move /REReds.FromRReds : hc0. move /REReds.FromEReds : hv'. eauto using relations.rtc_transitive.
 Qed.
 
-(* "Declarative" Joinability *)
+(* 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.
+
 Module DJoin.
   Definition R {n} (a b : PTm n) := exists c, rtc RERed.R a c /\ rtc RERed.R b c.
 
@@ -1914,4 +2176,81 @@ 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
new file mode 100644
index 0000000..5377dfb
--- /dev/null
+++ b/theories/logrel.v
@@ -0,0 +1,752 @@
+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.