From 3b8fe388dcaf8d1026060dc20db7a1b0254646a3 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <liuyiyun@seas.upenn.edu>
Date: Thu, 3 Apr 2025 21:18:17 -0400
Subject: [PATCH] Make the internal language even smaller

---
 syntax.sig                   |   4 +-
 theories/Autosubst2/syntax.v |  64 ++----
 theories/compile.v           | 169 ++++-----------
 theories/fp_red.v            | 400 +++++++----------------------------
 4 files changed, 133 insertions(+), 504 deletions(-)

diff --git a/syntax.sig b/syntax.sig
index e63c3b4..d2728a9 100644
--- a/syntax.sig
+++ b/syntax.sig
@@ -14,9 +14,7 @@ PAbs : (bind PTm in PTm) -> PTm
 PApp : PTm -> PTm -> PTm
 PPair : PTm -> PTm -> PTm
 PProj : PTag -> PTm -> PTm
-PConst : TTag -> PTm
-PUniv : nat -> PTm
-PBot : PTm
+PConst : nat -> PTm
 
 Abs : (bind Tm in Tm) -> Tm
 App : Tm -> Tm -> Tm
diff --git a/theories/Autosubst2/syntax.v b/theories/Autosubst2/syntax.v
index 659d8b0..3634dc1 100644
--- a/theories/Autosubst2/syntax.v
+++ b/theories/Autosubst2/syntax.v
@@ -19,29 +19,13 @@ Proof.
 exact (eq_refl).
 Qed.
 
-Inductive TTag : Type :=
-  | TPi : TTag
-  | TSig : TTag.
-
-Lemma congr_TPi : TPi = TPi.
-Proof.
-exact (eq_refl).
-Qed.
-
-Lemma congr_TSig : TSig = TSig.
-Proof.
-exact (eq_refl).
-Qed.
-
 Inductive PTm : Type :=
   | VarPTm : nat -> PTm
   | PAbs : PTm -> PTm
   | PApp : PTm -> PTm -> PTm
   | PPair : PTm -> PTm -> PTm
   | PProj : PTag -> PTm -> PTm
-  | PConst : TTag -> PTm
-  | PUniv : nat -> PTm
-  | PBot : PTm.
+  | PConst : nat -> PTm.
 
 Lemma congr_PAbs {s0 : PTm} {t0 : PTm} (H0 : s0 = t0) : PAbs s0 = PAbs t0.
 Proof.
@@ -69,22 +53,12 @@ exact (eq_trans (eq_trans eq_refl (ap (fun x => PProj x s1) H0))
          (ap (fun x => PProj t0 x) H1)).
 Qed.
 
-Lemma congr_PConst {s0 : TTag} {t0 : TTag} (H0 : s0 = t0) :
+Lemma congr_PConst {s0 : nat} {t0 : nat} (H0 : s0 = t0) :
   PConst s0 = PConst t0.
 Proof.
 exact (eq_trans eq_refl (ap (fun x => PConst x) H0)).
 Qed.
 
-Lemma congr_PUniv {s0 : nat} {t0 : nat} (H0 : s0 = t0) : PUniv s0 = PUniv t0.
-Proof.
-exact (eq_trans eq_refl (ap (fun x => PUniv x) H0)).
-Qed.
-
-Lemma congr_PBot : PBot = PBot.
-Proof.
-exact (eq_refl).
-Qed.
-
 Lemma upRen_PTm_PTm (xi : nat -> nat) : nat -> nat.
 Proof.
 exact (up_ren xi).
@@ -98,8 +72,6 @@ Fixpoint ren_PTm (xi_PTm : nat -> nat) (s : PTm) {struct s} : PTm :=
   | PPair s0 s1 => PPair (ren_PTm xi_PTm s0) (ren_PTm xi_PTm s1)
   | PProj s0 s1 => PProj s0 (ren_PTm xi_PTm s1)
   | PConst s0 => PConst s0
-  | PUniv s0 => PUniv s0
-  | PBot => PBot
   end.
 
 Lemma up_PTm_PTm (sigma : nat -> PTm) : nat -> PTm.
@@ -115,8 +87,6 @@ Fixpoint subst_PTm (sigma_PTm : nat -> PTm) (s : PTm) {struct s} : PTm :=
   | PPair s0 s1 => PPair (subst_PTm sigma_PTm s0) (subst_PTm sigma_PTm s1)
   | PProj s0 s1 => PProj s0 (subst_PTm sigma_PTm s1)
   | PConst s0 => PConst s0
-  | PUniv s0 => PUniv s0
-  | PBot => PBot
   end.
 
 Lemma upId_PTm_PTm (sigma : nat -> PTm) (Eq : forall x, sigma x = VarPTm x) :
@@ -145,8 +115,6 @@ subst_PTm sigma_PTm s = s :=
         (idSubst_PTm sigma_PTm Eq_PTm s1)
   | PProj s0 s1 => congr_PProj (eq_refl s0) (idSubst_PTm sigma_PTm Eq_PTm s1)
   | PConst s0 => congr_PConst (eq_refl s0)
-  | PUniv s0 => congr_PUniv (eq_refl s0)
-  | PBot => congr_PBot
   end.
 
 Lemma upExtRen_PTm_PTm (xi : nat -> nat) (zeta : nat -> nat)
@@ -177,8 +145,6 @@ ren_PTm xi_PTm s = ren_PTm zeta_PTm s :=
   | PProj s0 s1 =>
       congr_PProj (eq_refl s0) (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1)
   | PConst s0 => congr_PConst (eq_refl s0)
-  | PUniv s0 => congr_PUniv (eq_refl s0)
-  | PBot => congr_PBot
   end.
 
 Lemma upExt_PTm_PTm (sigma : nat -> PTm) (tau : nat -> PTm)
@@ -210,8 +176,6 @@ subst_PTm sigma_PTm s = subst_PTm tau_PTm s :=
   | PProj s0 s1 =>
       congr_PProj (eq_refl s0) (ext_PTm sigma_PTm tau_PTm Eq_PTm s1)
   | PConst s0 => congr_PConst (eq_refl s0)
-  | PUniv s0 => congr_PUniv (eq_refl s0)
-  | PBot => congr_PBot
   end.
 
 Lemma up_ren_ren_PTm_PTm (xi : nat -> nat) (zeta : nat -> nat)
@@ -242,8 +206,6 @@ Fixpoint compRenRen_PTm (xi_PTm : nat -> nat) (zeta_PTm : nat -> nat)
       congr_PProj (eq_refl s0)
         (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1)
   | PConst s0 => congr_PConst (eq_refl s0)
