diff --git a/Makefile b/Makefile
index ef5b76f..3c879f6 100644
--- a/Makefile
+++ b/Makefile
@@ -16,7 +16,7 @@ uninstall: $(COQMAKEFILE)
 	$(MAKE) -f $(COQMAKEFILE) uninstall
 
 theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v : syntax.sig
-	autosubst -f -v ge813 -s coq -o theories/Autosubst2/syntax.v syntax.sig
+	autosubst -f -v ge813 -s ucoq -o theories/Autosubst2/syntax.v syntax.sig
 
 .PHONY: clean FORCE
 
diff --git a/theories/Autosubst2/syntax.v b/theories/Autosubst2/syntax.v
index 5d04c05..3d1e1f6 100644
--- a/theories/Autosubst2/syntax.v
+++ b/theories/Autosubst2/syntax.v
@@ -1,4 +1,4 @@
-Require Import core fintype.
+Require Import core unscoped.
 
 Require Import Setoid Morphisms Relation_Definitions.
 
@@ -33,221 +33,177 @@ Proof.
 exact (eq_refl).
 Qed.
 
-Inductive PTm (n_PTm : nat) : Type :=
-  | VarPTm : fin n_PTm -> PTm n_PTm
-  | PAbs : PTm (S n_PTm) -> PTm n_PTm
-  | PApp : PTm n_PTm -> PTm n_PTm -> PTm n_PTm
-  | PPair : PTm n_PTm -> PTm n_PTm -> PTm n_PTm
-  | PProj : PTag -> PTm n_PTm -> PTm n_PTm
-  | PBind : BTag -> PTm n_PTm -> PTm (S n_PTm) -> PTm n_PTm
-  | PUniv : nat -> PTm n_PTm
-  | PBot : PTm n_PTm
-  | PNat : PTm n_PTm
-  | PZero : PTm n_PTm
-  | PSuc : PTm n_PTm -> PTm n_PTm
-  | PInd :
-      PTm (S n_PTm) ->
-      PTm n_PTm -> PTm n_PTm -> PTm (S (S n_PTm)) -> PTm n_PTm.
+Inductive PTm : Type :=
+  | VarPTm : nat -> PTm
+  | PAbs : PTm -> PTm
+  | PApp : PTm -> PTm -> PTm
+  | PPair : PTm -> PTm -> PTm
+  | PProj : PTag -> PTm -> PTm
+  | PBind : BTag -> PTm -> PTm -> PTm
+  | PUniv : nat -> PTm
+  | PBot : PTm
+  | PNat : PTm
+  | PZero : PTm
+  | PSuc : PTm -> PTm
+  | PInd : PTm -> PTm -> PTm -> PTm -> 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.
+Lemma congr_PAbs {s0 : PTm} {t0 : PTm} (H0 : s0 = t0) : PAbs s0 = PAbs t0.
 Proof.
-exact (eq_trans eq_refl (ap (fun x => PAbs m_PTm x) H0)).
+exact (eq_trans eq_refl (ap (fun x => PAbs x) H0)).
 Qed.
 
-Lemma congr_PApp {m_PTm : nat} {s0 : PTm m_PTm} {s1 : PTm m_PTm}
-  {t0 : PTm m_PTm} {t1 : PTm m_PTm} (H0 : s0 = t0) (H1 : s1 = t1) :
-  PApp m_PTm s0 s1 = PApp m_PTm t0 t1.
+Lemma congr_PApp {s0 : PTm} {s1 : PTm} {t0 : PTm} {t1 : PTm} (H0 : s0 = t0)
+  (H1 : s1 = t1) : PApp s0 s1 = PApp t0 t1.
 Proof.
-exact (eq_trans (eq_trans eq_refl (ap (fun x => PApp m_PTm x s1) H0))
-         (ap (fun x => PApp m_PTm t0 x) H1)).
+exact (eq_trans (eq_trans eq_refl (ap (fun x => PApp x s1) H0))
+         (ap (fun x => PApp t0 x) H1)).
 Qed.
 
-Lemma congr_PPair {m_PTm : nat} {s0 : PTm m_PTm} {s1 : PTm m_PTm}
-  {t0 : PTm m_PTm} {t1 : PTm m_PTm} (H0 : s0 = t0) (H1 : s1 = t1) :
-  PPair m_PTm s0 s1 = PPair m_PTm t0 t1.
+Lemma congr_PPair {s0 : PTm} {s1 : PTm} {t0 : PTm} {t1 : PTm} (H0 : s0 = t0)
+  (H1 : s1 = t1) : PPair s0 s1 = PPair t0 t1.
 Proof.
-exact (eq_trans (eq_trans eq_refl (ap (fun x => PPair m_PTm x s1) H0))
-         (ap (fun x => PPair m_PTm t0 x) H1)).
+exact (eq_trans (eq_trans eq_refl (ap (fun x => PPair x s1) H0))
+         (ap (fun x => PPair t0 x) H1)).
 Qed.
 
-Lemma congr_PProj {m_PTm : nat} {s0 : PTag} {s1 : PTm m_PTm} {t0 : PTag}
-  {t1 : PTm m_PTm} (H0 : s0 = t0) (H1 : s1 = t1) :
-  PProj m_PTm s0 s1 = PProj m_PTm t0 t1.
+Lemma congr_PProj {s0 : PTag} {s1 : PTm} {t0 : PTag} {t1 : PTm}
+  (H0 : s0 = t0) (H1 : s1 = t1) : PProj s0 s1 = PProj t0 t1.
 Proof.
-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)).
+exact (eq_trans (eq_trans eq_refl (ap (fun x => PProj x s1) H0))
+         (ap (fun x => PProj 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.
+Lemma congr_PBind {s0 : BTag} {s1 : PTm} {s2 : PTm} {t0 : BTag} {t1 : PTm}
+  {t2 : PTm} (H0 : s0 = t0) (H1 : s1 = t1) (H2 : s2 = t2) :
+  PBind s0 s1 s2 = PBind 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)).
+         (eq_trans (eq_trans eq_refl (ap (fun x => PBind x s1 s2) H0))
+            (ap (fun x => PBind t0 x s2) H1))
+         (ap (fun x => PBind 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.
+Lemma congr_PUniv {s0 : nat} {t0 : nat} (H0 : s0 = t0) : PUniv s0 = PUniv t0.
 Proof.
-exact (eq_trans eq_refl (ap (fun x => PUniv m_PTm x) H0)).
+exact (eq_trans eq_refl (ap (fun x => PUniv x) H0)).
 Qed.
 
-Lemma congr_PBot {m_PTm : nat} : PBot m_PTm = PBot m_PTm.
+Lemma congr_PBot : PBot = PBot.
 Proof.
 exact (eq_refl).
 Qed.
 
-Lemma congr_PNat {m_PTm : nat} : PNat m_PTm = PNat m_PTm.
+Lemma congr_PNat : PNat = PNat.
 Proof.
 exact (eq_refl).
 Qed.
 
-Lemma congr_PZero {m_PTm : nat} : PZero m_PTm = PZero m_PTm.
+Lemma congr_PZero : PZero = PZero.
 Proof.
 exact (eq_refl).
 Qed.
 
-Lemma congr_PSuc {m_PTm : nat} {s0 : PTm m_PTm} {t0 : PTm m_PTm}
-  (H0 : s0 = t0) : PSuc m_PTm s0 = PSuc m_PTm t0.
+Lemma congr_PSuc {s0 : PTm} {t0 : PTm} (H0 : s0 = t0) : PSuc s0 = PSuc t0.
 Proof.
-exact (eq_trans eq_refl (ap (fun x => PSuc m_PTm x) H0)).
+exact (eq_trans eq_refl (ap (fun x => PSuc x) H0)).
 Qed.
 
-Lemma congr_PInd {m_PTm : nat} {s0 : PTm (S m_PTm)} {s1 : PTm m_PTm}
-  {s2 : PTm m_PTm} {s3 : PTm (S (S m_PTm))} {t0 : PTm (S m_PTm)}
-  {t1 : PTm m_PTm} {t2 : PTm m_PTm} {t3 : PTm (S (S m_PTm))} (H0 : s0 = t0)
-  (H1 : s1 = t1) (H2 : s2 = t2) (H3 : s3 = t3) :
-  PInd m_PTm s0 s1 s2 s3 = PInd m_PTm t0 t1 t2 t3.
+Lemma congr_PInd {s0 : PTm} {s1 : PTm} {s2 : PTm} {s3 : PTm} {t0 : PTm}
+  {t1 : PTm} {t2 : PTm} {t3 : PTm} (H0 : s0 = t0) (H1 : s1 = t1)
+  (H2 : s2 = t2) (H3 : s3 = t3) : PInd s0 s1 s2 s3 = PInd t0 t1 t2 t3.
 Proof.
 exact (eq_trans
          (eq_trans
-            (eq_trans
-               (eq_trans eq_refl (ap (fun x => PInd m_PTm x s1 s2 s3) H0))
-               (ap (fun x => PInd m_PTm t0 x s2 s3) H1))
-            (ap (fun x => PInd m_PTm t0 t1 x s3) H2))
-         (ap (fun x => PInd m_PTm t0 t1 t2 x) H3)).
+            (eq_trans (eq_trans eq_refl (ap (fun x => PInd x s1 s2 s3) H0))
+               (ap (fun x => PInd t0 x s2 s3) H1))
+            (ap (fun x => PInd t0 t1 x s3) H2))
+         (ap (fun x => PInd t0 t1 t2 x) H3)).
 Qed.
 
-Lemma upRen_PTm_PTm {m : nat} {n : nat} (xi : fin m -> fin n) :
-  fin (S m) -> fin (S n).
+Lemma upRen_PTm_PTm (xi : nat -> nat) : nat -> nat.
 Proof.
 exact (up_ren xi).
 Defined.
 
-Lemma upRen_list_PTm_PTm (p : nat) {m : nat} {n : nat} (xi : fin m -> fin n)
-  : fin (plus p m) -> fin (plus p n).
-Proof.
-exact (upRen_p p xi).
-Defined.
-
-Fixpoint ren_PTm {m_PTm : nat} {n_PTm : nat}
-(xi_PTm : fin m_PTm -> fin n_PTm) (s : PTm m_PTm) {struct s} : PTm n_PTm :=
+Fixpoint ren_PTm (xi_PTm : nat -> nat) (s : PTm) {struct s} : PTm :=
   match s with
-  | VarPTm _ s0 => VarPTm n_PTm (xi_PTm s0)
-  | PAbs _ s0 => PAbs n_PTm (ren_PTm (upRen_PTm_PTm xi_PTm) s0)
-  | 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
-  | PNat _ => PNat n_PTm
-  | PZero _ => PZero n_PTm
-  | PSuc _ s0 => PSuc n_PTm (ren_PTm xi_PTm s0)
-  | PInd _ s0 s1 s2 s3 =>
-      PInd n_PTm (ren_PTm (upRen_PTm_PTm xi_PTm) s0) (ren_PTm xi_PTm s1)
+  | VarPTm s0 => VarPTm (xi_PTm s0)
+  | PAbs s0 => PAbs (ren_PTm (upRen_PTm_PTm xi_PTm) s0)
+  | PApp s0 s1 => PApp (ren_PTm xi_PTm s0) (ren_PTm xi_PTm s1)
+  | PPair s0 s1 => PPair (ren_PTm xi_PTm s0) (ren_PTm xi_PTm s1)
+  | PProj s0 s1 => PProj s0 (ren_PTm xi_PTm s1)
+  | PBind s0 s1 s2 =>
+      PBind s0 (ren_PTm xi_PTm s1) (ren_PTm (upRen_PTm_PTm xi_PTm) s2)
+  | PUniv s0 => PUniv s0
+  | PBot => PBot
+  | PNat => PNat
+  | PZero => PZero
+  | PSuc s0 => PSuc (ren_PTm xi_PTm s0)
+  | PInd s0 s1 s2 s3 =>
+      PInd (ren_PTm (upRen_PTm_PTm xi_PTm) s0) (ren_PTm xi_PTm s1)
         (ren_PTm xi_PTm s2)
         (ren_PTm (upRen_PTm_PTm (upRen_PTm_PTm xi_PTm)) s3)
   end.
 
-Lemma up_PTm_PTm {m : nat} {n_PTm : nat} (sigma : fin m -> PTm n_PTm) :
-  fin (S m) -> PTm (S n_PTm).
+Lemma up_PTm_PTm (sigma : nat -> PTm) : nat -> PTm.
 Proof.
-exact (scons (VarPTm (S n_PTm) var_zero) (funcomp (ren_PTm shift) sigma)).
+exact (scons (VarPTm var_zero) (funcomp (ren_PTm shift) sigma)).
 Defined.
 
-Lemma up_list_PTm_PTm (p : nat) {m : nat} {n_PTm : nat}
-  (sigma : fin m -> PTm n_PTm) : fin (plus p m) -> PTm (plus p n_PTm).
-Proof.
-exact (scons_p p (funcomp (VarPTm (plus p n_PTm)) (zero_p p))
-         (funcomp (ren_PTm (shift_p p)) sigma)).
-Defined.
-
-Fixpoint subst_PTm {m_PTm : nat} {n_PTm : nat}
-(sigma_PTm : fin m_PTm -> PTm n_PTm) (s : PTm m_PTm) {struct s} : PTm n_PTm
-:=
+Fixpoint subst_PTm (sigma_PTm : nat -> PTm) (s : PTm) {struct s} : PTm :=
   match s with
-  | VarPTm _ s0 => sigma_PTm s0
-  | PAbs _ s0 => PAbs n_PTm (subst_PTm (up_PTm_PTm sigma_PTm) s0)
-  | PApp _ s0 s1 =>
-      PApp n_PTm (subst_PTm sigma_PTm s0) (subst_PTm sigma_PTm s1)
-  | 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
-  | PNat _ => PNat n_PTm
-  | PZero _ => PZero n_PTm
-  | PSuc _ s0 => PSuc n_PTm (subst_PTm sigma_PTm s0)
-  | PInd _ s0 s1 s2 s3 =>
-      PInd n_PTm (subst_PTm (up_PTm_PTm sigma_PTm) s0)
-        (subst_PTm sigma_PTm s1) (subst_PTm sigma_PTm s2)
+  | VarPTm s0 => sigma_PTm s0
+  | PAbs s0 => PAbs (subst_PTm (up_PTm_PTm sigma_PTm) s0)
+  | PApp s0 s1 => PApp (subst_PTm sigma_PTm s0) (subst_PTm sigma_PTm s1)
+  | PPair s0 s1 => PPair (subst_PTm sigma_PTm s0) (subst_PTm sigma_PTm s1)
+  | PProj s0 s1 => PProj s0 (subst_PTm sigma_PTm s1)
+  | PBind s0 s1 s2 =>
+      PBind s0 (subst_PTm sigma_PTm s1) (subst_PTm (up_PTm_PTm sigma_PTm) s2)
+  | PUniv s0 => PUniv s0
+  | PBot => PBot
+  | PNat => PNat
+  | PZero => PZero
+  | PSuc s0 => PSuc (subst_PTm sigma_PTm s0)
+  | PInd s0 s1 s2 s3 =>
+      PInd (subst_PTm (up_PTm_PTm sigma_PTm) s0) (subst_PTm sigma_PTm s1)
+        (subst_PTm sigma_PTm s2)
         (subst_PTm (up_PTm_PTm (up_PTm_PTm sigma_PTm)) s3)
   end.
 
-Lemma upId_PTm_PTm {m_PTm : nat} (sigma : fin m_PTm -> PTm m_PTm)
-  (Eq : forall x, sigma x = VarPTm m_PTm x) :
-  forall x, up_PTm_PTm sigma x = VarPTm (S m_PTm) x.
+Lemma upId_PTm_PTm (sigma : nat -> PTm) (Eq : forall x, sigma x = VarPTm x) :
+  forall x, up_PTm_PTm sigma x = VarPTm x.
 Proof.
 exact (fun n =>
        match n with
-       | Some fin_n => ap (ren_PTm shift) (Eq fin_n)
-       | None => eq_refl
+       | S n' => ap (ren_PTm shift) (Eq n')
+       | O => eq_refl
        end).
 Qed.
 
