diff --git a/theories/fp_red.v b/theories/fp_red.v
index 1277775..e9cc8e9 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -1526,12 +1526,48 @@ Proof.
   - hauto lq:on inv:RPar.R ctrs:RPar.R.
 Qed.
 
+Function tstar' {n} (a : Tm n) :=
+  match a with
+  | VarTm i => a
+  | Abs a => Abs (tstar' a)
+  | App (Abs a) b => subst_Tm (scons (tstar' b) VarTm) (tstar' a)
+  | App a b => App (tstar' a) (tstar' b)
+  | Pair a b => Pair (tstar' a) (tstar' b)
+  | Proj p (Pair a b) => if p is PL then (tstar' a) else (tstar' b)
+  | Proj p a => Proj p (tstar' a)
+  | TBind p a b => TBind p (tstar' a) (tstar' b)
+  | Bot => Bot
+  | Univ i => Univ i
+  end.
+
+Lemma RPar'_triangle n (a : Tm n) : forall b, RPar'.R a b -> RPar'.R b (tstar' a).
+Proof.
+  apply tstar'_ind => {n a}.
+  - hauto lq:on inv:RPar'.R ctrs:RPar'.R.
+  - hauto lq:on inv:RPar'.R ctrs:RPar'.R.
+  - hauto lq:on use:RPar'.cong, RPar'.refl ctrs:RPar'.R inv:RPar'.R.
+  - hauto lq:on rew:off ctrs:RPar'.R inv:RPar'.R.
+  - hauto lq:on rew:off inv:RPar'.R ctrs:RPar'.R.
+  - hauto drew:off inv:RPar'.R use:RPar'.refl, RPar'.ProjPair'.
+  - hauto drew:off inv:RPar'.R use:RPar'.refl, RPar'.ProjPair'.
+  - hauto lq:on inv:RPar'.R ctrs:RPar'.R.
+  - hauto lq:on inv:RPar'.R ctrs:RPar'.R.
+  - hauto lq:on inv:RPar'.R ctrs:RPar'.R.
+  - hauto lq:on inv:RPar'.R ctrs:RPar'.R.
+Qed.
+
 Lemma RPar_diamond n (c a1 b1 : Tm n) :
   RPar.R c a1 ->
   RPar.R c b1 ->
   exists d2, RPar.R a1 d2 /\ RPar.R b1 d2.
 Proof. hauto l:on use:RPar_triangle. Qed.
 
+Lemma RPar'_diamond n (c a1 b1 : Tm n) :
+  RPar'.R c a1 ->
+  RPar'.R c b1 ->
+  exists d2, RPar'.R a1 d2 /\ RPar'.R b1 d2.
+Proof. hauto l:on use:RPar'_triangle. Qed.
+
 Lemma RPar_confluent n (c a1 b1 : Tm n) :
   rtc RPar.R c a1 ->
   rtc RPar.R c b1 ->
@@ -2331,7 +2367,7 @@ Proof. hauto lq:on unfold:join use:Pars.substing. Qed.
 Fixpoint ne {n} (a : Tm n) :=
   match a with
   | VarTm i => true
-  | TBind _ A B => nf A && nf B
+  | TBind _ A B => false
   | Bot => false
   | App a b => ne a && nf b
   | Abs a => false
diff --git a/theories/logrel.v b/theories/logrel.v
index 9a5c1ac..a4ac4fa 100644
--- a/theories/logrel.v
+++ b/theories/logrel.v
@@ -13,12 +13,15 @@ Definition ProdSpace {n} (PA : Tm n -> Prop)
 
 Definition SumSpace {n} (PA : Tm n -> Prop)
   (PF : Tm n -> (Tm n -> Prop) -> Prop) t : Prop :=
-  exists a b, rtc RPar.R t (Pair a b) /\ PA a /\ (forall PB, PF a PB -> PB b).
+  exists a b, rtc RPar'.R t (Pair a b) /\ PA a /\ (forall PB, PF a PB -> PB b).
 
 Definition BindSpace {n} p := if p is TPi then @ProdSpace n else SumSpace.
 
 Reserved Notation "⟦ A ⟧ i ;; I ↘ S" (at level 70).
 Inductive InterpExt {n} i (I : nat -> Tm n -> Prop) : Tm n -> (Tm n -> Prop) -> Prop :=
+| InterpExt_Ne A :
+  ne A ->
+  ⟦ A ⟧ i ;; I ↘ wne
 | InterpExt_Bind p A B PA PF :
   ⟦ A ⟧ i ;; I ↘ PA ->
   (forall a, PA a -> exists PB, PF a PB) ->
@@ -30,7 +33,7 @@ Inductive InterpExt {n} i (I : nat -> Tm n -> Prop) : Tm n -> (Tm n -> Prop) ->
   ⟦ Univ j ⟧ i ;; I ↘ (I j)
 
 | InterpExt_Step A A0 PA :
-  RPar.R A A0 ->
+  RPar'.R A A0 ->
   ⟦ A0 ⟧ i ;; I ↘ PA ->
   ⟦ A ⟧ i ;; I ↘ PA
 where "⟦ A ⟧ i ;; I ↘ S" := (InterpExt i I A S).
@@ -59,6 +62,7 @@ Lemma InterpExt_lt_impl n i I I' A (PA : Tm n -> Prop) :
 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.
@@ -90,8 +94,8 @@ Qed.
 #[export]Hint Rewrite @InterpUnivN_nolt : InterpUniv.
 
 Lemma RPar_substone n (a b : Tm (S n)) (c : Tm n):
-    RPar.R a b -> RPar.R (subst_Tm (scons c VarTm) a) (subst_Tm (scons c VarTm) b).
-  Proof. hauto l:on inv:option use:RPar.substing, RPar.refl. Qed.
+    RPar'.R a b -> RPar'.R (subst_Tm (scons c VarTm) a) (subst_Tm (scons c VarTm) b).
+  Proof. hauto l:on inv:option use:RPar'.substing, RPar'.refl. Qed.
 
 Lemma InterpExt_Bind_inv n p i I (A : Tm n) B P
   (h :  ⟦ TBind p A B ⟧ i ;; I ↘ P) :
@@ -104,12 +108,22 @@ Proof.
   move E : (TBind p A B) h => T h.
   move : A B E.
   elim : T P / h => //.
+  - move => //= *. scongruence.
   - hauto l:on.
   - move => A A0 PA hA hA0 hPi A1 B ?. subst.
-    elim /RPar.inv : hA => //= _ p0 A2 A3 B0 B1 hA1 hB0 [*]. subst.
+    elim /RPar'.inv : hA => //= _ p0 A2 A3 B0 B1 hA1 hB0 [*]. subst.
     hauto lq:on ctrs:InterpExt use:RPar_substone.
 Qed.
 
+Lemma InterpExt_Ne_inv n i A I P
+  (h :  ⟦ A : Tm n  ⟧ i ;; I ↘ P) :
+  ne A ->
+  P = wne.
+Proof.
+  elim : A P / h => //=.
+  qauto l:on ctrs:prov inv:prov use:nf_refl.
+Qed.
+
 Lemma InterpExt_Univ_inv n i I j P
   (h :  ⟦ Univ j : Tm n  ⟧ i ;; I ↘ P) :
   P = I j /\ j < i.
@@ -117,8 +131,9 @@ Proof.
   move : h.
   move E : (Univ j) => T h. move : j E.
   elim : T P /h => //.
+  - move => //= *. scongruence.
   - hauto l:on.
-  - hauto lq:on rew:off inv:RPar.R.
+  - hauto lq:on rew:off inv:RPar'.R.
 Qed.
 
 Lemma InterpExt_Bind_nopf n p i I (A : Tm n) B PA  :
@@ -155,53 +170,79 @@ Proof.
 Qed.
 
 Lemma InterpExt_preservation n i I (A : Tm n) B P (h : InterpExt i I A P) :
-  RPar.R A B ->
+  RPar'.R A B ->
   ⟦ B ⟧ i ;; I ↘ P.
 Proof.
   move : B.
   elim : A P / h; auto.
+  - hauto lq:on use:nf_refl ctrs:InterpExt.
   - move => p A B PA PF hPA ihPA hPB hPB' ihPB T hT.
-    elim /RPar.inv :  hT => //.
+    elim /RPar'.inv :  hT => //.
     move => hPar p0 A0 A1 B0 B1 h0 h1 [? ?] ? ?; subst.
     apply InterpExt_Bind; auto => a PB hPB0.
     apply : ihPB; eauto.
-    sfirstorder use:RPar.cong, RPar.refl.
-  - hauto lq:on inv:RPar.R ctrs:InterpExt.
+    sfirstorder use:RPar'.cong, RPar'.refl.
+  - hauto lq:on inv:RPar'.R ctrs:InterpExt.
   - move => A B P h0 h1 ih1 C hC.
-    have [D [h2 h3]] := RPar_diamond  _ _ _ _ h0 hC.
+    have [D [h2 h3]] := RPar'_diamond  _ _ _ _ h0 hC.
     hauto lq:on ctrs:InterpExt.
 Qed.
 
 Lemma InterpUnivN_preservation n i (A : Tm n) B P (h : ⟦ A ⟧ i ↘ P) :
-  RPar.R A B ->
+  RPar'.R A B ->
   ⟦ B ⟧ i ↘ P.
 Proof. hauto l:on rew:db:InterpUnivN use: InterpExt_preservation. Qed.
 
 Lemma InterpExt_back_preservation_star n i I (A : Tm n) B P (h : ⟦ B ⟧ i ;; I ↘ P) :
-  rtc RPar.R A B ->
+  rtc RPar'.R A B ->
   ⟦ A ⟧ i ;; I ↘ P.
 Proof. induction 1; hauto l:on ctrs:InterpExt. Qed.
 
 Lemma InterpExt_preservation_star n i I (A : Tm n) B P (h : ⟦ A ⟧ i ;; I ↘ P) :
-  rtc RPar.R A B ->
+  rtc RPar'.R A B ->
   ⟦ B ⟧ i ;; I ↘ P.
 Proof. induction 1; hauto l:on use:InterpExt_preservation. Qed.
 
 Lemma InterpUnivN_preservation_star n i (A : Tm n) B P (h : ⟦ A ⟧ i ↘ P) :
-  rtc RPar.R A B ->
+  rtc RPar'.R A B ->
   ⟦ B ⟧ i ↘ P.
 Proof. hauto l:on rew:db:InterpUnivN use:InterpExt_preservation_star. Qed.
 
 Lemma InterpUnivN_back_preservation_star n i (A : Tm n) B P (h : ⟦ B ⟧ i ↘ P) :
-  rtc RPar.R A B ->
+  rtc RPar'.R A B ->
   ⟦ A ⟧ i ↘ P.
 Proof. hauto l:on rew:db:InterpUnivN use:InterpExt_back_preservation_star. Qed.
 
+Function hfb {n} (A : Tm n) :=
+  match A with
+  | TBind _ _ _ => true
+  | Univ _ => true
+  | _ => ne A
+  end.
+
+Inductive hfb_case {n} : Tm n -> Prop :=
+| hfb_bind p A B :
+  hfb_case (TBind p A B)
+| hfb_univ i :
+  hfb_case (Univ i)
+| hfb_ne A :
+  ne A ->
+  hfb_case A.
+
+Derive Dependent Inversion hfb_inv with (forall n (a : Tm n), hfb_case a) Sort Prop.
+
+Lemma ne_hfb {n} (A : Tm n) : ne A -> hfb A.
+Proof. case : A => //=. Qed.
+
+Lemma hfb_caseP {n} (A : Tm n) : hfb A -> hfb_case A.
+Proof. hauto lq:on ctrs:hfb_case inv:Tm use:ne_hfb. Qed.
+
 Lemma InterpExtInv n i I (A : Tm n) PA :
   ⟦ A ⟧ i ;; I ↘ PA ->
-  exists B, hfb B /\ rtc RPar.R A B /\  ⟦ B ⟧ i ;; I ↘ PA.
+  exists B, hfb B /\ rtc RPar'.R A B /\  ⟦ B ⟧ i ;; I ↘ PA.
 Proof.
   move => h. elim : A PA /h.
+  - hauto q:on ctrs:InterpExt, rtc use:ne_hfb.
   - move => p A B PA PF hPA _ hPF hPF0 _.
     exists (TBind p A B). repeat split => //=.
     apply rtc_refl.
@@ -211,16 +252,21 @@ Proof.
   - hauto lq:on ctrs:rtc.
 Qed.
 
-Lemma RPars_Pars  (A B : Tm n) :
-  rtc RPar.R A B ->
+Lemma RPar'_Par n (A B : Tm n) :
+  RPar'.R A B ->
+  Par.R A B.
+Proof. induction 1; hauto lq:on ctrs:Par.R. Qed.
+
+Lemma RPar's_Pars n (A B : Tm n) :
+  rtc RPar'.R A B ->
   rtc Par.R A B.
-Proof. hauto lq:on use:RPar_Par, rtc_subrel. Qed.
+Proof. hauto lq:on use:RPar'_Par, rtc_subrel. Qed.
 
-Lemma RPars_join  (A B : Tm n) :
-  rtc RPar.R A B -> join A B.
-Proof. hauto lq:on ctrs:rtc use:RPars_Pars. Qed.
+Lemma RPar's_join n (A B : Tm n) :
+  rtc RPar'.R A B -> join A B.
+Proof. hauto lq:on ctrs:rtc use:RPar's_Pars. Qed.
 
-Lemma bindspace_iff  p (PA : Tm n -> Prop) PF PF0 b  :
+Lemma bindspace_iff n p (PA : Tm n -> Prop) PF PF0 b  :
   (forall (a : Tm n) (PB PB0 : Tm n -> Prop), 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) ->
@@ -242,21 +288,68 @@ Proof.
     hauto lq:on rew:off.
 Qed.
 
-Lemma InterpExt_Join i I (A B : Tm n) PA PB :
+Lemma ne_prov_inv n (a : Tm n) :
+  ne a -> exists i, prov (VarTm i) a /\ extract a = VarTm i.
+Proof.
+  elim : n /a => //=.
+  - hauto lq:on ctrs:prov.
+  - hauto lq:on rew:off ctrs:prov b:on.
+  - hauto lq:on ctrs:prov.
+Qed.
+
+Lemma join_bind_ne_contra n p (A : Tm n) B C :
+  ne C ->
+  join (TBind p A B) C -> False.
+Proof.
+  move => hC [D [h0 h1]].
+  move /pars_pi_inv : h0 => [A0 [B0 [h2 [h3 h4]]]].
+  have [i] : exists i, prov (VarTm i) C by sfirstorder use:ne_prov_inv.
+  move => h.
+  have {}h : prov (VarTm i) D by eauto using prov_pars.
+  have : extract D = VarTm i by sfirstorder use:prov_extract.
+  congruence.
+Qed.
+
+Lemma join_univ_ne_contra n i C :
+  ne C ->
+  join (Univ i : Tm n) C -> False.
+Proof.
+  move => hC [D [h0 h1]].
+  move /pars_univ_inv : h0 => ?.
+  have [j] : exists i, prov (VarTm i) C by sfirstorder use:ne_prov_inv.
+  move => h.
+  have {}h : prov (VarTm j) D by eauto using prov_pars.
+  have : extract D = VarTm j by sfirstorder use:prov_extract.
+  congruence.
+Qed.
+
+#[export]Hint Resolve join_univ_ne_contra join_bind_ne_contra join_univ_pi_contra join_symmetric join_transitive : join.
+
+Lemma InterpExt_Join n i I (A B : Tm n) PA PB :
   ⟦ A ⟧ i ;; I ↘ PA ->
   ⟦ B ⟧ i ;; I ↘ PB ->
   join A B ->
   PA = PB.
 Proof.
   move => h. move : B PB. elim : A PA /h.
+  - move => A hA B PB /InterpExtInv.
+    move => [B0 []].
+    move /hfb_caseP. elim/hfb_inv => _.
+    + move => p A0 B1 ? [/RPar's_join h0 h1] h2. subst. exfalso.
+      eauto with join.
+    + move => ? ? [/RPar's_join *]. subst. exfalso.
+      eauto with join.
+    + hauto lq:on use:InterpExt_Ne_inv.
   - move => p A B PA PF hPA ihPA hTot hRes ihPF U PU /InterpExtInv.
     move => [B0 []].
-    case : B0 => //=.
-    + move => p0 A0 B0 _ [hr hPi].
+    move /hfb_caseP.
+    elim /hfb_inv => _.
+    rename B0 into B00.
+    + move => p0 A0 B0 ?  [hr hPi]. subst.
       move /InterpExt_Bind_inv : hPi.
       move => [PA0][PF0][hPA0][hTot0][hRes0]?. subst.
       move => hjoin.
-      have{}hr : join U (TBind p0 A0 B0) by auto using RPars_join.
+      have{}hr : join U (TBind p0 A0 B0) by auto using RPar's_join.
       have hj : join (TBind p A B) (TBind p0 A0 B0) by eauto using join_transitive.
       have {hj} : p0 = p /\ join A A0 /\ join B B0 by hauto l:on use:join_pi_inj.
       move => [? [h0 h1]]. subst.
@@ -268,36 +361,38 @@ Proof.
       move => a PB PB0 hPB hPB0.
       apply : ihPF; eauto.
       by apply join_substing.
-    + move => j _.
+    + move => j ?. subst.
       move => [h0 h1] h.
-      have ? : join U (Univ j) by eauto using RPars_join.
+      have ? : join U (Univ j) by eauto using RPar's_join.
       have : join (TBind p A B) (Univ j) by eauto using join_transitive.
       move => ?. exfalso.
       eauto using join_univ_pi_contra.
+    + move => A0 ? ? [/RPar's_join ?]. subst.
+      move => _ ?. exfalso. eauto with join.
   - move => j ? B PB /InterpExtInv.
-    move => [+ []]. case => //=.
+    move => [? []]. move/hfb_caseP.
+    elim /hfb_inv => //= _.
     + move => p A0 B0 _ [].
-      move /RPars_join => *.
-      have ?  : join (TBind p A0 B0) (Univ j) by eauto using join_symmetric, join_transitive.
-      exfalso.
-      eauto using join_univ_pi_contra.
-    + move => m _ [/RPars_join h0 + h1].
+      move /RPar's_join => *.
+      exfalso. eauto with join.
+    + move => m _ [/RPar's_join h0 + h1].
       have /join_univ_inj {h0 h1} ?  : join (Univ j : Tm n) (Univ m) by eauto using join_transitive.
       subst.
       move /InterpExt_Univ_inv. firstorder.
+    + move => A ? ? [/RPar's_join] *. subst. exfalso. eauto with join.
   - move => A A0 PA h.
-    have /join_symmetric {}h : join A A0 by hauto lq:on ctrs:rtc use:RPar_Par, relations.rtc_once.
+    have /join_symmetric {}h : join A A0 by hauto lq:on ctrs:rtc use:RPar'_Par, relations.rtc_once.
     eauto using join_transitive.
 Qed.
 
-Lemma InterpUniv_Join i (A B : Tm n) PA PB :
+Lemma InterpUniv_Join n i (A B : Tm n) PA PB :
   ⟦ A ⟧ i ↘ PA ->
   ⟦ B ⟧ i ↘ PB ->
   join A B ->
   PA = PB.
 Proof. hauto l:on use:InterpExt_Join rew:db:InterpUniv. Qed.
 
-Lemma InterpUniv_Bind_inv p i  (A : Tm n) B P
+Lemma InterpUniv_Bind_inv n p i  (A : Tm n) B P
   (h :  ⟦ TBind p A B ⟧ i ↘ P) :
   exists (PA : Tm n -> Prop) (PF : Tm n -> (Tm n -> Prop) -> Prop),
      ⟦ A ⟧ i ↘ PA /\
@@ -306,24 +401,24 @@ Lemma InterpUniv_Bind_inv p i  (A : Tm n) B P
     P = BindSpace p PA PF.
 Proof. hauto l:on use:InterpExt_Bind_inv rew:db:InterpUniv. Qed.
 
-Lemma InterpUniv_Univ_inv i j P
+Lemma InterpUniv_Univ_inv n i j P
   (h :  ⟦ Univ j  ⟧ i ↘ P) :
   P = (fun (A : Tm n) => exists PA, ⟦ A ⟧ j ↘ PA) /\ j < i.
 Proof. hauto l:on use:InterpExt_Univ_inv rew:db:InterpUniv. Qed.
 
-Lemma InterpExt_Functional i I (A B : Tm n) PA PB :
+Lemma InterpExt_Functional n i I (A B : Tm n) PA PB :
   ⟦ A ⟧ i ;; I ↘ PA ->
   ⟦ A ⟧ i ;; I ↘ PB ->
   PA = PB.
 Proof. hauto use:InterpExt_Join, join_refl. Qed.
 
-Lemma InterpUniv_Functional i (A : Tm n) PA PB :
+Lemma InterpUniv_Functional n i (A : Tm n) PA PB :
   ⟦ A ⟧ i ↘ PA ->
   ⟦ A ⟧ i ↘ PB ->
   PA = PB.
 Proof. hauto use:InterpExt_Functional rew:db:InterpUniv. Qed.
 
-Lemma InterpUniv_Join' i j (A B : Tm n) PA PB :
+Lemma InterpUniv_Join' n i j (A B : Tm n) PA PB :
   ⟦ A ⟧ i ↘ PA ->
   ⟦ B ⟧ j ↘ PB ->
   join A B ->
@@ -336,15 +431,15 @@ Proof.
   eauto using InterpUniv_Join.
 Qed.
 
-Lemma InterpUniv_Functional' i j A PA PB :
-  ⟦ A ⟧ i ↘ PA ->
+Lemma InterpUniv_Functional' n i j A PA PB :
+  ⟦ A : Tm n ⟧ i ↘ PA ->
   ⟦ A ⟧ j ↘ PB ->
   PA = PB.
 Proof.
   hauto l:on use:InterpUniv_Join', join_refl.
 Qed.
 
-Lemma InterpExt_Bind_inv_nopf i I p A B P (h :  ⟦TBind p A B ⟧ i ;; I ↘ P) :
+Lemma InterpExt_Bind_inv_nopf i n I p A B P (h :  ⟦TBind p A B ⟧ i ;; I ↘ P) :
   exists (PA : Tm n -> Prop),
      ⟦ A ⟧ i ;; I ↘ PA /\
     (forall a, PA a -> exists PB, ⟦ subst_Tm (scons a VarTm) B ⟧ i ;; I ↘ PB) /\
@@ -366,34 +461,35 @@ Proof.
       split; hauto q:on use:InterpExt_Functional.
 Qed.
 
-Lemma InterpUniv_Bind_inv_nopf i p A B P (h :  ⟦TBind p A B ⟧ i ↘ P) :
+Lemma InterpUniv_Bind_inv_nopf n i p A B P (h :  ⟦TBind p A B ⟧ i ↘ P) :
   exists (PA : Tm n -> Prop),
      ⟦ A ⟧ i ↘ PA /\
     (forall a, PA a -> exists PB, ⟦ subst_Tm (scons a VarTm) B ⟧ i ↘ PB) /\
       P = BindSpace p PA (fun a PB => ⟦ subst_Tm (scons a VarTm) B ⟧ i ↘ PB).
 Proof. hauto l:on use:InterpExt_Bind_inv_nopf rew:db:InterpUniv. Qed.
 
-Lemma InterpExt_back_clos i I (A : Tm n) PA :
-  (forall j,  forall a b, (RPar.R a b) ->  I j b -> I j a) ->
+Lemma InterpExt_back_clos n i I (A : Tm n) PA :
+  (forall j,  forall a b, (RPar'.R a b) ->  I j b -> I j a) ->
     ⟦ A ⟧ i ;; I ↘ PA ->
-    forall a b, (RPar.R a b) ->
+    forall a b, (RPar'.R a b) ->
            PA b -> PA a.
 Proof.
   move => hI h.
   elim : A PA /h.
+  - hauto q:on ctrs:rtc unfold:wne.
   - move => p A B PA PF hPA ihPA hTot hRes ihPF a b hr.
     case : p => //=.
-    + have  : forall b0 b1 a, RPar.R b0 b1 -> RPar.R (App b0 a) (App b1 a)
-          by hauto lq:on ctrs:RPar.R use:RPar.refl.
+    + have  : forall b0 b1 a, RPar'.R b0 b1 -> RPar'.R (App b0 a) (App b1 a)
+          by hauto lq:on ctrs:RPar'.R use:RPar'.refl.
       hauto lq:on rew:off unfold:ProdSpace.
     + hauto lq:on ctrs:rtc unfold:SumSpace.
   - eauto.
   - eauto.
 Qed.
 
-Lemma InterpUniv_back_clos i (A : Tm n) PA :
+Lemma InterpUniv_back_clos n i (A : Tm n) PA :
     ⟦ A ⟧ i ↘ PA ->
-    forall a b, (RPar.R a b) ->
+    forall a b, (RPar'.R a b) ->
            PA b -> PA a.
 Proof.
   simp InterpUniv.
@@ -401,9 +497,9 @@ Proof.
   hauto lq:on ctrs:rtc use:InterpUnivN_back_preservation_star.
 Qed.
 
-Lemma InterpUniv_back_clos_star i (A : Tm n) PA :
+Lemma InterpUniv_back_clos_star n i (A : Tm n) PA :
     ⟦ A ⟧ i ↘ PA ->
-    forall a b, rtc RPar.R a b ->
+    forall a b, rtc RPar'.R a b ->
            PA b -> PA a.
 Proof.
   move => h  a b.
@@ -411,30 +507,31 @@ Proof.
   hauto lq:on use:InterpUniv_back_clos.
 Qed.
 
-Definition ρ_ok {n} Γ (ρ : fin n -> Tm n) := forall i m PA,
-  ⟦ subst_Tm ρ (Γ i) ⟧ m ↘ PA -> PA (ρ i).
+Definition ρ_ok {n} (Γ : fin n -> Tm n) m (ρ : fin n -> Tm m) := forall i k PA,
+  ⟦ subst_Tm ρ (Γ i) ⟧ k ↘ PA -> PA (ρ i).
 
-Definition SemWt {n} Γ (a A : Tm n) := forall ρ, ρ_ok Γ ρ -> exists m PA, ⟦ subst_Tm ρ A ⟧ m ↘ PA /\ PA (subst_Tm ρ a).
+Definition SemWt {n} Γ (a A : Tm n) := forall m ρ, ρ_ok Γ m ρ -> exists k PA, ⟦ subst_Tm ρ A ⟧ k ↘ PA /\ PA (subst_Tm ρ a).
 Notation "Γ ⊨ a ∈ A" := (SemWt Γ a A) (at level 70).
 
 (* Semantic context wellformedness *)
 Definition SemWff {n} Γ := forall (i : fin n), exists j, Γ ⊨ Γ i ∈ Univ j.
 Notation "⊨ Γ" := (SemWff Γ) (at level 70).
 
-Lemma ρ_ok_nil ρ :
-  ρ_ok null ρ.
+Lemma ρ_ok_id n (Γ : fin n -> Tm n)  :
+  ρ_ok Γ n VarTm.
 Proof.  rewrite /ρ_ok. inversion i; subst. Qed.
 
 Lemma ρ_ok_cons n i (Γ : fin n -> Tm n) ρ a PA A :
   ⟦ subst_Tm ρ A ⟧ i ↘ PA -> PA a ->
   ρ_ok Γ ρ ->
-  ρ_ok (funcomp (ren_Tm shift) (scons A Γ)) ((scons a ρ)).
+  ρ_ok (funcomp (ren_Tm 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'.
@@ -573,7 +670,7 @@ Proof.
   intros (m & PB0 & hPB0 & hPB0').
   replace PB0 with PB in * by hauto l:on use:InterpUniv_Functional'.
   apply : InterpUniv_back_clos; eauto.
-  apply : RPar.AppAbs'; eauto using RPar.refl.
+  apply : RPar'.AppAbs'; eauto using RPar'.refl.
   by asimpl.
 Qed.
 
@@ -629,22 +726,22 @@ Proof.
   rewrite /SumSpace.
   move => [a0 [b0 [h4 [h5 h6]]]].
   exists m, S. split => //=.
-  have {}h4 : rtc RPar.R (Proj PL (subst_Tm ρ a)) (Proj PL (Pair a0 b0)) by eauto using RPars.ProjCong.
-  have ? : RPar.R (Proj PL (Pair a0 b0)) a0 by hauto l:on use:RPar.refl, RPar.ProjPair'.
-  have : rtc RPar.R (Proj PL (subst_Tm ρ a)) a0 by eauto using @relations.rtc_r.
+  have {}h4 : rtc RPar'.R (Proj PL (subst_Tm ρ a)) (Proj PL (Pair a0 b0)) by eauto using RPar's.ProjCong.
+  have ? : RPar'.R (Proj PL (Pair a0 b0)) a0 by hauto l:on use:RPar'.refl, RPar'.ProjPair'.
+  have : rtc RPar'.R (Proj PL (subst_Tm ρ a)) a0 by eauto using @relations.rtc_r.
   move => h.
   apply : InterpUniv_back_clos_star; eauto.
 Qed.
 
-Lemma substing_RPar n m (A : Tm (S n)) ρ (B : Tm m) C :
-  RPar.R B C ->
-  RPar.R (subst_Tm (scons B ρ) A) (subst_Tm (scons C ρ) A).
-Proof. hauto lq:on inv:option use:RPar.morphing, RPar.refl. Qed.
+Lemma substing_RPar' n m (A : Tm (S n)) ρ (B : Tm m) C :
+  RPar'.R B C ->
+  RPar'.R (subst_Tm (scons B ρ) A) (subst_Tm (scons C ρ) A).
+Proof. hauto lq:on inv:option use:RPar'.morphing, RPar'.refl. Qed.
 
-Lemma substing_RPars n m (A : Tm (S n)) ρ (B : Tm m) C :
-  rtc RPar.R B C ->
-  rtc RPar.R (subst_Tm (scons B ρ) A) (subst_Tm (scons C ρ) A).
-Proof. induction 1; hauto lq:on ctrs:rtc use:substing_RPar. Qed.
+Lemma substing_RPar's n m (A : Tm (S n)) ρ (B : Tm m) C :
+  rtc RPar'.R B C ->
+  rtc RPar'.R (subst_Tm (scons B ρ) A) (subst_Tm (scons C ρ) A).
+Proof. induction 1; hauto lq:on ctrs:rtc use:substing_RPar'. Qed.
 
 Lemma ST_Proj2 n Γ (a : Tm n) A B :
   Γ ⊨ a ∈ TBind TSig A B ->
@@ -658,13 +755,13 @@ Proof.
   move => [a0 [b0 [h4 [h5 h6]]]].
   specialize h3 with (1 := h5).
   move : h3 => [PB hPB].
-  have hr : forall p, rtc RPar.R (Proj p (subst_Tm ρ a)) (Proj p (Pair a0 b0)) by eauto using RPars.ProjCong.
-  have hrl : RPar.R (Proj PL (Pair a0 b0)) a0 by hauto l:on use:RPar.ProjPair', RPar.refl.
-  have hrr : RPar.R (Proj PR (Pair a0 b0)) b0 by hauto l:on use:RPar.ProjPair', RPar.refl.
+  have hr : forall p, rtc RPar'.R (Proj p (subst_Tm ρ a)) (Proj p (Pair a0 b0)) by eauto using RPar's.ProjCong.
+  have hrl : RPar'.R (Proj PL (Pair a0 b0)) a0 by hauto l:on use:RPar'.ProjPair', RPar'.refl.
+  have hrr : RPar'.R (Proj PR (Pair a0 b0)) b0 by hauto l:on use:RPar'.ProjPair', RPar'.refl.
   exists m, PB.
   asimpl. split.
-  - have h : rtc RPar.R (Proj PL (subst_Tm ρ a)) a0 by eauto using @relations.rtc_r.
-    have {}h : rtc RPar.R (subst_Tm (scons (Proj PL (subst_Tm ρ a)) ρ) B) (subst_Tm (scons a0 ρ) B) by eauto using substing_RPars.
+  - have h : rtc RPar'.R (Proj PL (subst_Tm ρ a)) a0 by eauto using @relations.rtc_r.
+    have {}h : rtc RPar'.R (subst_Tm (scons (Proj PL (subst_Tm ρ a)) ρ) B) (subst_Tm (scons a0 ρ) B) by eauto using substing_RPar's.
     move : hPB. asimpl.
     eauto using InterpUnivN_back_preservation_star.
   - hauto lq:on use:@relations.rtc_r, InterpUniv_back_clos_star.