-  | PUniv s0 => congr_PUniv (eq_refl s0)
-  | PBot => congr_PBot
   end.
 
 Lemma up_ren_subst_PTm_PTm (xi : nat -> nat) (tau : nat -> PTm)
@@ -278,8 +240,6 @@ Fixpoint compRenSubst_PTm (xi_PTm : nat -> nat) (tau_PTm : nat -> PTm)
       congr_PProj (eq_refl s0)
         (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1)
   | PConst s0 => congr_PConst (eq_refl s0)
-  | PUniv s0 => congr_PUniv (eq_refl s0)
-  | PBot => congr_PBot
   end.
 
 Lemma up_subst_ren_PTm_PTm (sigma : nat -> PTm) (zeta_PTm : nat -> nat)
@@ -325,8 +285,6 @@ ren_PTm zeta_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s :=
       congr_PProj (eq_refl s0)
         (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1)
   | PConst s0 => congr_PConst (eq_refl s0)
-  | PUniv s0 => congr_PUniv (eq_refl s0)
-  | PBot => congr_PBot
   end.
 
 Lemma up_subst_subst_PTm_PTm (sigma : nat -> PTm) (tau_PTm : nat -> PTm)
@@ -373,8 +331,6 @@ subst_PTm tau_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s :=
       congr_PProj (eq_refl s0)
         (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1)
   | PConst s0 => congr_PConst (eq_refl s0)
-  | PUniv s0 => congr_PUniv (eq_refl s0)
-  | PBot => congr_PBot
   end.
 
 Lemma renRen_PTm (xi_PTm : nat -> nat) (zeta_PTm : nat -> nat) (s : PTm) :
@@ -464,8 +420,6 @@ Fixpoint rinst_inst_PTm (xi_PTm : nat -> nat) (sigma_PTm : nat -> PTm)
   | PProj s0 s1 =>
       congr_PProj (eq_refl s0) (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1)
   | PConst s0 => congr_PConst (eq_refl s0)
-  | PUniv s0 => congr_PUniv (eq_refl s0)
-  | PBot => congr_PBot
   end.
 
 Lemma rinstInst'_PTm (xi_PTm : nat -> nat) (s : PTm) :
@@ -527,6 +481,20 @@ Proof.
 exact (fun x => eq_refl).
 Qed.
 
+Inductive TTag : Type :=
+  | TPi : TTag
+  | TSig : TTag.
+
+Lemma congr_TPi : TPi = TPi.
+Proof.
+exact (eq_refl).
+Qed.
+
+Lemma congr_TSig : TSig = TSig.
+Proof.
+exact (eq_refl).
+Qed.
+
 Inductive Tm : Type :=
   | VarTm : nat -> Tm
   | Abs : Tm -> Tm
diff --git a/theories/compile.v b/theories/compile.v
index e481d71..878aac0 100644
--- a/theories/compile.v
+++ b/theories/compile.v
@@ -1,47 +1,47 @@
-Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax fp_red.
+Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax fp_red.
 Require Import ssreflect ssrbool.
 From Hammer Require Import Tactics.
 From stdpp Require Import relations (rtc(..)).
 
 Module Compile.
-  Fixpoint F {n} (a : Tm n) : Tm n :=
+  Definition compileTag p := if p is TPi then 0 else 1.
+
+  Fixpoint F (a : Tm) : PTm :=
     match a with
-    | TBind p A B => Pair (Pair (Const p) (F A)) (Abs (F B))
-    | Const k => Const k
-    | Univ i => Univ i
-    | Abs a => Abs (F a)
-    | App a b => App (F a) (F b)
-    | VarTm i => VarTm i
-    | Pair a b => Pair (F a) (F b)
-    | Proj t a => Proj t (F a)
-    | Bot => Bot
-    | If a b c => App (App (F a) (F b)) (F c)
-    | BVal b => if b then (Abs (Abs (VarTm (shift var_zero)))) else (Abs (Abs (VarTm var_zero)))
-    | Bool => Bool
+    | TBind p A B => PPair (PPair (PConst (compileTag p)) (F A)) (PAbs (F B))
+    | Univ i => PConst (3 + i)
+    | Abs a => PAbs (F a)
+    | App a b => PApp (F a) (F b)
+    | VarTm i => VarPTm i
+    | Pair a b => PPair (F a) (F b)
+    | Proj t a => PProj t (F a)
+    | If a b c => PApp (PApp (F a) (F b)) (F c)
+    | BVal b => if b then (PAbs (PAbs (VarPTm (shift var_zero)))) else (PAbs (PAbs (VarPTm var_zero)))
+    | Bool => PConst 2
     end.
 
-  Lemma renaming n m (a : Tm n) (ξ : fin n -> fin m) :
-    F (ren_Tm ξ a)= ren_Tm ξ (F a).
-  Proof. move : m ξ. elim : n  / a => //=; hauto lq:on. Qed.
+  Lemma renaming (a : Tm) (ξ : nat -> nat) :
+    F (ren_Tm ξ a)= ren_PTm ξ (F a).
+  Proof. move : ξ. elim : a => //=; hauto lq:on. Qed.
 
   #[local]Hint Rewrite Compile.renaming : compile.
 
-  Lemma morphing n m (a : Tm n) (ρ0 ρ1 : fin n -> Tm m) :
+  Lemma morphing (a : Tm) ρ0 ρ1 :
     (forall i, ρ0 i = F (ρ1 i)) ->
-    subst_Tm ρ0 (F a) = F (subst_Tm ρ1 a).
+    subst_PTm ρ0 (F a) = F (subst_Tm ρ1 a).
   Proof.
-    move : m ρ0 ρ1. elim : n / a => n//=.
-    - hauto lq:on inv:option rew:db:compile unfold:funcomp.
+    move : ρ0 ρ1. elim : a =>//=.
+    - hauto lq:on inv:nat rew:db:compile unfold:funcomp.
     - hauto lq:on rew:off.
     - hauto lq:on rew:off.
     - hauto lq:on.
-    - hauto lq:on inv:option rew:db:compile unfold:funcomp.
+    - hauto lq:on inv:nat rew:db:compile unfold:funcomp.
     - hauto lq:on rew:off.
     - hauto lq:on rew:off.
   Qed.
 
-  Lemma substing n b (a : Tm (S n)) :
-    subst_Tm (scons (F b) VarTm) (F a) = F (subst_Tm (scons b VarTm) a).
+  Lemma substing b (a : Tm) :
+    subst_PTm (scons (F b) VarPTm) (F a) = F (subst_Tm (scons b VarTm) a).
   Proof.
     apply morphing.
     case => //=.
@@ -53,38 +53,44 @@ End Compile.
 
 
 Module Join.