-Lemma upId_list_PTm_PTm {p : nat} {m_PTm : nat}
-  (sigma : fin m_PTm -> PTm m_PTm) (Eq : forall x, sigma x = VarPTm m_PTm x)
-  : forall x, up_list_PTm_PTm p sigma x = VarPTm (plus p m_PTm) x.
-Proof.
-exact (fun n =>
-       scons_p_eta (VarPTm (plus p m_PTm))
-         (fun n => ap (ren_PTm (shift_p p)) (Eq n)) (fun n => eq_refl)).
-Qed.
-
-Fixpoint idSubst_PTm {m_PTm : nat} (sigma_PTm : fin m_PTm -> PTm m_PTm)
-(Eq_PTm : forall x, sigma_PTm x = VarPTm m_PTm x) (s : PTm m_PTm) {struct s}
-   : subst_PTm sigma_PTm s = s :=
+Fixpoint idSubst_PTm (sigma_PTm : nat -> PTm)
+(Eq_PTm : forall x, sigma_PTm x = VarPTm x) (s : PTm) {struct s} :
+subst_PTm sigma_PTm s = s :=
   match s with
-  | VarPTm _ s0 => Eq_PTm s0
-  | PAbs _ s0 =>
+  | VarPTm s0 => Eq_PTm s0
+  | PAbs s0 =>
       congr_PAbs
         (idSubst_PTm (up_PTm_PTm sigma_PTm) (upId_PTm_PTm _ Eq_PTm) s0)
-  | PApp _ s0 s1 =>
+  | PApp s0 s1 =>
       congr_PApp (idSubst_PTm sigma_PTm Eq_PTm s0)
         (idSubst_PTm sigma_PTm Eq_PTm s1)
-  | PPair _ s0 s1 =>
+  | PPair s0 s1 =>
       congr_PPair (idSubst_PTm sigma_PTm Eq_PTm s0)
         (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 =>
+  | 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
-  | PNat _ => congr_PNat
-  | PZero _ => congr_PZero
-  | PSuc _ s0 => congr_PSuc (idSubst_PTm sigma_PTm Eq_PTm s0)
-  | PInd _ s0 s1 s2 s3 =>
+  | PUniv s0 => congr_PUniv (eq_refl s0)
+  | PBot => congr_PBot
+  | PNat => congr_PNat
+  | PZero => congr_PZero
+  | PSuc s0 => congr_PSuc (idSubst_PTm sigma_PTm Eq_PTm s0)
+  | PInd s0 s1 s2 s3 =>
       congr_PInd
         (idSubst_PTm (up_PTm_PTm sigma_PTm) (upId_PTm_PTm _ Eq_PTm) s0)
         (idSubst_PTm sigma_PTm Eq_PTm s1) (idSubst_PTm sigma_PTm Eq_PTm s2)
@@ -255,54 +211,43 @@ Fixpoint idSubst_PTm {m_PTm : nat} (sigma_PTm : fin m_PTm -> PTm m_PTm)
            (upId_PTm_PTm _ (upId_PTm_PTm _ Eq_PTm)) s3)
   end.
 
-Lemma upExtRen_PTm_PTm {m : nat} {n : nat} (xi : fin m -> fin n)
-  (zeta : fin m -> fin n) (Eq : forall x, xi x = zeta x) :
+Lemma upExtRen_PTm_PTm (xi : nat -> nat) (zeta : nat -> nat)
+  (Eq : forall x, xi x = zeta x) :
   forall x, upRen_PTm_PTm xi x = upRen_PTm_PTm zeta x.
 Proof.
-exact (fun n =>
-       match n with
-       | Some fin_n => ap shift (Eq fin_n)
-       | None => eq_refl
-       end).
+exact (fun n => match n with
+                | S n' => ap shift (Eq n')
+                | O => eq_refl
+                end).
 Qed.
 
-Lemma upExtRen_list_PTm_PTm {p : nat} {m : nat} {n : nat}
-  (xi : fin m -> fin n) (zeta : fin m -> fin n)
-  (Eq : forall x, xi x = zeta x) :
-  forall x, upRen_list_PTm_PTm p xi x = upRen_list_PTm_PTm p zeta x.
-Proof.
-exact (fun n =>
-       scons_p_congr (fun n => eq_refl) (fun n => ap (shift_p p) (Eq n))).
-Qed.
-
-Fixpoint extRen_PTm {m_PTm : nat} {n_PTm : nat}
-(xi_PTm : fin m_PTm -> fin n_PTm) (zeta_PTm : fin m_PTm -> fin n_PTm)
-(Eq_PTm : forall x, xi_PTm x = zeta_PTm x) (s : PTm m_PTm) {struct s} :
+Fixpoint extRen_PTm (xi_PTm : nat -> nat) (zeta_PTm : nat -> nat)
+(Eq_PTm : forall x, xi_PTm x = zeta_PTm x) (s : PTm) {struct s} :
 ren_PTm xi_PTm s = ren_PTm zeta_PTm s :=
   match s with
-  | VarPTm _ s0 => ap (VarPTm n_PTm) (Eq_PTm s0)
-  | PAbs _ s0 =>
+  | VarPTm s0 => ap (VarPTm) (Eq_PTm s0)
+  | PAbs s0 =>
       congr_PAbs
         (extRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm)
            (upExtRen_PTm_PTm _ _ Eq_PTm) s0)
-  | PApp _ s0 s1 =>
+  | PApp s0 s1 =>
       congr_PApp (extRen_PTm xi_PTm zeta_PTm Eq_PTm s0)
         (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1)
-  | PPair _ s0 s1 =>
+  | PPair s0 s1 =>
       congr_PPair (extRen_PTm xi_PTm zeta_PTm Eq_PTm s0)
         (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1)