-  Definition R {n} (a b : Tm n) := join (Compile.F a) (Compile.F b).
+  Definition R (a b : Tm) := join (Compile.F a) (Compile.F b).
 
-  Lemma BindInj n p0 p1 (A0 A1 : Tm n) B0 B1  :
+  Lemma compileTagInj p0 p1 :
+    Compile.compileTag p0 = Compile.compileTag p1 -> p0 = p1.
+  Proof.
+    case : p0 ; case : p1 => //.
+  Qed.
+
+  Lemma BindInj p0 p1 (A0 A1 : Tm) B0 B1  :
     R (TBind p0 A0 B0) (TBind p1 A1 B1) -> p0 = p1 /\ R A0 A1 /\ R B0 B1.
   Proof.
     rewrite /R /= !join_pair_inj.
-    move => [[/join_const_inj h0 h1] h2].
+    move => [[/join_const_inj /compileTagInj h0 h1] h2].
     apply abs_eq in h2.
-    evar (t : Tm (S n)).
-    have : join (App (ren_Tm shift (Abs (Compile.F B1))) (VarTm var_zero)) t by
+    evar (t : PTm ).
+    have : join (PApp (ren_PTm shift (PAbs (Compile.F B1))) (VarPTm var_zero)) t by
       apply Join.FromPar; apply Par.AppAbs; auto using Par.refl.
-    subst t. rewrite -/ren_Tm.
-    move : h2. move /join_transitive => /[apply]. asimpl => h2.
+    subst t. rewrite -/ren_PTm.
+    move : h2. move /join_transitive => /[apply]. asimpl; rewrite subst_id => h2.
     tauto.
   Qed.
 
-  Lemma UnivInj n i j : R (Univ i : Tm n) (Univ j) -> i = j.
-  Proof. hauto l:on use:join_univ_inj. Qed.
+  Lemma UnivInj i j : R (Univ i : Tm) (Univ j) -> i = j.
+  Proof. hauto l:on use:join_const_inj. Qed.
 
-  Lemma transitive n (a b c : Tm n) :
+  Lemma transitive (a b c : Tm) :
     R a b -> R b c -> R a c.
   Proof. hauto l:on use:join_transitive unfold:R. Qed.
 
-  Lemma symmetric n (a b : Tm n) :
+  Lemma symmetric (a b : Tm) :
     R a b -> R b a.
   Proof. hauto l:on use:join_symmetric. Qed.
 
-  Lemma reflexive n (a : Tm n) :
+  Lemma reflexive (a : Tm) :
     R a a.
   Proof. hauto l:on use:join_refl. Qed.
 
-  Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) :
+  Lemma substing (a b : Tm) (ρ : nat -> Tm) :
     R a b -> R (subst_Tm ρ a) (subst_Tm ρ b).
   Proof.
     rewrite /R.
@@ -95,92 +101,3 @@ Module Join.
   Qed.
 
 End Join.
-
-Module Equiv.
-  Inductive R {n} : Tm n -> Tm n ->  Prop :=
-  (***************** Beta ***********************)
-  | AppAbs a b :
-    R (App (Abs a) b)  (subst_Tm (scons b VarTm) a)
-  | ProjPair p a b :
-    R (Proj p (Pair a b)) (if p is PL then a else b)
-
-  (****************** Eta ***********************)
-  | AppEta a :
-    R a (Abs (App (ren_Tm shift a) (VarTm var_zero)))
-  | PairEta a :
-    R a (Pair (Proj PL a) (Proj PR a))
-
-  (*************** Congruence ********************)
-  | Var i : R (VarTm i) (VarTm i)
-  | AbsCong a b :
-    R a b ->
-    R (Abs a) (Abs b)
-  | AppCong a0 a1 b0 b1 :
-    R a0 a1 ->
-    R b0 b1 ->
-    R (App a0 b0) (App a1 b1)
-  | PairCong a0 a1 b0 b1 :
-    R a0 a1 ->
-    R b0 b1 ->
-    R (Pair a0 b0) (Pair a1 b1)
-  | ProjCong p a0 a1 :
-    R a0 a1 ->
-    R (Proj p a0) (Proj p a1)
-  | BindCong p A0 A1 B0 B1:
-    R A0 A1 ->
-    R B0 B1 ->
-    R (TBind p A0 B0) (TBind p A1 B1)
-  | UnivCong i :
-    R (Univ i) (Univ i).
-End Equiv.
-
-Module EquivJoin.
-  Lemma FromEquiv n (a b : Tm n) : Equiv.R a b -> Join.R a b.
-  Proof.
-    move => h. elim : n a b /h => n.
-    - move => a b.
-      rewrite /Join.R /join /=.
-      eexists. split. apply relations.rtc_once.
-      apply Par.AppAbs; auto using Par.refl.
-      rewrite Compile.substing.
-      apply relations.rtc_refl.
-    - move => p a b.
-      apply Join.FromPar.
-      simpl. apply : Par.ProjPair'; auto using Par.refl.
-      case : p => //=.
-    - move => a. apply Join.FromPar => /=.
-      apply : Par.AppEta'; auto using Par.refl.
-      by autorewrite with compile.
-    - move => a. apply Join.FromPar => /=.
-      apply : Par.PairEta; auto using Par.refl.
-    - hauto l:on use:Join.FromPar, Par.Var.
-    - hauto lq:on use:Join.AbsCong.
-    - qauto l:on use:Join.AppCong.
-    - qauto l:on use:Join.PairCong.
-    - qauto use:Join.ProjCong.
-    - rewrite /Join.R => p A0 A1 B0 B1 _ hA _ hB /=.
-      sfirstorder use:Join.PairCong,Join.AbsCong,Join.FromPar,Par.ConstCong.
-    - hauto l:on.
-  Qed.
-End EquivJoin.
-
-Lemma compile_rpar n (a b : Tm n) : RPar'.R a b -> RPar'.R (Compile.F a) (Compile.F b).
-Proof.
-  move => h. elim : n a b /h.
-  - move => n  a0 a1 b0 b1 ha iha hb ihb /=.
-    rewrite -Compile.substing.
-    apply RPar'.AppAbs => //.
-  - hauto q:on use:RPar'.ProjPair'.
-  - qauto ctrs:RPar'.R.
-  - hauto lq:on ctrs:RPar'.R.
-  - hauto lq:on ctrs:RPar'.R.
-  - hauto lq:on ctrs:RPar'.R.
-  - hauto lq:on ctrs:RPar'.R.
-  - hauto lq:on ctrs:RPar'.R.
-  - hauto lq:on ctrs:RPar'.R.
-  - hauto lq:on ctrs:RPar'.R.
-  - hauto lq:on ctrs:RPar'.R.
-Qed.
-
-Lemma compile_rpars n (a b : Tm n) : rtc RPar'.R a b -> rtc RPar'.R (Compile.F a) (Compile.F b).
-Proof. induction 1; hauto lq:on ctrs:rtc use:compile_rpar. Qed.
diff --git a/theories/fp_red.v b/theories/fp_red.v
index 40b1751..589d87a 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -66,11 +66,7 @@ Module Par.
     R a0 a1 ->
     R (PProj p a0) (PProj p a1)
   | ConstCong k :
-    R (PConst k) (PConst k)
-  | Univ i :
-    R (PUniv i) (PUniv i)
-  | Bot :
-    R PBot PBot.
+    R (PConst k) (PConst k).
 
   Lemma refl (a : PTm) : R a a.
     elim : a; hauto ctrs:R.
@@ -130,8 +126,6 @@ Module Par.
     - qauto l:on ctrs:R.
     - qauto l:on ctrs:R.
     - hauto l:on inv:option ctrs:R use:renaming.
-    - qauto l:on ctrs:R.
-    - qauto l:on ctrs:R.
   Qed.
 
   Lemma substing (a b : PTm) (ρ : nat -> PTm) :
@@ -204,8 +198,6 @@ Module Par.
       eexists. split. by apply ProjCong; eauto.
       done.
     - hauto q:on inv:PTm ctrs:R.
-    - hauto q:on inv:PTm ctrs:R.
-    - hauto q:on inv:PTm ctrs:R.
   Qed.
 
 End Par.
@@ -267,14 +259,6 @@ Module Pars.
 
 End Pars.
 
-Definition var_or_const (a : PTm) :=
-  match a with
-  | VarPTm _ => true
-  | PBot => true
-  | _ => false
-  end.
-
-
 (***************** Beta rules only ***********************)
 Module RPar.
   Inductive R : PTm -> PTm ->  Prop :=
@@ -314,11 +298,7 @@ Module RPar.
     R a0 a1 ->
     R (PProj p a0) (PProj p a1)
   | ConstCong k :
-    R (PConst k) (PConst k)
-  | Univ i :
-    R (PUniv i) (PUniv i)
-  | Bot :
-    R PBot PBot.
+    R (PConst k) (PConst k).
 
   Derive Dependent Inversion inv with (forall (a b : PTm), R a b) Sort Prop.
 
@@ -384,8 +364,6 @@ Module RPar.
     - hauto lq:on ctrs:R.
     - hauto lq:on ctrs:R.
     - hauto lq:on ctrs:R use:morphing_up.
-    - hauto lq:on ctrs:R.
-    - hauto lq:on ctrs:R.
   Qed.
 
   Lemma substing (a b : PTm) (ρ : nat -> PTm) :
@@ -404,120 +382,56 @@ Module RPar.
     - simpl. apply Var.
   Qed.
 
-  Lemma var_or_const_imp (a b : PTm) :
-    var_or_const a ->
-    a = b -> ~~ var_or_const b -> False.
-  Proof.
-    hauto lq:on inv:PTm.
-  Qed.
 
-  Lemma var_or_const_up (ρ : nat -> PTm) :
-    (forall i, var_or_const (ρ i)) ->
-    (forall i, var_or_const (up_PTm_PTm ρ i)).
-  Proof.
-    move => h /= [|i].
-    - sfirstorder.
-    - asimpl.
-      move /(_ i) in h.
-      rewrite /funcomp.
-      move : (ρ i) h.
-      case => //=.
-  Qed.
+  Ltac2 rec solve_anti_ren () :=
+    let x := Fresh.in_goal (Option.get (Ident.of_string "x")) in
+    intro $x;
+    lazy_match! Constr.type (Control.hyp x) with
+    | nat -> nat => (ltac1:(case;hauto q:on depth:2 ctrs:R))
+    | nat -> PTm => (ltac1:(case;hauto q:on depth:2 ctrs:R))
+    | _ => solve_anti_ren ()
+    end.
 
-  Local Ltac antiimp := qauto l:on use:var_or_const_imp.
+  Ltac solve_anti_ren := ltac2:(Control.enter solve_anti_ren).
 
-  Lemma antirenaming (a : PTm) (b : PTm) (ρ : nat -> PTm) :
-    (forall i, var_or_const (ρ i)) ->
-    R (subst_PTm ρ a) b -> exists b0, R a b0 /\ subst_PTm ρ b0 = b.
+  Lemma antirenaming (a : PTm) (b : PTm) (ρ : nat -> nat) :
+    R (ren_PTm ρ a) b -> exists b0, R a b0 /\ ren_PTm ρ b0 = b.
   Proof.
-    move E : (subst_PTm ρ a) => u hρ h.
-    move : ρ hρ a E. elim : u b/h.
-    - move => a0 a1 b0 b1 ha iha hb ihb ρ hρ []//=;
-               first by antiimp.
+    move E : (ren_PTm ρ a) => u h.
+    move : ρ a E. elim : u b/h; try solve_anti_ren.
+    - move => a0 a1 b0 b1 ha iha hb ihb ρ []//=.
       move => c c0 [+ ?]. subst.
-      case : c => //=; first by antiimp.
+      case : c => //=.
       move => c [?]. subst.
       spec_refl.
-      have /var_or_const_up hρ' := hρ.
-      move : iha hρ' => /[apply] iha.
-      move : ihb hρ => /[apply] ihb.
-      spec_refl.
       move : iha => [c1][ih0]?. subst.
       move : ihb => [c2][ih1]?. subst.
       eexists. split.
       apply AppAbs; eauto.
       by asimpl.
-    - move => a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc ρ hρ.
-      move => []//=;
-               first by antiimp.
-      move => []//=; first by antiimp.
-      move => t t0 t1 [*]. subst.
-      have  {}/iha := hρ => iha.
-      have  {}/ihb := hρ => ihb.
-      have  {}/ihc := hρ => ihc.
+    - move => a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc ρ.
+      move => []//=.
+      move => []//=.
+      move => p p0 p1 [*]. subst.
       spec_refl.
       move : iha => [? [*]].
       move : ihb => [? [*]].
-      move : ihc => [? [*]].
+      move : ihc => [? [*]]. subst.
       eexists. split.
-      apply AppPair; hauto. subst.
+      apply AppPair; hauto.
       by asimpl.
-    - move => p a0 a1 ha iha ρ hρ []//=;
-               first by antiimp.
-      move => p0 []//= t [*]; first by antiimp. subst.
-      have  /var_or_const_up {}/iha  := hρ => iha.
+    - move => p a0 a1 ha iha ρ []//=.
+      move => p0 []//= t [*]. subst.
       spec_refl. move : iha => [b0 [? ?]]. subst.
       eexists. split. apply ProjAbs; eauto. by asimpl.