-  | PProj _ s0 s1 =>
+  | PProj s0 s1 =>
       congr_PProj (eq_refl s0) (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1)
-  | PBind _ s0 s1 s2 =>
+  | 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
-  | PNat _ => congr_PNat
-  | PZero _ => congr_PZero
-  | PSuc _ s0 => congr_PSuc (extRen_PTm xi_PTm zeta_PTm Eq_PTm s0)
-  | PInd _ s0 s1 s2 s3 =>
+  | PUniv s0 => congr_PUniv (eq_refl s0)
+  | PBot => congr_PBot
+  | PNat => congr_PNat
+  | PZero => congr_PZero
+  | PSuc s0 => congr_PSuc (extRen_PTm xi_PTm zeta_PTm Eq_PTm s0)
+  | PInd s0 s1 s2 s3 =>
       congr_PInd
         (extRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm)
            (upExtRen_PTm_PTm _ _ Eq_PTm) s0)
@@ -313,55 +258,44 @@ ren_PTm xi_PTm s = ren_PTm zeta_PTm s :=
            (upExtRen_PTm_PTm _ _ (upExtRen_PTm_PTm _ _ Eq_PTm)) s3)
   end.
 
-Lemma upExt_PTm_PTm {m : nat} {n_PTm : nat} (sigma : fin m -> PTm n_PTm)
-  (tau : fin m -> PTm n_PTm) (Eq : forall x, sigma x = tau x) :
+Lemma upExt_PTm_PTm (sigma : nat -> PTm) (tau : nat -> PTm)
+  (Eq : forall x, sigma x = tau x) :
   forall x, up_PTm_PTm sigma x = up_PTm_PTm tau x.
 Proof.
 exact (fun n =>
        match n with
-       | Some fin_n => ap (ren_PTm shift) (Eq fin_n)
-       | None => eq_refl
+       | S n' => ap (ren_PTm shift) (Eq n')
+       | O => eq_refl
        end).
 Qed.
 
-Lemma upExt_list_PTm_PTm {p : nat} {m : nat} {n_PTm : nat}
-  (sigma : fin m -> PTm n_PTm) (tau : fin m -> PTm n_PTm)
-  (Eq : forall x, sigma x = tau x) :
-  forall x, up_list_PTm_PTm p sigma x = up_list_PTm_PTm p tau x.
-Proof.
-exact (fun n =>
-       scons_p_congr (fun n => eq_refl)
-         (fun n => ap (ren_PTm (shift_p p)) (Eq n))).
-Qed.
-
-Fixpoint ext_PTm {m_PTm : nat} {n_PTm : nat}
-(sigma_PTm : fin m_PTm -> PTm n_PTm) (tau_PTm : fin m_PTm -> PTm n_PTm)
-(Eq_PTm : forall x, sigma_PTm x = tau_PTm x) (s : PTm m_PTm) {struct s} :
+Fixpoint ext_PTm (sigma_PTm : nat -> PTm) (tau_PTm : nat -> PTm)
+(Eq_PTm : forall x, sigma_PTm x = tau_PTm x) (s : PTm) {struct s} :
 subst_PTm sigma_PTm s = subst_PTm tau_PTm s :=
   match s with
-  | VarPTm _ s0 => Eq_PTm s0
-  | PAbs _ s0 =>
+  | VarPTm s0 => Eq_PTm s0
+  | PAbs s0 =>
       congr_PAbs
         (ext_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm)
            (upExt_PTm_PTm _ _ Eq_PTm) s0)
-  | PApp _ s0 s1 =>
+  | PApp s0 s1 =>
       congr_PApp (ext_PTm sigma_PTm tau_PTm Eq_PTm s0)
         (ext_PTm sigma_PTm tau_PTm Eq_PTm s1)
-  | PPair _ s0 s1 =>
+  | PPair s0 s1 =>
       congr_PPair (ext_PTm sigma_PTm tau_PTm Eq_PTm s0)
         (ext_PTm sigma_PTm tau_PTm Eq_PTm s1)
-  | PProj _ s0 s1 =>
+  | PProj s0 s1 =>
       congr_PProj (eq_refl s0) (ext_PTm sigma_PTm tau_PTm Eq_PTm s1)
-  | PBind _ s0 s1 s2 =>
+  | 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
-  | PNat _ => congr_PNat
-  | PZero _ => congr_PZero
-  | PSuc _ s0 => congr_PSuc (ext_PTm sigma_PTm tau_PTm Eq_PTm s0)
-  | PInd _ s0 s1 s2 s3 =>
+  | PUniv s0 => congr_PUniv (eq_refl s0)
+  | PBot => congr_PBot
+  | PNat => congr_PNat
+  | PZero => congr_PZero
+  | PSuc s0 => congr_PSuc (ext_PTm sigma_PTm tau_PTm Eq_PTm s0)
+  | PInd s0 s1 s2 s3 =>
       congr_PInd
         (ext_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm)
            (upExt_PTm_PTm _ _ Eq_PTm) s0)
@@ -372,57 +306,44 @@ subst_PTm sigma_PTm s = subst_PTm tau_PTm s :=
            (upExt_PTm_PTm _ _ (upExt_PTm_PTm _ _ Eq_PTm)) s3)
   end.
 
-Lemma up_ren_ren_PTm_PTm {k : nat} {l : nat} {m : nat} (xi : fin k -> fin l)
-  (zeta : fin l -> fin m) (rho : fin k -> fin m)
-  (Eq : forall x, funcomp zeta xi x = rho x) :
+Lemma up_ren_ren_PTm_PTm (xi : nat -> nat) (zeta : nat -> nat)
+  (rho : nat -> nat) (Eq : forall x, funcomp zeta xi x = rho x) :
   forall x,
   funcomp (upRen_PTm_PTm zeta) (upRen_PTm_PTm xi) x = upRen_PTm_PTm rho x.
 Proof.
 exact (up_ren_ren xi zeta rho Eq).
 Qed.
 
-Lemma up_ren_ren_list_PTm_PTm {p : nat} {k : nat} {l : nat} {m : nat}
-  (xi : fin k -> fin l) (zeta : fin l -> fin m) (rho : fin k -> fin m)
-  (Eq : forall x, funcomp zeta xi x = rho x) :
-  forall x,
-  funcomp (upRen_list_PTm_PTm p zeta) (upRen_list_PTm_PTm p xi) x =
-  upRen_list_PTm_PTm p rho x.
-Proof.
-exact (up_ren_ren_p Eq).
-Qed.
-
-Fixpoint compRenRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
-(xi_PTm : fin m_PTm -> fin k_PTm) (zeta_PTm : fin k_PTm -> fin l_PTm)
-(rho_PTm : fin m_PTm -> fin l_PTm)
-(Eq_PTm : forall x, funcomp zeta_PTm xi_PTm x = rho_PTm x) (s : PTm m_PTm)
-{struct s} : ren_PTm zeta_PTm (ren_PTm xi_PTm s) = ren_PTm rho_PTm s :=
+Fixpoint compRenRen_PTm (xi_PTm : nat -> nat) (zeta_PTm : nat -> nat)
+(rho_PTm : nat -> nat)
+(Eq_PTm : forall x, funcomp zeta_PTm xi_PTm x = rho_PTm x) (s : PTm) {struct
+ s} : ren_PTm zeta_PTm (ren_PTm xi_PTm s) = ren_PTm rho_PTm s :=
   match s with
-  | VarPTm _ s0 => ap (VarPTm l_PTm) (Eq_PTm s0)
-  | PAbs _ s0 =>
+  | VarPTm s0 => ap (VarPTm) (Eq_PTm s0)
+  | PAbs s0 =>
       congr_PAbs
         (compRenRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm)
            (upRen_PTm_PTm rho_PTm) (up_ren_ren _ _ _ Eq_PTm) s0)
-  | PApp _ s0 s1 =>
+  | PApp s0 s1 =>
       congr_PApp (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s0)
         (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1)
-  | PPair _ s0 s1 =>
+  | PPair s0 s1 =>
       congr_PPair (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s0)
         (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1)
-  | PProj _ s0 s1 =>
+  | PProj s0 s1 =>
       congr_PProj (eq_refl s0)
         (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1)
-  | PBind _ s0 s1 s2 =>
+  | 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
-  | PNat _ => congr_PNat
-  | PZero _ => congr_PZero
-  | PSuc _ s0 =>
-      congr_PSuc (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s0)
-  | PInd _ s0 s1 s2 s3 =>
+  | PUniv s0 => congr_PUniv (eq_refl s0)
+  | PBot => congr_PBot
+  | PNat => congr_PNat
+  | PZero => congr_PZero
+  | PSuc s0 => congr_PSuc (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s0)
+  | PInd s0 s1 s2 s3 =>
       congr_PInd
         (compRenRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm)
            (upRen_PTm_PTm rho_PTm) (up_ren_ren _ _ _ Eq_PTm) s0)
@@ -434,66 +355,49 @@ Fixpoint compRenRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
            (up_ren_ren _ _ _ (up_ren_ren _ _ _ Eq_PTm)) s3)
   end.
 
-Lemma up_ren_subst_PTm_PTm {k : nat} {l : nat} {m_PTm : nat}
-  (xi : fin k -> fin l) (tau : fin l -> PTm m_PTm)
-  (theta : fin k -> PTm m_PTm) (Eq : forall x, funcomp tau xi x = theta x) :
+Lemma up_ren_subst_PTm_PTm (xi : nat -> nat) (tau : nat -> PTm)
+  (theta : nat -> PTm) (Eq : forall x, funcomp tau xi x = theta x) :
   forall x,
   funcomp (up_PTm_PTm tau) (upRen_PTm_PTm xi) x = up_PTm_PTm theta x.
 Proof.
 exact (fun n =>
        match n with
-       | Some fin_n => ap (ren_PTm shift) (Eq fin_n)
-       | None => eq_refl
+       | S n' => ap (ren_PTm shift) (Eq n')
+       | O => eq_refl
        end).
 Qed.
 