-    - move => p a0 a1 b0 b1 ha iha hb ihb ρ hρ []//=;
-               first by antiimp.
-      move => p0 []//=; first by antiimp. move => t t0[*].
+    - move => p a0 a1 b0 b1 ha iha hb ihb ρ []//=.
+      move => p0 []//=. move => t t0[*].
       subst.
-      have {}/iha := (hρ) => iha.
-      have {}/ihb := (hρ) => ihb.
       spec_refl.
       move : iha => [b0 [? ?]].
       move : ihb => [c0 [? ?]]. subst.
       eexists. split. by eauto using ProjPair.
       hauto q:on.
-    - move => i ρ hρ []//=.
-      hauto l:on.
-    - move => a0 a1 ha iha ρ hρ []//=; first by antiimp.
-      move => t [*]. subst.
-      have /var_or_const_up {}/iha := hρ => iha.
-      spec_refl.
-      move  :iha => [b0 [? ?]]. subst.
-      eexists. split. by apply AbsCong; eauto.
-      by asimpl.
-    - move => a0 a1 b0 b1 ha iha hb ihb ρ hρ []//=;
-               first by antiimp.
-      move => t t0 [*]. subst.
-      have {}/iha := (hρ) => iha.
-      have {}/ihb := (hρ) => ihb.
-      spec_refl.
-      move : iha => [b0 [? ?]]. subst.
-      move : ihb => [c0 [? ?]]. subst.
-      eexists. split. by apply AppCong; eauto.
-      done.
-    - move => a0 a1 b0 b1 ha iha hb ihb ρ hρ []//=;
-               first by antiimp.
-      move => t t0[*]. subst.
-      have {}/iha := (hρ) => iha.
-      have {}/ihb := (hρ) => ihb.
-      spec_refl.
-      move : iha => [b0 [? ?]]. subst.
-      move : ihb => [c0 [? ?]]. subst.
-      eexists. split. by apply PairCong; eauto.
-      by asimpl.
-    - move => p a0 a1 ha iha ρ hρ []//=;
-               first by antiimp.
-      move => p0 t [*]. subst.
-      have {}/iha := (hρ) => iha.
-      spec_refl.
-      move : iha => [b0 [? ?]]. subst.
-      eexists. split. apply ProjCong; eauto. reflexivity.
-    - hauto q:on ctrs:R inv:PTm.
-    - hauto q:on ctrs:R inv:PTm.
-    - hauto q:on ctrs:R inv:PTm.
   Qed.
 End RPar.
 
@@ -552,11 +466,7 @@ Module RPar'.
     R a0 a1 ->
     R (PProj p a0) (PProj p a1)
   | ConstCong k :
-    R (PConst k) (PConst k)
-  | UnivCong i :
-    R (PUniv i) (PUniv i)
-  | BotCong :
-    R PBot PBot.
+    R (PConst k) (PConst k).
 
   Derive Inversion inv with (forall (a b : PTm), R a b) Sort Prop.
 
@@ -620,8 +530,6 @@ Module RPar'.
     - hauto lq:on ctrs:R.
     - hauto lq:on ctrs:R.
     - hauto l:on ctrs:R use:morphing_up.
-    - hauto lq:on ctrs:R.
-    - hauto lq:on ctrs:R.
   Qed.
 
   Lemma substing (a b : PTm) (ρ : nat -> PTm) :
@@ -638,100 +546,39 @@ Module RPar'.
     hauto l:on ctrs:R inv:nat.
   Qed.
 
-  Lemma var_or_const_imp (a b : PTm) :
-    var_or_const a ->
-    a = b -> ~~ var_or_const b -> False.
-  Proof.
-    hauto lq:on inv:PTm.
-  Qed.
+  Ltac2 rec solve_anti_ren () :=
+    let x := Fresh.in_goal (Option.get (Ident.of_string "x")) in
+    intro $x;
+    lazy_match! Constr.type (Control.hyp x) with
+    | nat -> nat => (ltac1:(case;hauto q:on depth:2 ctrs:R))
+    | nat -> PTm => (ltac1:(case;hauto q:on depth:2 ctrs:R))
+    | _ => solve_anti_ren ()
+    end.
 
-  Lemma var_or_const_up (ρ : nat -> PTm) :
-    (forall i, var_or_const (ρ i)) ->
-    (forall i, var_or_const (up_PTm_PTm ρ i)).
-  Proof.
-    move => h /= [|i].
-    - sfirstorder.
-    - asimpl.
-      move /(_ i) in h.
-      rewrite /funcomp.
-      move : (ρ i) h.
-      case => //=.
-  Qed.
+  Ltac solve_anti_ren := ltac2:(Control.enter solve_anti_ren).
 
-  Local Ltac antiimp := qauto l:on use:var_or_const_imp.
-
-  Lemma antirenaming (a : PTm) (b : PTm) (ρ : nat -> PTm) :
-    (forall i, var_or_const (ρ i)) ->
-    R (subst_PTm ρ a) b -> exists b0, R a b0 /\ subst_PTm ρ b0 = b.
+  Lemma antirenaming (a : PTm) (b : PTm) (ρ : nat -> nat) :
+    R (ren_PTm ρ a) b -> exists b0, R a b0 /\ ren_PTm ρ b0 = b.
   Proof.
-    move E : (subst_PTm ρ a) => u hρ h.
-    move : ρ hρ a E. elim : u b/h.
-    - move => a0 a1 b0 b1 ha iha hb ihb ρ hρ []//=;
-               first by antiimp.
-      move => c c0 [+ ?]. subst.
-      case : c => //=; first by antiimp.
-      move => c [?]. subst.
-      spec_refl.
-      have /var_or_const_up hρ' := hρ.
-      move : iha hρ' => /[apply] iha.
-      move : ihb hρ => /[apply] ihb.
+    move E : (ren_PTm ρ a) => u h.
+    move : ρ a E. elim : u b/h; try solve_anti_ren.
+    - move => a0 a1 b0 b1 ha iha hb ihb ρ []//=.
+      move => []//=.
+      move => p p0 [*]. subst.
       spec_refl.
       move : iha => [c1][ih0]?. subst.
       move : ihb => [c2][ih1]?. subst.
       eexists. split.
       apply AppAbs; eauto.
       by asimpl.
-    - move => p a0 a1 b0 b1 ha iha hb ihb ρ hρ []//=;
-               first by antiimp.
-      move => p0 []//=; first by antiimp. move => t t0[*].
+    - move => p a0 a1 b0 b1 ha iha hb ihb ρ []//=.
+      move => p0 []//=. move => t t0[*].
       subst.
-      have {}/iha := (hρ) => iha.
-      have {}/ihb := (hρ) => ihb.
       spec_refl.
       move : iha => [b0 [? ?]].
       move : ihb => [c0 [? ?]]. subst.
       eexists. split. by eauto using ProjPair.
       hauto q:on.
-    - move => i ρ hρ []//=.
-      hauto l:on.
-    - move => a0 a1 ha iha ρ hρ []//=; first by antiimp.
-      move => t [*]. subst.
-      have /var_or_const_up {}/iha := hρ => iha.
-      spec_refl.
-      move  :iha => [b0 [? ?]]. subst.
-      eexists. split. by apply AbsCong; eauto.
-      by asimpl.
-    - move => a0 a1 b0 b1 ha iha hb ihb ρ hρ []//=;
-               first by antiimp.
-      move => t t0 [*]. subst.
-      have {}/iha := (hρ) => iha.
-      have {}/ihb := (hρ) => ihb.
-      spec_refl.
-      move : iha => [b0 [? ?]]. subst.
-      move : ihb => [c0 [? ?]]. subst.
-      eexists. split. by apply AppCong; eauto.
-      done.
-    - move => a0 a1 b0 b1 ha iha hb ihb ρ hρ []//=;
-               first by antiimp.
-      move => t t0[*]. subst.
-      have {}/iha := (hρ) => iha.
-      have {}/ihb := (hρ) => ihb.
-      spec_refl.
-      move : iha => [b0 [? ?]]. subst.
-      move : ihb => [c0 [? ?]]. subst.
-      eexists. split. by apply PairCong; eauto.
-      by asimpl.
-    - move => p a0 a1 ha iha ρ hρ []//=;
-               first by antiimp.
-      move => p0 t [*]. subst.
-      have {}/iha := (hρ) => iha.
-      spec_refl.
-      move : iha => [b0 [? ?]]. subst.
-      eexists. split. apply ProjCong; eauto. reflexivity.
-    - hauto q:on ctrs:R inv:PTm.
-    - move => i ρ hρ []//=; first by antiimp.
-      hauto l:on.
-    - hauto q:on inv:PTm ctrs:R.
   Qed.
 End RPar'.
 
@@ -852,11 +699,7 @@ Module EPar.
     R a0 a1 ->
     R (PProj p a0) (PProj p a1)
   | ConstCong k :
-    R (PConst k) (PConst k)
-  | UnivCong i :
-    R (PUniv i) (PUniv i)
-  | BotCong :
-    R PBot PBot.
+    R (PConst k) (PConst k).
 
   Lemma refl (a : PTm) : EPar.R a a.
   Proof.
@@ -899,8 +742,6 @@ Module EPar.
     - hauto q:on ctrs:R.
     - hauto q:on ctrs:R.
     - hauto l:on ctrs:R use:renaming inv:nat.
-    - hauto lq:on ctrs:R.
-    - hauto lq:on ctrs:R.
   Qed.
 
   Lemma substing a0 a1 (b0 b1 : PTm) :
@@ -1022,17 +863,15 @@ Module RPars.
     rtc RPar.R (subst_PTm (scons c VarPTm) a) (subst_PTm (scons c VarPTm) b).
   Proof. hauto lq:on use:morphing inv:nat. Qed.
 
-  Lemma antirenaming (a : PTm) (b : PTm) (ρ : nat -> PTm) :
-    (forall i, var_or_const (ρ i)) ->
-    rtc RPar.R (subst_PTm ρ a) b -> exists b0, rtc RPar.R a b0 /\ subst_PTm ρ b0 = b.
+  Lemma antirenaming (a : PTm) (b : PTm) (ρ : nat -> nat) :
+    rtc RPar.R (ren_PTm ρ a) b -> exists b0, rtc RPar.R a b0 /\ ren_PTm ρ b0 = b.
   Proof.
-    move E  :(subst_PTm ρ a) => u hρ h.
+    move E  :(ren_PTm ρ a) => u  h.
     move : a E.
     elim : u b /h.
     - sfirstorder.
     - move => a b c h0 h1 ih1 a0 ?. subst.
       move /RPar.antirenaming : h0.
-      move /(_ hρ).
       move => [b0 [h2 ?]]. subst.
       hauto lq:on rew:off ctrs:rtc.
   Qed.
@@ -1103,17 +942,15 @@ Module RPars'.
     rtc RPar'.R (subst_PTm (scons c VarPTm) a) (subst_PTm (scons c VarPTm) b).
   Proof. hauto lq:on use:morphing inv:nat. Qed.
 
-  Lemma antirenaming (a : PTm) (b : PTm) (ρ : nat -> PTm) :
-    (forall i, var_or_const (ρ i)) ->
-    rtc RPar'.R (subst_PTm ρ a) b -> exists b0, rtc RPar'.R a b0 /\ subst_PTm ρ b0 = b.
+  Lemma antirenaming (a : PTm) (b : PTm) (ρ : nat -> nat) :
+    rtc RPar'.R (ren_PTm ρ a) b -> exists b0, rtc RPar'.R a b0 /\ ren_PTm ρ b0 = b.
   Proof.
-    move E  :(subst_PTm ρ a) => u hρ h.
+    move E  :(ren_PTm ρ a) => u h.
     move : a E.
     elim : u b /h.
     - sfirstorder.
     - move => a b c h0 h1 ih1 a0 ?. subst.
       move /RPar'.antirenaming : h0.
-      move /(_ hρ).
       move => [b0 [h2 ?]]. subst.
       hauto lq:on rew:off ctrs:rtc.
   Qed.
@@ -1300,8 +1137,6 @@ Proof.
       hauto lq:on use:RPars.ProjCong, relations.rtc_transitive.
     + hauto lq:on ctrs:EPar.R use:RPars.ProjCong.
   - hauto l:on ctrs:EPar.R inv:RPar.R.
-  - hauto l:on ctrs:EPar.R inv:RPar.R.
-  - hauto l:on ctrs:EPar.R inv:RPar.R.
 Qed.
 
 Lemma commutativity1 (a b0 b1 : PTm) :
@@ -1400,34 +1235,6 @@ Lemma Const_EPar' k (u : PTm) :
   - hauto l:on ctrs:OExp.R.
 Qed.
 