-Lemma up_ren_subst_list_PTm_PTm {p : nat} {k : nat} {l : nat} {m_PTm : nat}
-  (xi : fin k -> fin l) (tau : fin l -> PTm m_PTm)
-  (theta : fin k -> PTm m_PTm) (Eq : forall x, funcomp tau xi x = theta x) :
-  forall x,
-  funcomp (up_list_PTm_PTm p tau) (upRen_list_PTm_PTm p xi) x =
-  up_list_PTm_PTm p theta x.
-Proof.
-exact (fun n =>
-       eq_trans (scons_p_comp' _ _ _ n)
-         (scons_p_congr (fun z => scons_p_head' _ _ z)
-            (fun z =>
-             eq_trans (scons_p_tail' _ _ (xi z))
-               (ap (ren_PTm (shift_p p)) (Eq z))))).
-Qed.
-
-Fixpoint compRenSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
-(xi_PTm : fin m_PTm -> fin k_PTm) (tau_PTm : fin k_PTm -> PTm l_PTm)
-(theta_PTm : fin m_PTm -> PTm l_PTm)
-(Eq_PTm : forall x, funcomp tau_PTm xi_PTm x = theta_PTm x) (s : PTm m_PTm)
-{struct s} : subst_PTm tau_PTm (ren_PTm xi_PTm s) = subst_PTm theta_PTm s :=
+Fixpoint compRenSubst_PTm (xi_PTm : nat -> nat) (tau_PTm : nat -> PTm)
+(theta_PTm : nat -> PTm)
+(Eq_PTm : forall x, funcomp tau_PTm xi_PTm x = theta_PTm x) (s : PTm) {struct
+ s} : subst_PTm tau_PTm (ren_PTm xi_PTm s) = subst_PTm theta_PTm s :=
   match s with
-  | VarPTm _ s0 => Eq_PTm s0
-  | PAbs _ s0 =>
+  | VarPTm s0 => Eq_PTm s0
+  | PAbs s0 =>
       congr_PAbs
         (compRenSubst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm tau_PTm)
            (up_PTm_PTm theta_PTm) (up_ren_subst_PTm_PTm _ _ _ Eq_PTm) s0)
-  | PApp _ s0 s1 =>
+  | PApp s0 s1 =>
       congr_PApp (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s0)
         (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1)
-  | PPair _ s0 s1 =>
+  | PPair s0 s1 =>
       congr_PPair (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s0)
         (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1)
-  | PProj _ s0 s1 =>
+  | PProj s0 s1 =>
       congr_PProj (eq_refl s0)
         (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1)
-  | PBind _ s0 s1 s2 =>
+  | 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
-  | PNat _ => congr_PNat
-  | PZero _ => congr_PZero
-  | PSuc _ s0 =>
+  | PUniv s0 => congr_PUniv (eq_refl s0)
+  | PBot => congr_PBot
+  | PNat => congr_PNat
+  | PZero => congr_PZero
+  | PSuc s0 =>
       congr_PSuc (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s0)
-  | PInd _ s0 s1 s2 s3 =>
+  | PInd s0 s1 s2 s3 =>
       congr_PInd
         (compRenSubst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm tau_PTm)
            (up_PTm_PTm theta_PTm) (up_ren_subst_PTm_PTm _ _ _ Eq_PTm) s0)
@@ -506,9 +410,8 @@ Fixpoint compRenSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
            s3)
   end.
 
-Lemma up_subst_ren_PTm_PTm {k : nat} {l_PTm : nat} {m_PTm : nat}
-  (sigma : fin k -> PTm l_PTm) (zeta_PTm : fin l_PTm -> fin m_PTm)
-  (theta : fin k -> PTm m_PTm)
+Lemma up_subst_ren_PTm_PTm (sigma : nat -> PTm) (zeta_PTm : nat -> nat)
+  (theta : nat -> PTm)
   (Eq : forall x, funcomp (ren_PTm zeta_PTm) sigma x = theta x) :
   forall x,
   funcomp (ren_PTm (upRen_PTm_PTm zeta_PTm)) (up_PTm_PTm sigma) x =