-Lemma Bot_EPar' (u : PTm) :
-  EPar.R (PBot) u ->
-  rtc OExp.R (PBot) u.
-  move E : (PBot) => t h.
-  move : E. elim : t u /h => //=.
-  - move => a0 a1 h ih ?. subst.
-    specialize ih with (1 := eq_refl).
-    hauto lq:on ctrs:OExp.R use:rtc_r.
-  - move => a0 a1 h ih ?. subst.
-    specialize ih with (1 := eq_refl).
-    hauto lq:on ctrs:OExp.R use:rtc_r.
-  - hauto l:on ctrs:OExp.R.
-Qed.
-
-Lemma Univ_EPar' i (u : PTm) :
-  EPar.R (PUniv i) u ->
-  rtc OExp.R (PUniv i) u.
-  move E : (PUniv i) => t h.
-  move : E. elim : t u /h => //=.
-  - move => a0 a1 h ih ?. subst.
-    specialize ih with (1 := eq_refl).
-    hauto lq:on ctrs:OExp.R use:rtc_r.
-  - move => a0 a1 h ih ?. subst.
-    specialize ih with (1 := eq_refl).
-    hauto lq:on ctrs:OExp.R use:rtc_r.
-  - hauto l:on ctrs:OExp.R.
-Qed.
-
 Lemma EPar_diamond (c a1 b1 : PTm) :
   EPar.R c a1 ->
   EPar.R c b1 ->
@@ -1469,8 +1276,6 @@ Proof.
     move => [d1 h1].
     exists d1. hauto lq:on rew:off ctrs:EPar.R use:OExp.merge.
   - qauto use:Const_EPar', EPar.refl.
-  - qauto use:Univ_EPar', EPar.refl.
-  - qauto use:Bot_EPar', EPar.refl.
 Qed.
 
 Function tstar (a : PTm) :=
@@ -1486,8 +1291,6 @@ Function tstar (a : PTm) :=
   | PProj p (PAbs a) => (PAbs (PProj p (tstar a)))
   | PProj p a => PProj p (tstar a)
   | PConst k => PConst k
-  | PUniv i => PUniv i
-  | PBot => PBot
   end.
 
 Lemma RPar_triangle (a : PTm) : forall b, RPar.R a b -> RPar.R b (tstar a).
@@ -1504,8 +1307,6 @@ Proof.
   - hauto lq:on inv:RPar.R ctrs:RPar.R.
   - hauto lq:on inv:RPar.R ctrs:RPar.R.
   - hauto lq:on inv:RPar.R ctrs:RPar.R.
-  - hauto lq:on inv:RPar.R ctrs:RPar.R.
-  - hauto lq:on inv:RPar.R ctrs:RPar.R.
 Qed.
 
 Function tstar' (a : PTm) :=
@@ -1518,8 +1319,6 @@ Function tstar' (a : PTm) :=
   | PProj p (PPair a b) => if p is PL then (tstar' a) else (tstar' b)
   | PProj p a => PProj p (tstar' a)
   | PConst k => PConst k
-  | PUniv i => PUniv i
-  | PBot => PBot
   end.
 
 Lemma RPar'_triangle (a : PTm) : forall b, RPar'.R a b -> RPar'.R b (tstar' a).
@@ -1534,8 +1333,6 @@ Proof.
   - 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 (c a1 b1 : PTm) :
@@ -1583,11 +1380,7 @@ Inductive prov : PTm -> PTm -> Prop :=
 | P_Const k  :
   prov (PConst k) (PConst k)
 | P_Var i :
-  prov (VarPTm i) (VarPTm i)
-| P_Univ i :
-  prov (PUniv i) (PUniv i)
-| P_Bot :
-  prov PBot PBot.
+  prov (VarPTm i) (VarPTm i).
 
 Lemma ERed_EPar (a b : PTm) : ERed.R a b -> EPar.R a b.
 Proof.
@@ -1605,8 +1398,6 @@ Proof.
   - eauto using EReds.PairCong.
   - eauto using EReds.ProjCong.
   - auto using rtc_refl.
-  - auto using rtc_refl.
-  - auto using rtc_refl.
 Qed.
 
 Lemma EPar_Par (a b : PTm) : EPar.R a b -> Par.R a b.
@@ -1658,8 +1449,6 @@ Proof.
     + hauto lq:on ctrs:prov.
   - hauto lq:on ctrs:prov inv:RPar.R.
   - hauto l:on ctrs:RPar.R inv:RPar.R.
-  - hauto l:on ctrs:RPar.R inv:RPar.R.
-  - hauto l:on ctrs:RPar.R inv:RPar.R.
 Qed.
 
 
@@ -1668,7 +1457,7 @@ Proof.
   split.
   move => h. constructor. move => b. asimpl. by constructor.
   inversion 1; subst.
-  specialize H2 with (b := PBot).
+  specialize H2 with (b := (VarPTm var_zero)).
   move : H2. asimpl. inversion 1; subst. done.
 Qed.
 
@@ -1703,8 +1492,6 @@ Proof.
   - hauto lq:on inv:ERed.R, prov ctrs:prov.
   - hauto lq:on inv:ERed.R, prov ctrs:prov.
   - hauto lq:on inv:ERed.R, prov ctrs:prov.
-  - hauto lq:on inv:ERed.R, prov ctrs:prov.
-  - hauto lq:on inv:ERed.R, prov ctrs:prov.
 Qed.
 
 Lemma prov_ereds (u : PTm) a b : prov u a -> rtc ERed.R a b -> prov u b.
@@ -1714,14 +1501,12 @@ Qed.
 
 Fixpoint extract (a : PTm) : PTm :=
   match a with
-  | PAbs a => subst_PTm (scons PBot VarPTm) (extract a)
+  | PAbs a => subst_PTm (scons (PConst 0) VarPTm) (extract a)
   | PApp a b => extract a
   | PPair a b => extract a
   | PProj p a => extract a
   | PConst k => PConst k
   | VarPTm i => VarPTm i
-  | PUniv i => PUniv i
-  | PBot => PBot
   end.
 
 Lemma ren_extract (a : PTm) (ξ : nat -> nat) :
@@ -1736,8 +1521,6 @@ Proof.
   - hauto q:on.
   - hauto q:on.
   - hauto q:on.
-  - sfirstorder.
-  - sfirstorder.
 Qed.
 
 Lemma ren_morphing (a : PTm) (ρ : nat -> PTm) :
@@ -1756,17 +1539,15 @@ Proof.
 Qed.
 
 Lemma ren_subst_bot (a : PTm) :
-  extract (subst_PTm (scons PBot VarPTm) a) = subst_PTm (scons PBot VarPTm) (extract a).
+  extract (subst_PTm (scons (PConst 0) VarPTm) a) = subst_PTm (scons (PConst 0) VarPTm) (extract a).
 Proof.
   apply ren_morphing. destruct i => //=.
 Qed.
 
 Definition prov_extract_spec u (a : PTm) :=
   match u with