@@ -516,76 +419,51 @@ Lemma up_subst_ren_PTm_PTm {k : nat} {l_PTm : nat} {m_PTm : nat}
 Proof.
 exact (fun n =>
        match n with
-       | Some fin_n =>
+       | S n' =>
            eq_trans
              (compRenRen_PTm shift (upRen_PTm_PTm zeta_PTm)
-                (funcomp shift zeta_PTm) (fun x => eq_refl) (sigma fin_n))
+                (funcomp shift zeta_PTm) (fun x => eq_refl) (sigma n'))
              (eq_trans
                 (eq_sym
                    (compRenRen_PTm zeta_PTm shift (funcomp shift zeta_PTm)
-                      (fun x => eq_refl) (sigma fin_n)))
-                (ap (ren_PTm shift) (Eq fin_n)))
-       | None => eq_refl
+                      (fun x => eq_refl) (sigma n')))
+                (ap (ren_PTm shift) (Eq n')))
+       | O => eq_refl
        end).
 Qed.
 
-Lemma up_subst_ren_list_PTm_PTm {p : nat} {k : nat} {l_PTm : nat}
-  {m_PTm : nat} (sigma : fin k -> PTm l_PTm)
-  (zeta_PTm : fin l_PTm -> fin m_PTm) (theta : fin k -> PTm m_PTm)
-  (Eq : forall x, funcomp (ren_PTm zeta_PTm) sigma x = theta x) :
-  forall x,
-  funcomp (ren_PTm (upRen_list_PTm_PTm p zeta_PTm)) (up_list_PTm_PTm p sigma)
-    x = up_list_PTm_PTm p theta x.
-Proof.
-exact (fun n =>
-       eq_trans (scons_p_comp' _ _ _ n)
-         (scons_p_congr
-            (fun x => ap (VarPTm (plus p m_PTm)) (scons_p_head' _ _ x))
-            (fun n =>
-             eq_trans
-               (compRenRen_PTm (shift_p p) (upRen_list_PTm_PTm p zeta_PTm)
-                  (funcomp (shift_p p) zeta_PTm)
-                  (fun x => scons_p_tail' _ _ x) (sigma n))
-               (eq_trans
-                  (eq_sym
-                     (compRenRen_PTm zeta_PTm (shift_p p)
-                        (funcomp (shift_p p) zeta_PTm) (fun x => eq_refl)
-                        (sigma n))) (ap (ren_PTm (shift_p p)) (Eq n)))))).
-Qed.
-
-Fixpoint compSubstRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
-(sigma_PTm : fin m_PTm -> PTm k_PTm) (zeta_PTm : fin k_PTm -> fin l_PTm)
-(theta_PTm : fin m_PTm -> PTm l_PTm)
+Fixpoint compSubstRen_PTm (sigma_PTm : nat -> PTm) (zeta_PTm : nat -> nat)
+(theta_PTm : nat -> PTm)
 (Eq_PTm : forall x, funcomp (ren_PTm zeta_PTm) sigma_PTm x = theta_PTm x)
-(s : PTm m_PTm) {struct s} :
+(s : PTm) {struct s} :
 ren_PTm zeta_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s :=
   match s with
-  | VarPTm _ s0 => Eq_PTm s0
-  | PAbs _ s0 =>
+  | VarPTm s0 => Eq_PTm s0
+  | PAbs s0 =>
       congr_PAbs
         (compSubstRen_PTm (up_PTm_PTm sigma_PTm) (upRen_PTm_PTm zeta_PTm)
            (up_PTm_PTm theta_PTm) (up_subst_ren_PTm_PTm _ _ _ Eq_PTm) s0)
-  | PApp _ s0 s1 =>
+  | PApp s0 s1 =>
       congr_PApp (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s0)
         (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1)
-  | PPair _ s0 s1 =>
+  | PPair s0 s1 =>
       congr_PPair (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s0)
         (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1)
-  | PProj _ s0 s1 =>
+  | PProj s0 s1 =>
       congr_PProj (eq_refl s0)
         (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1)
-  | PBind _ s0 s1 s2 =>
+  | 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
-  | PNat _ => congr_PNat
-  | PZero _ => congr_PZero
-  | PSuc _ s0 =>
+  | PUniv s0 => congr_PUniv (eq_refl s0)
+  | PBot => congr_PBot
+  | PNat => congr_PNat
+  | PZero => congr_PZero
+  | PSuc s0 =>
       congr_PSuc (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s0)
-  | PInd _ s0 s1 s2 s3 =>
+  | PInd s0 s1 s2 s3 =>
       congr_PInd
         (compSubstRen_PTm (up_PTm_PTm sigma_PTm) (upRen_PTm_PTm zeta_PTm)
            (up_PTm_PTm theta_PTm) (up_subst_ren_PTm_PTm _ _ _ Eq_PTm) s0)
@@ -598,9 +476,8 @@ ren_PTm zeta_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s :=
            s3)
   end.
 
-Lemma up_subst_subst_PTm_PTm {k : nat} {l_PTm : nat} {m_PTm : nat}
-  (sigma : fin k -> PTm l_PTm) (tau_PTm : fin l_PTm -> PTm m_PTm)
-  (theta : fin k -> PTm m_PTm)
+Lemma up_subst_subst_PTm_PTm (sigma : nat -> PTm) (tau_PTm : nat -> PTm)
+  (theta : nat -> PTm)
   (Eq : forall x, funcomp (subst_PTm tau_PTm) sigma x = theta x) :
   forall x,
   funcomp (subst_PTm (up_PTm_PTm tau_PTm)) (up_PTm_PTm sigma) x =
@@ -608,78 +485,52 @@ Lemma up_subst_subst_PTm_PTm {k : nat} {l_PTm : nat} {m_PTm : nat}
 Proof.
 exact (fun n =>
        match n with
-       | Some fin_n =>
+       | S n' =>
            eq_trans
              (compRenSubst_PTm shift (up_PTm_PTm tau_PTm)
                 (funcomp (up_PTm_PTm tau_PTm) shift) (fun x => eq_refl)
-                (sigma fin_n))
+                (sigma n'))
              (eq_trans
                 (eq_sym
                    (compSubstRen_PTm tau_PTm shift
                       (funcomp (ren_PTm shift) tau_PTm) (fun x => eq_refl)
-                      (sigma fin_n))) (ap (ren_PTm shift) (Eq fin_n)))
-       | None => eq_refl
+                      (sigma n'))) (ap (ren_PTm shift) (Eq n')))
+       | O => eq_refl
        end).
 Qed.
 
-Lemma up_subst_subst_list_PTm_PTm {p : nat} {k : nat} {l_PTm : nat}
-  {m_PTm : nat} (sigma : fin k -> PTm l_PTm)
-  (tau_PTm : fin l_PTm -> PTm m_PTm) (theta : fin k -> PTm m_PTm)
-  (Eq : forall x, funcomp (subst_PTm tau_PTm) sigma x = theta x) :
-  forall x,
-  funcomp (subst_PTm (up_list_PTm_PTm p tau_PTm)) (up_list_PTm_PTm p sigma) x =
-  up_list_PTm_PTm p theta x.
-Proof.
-exact (fun n =>
-       eq_trans
-         (scons_p_comp' (funcomp (VarPTm (plus p l_PTm)) (zero_p p)) _ _ n)
-         (scons_p_congr
-            (fun x => scons_p_head' _ (fun z => ren_PTm (shift_p p) _) x)
-            (fun n =>
-             eq_trans
-               (compRenSubst_PTm (shift_p p) (up_list_PTm_PTm p tau_PTm)
-                  (funcomp (up_list_PTm_PTm p tau_PTm) (shift_p p))
-                  (fun x => eq_refl) (sigma n))
-               (eq_trans
-                  (eq_sym
-                     (compSubstRen_PTm tau_PTm (shift_p p) _
-                        (fun x => eq_sym (scons_p_tail' _ _ x)) (sigma n)))
-                  (ap (ren_PTm (shift_p p)) (Eq n)))))).
-Qed.
-
-Fixpoint compSubstSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
-(sigma_PTm : fin m_PTm -> PTm k_PTm) (tau_PTm : fin k_PTm -> PTm l_PTm)
-(theta_PTm : fin m_PTm -> PTm l_PTm)
+Fixpoint compSubstSubst_PTm (sigma_PTm : nat -> PTm) (tau_PTm : nat -> PTm)
+(theta_PTm : nat -> PTm)
 (Eq_PTm : forall x, funcomp (subst_PTm tau_PTm) sigma_PTm x = theta_PTm x)
-(s : PTm m_PTm) {struct s} :
+(s : PTm) {struct s} :
 subst_PTm tau_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s :=
   match s with
-  | VarPTm _ s0 => Eq_PTm s0
-  | PAbs _ s0 =>
+  | VarPTm s0 => Eq_PTm s0
+  | PAbs s0 =>
       congr_PAbs
         (compSubstSubst_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm)
            (up_PTm_PTm theta_PTm) (up_subst_subst_PTm_PTm _ _ _ Eq_PTm) s0)
-  | PApp _ s0 s1 =>
+  | PApp s0 s1 =>
       congr_PApp (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s0)
         (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1)
-  | PPair _ s0 s1 =>
+  | PPair s0 s1 =>
       congr_PPair (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s0)
         (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1)
-  | PProj _ s0 s1 =>
+  | PProj s0 s1 =>
       congr_PProj (eq_refl s0)
         (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1)
-  | PBind _ s0 s1 s2 =>
+  | 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
-  | PNat _ => congr_PNat
-  | PZero _ => congr_PZero
-  | PSuc _ s0 =>
+  | PUniv s0 => congr_PUniv (eq_refl s0)
+  | PBot => congr_PBot
+  | PNat => congr_PNat
+  | PZero => congr_PZero
+  | PSuc s0 =>
       congr_PSuc (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s0)
-  | PInd _ s0 s1 s2 s3 =>
+  | PInd s0 s1 s2 s3 =>
       congr_PInd
         (compSubstSubst_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm)
            (up_PTm_PTm theta_PTm) (up_subst_subst_PTm_PTm _ _ _ Eq_PTm) s0)
@@ -692,126 +543,102 @@ subst_PTm tau_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s :=
               (up_subst_subst_PTm_PTm _ _ _ Eq_PTm)) s3)
   end.
 
-Lemma renRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
-  (xi_PTm : fin m_PTm -> fin k_PTm) (zeta_PTm : fin k_PTm -> fin l_PTm)
-  (s : PTm m_PTm) :
+Lemma renRen_PTm (xi_PTm : nat -> nat) (zeta_PTm : nat -> nat) (s : PTm) :
   ren_PTm zeta_PTm (ren_PTm xi_PTm s) = ren_PTm (funcomp zeta_PTm xi_PTm) s.
 Proof.
 exact (compRenRen_PTm xi_PTm zeta_PTm _ (fun n => eq_refl) s).
 Qed.
 
-Lemma renRen'_PTm_pointwise {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
-  (xi_PTm : fin m_PTm -> fin k_PTm) (zeta_PTm : fin k_PTm -> fin l_PTm) :
+Lemma renRen'_PTm_pointwise (xi_PTm : nat -> nat) (zeta_PTm : nat -> nat) :
   pointwise_relation _ eq (funcomp (ren_PTm zeta_PTm) (ren_PTm xi_PTm))
     (ren_PTm (funcomp zeta_PTm xi_PTm)).
 Proof.
 exact (fun s => compRenRen_PTm xi_PTm zeta_PTm _ (fun n => eq_refl) s).
 Qed.
 
-Lemma renSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
-  (xi_PTm : fin m_PTm -> fin k_PTm) (tau_PTm : fin k_PTm -> PTm l_PTm)
-  (s : PTm m_PTm) :
+Lemma renSubst_PTm (xi_PTm : nat -> nat) (tau_PTm : nat -> PTm) (s : PTm) :
   subst_PTm tau_PTm (ren_PTm xi_PTm s) = subst_PTm (funcomp tau_PTm xi_PTm) s.
 Proof.
 exact (compRenSubst_PTm xi_PTm tau_PTm _ (fun n => eq_refl) s).
 Qed.
 
-Lemma renSubst_PTm_pointwise {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
-  (xi_PTm : fin m_PTm -> fin k_PTm) (tau_PTm : fin k_PTm -> PTm l_PTm) :
+Lemma renSubst_PTm_pointwise (xi_PTm : nat -> nat) (tau_PTm : nat -> PTm) :
   pointwise_relation _ eq (funcomp (subst_PTm tau_PTm) (ren_PTm xi_PTm))
     (subst_PTm (funcomp tau_PTm xi_PTm)).
 Proof.
 exact (fun s => compRenSubst_PTm xi_PTm tau_PTm _ (fun n => eq_refl) s).
 Qed.
 
-Lemma substRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
-  (sigma_PTm : fin m_PTm -> PTm k_PTm) (zeta_PTm : fin k_PTm -> fin l_PTm)
-  (s : PTm m_PTm) :
+Lemma substRen_PTm (sigma_PTm : nat -> PTm) (zeta_PTm : nat -> nat) (s : PTm)
+  :
   ren_PTm zeta_PTm (subst_PTm sigma_PTm s) =
   subst_PTm (funcomp (ren_PTm zeta_PTm) sigma_PTm) s.
 Proof.
 exact (compSubstRen_PTm sigma_PTm zeta_PTm _ (fun n => eq_refl) s).
 Qed.
 
-Lemma substRen_PTm_pointwise {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
-  (sigma_PTm : fin m_PTm -> PTm k_PTm) (zeta_PTm : fin k_PTm -> fin l_PTm) :
+Lemma substRen_PTm_pointwise (sigma_PTm : nat -> PTm) (zeta_PTm : nat -> nat)
+  :
   pointwise_relation _ eq (funcomp (ren_PTm zeta_PTm) (subst_PTm sigma_PTm))
     (subst_PTm (funcomp (ren_PTm zeta_PTm) sigma_PTm)).
 Proof.
 exact (fun s => compSubstRen_PTm sigma_PTm zeta_PTm _ (fun n => eq_refl) s).
 Qed.
 
-Lemma substSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
-  (sigma_PTm : fin m_PTm -> PTm k_PTm) (tau_PTm : fin k_PTm -> PTm l_PTm)
-  (s : PTm m_PTm) :
+Lemma substSubst_PTm (sigma_PTm : nat -> PTm) (tau_PTm : nat -> PTm)
+  (s : PTm) :
   subst_PTm tau_PTm (subst_PTm sigma_PTm s) =
   subst_PTm (funcomp (subst_PTm tau_PTm) sigma_PTm) s.
 Proof.
 exact (compSubstSubst_PTm sigma_PTm tau_PTm _ (fun n => eq_refl) s).
 Qed.
 
-Lemma substSubst_PTm_pointwise {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
-  (sigma_PTm : fin m_PTm -> PTm k_PTm) (tau_PTm : fin k_PTm -> PTm l_PTm) :
+Lemma substSubst_PTm_pointwise (sigma_PTm : nat -> PTm)
+  (tau_PTm : nat -> PTm) :
   pointwise_relation _ eq (funcomp (subst_PTm tau_PTm) (subst_PTm sigma_PTm))
     (subst_PTm (funcomp (subst_PTm tau_PTm) sigma_PTm)).
 Proof.
 exact (fun s => compSubstSubst_PTm sigma_PTm tau_PTm _ (fun n => eq_refl) s).
 Qed.
 
-Lemma rinstInst_up_PTm_PTm {m : nat} {n_PTm : nat} (xi : fin m -> fin n_PTm)
-  (sigma : fin m -> PTm n_PTm)
-  (Eq : forall x, funcomp (VarPTm n_PTm) xi x = sigma x) :
-  forall x,
-  funcomp (VarPTm (S n_PTm)) (upRen_PTm_PTm xi) x = up_PTm_PTm sigma x.
+Lemma rinstInst_up_PTm_PTm (xi : nat -> nat) (sigma : nat -> PTm)
+  (Eq : forall x, funcomp (VarPTm) xi x = sigma x) :
+  forall x, funcomp (VarPTm) (upRen_PTm_PTm xi) x = up_PTm_PTm sigma x.
 Proof.
 exact (fun n =>
        match n with
-       | Some fin_n => ap (ren_PTm shift) (Eq fin_n)
-       | None => eq_refl
+       | S n' => ap (ren_PTm shift) (Eq n')
+       | O => eq_refl
        end).
 Qed.
 
-Lemma rinstInst_up_list_PTm_PTm {p : nat} {m : nat} {n_PTm : nat}
-  (xi : fin m -> fin n_PTm) (sigma : fin m -> PTm n_PTm)
-  (Eq : forall x, funcomp (VarPTm n_PTm) xi x = sigma x) :
-  forall x,
-  funcomp (VarPTm (plus p n_PTm)) (upRen_list_PTm_PTm p xi) x =
-  up_list_PTm_PTm p sigma x.
-Proof.
-exact (fun n =>
-       eq_trans (scons_p_comp' _ _ (VarPTm (plus p n_PTm)) n)
-         (scons_p_congr (fun z => eq_refl)
-            (fun n => ap (ren_PTm (shift_p p)) (Eq n)))).
-Qed.
-
-Fixpoint rinst_inst_PTm {m_PTm : nat} {n_PTm : nat}
-(xi_PTm : fin m_PTm -> fin n_PTm) (sigma_PTm : fin m_PTm -> PTm n_PTm)
-(Eq_PTm : forall x, funcomp (VarPTm n_PTm) xi_PTm x = sigma_PTm x)
-(s : PTm m_PTm) {struct s} : ren_PTm xi_PTm s = subst_PTm sigma_PTm s :=
+Fixpoint rinst_inst_PTm (xi_PTm : nat -> nat) (sigma_PTm : nat -> PTm)
+(Eq_PTm : forall x, funcomp (VarPTm) xi_PTm x = sigma_PTm x) (s : PTm)
+{struct s} : ren_PTm xi_PTm s = subst_PTm sigma_PTm s :=
   match s with
-  | VarPTm _ s0 => Eq_PTm s0
-  | PAbs _ s0 =>
+  | VarPTm s0 => Eq_PTm s0
+  | PAbs s0 =>
       congr_PAbs
         (rinst_inst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm sigma_PTm)
            (rinstInst_up_PTm_PTm _ _ Eq_PTm) s0)
-  | PApp _ s0 s1 =>
+  | PApp s0 s1 =>
       congr_PApp (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s0)
         (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1)
-  | PPair _ s0 s1 =>
+  | PPair s0 s1 =>
       congr_PPair (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s0)
         (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1)
-  | PProj _ s0 s1 =>
+  | PProj s0 s1 =>
       congr_PProj (eq_refl s0) (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1)
-  | PBind _ s0 s1 s2 =>
+  | 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
-  | PNat _ => congr_PNat
-  | PZero _ => congr_PZero
-  | PSuc _ s0 => congr_PSuc (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s0)
-  | PInd _ s0 s1 s2 s3 =>
+  | PUniv s0 => congr_PUniv (eq_refl s0)
+  | PBot => congr_PBot
+  | PNat => congr_PNat
+  | PZero => congr_PZero
+  | PSuc s0 => congr_PSuc (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s0)
+  | PInd s0 s1 s2 s3 =>
       congr_PInd
         (rinst_inst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm sigma_PTm)
            (rinstInst_up_PTm_PTm _ _ Eq_PTm) s0)
@@ -822,71 +649,61 @@ Fixpoint rinst_inst_PTm {m_PTm : nat} {n_PTm : nat}
            (rinstInst_up_PTm_PTm _ _ (rinstInst_up_PTm_PTm _ _ Eq_PTm)) s3)
   end.
 
-Lemma rinstInst'_PTm {m_PTm : nat} {n_PTm : nat}
-  (xi_PTm : fin m_PTm -> fin n_PTm) (s : PTm m_PTm) :
-  ren_PTm xi_PTm s = subst_PTm (funcomp (VarPTm n_PTm) xi_PTm) s.
+Lemma rinstInst'_PTm (xi_PTm : nat -> nat) (s : PTm) :
+  ren_PTm xi_PTm s = subst_PTm (funcomp (VarPTm) xi_PTm) s.
 Proof.
 exact (rinst_inst_PTm xi_PTm _ (fun n => eq_refl) s).
 Qed.
 
-Lemma rinstInst'_PTm_pointwise {m_PTm : nat} {n_PTm : nat}
-  (xi_PTm : fin m_PTm -> fin n_PTm) :
+Lemma rinstInst'_PTm_pointwise (xi_PTm : nat -> nat) :
   pointwise_relation _ eq (ren_PTm xi_PTm)
-    (subst_PTm (funcomp (VarPTm n_PTm) xi_PTm)).
+    (subst_PTm (funcomp (VarPTm) xi_PTm)).
 Proof.
 exact (fun s => rinst_inst_PTm xi_PTm _ (fun n => eq_refl) s).
 Qed.
 
-Lemma instId'_PTm {m_PTm : nat} (s : PTm m_PTm) :
-  subst_PTm (VarPTm m_PTm) s = s.
+Lemma instId'_PTm (s : PTm) : subst_PTm (VarPTm) s = s.
 Proof.
-exact (idSubst_PTm (VarPTm m_PTm) (fun n => eq_refl) s).
+exact (idSubst_PTm (VarPTm) (fun n => eq_refl) s).
 Qed.
 
-Lemma instId'_PTm_pointwise {m_PTm : nat} :
-  pointwise_relation _ eq (subst_PTm (VarPTm m_PTm)) id.
+Lemma instId'_PTm_pointwise : pointwise_relation _ eq (subst_PTm (VarPTm)) id.
 Proof.
-exact (fun s => idSubst_PTm (VarPTm m_PTm) (fun n => eq_refl) s).
+exact (fun s => idSubst_PTm (VarPTm) (fun n => eq_refl) s).
 Qed.
 
-Lemma rinstId'_PTm {m_PTm : nat} (s : PTm m_PTm) : ren_PTm id s = s.
+Lemma rinstId'_PTm (s : PTm) : ren_PTm id s = s.
 Proof.
 exact (eq_ind_r (fun t => t = s) (instId'_PTm s) (rinstInst'_PTm id s)).
 Qed.
 
-Lemma rinstId'_PTm_pointwise {m_PTm : nat} :
-  pointwise_relation _ eq (@ren_PTm m_PTm m_PTm id) id.
+Lemma rinstId'_PTm_pointwise : pointwise_relation _ eq (@ren_PTm id) id.
 Proof.
 exact (fun s =>
        eq_ind_r (fun t => t = s) (instId'_PTm s) (rinstInst'_PTm id s)).
 Qed.
 
-Lemma varL'_PTm {m_PTm : nat} {n_PTm : nat}
-  (sigma_PTm : fin m_PTm -> PTm n_PTm) (x : fin m_PTm) :
-  subst_PTm sigma_PTm (VarPTm m_PTm x) = sigma_PTm x.
+Lemma varL'_PTm (sigma_PTm : nat -> PTm) (x : nat) :
+  subst_PTm sigma_PTm (VarPTm x) = sigma_PTm x.
 Proof.
 exact (eq_refl).
 Qed.
 
-Lemma varL'_PTm_pointwise {m_PTm : nat} {n_PTm : nat}
-  (sigma_PTm : fin m_PTm -> PTm n_PTm) :
-  pointwise_relation _ eq (funcomp (subst_PTm sigma_PTm) (VarPTm m_PTm))
-    sigma_PTm.
+Lemma varL'_PTm_pointwise (sigma_PTm : nat -> PTm) :
+  pointwise_relation _ eq (funcomp (subst_PTm sigma_PTm) (VarPTm)) sigma_PTm.
 Proof.
 exact (fun x => eq_refl).
 Qed.
 
-Lemma varLRen'_PTm {m_PTm : nat} {n_PTm : nat}
-  (xi_PTm : fin m_PTm -> fin n_PTm) (x : fin m_PTm) :
-  ren_PTm xi_PTm (VarPTm m_PTm x) = VarPTm n_PTm (xi_PTm x).
+Lemma varLRen'_PTm (xi_PTm : nat -> nat) (x : nat) :
+  ren_PTm xi_PTm (VarPTm x) = VarPTm (xi_PTm x).
 Proof.
 exact (eq_refl).
 Qed.
 
-Lemma varLRen'_PTm_pointwise {m_PTm : nat} {n_PTm : nat}
-  (xi_PTm : fin m_PTm -> fin n_PTm) :
-  pointwise_relation _ eq (funcomp (ren_PTm xi_PTm) (VarPTm m_PTm))
-    (funcomp (VarPTm n_PTm) xi_PTm).
+Lemma varLRen'_PTm_pointwise (xi_PTm : nat -> nat) :
+  pointwise_relation _ eq (funcomp (ren_PTm xi_PTm) (VarPTm))
+    (funcomp (VarPTm) xi_PTm).
 Proof.
 exact (fun x => eq_refl).
 Qed.
@@ -894,18 +711,14 @@ Qed.
 Class Up_PTm X Y :=
     up_PTm : X -> Y.
 
-#[global]
-Instance Subst_PTm  {m_PTm n_PTm : nat}: (Subst1 _ _ _) :=
- (@subst_PTm m_PTm n_PTm).
+#[global]Instance Subst_PTm : (Subst1 _ _ _) := @subst_PTm.
+
+#[global]Instance Up_PTm_PTm : (Up_PTm _ _) := @up_PTm_PTm.
+
+#[global]Instance Ren_PTm : (Ren1 _ _ _) := @ren_PTm.
 
 #[global]
-Instance Up_PTm_PTm  {m n_PTm : nat}: (Up_PTm _ _) := (@up_PTm_PTm m n_PTm).
-
-#[global]
-Instance Ren_PTm  {m_PTm n_PTm : nat}: (Ren1 _ _ _) := (@ren_PTm m_PTm n_PTm).
-
-#[global]
-Instance VarInstance_PTm  {n_PTm : nat}: (Var _ _) := (@VarPTm n_PTm).
+Instance VarInstance_PTm : (Var _ _) := @VarPTm.
 
 Notation "[ sigma_PTm ]" := (subst_PTm sigma_PTm)
 ( at level 1, left associativity, only printing)  : fscope.
@@ -932,9 +745,9 @@ Notation "x '__PTm'" := (VarPTm x) ( at level 5, format "x __PTm")  :
 subst_scope.
 
 #[global]
-Instance subst_PTm_morphism  {m_PTm : nat} {n_PTm : nat}:
+Instance subst_PTm_morphism :
  (Proper (respectful (pointwise_relation _ eq) (respectful eq eq))
-    (@subst_PTm m_PTm n_PTm)).
+    (@subst_PTm)).
 Proof.
 exact (fun f_PTm g_PTm Eq_PTm s t Eq_st =>
        eq_ind s (fun t' => subst_PTm f_PTm s = subst_PTm g_PTm t')
@@ -942,17 +755,16 @@ exact (fun f_PTm g_PTm Eq_PTm s t Eq_st =>
 Qed.
 
 #[global]
-Instance subst_PTm_morphism2  {m_PTm : nat} {n_PTm : nat}:
+Instance subst_PTm_morphism2 :
  (Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq))
-    (@subst_PTm m_PTm n_PTm)).
+    (@subst_PTm)).
 Proof.
 exact (fun f_PTm g_PTm Eq_PTm s => ext_PTm f_PTm g_PTm Eq_PTm s).
 Qed.
 
 #[global]
-Instance ren_PTm_morphism  {m_PTm : nat} {n_PTm : nat}:
- (Proper (respectful (pointwise_relation _ eq) (respectful eq eq))
-    (@ren_PTm m_PTm n_PTm)).
+Instance ren_PTm_morphism :
+ (Proper (respectful (pointwise_relation _ eq) (respectful eq eq)) (@ren_PTm)).
 Proof.
 exact (fun f_PTm g_PTm Eq_PTm s t Eq_st =>
        eq_ind s (fun t' => ren_PTm f_PTm s = ren_PTm g_PTm t')
@@ -960,9 +772,9 @@ exact (fun f_PTm g_PTm Eq_PTm s t Eq_st =>
 Qed.
 
 #[global]
-Instance ren_PTm_morphism2  {m_PTm : nat} {n_PTm : nat}:
+Instance ren_PTm_morphism2 :
  (Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq))
-    (@ren_PTm m_PTm n_PTm)).
+    (@ren_PTm)).
 Proof.
 exact (fun f_PTm g_PTm Eq_PTm s => extRen_PTm f_PTm g_PTm Eq_PTm s).
 Qed.
@@ -994,9 +806,7 @@ Ltac asimpl' := repeat (first
                  | progress setoid_rewrite rinstId'_PTm
                  | progress setoid_rewrite instId'_PTm_pointwise
                  | progress setoid_rewrite instId'_PTm
-                 | progress
-                    unfold up_list_PTm_PTm, up_PTm_PTm, upRen_list_PTm_PTm,
-                     upRen_PTm_PTm, up_ren
+                 | progress unfold up_PTm_PTm, upRen_PTm_PTm, up_ren
                  | progress cbn[subst_PTm ren_PTm]
                  | progress fsimpl ]).
 
@@ -1021,32 +831,7 @@ End Core.
 
 Module Extra.
 
-Import
-Core.
-
-Arguments VarPTm {n_PTm}.
-
-Arguments PInd {n_PTm}.
-
-Arguments PSuc {n_PTm}.
-
-Arguments PZero {n_PTm}.
-
-Arguments PNat {n_PTm}.
-
-Arguments PBot {n_PTm}.
-
-Arguments PUniv {n_PTm}.
-
-Arguments PBind {n_PTm}.
-
-Arguments PProj {n_PTm}.
-
-Arguments PPair {n_PTm}.
-
-Arguments PApp {n_PTm}.
-
-Arguments PAbs {n_PTm}.
+Import Core.
 
 #[global]Hint Opaque subst_PTm: rewrite.
 
diff --git a/theories/Autosubst2/unscoped.v b/theories/Autosubst2/unscoped.v
new file mode 100644
index 0000000..55f8172
--- /dev/null
+++ b/theories/Autosubst2/unscoped.v
@@ -0,0 +1,213 @@
+(** * Autosubst Header for Unnamed Syntax
+
+Version: December 11, 2019.
+ *)
+
+(* Adrian:
+ I changed this library a bit to work better with my generated code.
+ 1. I use nat directly instead of defining fin to be nat and using Some/None as S/O
+ 2. I removed the "s, sigma" notation for scons because it interacts with dependent function types "forall x, A"*)
+Require Import core.
+Require Import Setoid Morphisms Relation_Definitions.
+
+Definition ap {X Y} (f : X -> Y) {x y : X} (p : x = y) : f x = f y :=
+  match p with eq_refl => eq_refl end.
+
+Definition apc {X Y} {f g : X -> Y} {x y : X} (p : f = g) (q : x = y) : f x = g y :=
+  match q with eq_refl => match p with eq_refl => eq_refl end end.
+
+(** ** Primitives of the Sigma Calculus. *)
+
+Definition shift  := S.
+
+Definition var_zero := 0.
+
+Definition id {X} := @Datatypes.id X.
+
+Definition scons {X: Type} (x : X) (xi : nat -> X) :=
+  fun n => match n with
+        | 0 => x
+        | S n => xi n
+        end.
+
+#[ export ]
+Hint Opaque scons : rewrite.
+
+(** ** Type Class Instances for Notation
+Required to make notation work. *)
+
+(** *** Type classes for renamings. *)
+
+Class Ren1 (X1  : Type) (Y Z : Type) :=
+  ren1 : X1 -> Y -> Z.
+
+Class Ren2 (X1 X2 : Type) (Y Z : Type) :=
+  ren2 : X1 -> X2 -> Y -> Z.
+
+Class Ren3 (X1 X2 X3 : Type) (Y Z : Type) :=
+  ren3 : X1 -> X2 -> X3 -> Y -> Z.
+
+Class Ren4 (X1 X2 X3 X4 : Type) (Y Z : Type) :=
+  ren4 : X1 -> X2 -> X3 -> X4 -> Y -> Z.
+
+Class Ren5 (X1 X2 X3 X4 X5 : Type) (Y Z : Type) :=
+  ren5 : X1 -> X2 -> X3 -> X4 -> X5 -> Y -> Z.
+
+Module RenNotations.
+  Notation "s ⟨ xi1 ⟩" := (ren1 xi1 s) (at level 7, left associativity, format "s  ⟨ xi1 ⟩") : subst_scope.
+
+  Notation "s ⟨ xi1 ; xi2 ⟩" := (ren2 xi1 xi2 s) (at level 7, left associativity, format "s  ⟨ xi1 ; xi2 ⟩") : subst_scope.
+
+  Notation "s ⟨ xi1 ; xi2 ; xi3 ⟩" := (ren3 xi1 xi2 xi3 s) (at level 7, left associativity, format "s  ⟨ xi1 ; xi2 ; xi3 ⟩") : subst_scope.
+
+  Notation "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ⟩" := (ren4  xi1 xi2 xi3 xi4 s) (at level 7, left associativity, format "s  ⟨ xi1 ; xi2 ; xi3 ; xi4 ⟩") : subst_scope.
+
+  Notation "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ; xi5 ⟩" := (ren5  xi1 xi2 xi3 xi4 xi5 s) (at level 7, left associativity, format "s  ⟨ xi1 ; xi2 ; xi3 ; xi4 ; xi5 ⟩") : subst_scope.
+
+  Notation "⟨ xi ⟩" := (ren1 xi) (at level 1, left associativity, format "⟨ xi ⟩") : fscope.
+
+  Notation "⟨ xi1 ; xi2 ⟩" := (ren2 xi1 xi2) (at level 1, left associativity, format "⟨ xi1 ; xi2 ⟩") : fscope.
+End RenNotations.
+
+(** *** Type Classes for Substiution *)
+
+Class Subst1 (X1 : Type) (Y Z: Type) :=
+  subst1 : X1 -> Y -> Z.
+
+Class Subst2 (X1 X2 : Type) (Y Z: Type) :=
+  subst2 : X1 -> X2 -> Y  -> Z.
+
+Class Subst3 (X1 X2 X3 : Type) (Y Z: Type) :=
+  subst3 : X1 -> X2 -> X3 ->  Y  -> Z.
+
+Class Subst4 (X1 X2 X3 X4: Type) (Y Z: Type) :=
+  subst4 : X1 -> X2 -> X3 -> X4 -> Y  -> Z.
+
+Class Subst5 (X1 X2 X3 X4 X5 : Type) (Y Z: Type) :=
+  subst5 : X1 -> X2 -> X3 -> X4 -> X5  -> Y  -> Z.
+
+Module SubstNotations.
+  Notation "s [ sigma ]" := (subst1 sigma s) (at level 7, left associativity, format "s '/' [ sigma ]") : subst_scope.
+
+  Notation "s [ sigma ; tau ]" := (subst2 sigma tau s) (at level 7, left associativity, format "s '/' [ sigma ; '/'  tau ]") : subst_scope.
+End SubstNotations.
+
+(** *** Type Class for Variables *)
+
+Class Var X Y :=
+  ids : X -> Y.
+
+#[export] Instance idsRen : Var nat nat := id.
+
+(** ** Proofs for the substitution primitives. *)
+
+Arguments funcomp {X Y Z} (g)%fscope (f)%fscope.
+
+Module CombineNotations.
+  Notation "f >> g" := (funcomp g f) (at level 50) : fscope.
+
+  Notation "s .: sigma" := (scons s sigma) (at level 55, sigma at next level, right associativity) : subst_scope.
+
+  #[ global ]
+  Open Scope fscope.
+  #[ global ]
+  Open Scope subst_scope.
+End CombineNotations.
+
+Import CombineNotations.
+
+
+(** A generic lifting of a renaming. *)
+Definition up_ren (xi : nat -> nat) :=
+  0 .: (xi >> S).
+
+(** A generic proof that lifting of renamings composes. *)
+Lemma up_ren_ren (xi: nat -> nat) (zeta : nat -> nat) (rho: nat -> nat) (E: forall x, (xi >> zeta) x = rho x) :
+  forall x, (up_ren xi >> up_ren zeta) x = up_ren rho x.
+Proof.
+  intros [|x].
+  - reflexivity.
+  - unfold up_ren. cbn. unfold funcomp. f_equal. apply E.
+Qed.
+
+(** Eta laws. *)
+Lemma scons_eta' {T} (f : nat -> T) :
+  pointwise_relation _ eq (f var_zero .: (funcomp f shift)) f.
+Proof. intros x. destruct x; reflexivity. Qed.
+
+Lemma scons_eta_id' :
+  pointwise_relation _ eq (var_zero .: shift) id.
+Proof. intros x. destruct x; reflexivity. Qed.
+
+Lemma scons_comp' (T: Type) {U} (s: T) (sigma: nat -> T) (tau: T -> U) :
+  pointwise_relation _ eq (funcomp tau (s .: sigma)) ((tau s) .: (funcomp tau sigma)).
+Proof. intros x. destruct x; reflexivity. Qed.
+
+(* Morphism for Setoid Rewriting. The only morphism that can be defined statically. *)
+#[export] Instance scons_morphism {X: Type} :
+  Proper (eq ==> pointwise_relation _ eq ==> pointwise_relation _ eq) (@scons X).
+Proof.
+  intros ? t -> sigma tau H.
+  intros [|x].
+  cbn. reflexivity.
+  apply H.
+Qed.
+
+#[export] Instance scons_morphism2 {X: Type} :
+  Proper (eq ==> pointwise_relation _ eq ==> eq ==> eq) (@scons X).
+Proof.
+  intros ? t -> sigma tau H ? x ->.
+  destruct x as [|x].
+  cbn. reflexivity.
+  apply H.
+Qed.
+
+(** ** Generic lifting of an allfv predicate *)
+Definition up_allfv (p: nat -> Prop) : nat -> Prop := scons True p.
+
+(** ** Notations for unscoped syntax *)
+Module UnscopedNotations.
+  Include RenNotations.
+  Include SubstNotations.
+  Include CombineNotations.
+  
+  (* Notation "s , sigma" := (scons s sigma) (at level 60, format "s ,  sigma", right associativity) : subst_scope. *)
+
+  Notation "s '..'" := (scons s ids) (at level 1, format "s ..") : subst_scope.
+
+  Notation "↑" := (shift) : subst_scope.
+
+  #[global]
+  Open Scope fscope.
+  #[global]
+  Open Scope subst_scope.
+End UnscopedNotations.
+
+(** ** Tactics for unscoped syntax *)
+
+(** Automatically does a case analysis on a natural number, useful for proofs with context renamings/context morphisms. *)
+Tactic Notation "auto_case" tactic(t) :=  (match goal with
+                                           | [|- forall (i : nat), _] => intros []; t
+                                           end).
+
+
+(** Generic fsimpl tactic: simplifies the above primitives in a goal. *)
+Ltac fsimpl :=
+  repeat match goal with
+         | [|- context[id >> ?f]] => change (id >> f) with f (* AsimplCompIdL *)
+         | [|- context[?f >> id]] => change (f >> id) with f (* AsimplCompIdR *)
+         | [|- context [id ?s]] => change (id s) with s
+         | [|- context[(?f >> ?g) >> ?h]] => change ((f >> g) >> h) with (f >> (g >> h))
+         | [|- context[(?v .: ?g) var_zero]] => change ((v .: g) var_zero) with v
+         | [|- context[(?v .: ?g) 0]] => change ((v .: g) 0) with v
+         | [|- context[(?v .: ?g) (S ?n)]] => change ((v .: g) (S n)) with (g n)
+         | [|- context[?f >> (?x .: ?g)]] => change (f >> (x .: g)) with g (* f should evaluate to shift *)
+         | [|- context[var_zero]] =>  change var_zero with 0
+         | [|- context[?x2 .: (funcomp ?f shift)]] => change (scons x2 (funcomp f shift)) with (scons (f var_zero) (funcomp f shift)); setoid_rewrite (@scons_eta' _ _ f)
+         | [|- context[?f var_zero .: ?g]] => change (scons (f var_zero) g) with (scons (f var_zero) (funcomp f shift)); rewrite scons_eta'
+         | [|- _ =  ?h (?f ?s)] => change (h (f s)) with ((f >> h) s)
+         | [|-  ?h (?f ?s) = _] => change (h (f s)) with ((f >> h) s)
+         (* DONE had to put an underscore as the last argument to scons. This might be an argument against unfolding funcomp *)
+         | [|- context[funcomp _ (scons _ _)]] => setoid_rewrite scons_comp'; eta_reduce
+         | [|- context[scons var_zero shift]] => setoid_rewrite scons_eta_id'; eta_reduce
+                        end.
\ No newline at end of file
diff --git a/theories/common.v b/theories/common.v
index 282038d..51fad7b 100644
--- a/theories/common.v
+++ b/theories/common.v
@@ -4,6 +4,7 @@ Import Ltac2.Notations.
 Import Ltac2.Control.
 From Hammer Require Import Tactics.
 
+
 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).
 
diff --git a/theories/executable.v b/theories/executable.v
index dd7d2aa..04ab661 100644
--- a/theories/executable.v
+++ b/theories/executable.v
@@ -1,13 +1,64 @@
 From Equations Require Import Equations.
-Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax
-  common typing preservation admissible fp_red structural soundness.
-Require Import algorithmic.
-From stdpp Require Import relations (rtc(..), nsteps(..)).
+Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax.
+Derive NoConfusion for nat PTag BTag PTm.
+
 Require Import ssreflect ssrbool.
 From Hammer Require Import Tactics.
 
 
-Inductive algo_dom {n} : PTm n -> PTm n -> Prop :=
+Definition ishf (a : PTm) :=
+  match a with
+  | PPair _ _ => true
+  | PAbs _ => true
+  | PUniv _ => true
+  | PBind _ _ _ => true
+  | PNat => true
+  | PSuc _ => true
+  | PZero => true
+  | _ => false
+  end.
+
+Fixpoint ishne (a : PTm) :=
+  match a with
+  | VarPTm _ => true
+  | PApp a _ => ishne a
+  | PProj _ a => ishne a
+  | PBot => true
+  | PInd _ n _ _ => ishne n
+  | _ => false
+  end.
+
+Module HRed.
+  Inductive R : PTm -> PTm ->  Prop :=
+  (****************** Beta ***********************)
+  | AppAbs a b :
+    R (PApp (PAbs a) b)  (subst_PTm (scons b VarPTm) a)
+
+  | ProjPair p a b :
+    R (PProj p (PPair a b)) (if p is PL then a else b)
+
+  | IndZero P b c :
+    R (PInd P PZero b c) b
+
+  | IndSuc P a b c :
+    R (PInd P (PSuc a) b c) (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c)
+
+  (*************** Congruence ********************)
+  | AppCong a0 a1 b :
+    R a0 a1 ->
+    R (PApp a0 b) (PApp a1 b)
+  | ProjCong p a0 a1 :
+    R a0 a1 ->
+    R (PProj p a0) (PProj p a1)
+  | IndCong P a0 a1 b c :
+    R a0 a1 ->
+    R (PInd P a0 b c) (PInd P a1 b c).
+
+  Definition nf a := forall b, ~ R a b.
+End HRed.
+
+
+Inductive algo_dom : PTm -> PTm -> Prop :=
 | A_AbsAbs a b :
   algo_dom_r a b ->
   (* --------------------- *)
@@ -74,7 +125,7 @@ Inductive algo_dom {n} : PTm n -> PTm n -> Prop :=
   (* ------------------------- *)
   algo_dom (PApp u0 a0) (PApp u1 a1)
 
-with algo_dom_r {n} : PTm n -> PTm n -> Prop :=
+with algo_dom_r : PTm  -> PTm -> Prop :=
 | A_NfNf a b :
   algo_dom a b ->
   algo_dom_r a b
@@ -92,67 +143,26 @@ with algo_dom_r {n} : PTm n -> PTm n -> Prop :=
   (* ----------------------- *)
   algo_dom_r a b.
 
-Derive Signature for algo_dom algo_dom_r.
-Derive NoConfusion for PTm.
-Next Obligation.
-Admitted.
-Next Obligation.
-Admitted.
-
-Derive Dependent Inversion adom_inv with (forall n (a b : PTm n), algo_dom a b) Sort Prop.
-
-Lemma algo_dom_hf_hne n (a b : PTm n) :
+Lemma algo_dom_hf_hne (a b : PTm) :
   algo_dom a b ->
   (ishf a \/ ishne a) /\ (ishf b \/ ishne b).
 Proof.
   induction 1 =>//=; hauto lq:on.
 Qed.
 
-Lemma hf_no_hred n (a b : PTm n) :
+Lemma hf_no_hred (a b : PTm) :
   ishf a ->
   HRed.R a b ->
   False.
 Proof. hauto l:on inv:HRed.R. Qed.
 
-Lemma hne_no_hred n (a b : PTm n) :
+Lemma hne_no_hred (a b : PTm) :
   ishne a ->
   HRed.R a b ->
   False.
 Proof. elim : a b => //=; hauto l:on inv:HRed.R. Qed.
 
-Definition fin_beq {n} (i j : fin n) : bool.
-Proof.
-  induction n.
-  - by exfalso.
-  - refine (match i , j with
-            | None, None => true
-            | Some i, Some j => IHn i j
-            | _, _ => false
-            end).
-Defined.
-
-Lemma fin_eq_dec {n} (i j : fin n) :
-  Bool.reflect (i = j) (fin_beq i j).
-Proof.
-  revert i j. induction n.
-  - destruct i.
-  - destruct i; destruct j.
-    + specialize (IHn f f0).
-      inversion IHn; subst.
-      simpl. rewrite -H.
-      apply ReflectT.
-      reflexivity.
-      simpl. rewrite -H.
-      apply ReflectF.
-      injection. tauto.
-    + by apply ReflectF.
-    + by apply ReflectF.
-    + by apply ReflectT.
-Defined.
-
-Scheme Equality for PTag.
-Scheme Equality for BTag.
-
+Derive Signature for algo_dom.
 (* Fixpoint PTm_eqb {n} (a b : PTm n) := *)
 (*   match a, b with *)
 (*   | VarPTm i, VarPTm j => fin_eq i j *)
@@ -171,7 +181,7 @@ Scheme Equality for BTag.
 (*     destruct IHa1. *)
 (*     destruct a1. *)
 
-Fixpoint hred {n} (a : PTm n) : option (PTm n) :=
+Fixpoint hred (a : PTm) : option (PTm) :=
     match a with
     | VarPTm i => None
     | PAbs a => None
@@ -204,31 +214,31 @@ Fixpoint hred {n} (a : PTm n) : option (PTm n) :=
         end
     end.
 
-Lemma hred_complete n (a b : PTm n) :
+Lemma hred_complete (a b : PTm) :
   HRed.R a b -> hred a = Some b.
 Proof.
   induction 1; hauto lq:on rew:off inv:HRed.R b:on.
 Qed.
 
-Lemma hred_sound n (a b : PTm n):
+Lemma hred_sound (a b : PTm):
   hred a = Some b -> HRed.R a b.
 Proof.
   elim : a b; hauto q:on dep:on ctrs:HRed.R.
 Qed.
 
-Lemma hred_deter n (a b0 b1 : PTm n) :
+Lemma hred_deter (a b0 b1 : PTm) :
   HRed.R a b0 -> HRed.R a b1 -> b0 = b1.
 Proof.
   move /hred_complete => + /hred_complete. congruence.
 Qed.
 
-Definition hred_fancy n (a : PTm n) :
-  relations.nf HRed.R a + {x | HRed.R a x}.
+Definition hred_fancy  (a : PTm) :
+  HRed.nf a + {x | HRed.R a x}.
 Proof.
   destruct (hred a) as [a'|] eqn:eq .
   - right. exists a'. hauto q:on use:hred_sound.
   - left.
-    move => [a' h].
+    move => a' h.
     move /hred_complete in h.
     congruence.
 Defined.
@@ -241,6 +251,8 @@ Ltac check_equal_triv :=
   | _ => idtac
   end.
 
+Scheme Equality for nat. Scheme Equality for PTag.
+Scheme Equality for BTag. Scheme Equality for PTm.
 (* Program Fixpoint check_equal {n} (a b : PTm n) (h : algo_dom a b) {struct h} : bool := *)
 (*   match a, b with *)
 (*   | VarPTm i, VarPTm j => fin_beq i j *)
@@ -255,9 +267,9 @@ Ltac check_equal_triv :=
 (* Next Obligation. *)
 (*   simpl. *)
 
-Equations check_equal {n} (a b : PTm n) (h : algo_dom a b) :
+Equations check_equal (a b : PTm) (h : algo_dom a b) :
   bool by struct h :=
-  check_equal (VarPTm i) (VarPTm j) h := fin_beq i j;
+  check_equal (VarPTm i) (VarPTm j) h := nat_beq i j;
   check_equal (PAbs a) (PAbs b) h := check_equal_r a b ltac:(check_equal_triv);
   check_equal (PAbs a) b h := check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) ltac:(check_equal_triv);
   check_equal a (PAbs b) h := check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b ltac:(check_equal_triv);
@@ -274,26 +286,24 @@ Equations check_equal {n} (a b : PTm n) (h : algo_dom a b) :
   check_equal (PSuc a) (PSuc b) h := check_equal_r a b ltac:(check_equal_triv);
   check_equal (PUniv i) (PUniv j) _ := Nat.eqb i j;
   check_equal a b h := false;
-  with check_equal_r {n} (a b : PTm n) (h : algo_dom_r a b) :
+  with check_equal_r (a b : PTm) (h : algo_dom_r a b) :
   bool by struct h :=
-  check_equal_r a b h with hred_fancy _ a =>
+  check_equal_r a b h with hred_fancy a =>
     { check_equal_r a b h (inr a') := check_equal_r (proj1_sig a') b _;
-      check_equal_r a b h (inl _) with hred_fancy _ b =>
+      check_equal_r a b h (inl _) with hred_fancy b =>
         { check_equal_r a b h (inl _) (inl _) := check_equal a b _;
           check_equal_r a b h (inl _) (inr b') := check_equal_r a (proj1_sig b')  _}} .
 
 
 Next Obligation.
-  move => /= ih ihr n a nfa b nfb.
-  inversion 1; subst=>//=.
+  inversion h; subst=>//=.
   exfalso. sfirstorder.
   exfalso. sfirstorder.
 Defined.
 
 Next Obligation.
   simpl.
-  move => /= ih ihr n a nfa b [b' hb'].
-  inversion 1; subst =>//=.
+  inversion h; subst =>//=.
   exfalso. hauto lq:on use:algo_dom_hf_hne, hf_no_hred, hne_no_hred.
   exfalso. sfirstorder.
   have ? : b' = b'0 by eauto using hred_deter.
@@ -302,8 +312,7 @@ Next Obligation.
 Defined.
 
 Next Obligation.
-  simpl => ih ihr n a [a' ha'] b.
-  inversion 1; subst => //=.
+  inversion h; subst => //=.
   exfalso. hauto lq:on use:algo_dom_hf_hne, hf_no_hred, hne_no_hred.
   suff ? : a'0 = a' by subst; assumption.
   by eauto using hred_deter.