-  | PUniv i => extract a = PUniv i
   | VarPTm i => extract a = VarPTm i
   | (PConst i) => extract a = (PConst i)
-  | PBot => extract a = PBot
   | _ => True
   end.
 
@@ -1778,23 +1559,16 @@ Proof.
   - move => h a ha ih.
     case : h ha ih => //=.
     + move => i ha ih.
-      move /(_ PBot) in ih.
+      move /(_ (PConst 0)) in ih.
       rewrite -ih.
       by rewrite ren_subst_bot.
-    + move => p _ /(_ PBot).
-      by rewrite ren_subst_bot.
-    + move => i h /(_ PBot).
-      by rewrite ren_subst_bot => ->.
-    + move /(_ PBot).
-      move => h /(_ PBot).
+    + move => p _ /(_ (PConst 0)).
       by rewrite ren_subst_bot.
   - hauto lq:on.
   - hauto lq:on.
   - hauto lq:on.
   - case => //=.
   - sfirstorder.
-  - sfirstorder.
-  - sfirstorder.
 Qed.
 
 Definition union {A : Type} (R0 R1 : A -> A -> Prop) a b :=
@@ -1970,8 +1744,6 @@ Proof.
   - sfirstorder use:ERPars.PairCong.
   - sfirstorder use:ERPars.ProjCong.
   - sfirstorder.
-  - sfirstorder.
-  - sfirstorder.
 Qed.
 
 Lemma Pars_ERPar (a b : PTm) : rtc Par.R a b -> rtc ERPar.R a b.
@@ -2139,15 +1911,6 @@ Proof.
   hauto lq:on use:rtc_union.
 Qed.
 
-Lemma pars_univ_inv i (c : PTm) :
-  rtc Par.R (PUniv i) c ->
-  extract c = PUniv i.
-Proof.
-  have : prov (PUniv i) (PUniv i : PTm) by sfirstorder.
-  move : prov_pars. repeat move/[apply].
-  apply prov_extract.
-Qed.
-
 Lemma pars_const_inv i (c : PTm) :
   rtc Par.R (PConst i) c ->
   extract c = PConst i.
@@ -2166,14 +1929,6 @@ Proof.
   apply prov_extract.
 Qed.
 
-Lemma pars_univ_inj i j (C : PTm) :
-  rtc Par.R (PUniv i) C ->
-  rtc Par.R (PUniv j) C ->
-  i = j.
-Proof.
-  sauto l:on use:pars_univ_inv.
-Qed.
-
 Lemma pars_const_inj i j (C : PTm) :
   rtc Par.R (PConst i) C ->
   rtc Par.R (PConst j) C ->
@@ -2202,12 +1957,6 @@ Proof. sfirstorder unfold:join. Qed.
 Lemma join_refl (a : PTm) : join a a.
 Proof. hauto lq:on ctrs:rtc unfold:join. Qed.
 
-Lemma join_univ_inj i j :
-  join (PUniv i : PTm) (PUniv j) -> i = j.
-Proof.
-  sfirstorder use:pars_univ_inj.
-Qed.
-
 Lemma join_const_inj i j :
   join (PConst i : PTm) (PConst j) -> i = j.
 Proof.
@@ -2224,22 +1973,18 @@ Fixpoint ne (a : PTm) :=
   | VarPTm i => true
   | PApp a b => ne a && nf b
   | PAbs a => false
-  | PUniv _ => false
   | PProj _ a => ne a
   | PPair _ _ => false
   | PConst _ => false
-  | PBot => true
   end
 with nf (a : PTm) :=
   match a with
   | VarPTm i => true
   | PApp a b => ne a && nf b
   | PAbs a => nf a
-  | PUniv _ => true
   | PProj _ a => ne a
   | PPair a b => nf a && nf b
   | PConst _ => true
-  | PBot => true
 end.
 
 Lemma ne_nf a : ne a -> nf a.
@@ -2297,31 +2042,30 @@ Qed.
 Create HintDb nfne.
 #[export]Hint Resolve nf_wn ne_nf wne_wn nf_refl : nfne.
 
-Lemma ne_nf_antiren (a : PTm) (ρ : nat -> PTm) :
-  (forall i, var_or_const (ρ i)) ->
-  (ne (subst_PTm ρ a) -> ne a) /\ (nf (subst_PTm ρ a) -> nf a).
+Lemma ne_nf_antiren (a : PTm) (ρ : nat -> nat) :
+  (ne (ren_PTm ρ a) -> ne a) /\ (nf (ren_PTm ρ a) -> nf a).
 Proof.
   move : ρ. elim : a => //;
-   hauto b:on drew:off use:RPar.var_or_const_up.
+   hauto b:on drew:off .
 Qed.
 
-Lemma wn_antirenaming a (ρ : nat -> PTm) :
-  (forall i, var_or_const (ρ i)) ->
-  wn (subst_PTm ρ a) -> wn a.
+Lemma wn_antirenaming a (ρ : nat -> nat) :
+  wn (ren_PTm ρ a) -> wn a.
 Proof.
-  rewrite /wn => hρ.
+  rewrite /wn.
   move => [v [rv nfv]].
   move /RPars'.antirenaming : rv.
-  move /(_ hρ) => [b [hb ?]]. subst.
+  move => [b [hb ?]]. subst.
   exists b. split => //=.
   move : nfv.
   by eapply ne_nf_antiren.
 Qed.
 
 Lemma ext_wn (a : PTm) :
-    wn (PApp a PBot) ->
+    wn (PApp a (VarPTm var_zero)) ->
     wn a.
 Proof.
+  set PBot := VarPTm var_zero.
   move E : (PApp a (PBot)) => a0 [v [hr hv]].
   move : a E.
   move : hv.
@@ -2335,10 +2079,12 @@ Proof.
     + move => a0 a3 b2 b3 ? ? [? ?] ? [? ?]. subst.
       have ? : b3 = (PBot) by hauto lq:on inv:RPar'.R. subst.
       suff : wn (PAbs a3) by hauto lq:on ctrs:RPar'.R, rtc unfold:wn.
-      have : wn (subst_PTm (scons (PBot) VarPTm) a3) by sfirstorder.
+      have : wn (subst_PTm (scons (VarPTm var_zero) VarPTm) a3) by sfirstorder.
+      asimpl.
       move => h. apply wn_abs.
-      move : h. apply wn_antirenaming.
-      hauto lq:on rew:off inv:nat.
+      move : h.
+      have -> : subst_PTm (scons (VarPTm var_zero) VarPTm) a3 = ren_PTm (scons var_zero id) a3 by substify; asimpl.
+      apply wn_antirenaming.
     + hauto q:on inv:RPar'.R ctrs:rtc b:on.
 Qed.