From f402f4e528b61a50cf7f259ef1cedbe6423048cf Mon Sep 17 00:00:00 2001
From: Yiyun Liu <liuyiyun@seas.upenn.edu>
Date: Thu, 3 Apr 2025 16:21:25 -0400
Subject: [PATCH] Fix fp_red

---
 theories/fp_red.v | 654 +++++++++++++++++++++++-----------------------
 1 file changed, 332 insertions(+), 322 deletions(-)

diff --git a/theories/fp_red.v b/theories/fp_red.v
index f9abc08..40b1751 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -211,19 +211,19 @@ Module Par.
 End Par.
 
 Module Pars.
-  Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) :
+  Lemma renaming (a b : PTm) (ξ : nat -> nat) :
     rtc Par.R a b -> rtc Par.R (ren_PTm ξ a) (ren_PTm ξ b).
   Proof.
     induction 1; hauto lq:on ctrs:rtc use:Par.renaming.
   Qed.
 
-  Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) :
+  Lemma substing (a b : PTm) (ρ : nat -> PTm) :
     rtc Par.R a b ->
     rtc Par.R (subst_PTm ρ a) (subst_PTm ρ b).
     induction 1; hauto l:on ctrs:rtc use:Par.substing.
   Qed.
 
-  Lemma antirenaming n m (a : PTm n) (b : PTm m) (ξ : fin n -> fin m) :
+  Lemma antirenaming (a : PTm) (b : PTm) (ξ : nat -> nat) :
     rtc Par.R (ren_PTm ξ a) b -> exists b0, rtc Par.R a b0 /\ ren_PTm ξ b0 = b.
   Proof.
     move E  :(ren_PTm ξ a) => u h.
@@ -243,31 +243,31 @@ Module Pars.
   #[local]Ltac solve_s :=
     repeat (induction 1; last by solve_s_rec); apply rtc_refl.
 
-  Lemma ProjCong n p (a0 a1 : PTm n) :
+  Lemma ProjCong p (a0 a1 : PTm) :
     rtc Par.R a0 a1 ->
     rtc Par.R (PProj p a0) (PProj p a1).
   Proof. solve_s. Qed.
 
-  Lemma PairCong n (a0 a1 b0 b1 : PTm n) :
+  Lemma PairCong (a0 a1 b0 b1 : PTm) :
     rtc Par.R a0 a1 ->
     rtc Par.R b0 b1 ->
     rtc Par.R (PPair a0 b0) (PPair a1 b1).
   Proof. solve_s. Qed.
 
-  Lemma AppCong n (a0 a1 b0 b1 : PTm n) :
+  Lemma AppCong (a0 a1 b0 b1 : PTm) :
     rtc Par.R a0 a1 ->
     rtc Par.R b0 b1 ->
     rtc Par.R (PApp a0 b0) (PApp a1 b1).
   Proof. solve_s. Qed.
 
-  Lemma AbsCong n (a b : PTm (S n)) :
+  Lemma AbsCong (a b : PTm) :
     rtc Par.R a b ->
     rtc Par.R (PAbs a) (PAbs b).
   Proof. solve_s. Qed.
 
 End Pars.
 
-Definition var_or_const {n} (a : PTm n) :=
+Definition var_or_const (a : PTm) :=
   match a with
   | VarPTm _ => true
   | PBot => true
@@ -277,7 +277,7 @@ Definition var_or_const {n} (a : PTm n) :=
 
 (***************** Beta rules only ***********************)
 Module RPar.
-  Inductive R {n} : PTm n -> PTm n ->  Prop :=
+  Inductive R : PTm -> PTm ->  Prop :=
   (***************** Beta ***********************)
   | AppAbs a0 a1 b0 b1 :
     R a0 a1 ->
@@ -320,58 +320,58 @@ Module RPar.
   | Bot :
     R PBot PBot.
 
-  Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop.
+  Derive Dependent Inversion inv with (forall (a b : PTm), R a b) Sort Prop.
 
-  Lemma refl n (a : PTm n) : R a a.
+  Lemma refl (a : PTm) : R a a.
   Proof.
     induction a; hauto lq:on ctrs:R.
   Qed.
 
-  Lemma AppAbs' n a0 a1 (b0 b1 t : PTm n) :
+  Lemma AppAbs' a0 a1 (b0 b1 t : PTm) :
     t = subst_PTm (scons b1 VarPTm) a1 ->
     R a0 a1 ->
     R b0 b1 ->
     R (PApp (PAbs a0) b0) t.
   Proof. move => ->. apply AppAbs. Qed.
 
-  Lemma ProjPair' n p (a0 a1 b0 b1 : PTm n) t :
+  Lemma ProjPair' p (a0 a1 b0 b1 : PTm) t :
     t = (if p is PL then a1 else b1) ->
     R a0 a1 ->
     R b0 b1 ->
     R (PProj p (PPair a0 b0)) t.
   Proof.  move => > ->. apply ProjPair. Qed.
 
-  Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) :
+  Lemma renaming (a b : PTm) (ξ : nat -> nat) :
     R a b -> R (ren_PTm ξ a) (ren_PTm ξ b).
   Proof.
-    move => h. move : m ξ.
-    elim : n a b /h.
+    move => h. move : ξ.
+    elim : a b /h.
     move => *; apply : AppAbs'; eauto; by asimpl.
     all : qauto ctrs:R use:ProjPair'.
   Qed.
 
-  Lemma morphing_ren n m p (ρ0 ρ1 : fin n -> PTm m) (ξ : fin m -> fin p) :
+  Lemma morphing_ren (ρ0 ρ1 : nat -> PTm) (ξ : nat -> nat) :
     (forall i, R (ρ0 i) (ρ1 i)) ->
     (forall i, R ((funcomp (ren_PTm ξ) ρ0) i) ((funcomp (ren_PTm ξ) ρ1) i)).
   Proof. eauto using renaming. Qed.
 
-  Lemma morphing_ext n m (ρ0 ρ1 : fin n -> PTm m) a b  :
+  Lemma morphing_ext (ρ0 ρ1 : nat -> PTm) a b  :
     R a b ->
     (forall i, R (ρ0 i) (ρ1 i)) ->
     (forall i, R ((scons a ρ0) i) ((scons b ρ1) i)).
   Proof. hauto q:on inv:nat. Qed.
 
-  Lemma morphing_up n m (ρ0 ρ1 : fin n -> PTm m) :
+  Lemma morphing_up (ρ0 ρ1 : nat -> PTm) :
     (forall i, R (ρ0 i) (ρ1 i)) ->
     (forall i, R (up_PTm_PTm ρ0 i) (up_PTm_PTm ρ1 i)).
   Proof. hauto l:on ctrs:R use:morphing_ext, morphing_ren unfold:up_PTm_PTm. Qed.
 
-  Lemma morphing n m (a b : PTm n) (ρ0 ρ1 : fin n -> PTm m) :
+  Lemma morphing (a b : PTm) (ρ0 ρ1 : nat -> PTm) :
     (forall i, R (ρ0 i) (ρ1 i)) ->
     R a b -> R (subst_PTm ρ0 a) (subst_PTm ρ1 b).
   Proof.
-    move => + h. move : m ρ0 ρ1.
-    elim : n a b /h.
+    move => + h. move : ρ0 ρ1.
+    elim : a b /h.
     - move => *.
       apply : AppAbs'; eauto using morphing_up.
       by asimpl.
@@ -388,49 +388,51 @@ Module RPar.
     - hauto lq:on ctrs:R.
   Qed.
 
-  Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) :
+  Lemma substing (a b : PTm) (ρ : nat -> PTm) :
     R a b ->
     R (subst_PTm ρ a) (subst_PTm ρ b).
   Proof. hauto l:on use:morphing, refl. Qed.
 
-  Lemma cong n (a b : PTm (S n)) c d :
+  Lemma cong (a b : PTm) c d :
     R a b ->
     R c d ->
     R (subst_PTm (scons c VarPTm) a) (subst_PTm (scons d VarPTm) b).
   Proof.
     move => h0 h1. apply morphing => //=.
-    qauto l:on ctrs:R inv:nat.
+    destruct i as [|i].
+    - done.
+    - simpl. apply Var.
   Qed.
 
-  Lemma var_or_const_imp {n} (a b : PTm n) :
+  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 n m (ρ : fin n -> PTm m) :
+  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|].
+    move => h /= [|i].
+    - sfirstorder.
     - asimpl.
       move /(_ i) in h.
       rewrite /funcomp.
       move : (ρ i) h.
       case => //=.
-    - sfirstorder.
   Qed.
 
   Local Ltac antiimp := qauto l:on use:var_or_const_imp.
 
-  Lemma antirenaming n m (a : PTm n) (b : PTm m) (ρ : fin n -> PTm m) :
+  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.
   Proof.
     move E : (subst_PTm ρ a) => u hρ h.
-    move : n ρ hρ a E. elim : m u b/h.
-    - move => n a0 a1 b0 b1 ha iha hb ihb m ρ 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.
@@ -445,7 +447,7 @@ Module RPar.
       eexists. split.
       apply AppAbs; eauto.
       by asimpl.
-    - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ρ hρ.
+    - move => a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc ρ hρ.
       move => []//=;
                first by antiimp.
       move => []//=; first by antiimp.
@@ -460,13 +462,13 @@ Module RPar.
       eexists. split.
       apply AppPair; hauto. subst.
       by asimpl.
-    - move => n p a0 a1 ha iha m ρ hρ []//=;
+    - 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.
       spec_refl. move : iha => [b0 [? ?]]. subst.
       eexists. split. apply ProjAbs; eauto. by asimpl.
-    - move => n p a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=;
+    - move => p a0 a1 b0 b1 ha iha hb ihb ρ hρ []//=;
                first by antiimp.
       move => p0 []//=; first by antiimp. move => t t0[*].
       subst.
@@ -477,16 +479,16 @@ Module RPar.
       move : ihb => [c0 [? ?]]. subst.
       eexists. split. by eauto using ProjPair.
       hauto q:on.
-    - move => n i m ρ hρ []//=.
+    - move => i ρ hρ []//=.
       hauto l:on.
-    - move => n a0 a1 ha iha m ρ hρ []//=; first by antiimp.
+    - 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 => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=;
+    - move => a0 a1 b0 b1 ha iha hb ihb ρ hρ []//=;
                first by antiimp.
       move => t t0 [*]. subst.
       have {}/iha := (hρ) => iha.
@@ -496,7 +498,7 @@ Module RPar.
       move : ihb => [c0 [? ?]]. subst.
       eexists. split. by apply AppCong; eauto.
       done.
-    - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=;
+    - move => a0 a1 b0 b1 ha iha hb ihb ρ hρ []//=;
                first by antiimp.
       move => t t0[*]. subst.
       have {}/iha := (hρ) => iha.
@@ -506,7 +508,7 @@ Module RPar.
       move : ihb => [c0 [? ?]]. subst.
       eexists. split. by apply PairCong; eauto.
       by asimpl.
-    - move => n p a0 a1 ha iha m ρ hρ []//=;
+    - move => p a0 a1 ha iha ρ hρ []//=;
                first by antiimp.
       move => p0 t [*]. subst.
       have {}/iha := (hρ) => iha.
@@ -521,7 +523,7 @@ End RPar.
 
 (***************** Beta rules only ***********************)
 Module RPar'.
-  Inductive R {n} : PTm n -> PTm n ->  Prop :=
+  Inductive R : PTm -> PTm ->  Prop :=
   (***************** Beta ***********************)
   | AppAbs a0 a1 b0 b1 :
     R a0 a1 ->
@@ -556,58 +558,58 @@ Module RPar'.
   | BotCong :
     R PBot PBot.
 
-  Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop.
+  Derive Inversion inv with (forall (a b : PTm), R a b) Sort Prop.
 
-  Lemma refl n (a : PTm n) : R a a.
+  Lemma refl (a : PTm) : R a a.
   Proof.
     induction a; hauto lq:on ctrs:R.
   Qed.
 
-  Lemma AppAbs' n a0 a1 (b0 b1 t : PTm n) :
+  Lemma AppAbs' a0 a1 (b0 b1 t : PTm) :
     t = subst_PTm (scons b1 VarPTm) a1 ->
     R a0 a1 ->
     R b0 b1 ->
     R (PApp (PAbs a0) b0) t.
   Proof. move => ->. apply AppAbs. Qed.
 
-  Lemma ProjPair' n p (a0 a1 b0 b1 : PTm n) t :
+  Lemma ProjPair' p (a0 a1 b0 b1 : PTm) t :
     t = (if p is PL then a1 else b1) ->
     R a0 a1 ->
     R b0 b1 ->
     R (PProj p (PPair a0 b0)) t.
   Proof.  move => > ->. apply ProjPair. Qed.
 
-  Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) :
+  Lemma renaming  (a b : PTm) (ξ : nat -> nat) :
     R a b -> R (ren_PTm ξ a) (ren_PTm ξ b).
   Proof.
-    move => h. move : m ξ.
-    elim : n a b /h.
+    move => h. move : ξ.
+    elim : a b /h.
     move => *; apply : AppAbs'; eauto; by asimpl.
     all : qauto ctrs:R use:ProjPair'.
   Qed.
 
-  Lemma morphing_ren n m p (ρ0 ρ1 : fin n -> PTm m) (ξ : fin m -> fin p) :
+  Lemma morphing_ren (ρ0 ρ1 : nat -> PTm) (ξ : nat -> nat) :
     (forall i, R (ρ0 i) (ρ1 i)) ->
     (forall i, R ((funcomp (ren_PTm ξ) ρ0) i) ((funcomp (ren_PTm ξ) ρ1) i)).
   Proof. eauto using renaming. Qed.
 
-  Lemma morphing_ext n m (ρ0 ρ1 : fin n -> PTm m) a b  :
+  Lemma morphing_ext (ρ0 ρ1 : nat -> PTm) a b  :
     R a b ->
     (forall i, R (ρ0 i) (ρ1 i)) ->
     (forall i, R ((scons a ρ0) i) ((scons b ρ1) i)).
   Proof. hauto q:on inv:nat. Qed.
 
-  Lemma morphing_up n m (ρ0 ρ1 : fin n -> PTm m) :
+  Lemma morphing_up (ρ0 ρ1 : nat -> PTm) :
     (forall i, R (ρ0 i) (ρ1 i)) ->
     (forall i, R (up_PTm_PTm ρ0 i) (up_PTm_PTm ρ1 i)).
   Proof. hauto l:on ctrs:R use:morphing_ext, morphing_ren unfold:up_PTm_PTm. Qed.
 
-  Lemma morphing n m (a b : PTm n) (ρ0 ρ1 : fin n -> PTm m) :
+  Lemma morphing  (a b : PTm) (ρ0 ρ1 : nat -> PTm) :
     (forall i, R (ρ0 i) (ρ1 i)) ->
     R a b -> R (subst_PTm ρ0 a) (subst_PTm ρ1 b).
   Proof.
-    move => + h. move : m ρ0 ρ1.
-    elim : n a b /h.
+    move => + h. move : ρ0 ρ1.
+    elim : a b /h.
     - move => *.
       apply : AppAbs'; eauto using morphing_up.
       by asimpl.
@@ -622,49 +624,49 @@ Module RPar'.
     - hauto lq:on ctrs:R.
   Qed.
 
-  Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) :
+  Lemma substing (a b : PTm) (ρ : nat -> PTm) :
     R a b ->
     R (subst_PTm ρ a) (subst_PTm ρ b).
   Proof. hauto l:on use:morphing, refl. Qed.
 
-  Lemma cong n (a b : PTm (S n)) c d :
+  Lemma cong (a b : PTm) c d :
     R a b ->
     R c d ->
     R (subst_PTm (scons c VarPTm) a) (subst_PTm (scons d VarPTm) b).
   Proof.
     move => h0 h1. apply morphing => //=.
-    qauto l:on ctrs:R inv:nat.
+    hauto l:on ctrs:R inv:nat.
   Qed.
 
-  Lemma var_or_const_imp {n} (a b : PTm n) :
+  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 n m (ρ : fin n -> PTm m) :
+  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|].
+    move => h /= [|i].
+    - sfirstorder.
     - asimpl.
       move /(_ i) in h.
       rewrite /funcomp.
       move : (ρ i) h.
       case => //=.
-    - sfirstorder.
   Qed.
 
   Local Ltac antiimp := qauto l:on use:var_or_const_imp.
 
-  Lemma antirenaming n m (a : PTm n) (b : PTm m) (ρ : fin n -> PTm m) :
+  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.
   Proof.
     move E : (subst_PTm ρ a) => u hρ h.
-    move : n ρ hρ a E. elim : m u b/h.
-    - move => n a0 a1 b0 b1 ha iha hb ihb m ρ 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.
@@ -679,7 +681,7 @@ Module RPar'.
       eexists. split.
       apply AppAbs; eauto.
       by asimpl.
-    - move => n p a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=;
+    - move => p a0 a1 b0 b1 ha iha hb ihb ρ hρ []//=;
                first by antiimp.
       move => p0 []//=; first by antiimp. move => t t0[*].
       subst.
@@ -690,16 +692,16 @@ Module RPar'.
       move : ihb => [c0 [? ?]]. subst.
       eexists. split. by eauto using ProjPair.
       hauto q:on.
-    - move => n i m ρ hρ []//=.
+    - move => i ρ hρ []//=.
       hauto l:on.
-    - move => n a0 a1 ha iha m ρ hρ []//=; first by antiimp.
+    - 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 => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=;
+    - move => a0 a1 b0 b1 ha iha hb ihb ρ hρ []//=;
                first by antiimp.
       move => t t0 [*]. subst.
       have {}/iha := (hρ) => iha.
@@ -709,7 +711,7 @@ Module RPar'.
       move : ihb => [c0 [? ?]]. subst.
       eexists. split. by apply AppCong; eauto.
       done.
-    - move => n a0 a1 b0 b1 ha iha hb ihb m ρ hρ []//=;
+    - move => a0 a1 b0 b1 ha iha hb ihb ρ hρ []//=;
                first by antiimp.
       move => t t0[*]. subst.
       have {}/iha := (hρ) => iha.
@@ -719,7 +721,7 @@ Module RPar'.
       move : ihb => [c0 [? ?]]. subst.
       eexists. split. by apply PairCong; eauto.
       by asimpl.
-    - move => n p a0 a1 ha iha m ρ hρ []//=;
+    - move => p a0 a1 ha iha ρ hρ []//=;
                first by antiimp.
       move => p0 t [*]. subst.
       have {}/iha := (hρ) => iha.
@@ -727,14 +729,14 @@ Module RPar'.
       move : iha => [b0 [? ?]]. subst.
       eexists. split. apply ProjCong; eauto. reflexivity.
     - hauto q:on ctrs:R inv:PTm.
-    - move => n i n0 ρ hρ []//=; first by antiimp.
+    - move => i ρ hρ []//=; first by antiimp.
       hauto l:on.
     - hauto q:on inv:PTm ctrs:R.
   Qed.
 End RPar'.
 
 Module ERed.
-  Inductive R {n} : PTm n -> PTm n ->  Prop :=
+  Inductive R : PTm -> PTm ->  Prop :=
   (****************** Eta ***********************)
   | AppEta a :
     R a (PAbs (PApp (ren_PTm shift a) (VarPTm var_zero)))
@@ -761,30 +763,30 @@ Module ERed.
     R a0 a1 ->
     R (PProj p a0) (PProj p a1).
 
-  Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop.
+  Derive Inversion inv with (forall (a b : PTm), R a b) Sort Prop.
 
-  Lemma AppEta' n a (u : PTm n) :
+  Lemma AppEta' a (u : PTm) :
     u = (PAbs (PApp (ren_PTm shift a) (VarPTm var_zero))) ->
     R a u.
   Proof. move => ->. apply AppEta. Qed.
 
-  Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) :
+  Lemma renaming (a b : PTm) (ξ : nat -> nat) :
     R a b -> R (ren_PTm ξ a) (ren_PTm ξ b).
   Proof.
-    move => h. move : m ξ.
-    elim : n a b /h.
+    move => h. move : ξ.
+    elim : a b /h.
 
-    move => n a m ξ.
+    move => a ξ.
     apply AppEta'. by asimpl.
     all : qauto ctrs:R.
   Qed.
 
-  Lemma substing n m (a : PTm n) b (ρ : fin n -> PTm m) :
+  Lemma substing (a : PTm) b (ρ : nat -> PTm) :
     R a b ->
     R (subst_PTm ρ a) (subst_PTm ρ b).
   Proof.
-    move => h. move : m ρ. elim : n a b / h => n.
-    move => a m ρ /=.
+    move => h. move : ρ. elim : a b / h.
+    move => a ρ /=.
     apply : AppEta'; eauto. by asimpl.
     all : hauto ctrs:R inv:nat use:renaming.
   Qed.
@@ -800,31 +802,31 @@ Module EReds.
   #[local]Ltac solve_s :=
     repeat (induction 1; last by solve_s_rec); apply rtc_refl.
 
-  Lemma AbsCong n (a b : PTm (S n)) :
+  Lemma AbsCong (a b : PTm) :
     rtc ERed.R a b ->
     rtc ERed.R (PAbs a) (PAbs b).
   Proof. solve_s. Qed.
 
-  Lemma AppCong n (a0 a1 b0 b1 : PTm n) :
+  Lemma AppCong (a0 a1 b0 b1 : PTm) :
     rtc ERed.R a0 a1 ->
     rtc ERed.R b0 b1 ->
     rtc ERed.R (PApp a0 b0) (PApp a1 b1).
   Proof. solve_s. Qed.
 
-  Lemma PairCong n (a0 a1 b0 b1 : PTm n) :
+  Lemma PairCong (a0 a1 b0 b1 : PTm) :
     rtc ERed.R a0 a1 ->
     rtc ERed.R b0 b1 ->
     rtc ERed.R (PPair a0 b0) (PPair a1 b1).
   Proof. solve_s. Qed.
 
-  Lemma ProjCong n p (a0 a1  : PTm n) :
+  Lemma ProjCong p (a0 a1  : PTm) :
     rtc ERed.R a0 a1 ->
     rtc ERed.R (PProj p a0) (PProj p a1).
   Proof. solve_s. Qed.
 End EReds.
 
 Module EPar.
-  Inductive R {n} : PTm n -> PTm n ->  Prop :=
+  Inductive R : PTm -> PTm ->  Prop :=
   (****************** Eta ***********************)
   | AppEta a0 a1 :
     R a0 a1 ->
@@ -856,39 +858,39 @@ Module EPar.
   | BotCong :
     R PBot PBot.
 
-  Lemma refl n (a : PTm n) : EPar.R a a.
+  Lemma refl (a : PTm) : EPar.R a a.
   Proof.
     induction a; hauto lq:on ctrs:EPar.R.
   Qed.
 
-  Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) :
+  Lemma renaming (a b : PTm) (ξ : nat -> nat) :
     R a b -> R (ren_PTm ξ a) (ren_PTm ξ b).
   Proof.
-    move => h. move : m ξ.
-    elim : n a b /h.
+    move => h. move : ξ.
+    elim : a b /h.
 
-    move => n a0 a1 ha iha m ξ /=.
-    move /(_ _ ξ) /AppEta : iha.
+    move => a0 a1 ha iha ξ /=.
+    move /(_ ξ) /AppEta : iha.
     by asimpl.
 
     all : qauto ctrs:R.
   Qed.
 
-  Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop.
+  Derive Inversion inv with (forall (a b : PTm), R a b) Sort Prop.
 
-  Lemma AppEta' n (a0 a1 b : PTm n) :
+  Lemma AppEta' (a0 a1 b : PTm) :
     b = (PAbs (PApp (ren_PTm shift a1) (VarPTm var_zero))) ->
     R a0 a1 ->
     R a0 b.
   Proof. move => ->; apply AppEta. Qed.
 
-  Lemma morphing n m (a b : PTm n) (ρ0 ρ1 : fin n -> PTm m) :
+  Lemma morphing (a b : PTm) (ρ0 ρ1 : nat -> PTm) :
     R a b ->
     (forall i, R (ρ0 i) (ρ1 i)) ->
     R (subst_PTm ρ0 a) (subst_PTm ρ1 b).
   Proof.
-    move => h. move : m ρ0 ρ1. elim : n a b / h => n.
-    - move => a0 a1 ha iha m ρ0 ρ1 hρ /=.
+    move => h. move : ρ0 ρ1. elim : a b / h.
+    - move => a0 a1 ha iha ρ0 ρ1 hρ /=.
       apply : AppEta'; eauto. by asimpl.
     - hauto lq:on ctrs:R.
     - hauto lq:on ctrs:R.
@@ -901,7 +903,7 @@ Module EPar.
     - hauto lq:on ctrs:R.
   Qed.
 
-  Lemma substing n a0 a1 (b0 b1 : PTm n) :
+  Lemma substing a0 a1 (b0 b1 : PTm) :
     R a0 a1 ->
     R b0 b1 ->
     R (subst_PTm (scons b0 VarPTm) a0) (subst_PTm (scons b1 VarPTm) a1).
@@ -914,14 +916,14 @@ End EPar.
 
 
 Module OExp.
-  Inductive R {n} : PTm n -> PTm n ->  Prop :=
+  Inductive R : PTm -> PTm ->  Prop :=
   (****************** Eta ***********************)
   | AppEta a :
     R a (PAbs (PApp (ren_PTm shift a) (VarPTm var_zero)))
   | PairEta a :
     R a (PPair (PProj PL a) (PProj PR a)).
 
-  Lemma merge n (t a b : PTm n) :
+  Lemma merge (t a b : PTm) :
     rtc R a b ->
     EPar.R t a ->
     EPar.R t b.
@@ -931,7 +933,7 @@ Module OExp.
     - hauto q:on ctrs:EPar.R inv:R.
   Qed.
 
-  Lemma commutativity n (a b c : PTm n) :
+  Lemma commutativity (a b c : PTm) :
     EPar.R a b -> R a c -> exists d, R b d /\ EPar.R c d.
   Proof.
     move => h.
@@ -940,7 +942,7 @@ Module OExp.
     - hauto lq:on ctrs:EPar.R, R.
   Qed.
 
-  Lemma commutativity0 n (a b c : PTm n) :
+  Lemma commutativity0 (a b c : PTm) :
     EPar.R a b -> rtc R a c -> exists d, rtc R b d /\ EPar.R c d.
   Proof.
     move => + h. move : b.
@@ -965,29 +967,29 @@ Module RPars.
   #[local]Ltac solve_s :=
     repeat (induction 1; last by solve_s_rec); apply rtc_refl.
 
-  Lemma AbsCong n (a b : PTm (S n)) :
+  Lemma AbsCong (a b : PTm) :
     rtc RPar.R a b ->
     rtc RPar.R (PAbs a) (PAbs b).
   Proof. solve_s. Qed.
 
-  Lemma AppCong n (a0 a1 b0 b1 : PTm n) :
+  Lemma AppCong (a0 a1 b0 b1 : PTm) :
     rtc RPar.R a0 a1 ->
     rtc RPar.R b0 b1 ->
     rtc RPar.R (PApp a0 b0) (PApp a1 b1).
   Proof. solve_s. Qed.
 
-  Lemma PairCong n (a0 a1 b0 b1 : PTm n) :
+  Lemma PairCong (a0 a1 b0 b1 : PTm) :
     rtc RPar.R a0 a1 ->
     rtc RPar.R b0 b1 ->
     rtc RPar.R (PPair a0 b0) (PPair a1 b1).
   Proof. solve_s. Qed.
 
-  Lemma ProjCong n p (a0 a1  : PTm n) :
+  Lemma ProjCong p (a0 a1  : PTm) :
     rtc RPar.R a0 a1 ->
     rtc RPar.R (PProj p a0) (PProj p a1).
   Proof. solve_s. Qed.
 
-  Lemma renaming n (a0 a1 : PTm n) m (ξ : fin n -> fin m) :
+  Lemma renaming (a0 a1 : PTm) (ξ : nat -> nat) :
     rtc RPar.R a0 a1 ->
     rtc RPar.R (ren_PTm ξ a0) (ren_PTm ξ a1).
   Proof.
@@ -996,12 +998,12 @@ Module RPars.
     - eauto using RPar.renaming, rtc_l.
   Qed.
 
-  Lemma weakening n (a0 a1 : PTm n) :
+  Lemma weakening (a0 a1 : PTm) :
     rtc RPar.R a0 a1 ->
     rtc RPar.R (ren_PTm shift a0) (ren_PTm shift a1).
   Proof. apply renaming. Qed.
 
-  Lemma Abs_inv n (a : PTm (S n)) b :
+  Lemma Abs_inv (a : PTm) b :
     rtc RPar.R (PAbs a) b -> exists a', b = PAbs a' /\ rtc RPar.R a a'.
   Proof.
     move E : (PAbs a) => b0 h. move : a E.
@@ -1010,17 +1012,17 @@ Module RPars.
     - hauto lq:on ctrs:rtc inv:RPar.R, rtc.
   Qed.
 
-  Lemma morphing n m (a b : PTm n) (ρ : fin n -> PTm m) :
+  Lemma morphing (a b : PTm) (ρ : nat -> PTm) :
     rtc RPar.R a b ->
     rtc RPar.R (subst_PTm ρ a) (subst_PTm ρ b).
   Proof. induction 1; qauto l:on ctrs:rtc use:RPar.substing. Qed.
 
-  Lemma substing n (a b : PTm (S n)) c :
+  Lemma substing (a b : PTm) c :
     rtc RPar.R a b ->
     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 n m (a : PTm n) (b : PTm m) (ρ : fin n -> PTm m) :
+  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.
   Proof.
@@ -1046,29 +1048,29 @@ Module RPars'.
   #[local]Ltac solve_s :=
     repeat (induction 1; last by solve_s_rec); apply rtc_refl.
 
-  Lemma AbsCong n (a b : PTm (S n)) :
+  Lemma AbsCong (a b : PTm) :
     rtc RPar'.R a b ->
     rtc RPar'.R (PAbs a) (PAbs b).
   Proof. solve_s. Qed.
 
-  Lemma AppCong n (a0 a1 b0 b1 : PTm n) :
+  Lemma AppCong (a0 a1 b0 b1 : PTm) :
     rtc RPar'.R a0 a1 ->
     rtc RPar'.R b0 b1 ->
     rtc RPar'.R (PApp a0 b0) (PApp a1 b1).
   Proof. solve_s. Qed.
 
-  Lemma PairCong n (a0 a1 b0 b1 : PTm n) :
+  Lemma PairCong (a0 a1 b0 b1 : PTm) :
     rtc RPar'.R a0 a1 ->
     rtc RPar'.R b0 b1 ->
     rtc RPar'.R (PPair a0 b0) (PPair a1 b1).
   Proof. solve_s. Qed.
 
-  Lemma ProjCong n p (a0 a1  : PTm n) :
+  Lemma ProjCong p (a0 a1  : PTm) :
     rtc RPar'.R a0 a1 ->
     rtc RPar'.R (PProj p a0) (PProj p a1).
   Proof. solve_s. Qed.
 
-  Lemma renaming n (a0 a1 : PTm n) m (ξ : fin n -> fin m) :
+  Lemma renaming (a0 a1 : PTm) (ξ : nat -> nat) :
     rtc RPar'.R a0 a1 ->
     rtc RPar'.R (ren_PTm ξ a0) (ren_PTm ξ a1).
   Proof.
@@ -1077,12 +1079,12 @@ Module RPars'.
     - eauto using RPar'.renaming, rtc_l.
   Qed.
 
-  Lemma weakening n (a0 a1 : PTm n) :
+  Lemma weakening (a0 a1 : PTm) :
     rtc RPar'.R a0 a1 ->
     rtc RPar'.R (ren_PTm shift a0) (ren_PTm shift a1).
   Proof. apply renaming. Qed.
 
-  Lemma Abs_inv n (a : PTm (S n)) b :
+  Lemma Abs_inv (a : PTm) b :
     rtc RPar'.R (PAbs a) b -> exists a', b = PAbs a' /\ rtc RPar'.R a a'.
   Proof.
     move E : (PAbs a) => b0 h. move : a E.
@@ -1091,17 +1093,17 @@ Module RPars'.
     - hauto lq:on ctrs:rtc inv:RPar'.R, rtc.
   Qed.
 
-  Lemma morphing n m (a b : PTm n) (ρ : fin n -> PTm m) :
+  Lemma morphing (a b : PTm) (ρ : nat -> PTm) :
     rtc RPar'.R a b ->
     rtc RPar'.R (subst_PTm ρ a) (subst_PTm ρ b).
   Proof. induction 1; qauto l:on ctrs:rtc use:RPar'.substing. Qed.
 
-  Lemma substing n (a b : PTm (S n)) c :
+  Lemma substing (a b : PTm ) c :
     rtc RPar'.R a b ->
     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 n m (a : PTm n) (b : PTm m) (ρ : fin n -> PTm m) :
+  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.
   Proof.
@@ -1118,7 +1120,16 @@ Module RPars'.
 
 End RPars'.
 
-Lemma Abs_EPar n a (b : PTm n) :
+Lemma subst_id: forall d : PTm, subst_PTm (scons (VarPTm 0) (funcomp VarPTm shift)) d = d.
+Proof.
+  intros d.
+  have h : d = subst_PTm VarPTm d by asimpl.
+  rewrite {2}h.
+  apply ext_PTm.
+  destruct x => //=.
+Qed.
+
+Lemma Abs_EPar a (b : PTm) :
   EPar.R (PAbs a) b ->
   (exists d, EPar.R a d /\
      rtc RPar.R (PApp (ren_PTm shift b) (VarPTm var_zero)) d) /\
@@ -1128,8 +1139,8 @@ Lemma Abs_EPar n a (b : PTm n) :
 Proof.
   move E : (PAbs a) => u h.
   move : a E.
-  elim : n u b /h => //=.
-  - move => n a0 a1 ha iha b ?. subst.
+  elim : u b /h => //=.
+  - move => a0 a1 ha iha b ?. subst.
     specialize iha with (1 := eq_refl).
     move : iha => [[d [ih0 ih1]] _].
     split; exists d.
@@ -1144,7 +1155,7 @@ Proof.
       apply : RPar.ProjAbs.
       by apply RPar.refl.
       eauto using RPars.ProjCong, RPars.AbsCong.
-  - move => n ? a1 ha iha a0 ?. subst. specialize iha with (1 := eq_refl).
+  - move => ? a1 ha iha a0 ?. subst. specialize iha with (1 := eq_refl).
     move : iha => [_ [d [ih0 ih1]]].
     split.
     + exists (PPair (PProj PL d) (PProj PR d)).
@@ -1158,19 +1169,20 @@ Proof.
       by eauto using RPars.AppCong, rtc_refl.
       apply relations.rtc_once => /=.
       apply : RPar.AppAbs'; eauto using RPar.refl.
-      by asimpl.
+      simpl. f_equal. asimpl. clear.
+      by rewrite subst_id.
     + exists d. repeat split => //. move => p.
       apply : rtc_l; eauto.
       hauto q:on use:RPar.ProjPair', RPar.refl.
-  - move => n a0 a1 ha _ ? [*]. subst.
+  - move => a0 a1 ha _ ? [*]. subst.
     split.
     + exists a1. split => //.
-      apply rtc_once. apply : RPar.AppAbs'; eauto using RPar.refl. by asimpl.
+      apply rtc_once. apply : RPar.AppAbs'; eauto using RPar.refl. by asimpl; rewrite subst_id.
     + exists a1. split => // p.
       apply rtc_once. apply : RPar.ProjAbs; eauto using RPar.refl.
 Qed.
 
-Lemma Pair_EPar n (a b c : PTm n) :
+Lemma Pair_EPar (a b c : PTm) :
   EPar.R (PPair a b) c ->
   (forall p, exists d, rtc RPar.R (PProj p c) d /\ EPar.R (if p is PL then a else b) d) /\
     (exists d0 d1, rtc RPar.R (PApp (ren_PTm shift c) (VarPTm var_zero))
@@ -1178,8 +1190,8 @@ Lemma Pair_EPar n (a b c : PTm n) :
     EPar.R a d0 /\ EPar.R b d1).
 Proof.
   move E : (PPair a b) => u h. move : a b E.
-  elim : n u c /h => //=.
-  - move => n a0 a1 ha iha a b ?. subst.
+  elim : u c /h => //=.
+  - move => a0 a1 ha iha a b ?. subst.
     specialize iha with (1 := eq_refl).
     move : iha => [_ [d0 [d1 [ih0 [ih1 ih2]]]]].
     split.
@@ -1196,7 +1208,7 @@ Proof.
       repeat split => //.
       apply : rtc_l. apply : RPar.AppAbs'; eauto using RPar.refl => //=.
       by asimpl; renamify.
-  - move => n a0 a1 ha iha a b ?. subst. specialize iha with (1 := eq_refl).
+  - move => a0 a1 ha iha a b ?. subst. specialize iha with (1 := eq_refl).
     split => [p|].
     + move : iha => [/(_ p) [d [ih0 ih1]] _].
       exists d. split=>//.
@@ -1211,7 +1223,7 @@ Proof.
       repeat split => //=.
       apply : rtc_l. apply RPar.AppPair; eauto using RPar.refl.
       apply RPars.PairCong; apply RPars.AppCong; eauto using rtc_refl.
-  - move => n a0 a1 b0 b1 ha _ hb _ a b [*]. subst.
+  - move => a0 a1 b0 b1 ha _ hb _ a b [*]. subst.
     split.
     + move => p.
       exists (if p is PL then a1 else b1).
@@ -1223,30 +1235,30 @@ Proof.
       split => //.
 Qed.
 
-Lemma commutativity0 n (a b0 b1 : PTm n) :
+Lemma commutativity0 (a b0 b1 : PTm) :
   EPar.R a b0 -> RPar.R a b1 -> exists c, rtc RPar.R b0 c /\ EPar.R b1 c.
 Proof.
   move => h. move : b1.
-  elim : n a b0 / h.
-  - move => n a b0 ha iha b1 hb.
+  elim : a b0 / h.
+  - move => a b0 ha iha b1 hb.
     move : iha (hb) => /[apply].
     move => [c [ih0 ih1]].
     exists (PAbs (PApp (ren_PTm shift c) (VarPTm var_zero))).
     split.
     + hauto lq:on ctrs:rtc use:RPars.AbsCong, RPars.AppCong, RPars.renaming.
     + hauto lq:on ctrs:EPar.R use:EPar.refl, EPar.renaming.
-  - move => n a b0 hb0 ihb0 b1 /[dup] hb1 {}/ihb0.
+  - move => a b0 hb0 ihb0 b1 /[dup] hb1 {}/ihb0.
     move => [c [ih0 ih1]].
     exists (PPair (PProj PL c) (PProj PR c)). split.
     + apply RPars.PairCong;
       by apply RPars.ProjCong.
     + hauto lq:on ctrs:EPar.R use:EPar.refl, EPar.renaming.
   - hauto l:on ctrs:rtc inv:RPar.R.
-  - move => n a0 a1 h ih b1.
+  - move => a0 a1 h ih b1.
     elim /RPar.inv => //= _.
     move => a2 a3 ? [*]. subst.
     hauto lq:on ctrs:rtc, RPar.R, EPar.R use:RPars.AbsCong.
-  - move => n a0 a1 b0 b1 ha iha hb ihb b2.
+  - move => a0 a1 b0 b1 ha iha hb ihb b2.
     elim /RPar.inv => //= _.
     + move =>  a2 a3 b3 b4 h0 h1 [*]. subst.
       move /(_ _ ltac:(by eauto)) : ihb => [b [ihb0 ihb1]].
@@ -1274,7 +1286,7 @@ Proof.
       apply EPar.PairCong; by apply EPar.AppCong.
     + hauto lq:on ctrs:EPar.R use:RPars.AppCong.
   - hauto lq:on ctrs:EPar.R inv:RPar.R use:RPars.PairCong.
-  - move => n p a b0 h0 ih0 b1.
+  - move => p a b0 h0 ih0 b1.
     elim /RPar.inv => //= _.
     + move => ? a0 a1 h [*]. subst.
       move /(_ _ ltac:(by eauto using RPar.AbsCong)) : ih0 => [c [ih0 ih1]].
@@ -1292,7 +1304,7 @@ Proof.
   - hauto l:on ctrs:EPar.R inv:RPar.R.
 Qed.
 
-Lemma commutativity1 n (a b0 b1 : PTm n) :
+Lemma commutativity1 (a b0 b1 : PTm) :
   EPar.R a b0 -> rtc RPar.R a b1 -> exists c, rtc RPar.R b0 c /\ EPar.R b1 c.
 Proof.
   move => + h. move : b0.
@@ -1301,7 +1313,7 @@ Proof.
   - qauto l:on use:relations.rtc_transitive, commutativity0.
 Qed.
 
-Lemma commutativity n (a b0 b1 : PTm n) :
+Lemma commutativity (a b0 b1 : PTm) :
   rtc EPar.R a b0 -> rtc RPar.R a b1 -> exists c, rtc RPar.R b0 c /\ rtc EPar.R b1 c.
   move => h. move : b1. elim : a b0 /h.
   - sfirstorder.
@@ -1310,124 +1322,124 @@ Lemma commutativity n (a b0 b1 : PTm n) :
     hauto q:on ctrs:rtc.
 Qed.
 
-Lemma Abs_EPar' n a (b : PTm n) :
+Lemma Abs_EPar' a (b : PTm) :
   EPar.R (PAbs a) b ->
   (exists d, EPar.R a d /\
           rtc OExp.R (PAbs d) b).
 Proof.
   move E : (PAbs a) => u h.
   move : a E.
-  elim : n u b /h => //=.
-  - move => n a0 a1 ha iha a ?. subst.
+  elim : u b /h => //=.
+  - move => a0 a1 ha iha a ?. subst.
     specialize iha with (1 := eq_refl).
     hauto lq:on ctrs:OExp.R use:rtc_r.
-  - move => n a0 a1 ha iha a ?. subst.
+  - move => a0 a1 ha iha a ?. subst.
     specialize iha with (1 := eq_refl).
     hauto lq:on ctrs:OExp.R use:rtc_r.
   - hauto l:on ctrs:OExp.R.
 Qed.
 
-Lemma Proj_EPar' n p a (b : PTm n) :
+Lemma Proj_EPar' p a (b : PTm) :
   EPar.R (PProj p a) b ->
   (exists d, EPar.R a d /\
           rtc OExp.R (PProj p d) b).
 Proof.
   move E : (PProj p a) => u h.
   move : p a E.
-  elim : n u b /h => //=.
-  - move => n a0 a1 ha iha a p ?. subst.
+  elim : u b /h => //=.
+  - move => a0 a1 ha iha a p ?. subst.
     specialize iha with (1 := eq_refl).
     hauto lq:on ctrs:OExp.R use:rtc_r.
-  - move => n a0 a1 ha iha a p ?. subst.
+  - move => a0 a1 ha iha a p ?. subst.
     specialize iha with (1 := eq_refl).
     hauto lq:on ctrs:OExp.R use:rtc_r.
   - hauto l:on ctrs:OExp.R.
 Qed.
 
-Lemma App_EPar' n (a b u : PTm n)  :
+Lemma App_EPar' (a b u : PTm)  :
   EPar.R (PApp a b) u ->
   (exists a0 b0, EPar.R a a0 /\ EPar.R b b0 /\ rtc OExp.R (PApp a0 b0) u).
 Proof.
   move E : (PApp a b) => t h.
-  move : a b E. elim : n t u /h => //=.
-  - move => n a0 a1 ha iha a b ?. subst.
+  move : a b E. elim : t u /h => //=.
+  - move => a0 a1 ha iha a b ?. subst.
     specialize iha with (1 := eq_refl).
     hauto lq:on ctrs:OExp.R use:rtc_r.
-  - move => n a0 a1 ha iha a b ?. subst.
+  - move => a0 a1 ha iha a b ?. subst.
     specialize iha with (1 := eq_refl).
     hauto lq:on ctrs:OExp.R use:rtc_r.
   - hauto l:on ctrs:OExp.R.
 Qed.
 
-Lemma Pair_EPar' n (a b u : PTm n) :
+Lemma Pair_EPar' (a b u : PTm) :
   EPar.R (PPair a b) u ->
   exists a0 b0, EPar.R a a0 /\ EPar.R b b0 /\ rtc OExp.R (PPair a0 b0) u.
 Proof.
   move E : (PPair a b) => t h.
-  move : a b E. elim : n t u /h => //=.
-  - move => n a0 a1 ha iha a b ?. subst.
+  move : a b E. elim : t u /h => //=.
+  - move => a0 a1 ha iha a b ?. subst.
     specialize iha with (1 := eq_refl).
     hauto lq:on ctrs:OExp.R use:rtc_r.
-  - move => n a0 a1 ha iha a b ?. subst.
+  - move => a0 a1 ha iha a b ?. subst.
     specialize iha with (1 := eq_refl).
     hauto lq:on ctrs:OExp.R use:rtc_r.
   - hauto l:on ctrs:OExp.R.
 Qed.
 
-Lemma Const_EPar' n k (u : PTm n) :
+Lemma Const_EPar' k (u : PTm) :
   EPar.R (PConst k) u ->
   rtc OExp.R (PConst k) u.
   move E : (PConst k) => t h.
-  move : k E. elim : n t u /h => //=.
-  - move => n a0 a1 h ih k ?. subst.
+  move : k E. elim : t u /h => //=.
+  - move => a0 a1 h ih k ?. subst.
     specialize ih with (1 := eq_refl).
     hauto lq:on ctrs:OExp.R use:rtc_r.
-  - move => n a0 a1 h ih k ?. subst.
+  - move => a0 a1 h ih k ?. subst.
     specialize ih with (1 := eq_refl).
     hauto lq:on ctrs:OExp.R use:rtc_r.
   - hauto l:on ctrs:OExp.R.
 Qed.
 
-Lemma Bot_EPar' n (u : PTm n) :
+Lemma Bot_EPar' (u : PTm) :
   EPar.R (PBot) u ->
   rtc OExp.R (PBot) u.
   move E : (PBot) => t h.
-  move : E. elim : n t u /h => //=.
-  - move => n a0 a1 h ih ?. subst.
+  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 => n a0 a1 h ih ?. subst.
+  - 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' n i (u : PTm n) :
+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 : n t u /h => //=.
-  - move => n a0 a1 h ih ?. subst.
+  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 => n a0 a1 h ih ?. subst.
+  - 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 n (c a1 b1 : PTm n) :
+Lemma EPar_diamond (c a1 b1 : PTm) :
   EPar.R c a1 ->
   EPar.R c b1 ->
   exists d2, EPar.R a1 d2 /\ EPar.R b1 d2.
 Proof.
-  move => h. move : b1. elim : n c a1 / h.
-  - move => n c a1 ha iha b1 /iha [d2 [hd0 hd1]].
+  move => h. move : b1. elim : c a1 / h.
+  - move => c a1 ha iha b1 /iha [d2 [hd0 hd1]].
     exists(PAbs (PApp (ren_PTm shift d2) (VarPTm var_zero))).
     hauto lq:on ctrs:EPar.R use:EPar.renaming.
   - hauto lq:on rew:off ctrs:EPar.R.
   - hauto lq:on use:EPar.refl.
-  - move => n a0 a1 ha iha a2.
+  - move => a0 a1 ha iha a2.
     move /Abs_EPar' => [d [hd0 hd1]].
     move : iha hd0; repeat move/[apply].
     move => [d2 [h0 h1]].
@@ -1435,21 +1447,21 @@ Proof.
     move : OExp.commutativity0 hd1; repeat move/[apply].
     move => [d1 [hd1 hd2]].
     exists d1. hauto lq:on ctrs:EPar.R use:OExp.merge.
-  - move => n a0 a1 b0 b1 ha iha hb ihb c.
+  - move => a0 a1 b0 b1 ha iha hb ihb c.
     move /App_EPar' => [a2][b2][/iha [a3 h0]][/ihb [b3 h1]]h2 {iha ihb}.
     have : EPar.R (PApp a2 b2)(PApp a3 b3)
       by hauto l:on use:EPar.AppCong.
     move : OExp.commutativity0 h2; repeat move/[apply].
     move => [d h].
     exists d. hauto lq:on rew:off ctrs:EPar.R use:OExp.merge.
-  - move => n a0 a1 b0 b1 ha iha hb ihb c.
+  - move => a0 a1 b0 b1 ha iha hb ihb c.
     move /Pair_EPar' => [a2][b2][/iha [a3 h0]][/ihb [b3 h1]]h2 {iha ihb}.
     have : EPar.R (PPair a2 b2)(PPair a3 b3)
       by hauto l:on use:EPar.PairCong.
     move : OExp.commutativity0 h2; repeat move/[apply].
     move => [d h].
     exists d. hauto lq:on rew:off ctrs:EPar.R use:OExp.merge.
-  - move => n p a0 a1 ha iha b.
+  - move => p a0 a1 ha iha b.
     move /Proj_EPar' => [d [/iha [d2 h] h1]] {iha}.
     have : EPar.R (PProj p d) (PProj p d2)
       by hauto l:on use:EPar.ProjCong.
@@ -1461,7 +1473,7 @@ Proof.
   - qauto use:Bot_EPar', EPar.refl.
 Qed.
 
-Function tstar {n} (a : PTm n) :=
+Function tstar (a : PTm) :=
   match a with
   | VarPTm i => a
   | PAbs a => PAbs (tstar a)
@@ -1478,9 +1490,9 @@ Function tstar {n} (a : PTm n) :=
   | PBot => PBot
   end.
 
-Lemma RPar_triangle n (a : PTm n) : forall b, RPar.R a b -> RPar.R b (tstar a).
+Lemma RPar_triangle (a : PTm) : forall b, RPar.R a b -> RPar.R b (tstar a).
 Proof.
-  apply tstar_ind => {n a}.
+  apply tstar_ind => {a}.
   - hauto lq:on inv:RPar.R ctrs:RPar.R.
   - hauto lq:on inv:RPar.R ctrs:RPar.R.
   - hauto lq:on use:RPar.cong, RPar.refl ctrs:RPar.R inv:RPar.R.
@@ -1496,7 +1508,7 @@ Proof.
   - hauto lq:on inv:RPar.R ctrs:RPar.R.
 Qed.
 
-Function tstar' {n} (a : PTm n) :=
+Function tstar' (a : PTm) :=
   match a with
   | VarPTm i => a
   | PAbs a => PAbs (tstar' a)
@@ -1510,9 +1522,9 @@ Function tstar' {n} (a : PTm n) :=
   | PBot => PBot
   end.
 
-Lemma RPar'_triangle n (a : PTm n) : forall b, RPar'.R a b -> RPar'.R b (tstar' a).
+Lemma RPar'_triangle (a : PTm) : forall b, RPar'.R a b -> RPar'.R b (tstar' a).
 Proof.
-  apply tstar'_ind => {n a}.
+  apply tstar'_ind => {a}.
   - hauto lq:on inv:RPar'.R ctrs:RPar'.R.
   - hauto lq:on inv:RPar'.R ctrs:RPar'.R.
   - hauto lq:on use:RPar'.cong, RPar'.refl ctrs:RPar'.R inv:RPar'.R.
@@ -1526,19 +1538,19 @@ Proof.
   - hauto lq:on inv:RPar'.R ctrs:RPar'.R.
 Qed.
 
-Lemma RPar_diamond n (c a1 b1 : PTm n) :
+Lemma RPar_diamond (c a1 b1 : PTm) :
   RPar.R c a1 ->
   RPar.R c b1 ->
   exists d2, RPar.R a1 d2 /\ RPar.R b1 d2.
 Proof. hauto l:on use:RPar_triangle. Qed.
 
-Lemma RPar'_diamond n (c a1 b1 : PTm n) :
+Lemma RPar'_diamond (c a1 b1 : PTm) :
   RPar'.R c a1 ->
   RPar'.R c b1 ->
   exists d2, RPar'.R a1 d2 /\ RPar'.R b1 d2.
 Proof. hauto l:on use:RPar'_triangle. Qed.
 
-Lemma RPar_confluent n (c a1 b1 : PTm n) :
+Lemma RPar_confluent (c a1 b1 : PTm) :
   rtc RPar.R c a1 ->
   rtc RPar.R c b1 ->
   exists d2, rtc RPar.R a1 d2 /\ rtc RPar.R b1 d2.
@@ -1546,7 +1558,7 @@ Proof.
   sfirstorder use:relations.diamond_confluent, RPar_diamond.
 Qed.
 
-Lemma EPar_confluent n (c a1 b1 : PTm n) :
+Lemma EPar_confluent (c a1 b1 : PTm) :
   rtc EPar.R c a1 ->
   rtc EPar.R c b1 ->
   exists d2, rtc EPar.R a1 d2 /\ rtc EPar.R b1 d2.
@@ -1554,7 +1566,7 @@ Proof.
   sfirstorder use:relations.diamond_confluent, EPar_diamond.
 Qed.
 
-Inductive prov {n} : PTm n -> PTm n -> Prop :=
+Inductive prov : PTm -> PTm -> Prop :=
 | P_Abs h a :
   (forall b, prov h (subst_PTm (scons b VarPTm) a)) ->
   prov h (PAbs a)
@@ -1577,14 +1589,14 @@ Inductive prov {n} : PTm n -> PTm n -> Prop :=
 | P_Bot :
   prov PBot PBot.
 
-Lemma ERed_EPar n (a b : PTm n) : ERed.R a b -> EPar.R a b.
+Lemma ERed_EPar (a b : PTm) : ERed.R a b -> EPar.R a b.
 Proof.
   induction 1; hauto lq:on ctrs:EPar.R use:EPar.refl.
 Qed.
 
-Lemma EPar_ERed n (a b : PTm n) : EPar.R a b -> rtc ERed.R a b.
+Lemma EPar_ERed (a b : PTm) : EPar.R a b -> rtc ERed.R a b.
 Proof.
-  move => h. elim : n a b /h.
+  move => h. elim : a b /h.
   - eauto using rtc_r, ERed.AppEta.
   - eauto using rtc_r, ERed.PairEta.
   - auto using rtc_refl.
@@ -1597,27 +1609,27 @@ Proof.
   - auto using rtc_refl.
 Qed.
 
-Lemma EPar_Par n (a b : PTm n) : EPar.R a b -> Par.R a b.
+Lemma EPar_Par (a b : PTm) : EPar.R a b -> Par.R a b.
 Proof.
-  move => h. elim : n a b /h; qauto ctrs:Par.R.
+  move => h. elim : a b /h; qauto ctrs:Par.R.
 Qed.
 
-Lemma RPar_Par n (a b : PTm n) : RPar.R a b -> Par.R a b.
+Lemma RPar_Par (a b : PTm) : RPar.R a b -> Par.R a b.
 Proof.
-  move => h. elim : n a b /h; hauto lq:on ctrs:Par.R.
+  move => h. elim : a b /h; hauto lq:on ctrs:Par.R.
 Qed.
 
-Lemma rtc_idem n (R : PTm n -> PTm n -> Prop) (a b : PTm n) : rtc (rtc R) a b -> rtc R a b.
+Lemma rtc_idem (R : PTm -> PTm -> Prop) (a b : PTm) : rtc (rtc R) a b -> rtc R a b.
 Proof.
   induction 1; hauto l:on use:@relations.rtc_transitive, @rtc_r.
 Qed.
 
-Lemma EPars_EReds {n} (a b : PTm n) : rtc EPar.R a b <-> rtc ERed.R a b.
+Lemma EPars_EReds (a b : PTm) : rtc EPar.R a b <-> rtc ERed.R a b.
 Proof.
   sfirstorder use:@relations.rtc_subrel, EPar_ERed, rtc_idem, ERed_EPar.
 Qed.
 
-Lemma prov_rpar n (u : PTm n) a b : prov u a -> RPar.R a b -> prov u b.
+Lemma prov_rpar (u : PTm) a b : prov u a -> RPar.R a b -> prov u b.
 Proof.
   move => h.
   move : b.
@@ -1651,7 +1663,7 @@ Proof.
 Qed.
 
 
-Lemma prov_lam n (u : PTm n) a : prov u a <-> prov u (PAbs (PApp (ren_PTm shift a) (VarPTm var_zero))).
+Lemma prov_lam (u : PTm) a : prov u a <-> prov u (PAbs (PApp (ren_PTm shift a) (VarPTm var_zero))).
 Proof.
   split.
   move => h. constructor. move => b. asimpl. by constructor.
@@ -1660,10 +1672,10 @@ Proof.
   move : H2. asimpl. inversion 1; subst. done.
 Qed.
 
-Lemma prov_pair n (u : PTm n) a : prov u a <-> prov u (PPair (PProj PL a) (PProj PR a)).
+Lemma prov_pair (u : PTm) a : prov u a <-> prov u (PPair (PProj PL a) (PProj PR a)).
 Proof. hauto lq:on inv:prov ctrs:prov. Qed.
 
-Lemma prov_ered n (u : PTm n) a b : prov u a -> ERed.R a b -> prov u b.
+Lemma prov_ered (u : PTm) a b : prov u a -> ERed.R a b -> prov u b.
 Proof.
   move => h.
   move : b.
@@ -1695,12 +1707,12 @@ Proof.
   - hauto lq:on inv:ERed.R, prov ctrs:prov.
 Qed.
 
-Lemma prov_ereds n (u : PTm n) a b : prov u a -> rtc ERed.R a b -> prov u b.
+Lemma prov_ereds (u : PTm) a b : prov u a -> rtc ERed.R a b -> prov u b.
 Proof.
   induction 2; sfirstorder use:prov_ered.
 Qed.
 
-Fixpoint extract {n} (a : PTm n) : PTm n :=
+Fixpoint extract (a : PTm) : PTm :=
   match a with
   | PAbs a => subst_PTm (scons PBot VarPTm) (extract a)
   | PApp a b => extract a
@@ -1712,12 +1724,12 @@ Fixpoint extract {n} (a : PTm n) : PTm n :=
   | PBot => PBot
   end.
 
-Lemma ren_extract n m (a : PTm n) (ξ : fin n -> fin m) :
+Lemma ren_extract (a : PTm) (ξ : nat -> nat) :
   extract (ren_PTm ξ a) = ren_PTm ξ (extract a).
 Proof.
-  move : m ξ. elim : n/a.
+  move : ξ. elim : a.
   - sfirstorder.
-  - move => n a ih m ξ /=.
+  - move => a ih ξ /=.
     rewrite ih.
     by asimpl.
   - hauto q:on.
@@ -1728,28 +1740,28 @@ Proof.
   - sfirstorder.
 Qed.
 
-Lemma ren_morphing n m (a : PTm n) (ρ : fin n -> PTm m) :
+Lemma ren_morphing (a : PTm) (ρ : nat -> PTm) :
   (forall i, ρ i = extract (ρ i)) ->
   extract (subst_PTm ρ a) = subst_PTm ρ (extract a).
 Proof.
-  move : m ρ.
-  elim : n /a => n //=.
-  move => a ha m ρ hi.
+  move : ρ.
+  elim : a => //=.
+  move => a ha ρ hi.
   rewrite ha.
-  - destruct i as [i|] => //.
+  - destruct i as [|i] => //.
     rewrite ren_extract.
     rewrite -hi.
     by asimpl.
   - by asimpl.
 Qed.
 
-Lemma ren_subst_bot n (a : PTm (S n)) :
+Lemma ren_subst_bot (a : PTm) :
   extract (subst_PTm (scons PBot VarPTm) a) = subst_PTm (scons PBot VarPTm) (extract a).
 Proof.
-  apply ren_morphing. destruct i as [i|] => //=.
+  apply ren_morphing. destruct i => //=.
 Qed.
 
-Definition prov_extract_spec {n} u (a : PTm n) :=
+Definition prov_extract_spec u (a : PTm) :=
   match u with
   | PUniv i => extract a = PUniv i
   | VarPTm i => extract a = VarPTm i
@@ -1758,7 +1770,7 @@ Definition prov_extract_spec {n} u (a : PTm n) :=
   | _ => True
   end.
 
-Lemma prov_extract n u (a : PTm n) :
+Lemma prov_extract u (a : PTm) :
   prov u a -> prov_extract_spec u a.
 Proof.
   move => h.
@@ -1789,19 +1801,19 @@ Definition union {A : Type} (R0 R1 : A -> A -> Prop) a b :=
   R0 a b \/ R1 a b.
 
 Module ERPar.
-  Definition R {n} (a b : PTm n) := union RPar.R EPar.R a b.
-  Lemma RPar {n} (a b : PTm n) : RPar.R a b -> R a b.
+  Definition R (a b : PTm) := union RPar.R EPar.R a b.
+  Lemma RPar (a b : PTm) : RPar.R a b -> R a b.
   Proof. sfirstorder. Qed.
 
-  Lemma EPar {n} (a b : PTm n) : EPar.R a b -> R a b.
+  Lemma EPar (a b : PTm) : EPar.R a b -> R a b.
   Proof. sfirstorder. Qed.
 
-  Lemma refl {n} ( a : PTm n) : ERPar.R a a.
+  Lemma refl ( a : PTm) : ERPar.R a a.
   Proof.
     sfirstorder use:RPar.refl, EPar.refl.
   Qed.
 
-  Lemma ProjCong n p (a0 a1 : PTm n) :
+  Lemma ProjCong p (a0 a1 : PTm) :
     R a0 a1 ->
     rtc R (PProj p a0) (PProj p a1).
   Proof.
@@ -1816,7 +1828,7 @@ Module ERPar.
       by apply EPar.ProjCong.
   Qed.
 
-  Lemma AbsCong n (a0 a1 : PTm (S n)) :
+  Lemma AbsCong (a0 a1 : PTm) :
     R a0 a1 ->
     rtc R (PAbs a0) (PAbs a1).
   Proof.
@@ -1831,7 +1843,7 @@ Module ERPar.
       by apply EPar.AbsCong.
   Qed.
 
-  Lemma AppCong n (a0 a1 b0 b1 : PTm n) :
+  Lemma AppCong (a0 a1 b0 b1 : PTm) :
     R a0 a1 ->
     R b0 b1 ->
     rtc R (PApp a0 b0) (PApp a1 b1).
@@ -1851,7 +1863,7 @@ Module ERPar.
     - sfirstorder use:EPar.AppCong, @rtc_once.
   Qed.
 
-  Lemma PairCong n (a0 a1 b0 b1 : PTm n) :
+  Lemma PairCong (a0 a1 b0 b1 : PTm) :
     R a0 a1 ->
     R b0 b1 ->
     rtc R (PPair a0 b0) (PPair a1 b1).
@@ -1871,7 +1883,7 @@ Module ERPar.
     - sfirstorder use:EPar.PairCong, @rtc_once.
   Qed.
 
-  Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) :
+  Lemma renaming (a b : PTm) (ξ : nat -> nat) :
     R a b -> R (ren_PTm ξ a) (ren_PTm ξ b).
   Proof.
     sfirstorder use:EPar.renaming, RPar.renaming.
@@ -1888,29 +1900,29 @@ Module ERPars.
   #[local]Ltac solve_s :=
     repeat (induction 1; last by solve_s_rec); apply rtc_refl.
 
-  Lemma AppCong n (a0 a1 b0 b1 : PTm n) :
+  Lemma AppCong (a0 a1 b0 b1 : PTm) :
     rtc ERPar.R a0 a1 ->
     rtc ERPar.R b0 b1 ->
     rtc ERPar.R (PApp a0 b0) (PApp a1 b1).
   Proof. solve_s. Qed.
 
-  Lemma AbsCong n (a0 a1 : PTm (S n)) :
+  Lemma AbsCong (a0 a1 : PTm) :
     rtc ERPar.R a0 a1 ->
     rtc ERPar.R (PAbs a0) (PAbs a1).
   Proof. solve_s. Qed.
 
-  Lemma PairCong n (a0 a1 b0 b1 : PTm n) :
+  Lemma PairCong (a0 a1 b0 b1 : PTm) :
     rtc ERPar.R a0 a1 ->
     rtc ERPar.R b0 b1 ->
     rtc ERPar.R (PPair a0 b0) (PPair a1 b1).
   Proof. solve_s. Qed.
 
-  Lemma ProjCong n p (a0 a1 : PTm n) :
+  Lemma ProjCong p (a0 a1 : PTm) :
     rtc ERPar.R a0 a1 ->
     rtc ERPar.R (PProj p a0) (PProj p a1).
   Proof. solve_s. Qed.
 
-  Lemma renaming n (a0 a1 : PTm n) m (ξ : fin n -> fin m) :
+  Lemma renaming (a0 a1 : PTm) (ξ : nat -> nat) :
     rtc ERPar.R a0 a1 ->
     rtc ERPar.R (ren_PTm ξ a0) (ren_PTm ξ a1).
   Proof.
@@ -1921,35 +1933,35 @@ Module ERPars.
 
 End ERPars.
 
-Lemma ERPar_Par n (a b : PTm n) : ERPar.R a b -> Par.R a b.
+Lemma ERPar_Par (a b : PTm) : ERPar.R a b -> Par.R a b.
 Proof.
   sfirstorder use:EPar_Par, RPar_Par.
 Qed.
 
-Lemma Par_ERPar n (a b : PTm n) : Par.R a b -> rtc ERPar.R a b.
+Lemma Par_ERPar (a b : PTm) : Par.R a b -> rtc ERPar.R a b.
 Proof.
-  move => h. elim : n a b /h.
-  - move => n a0 a1 b0 b1 ha iha hb ihb.
+  move => h. elim : a b /h.
+  - move => a0 a1 b0 b1 ha iha hb ihb.
     suff ? : rtc ERPar.R (PApp (PAbs a0) b0) (PApp (PAbs a1) b1).
     apply : relations.rtc_transitive; eauto.
     apply rtc_once. apply ERPar.RPar.
     by apply RPar.AppAbs; eauto using RPar.refl.
     eauto using ERPars.AppCong,ERPars.AbsCong.
-  - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc.
+  - move => a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc.
     apply : rtc_l. apply ERPar.RPar.
     apply RPar.AppPair; eauto using RPar.refl.
     sfirstorder use:ERPars.AppCong, ERPars.PairCong.
-  - move => n p a0 a1 ha iha.
+  - move => p a0 a1 ha iha.
     apply : rtc_l. apply ERPar.RPar. apply RPar.ProjAbs; eauto using RPar.refl.
     sfirstorder use:ERPars.AbsCong, ERPars.ProjCong.
-  - move => n p a0 a1 b0 b1 ha iha hb ihb.
+  - move => p a0 a1 b0 b1 ha iha hb ihb.
     apply : rtc_l. apply ERPar.RPar. apply RPar.ProjPair; eauto using RPar.refl.
     hauto lq:on.
-  - move => n a0 a1 ha iha.
+  - move => a0 a1 ha iha.
     apply : rtc_l. apply ERPar.EPar. apply EPar.AppEta; eauto using EPar.refl.
     hauto lq:on ctrs:rtc
       use:ERPars.AppCong, ERPars.AbsCong, ERPars.renaming.
-  - move => n a0 a1 ha iha.
+  - move => a0 a1 ha iha.
     apply : rtc_l. apply ERPar.EPar. apply EPar.PairEta; eauto using EPar.refl.
     sfirstorder use:ERPars.PairCong, ERPars.ProjCong.
   - sfirstorder.
@@ -1962,44 +1974,44 @@ Proof.
   - sfirstorder.
 Qed.
 
-Lemma Pars_ERPar n (a b : PTm n) : rtc Par.R a b -> rtc ERPar.R a b.
+Lemma Pars_ERPar (a b : PTm) : rtc Par.R a b -> rtc ERPar.R a b.
 Proof.
   induction 1; hauto l:on use:Par_ERPar, @relations.rtc_transitive.
 Qed.
 
-Lemma Par_ERPar_iff n (a b : PTm n) : rtc Par.R a b <-> rtc ERPar.R a b.
+Lemma Par_ERPar_iff (a b : PTm) : rtc Par.R a b <-> rtc ERPar.R a b.
 Proof.
   split.
   sfirstorder use:Pars_ERPar, @relations.rtc_subrel.
   sfirstorder use:ERPar_Par, @relations.rtc_subrel.
 Qed.
 
-Lemma RPar_ERPar n (a b : PTm n) : rtc RPar.R a b -> rtc ERPar.R a b.
+Lemma RPar_ERPar (a b : PTm) : rtc RPar.R a b -> rtc ERPar.R a b.
 Proof.
   sfirstorder use:@relations.rtc_subrel.
 Qed.
 
-Lemma EPar_ERPar n (a b : PTm n) : rtc EPar.R a b -> rtc ERPar.R a b.
+Lemma EPar_ERPar (a b : PTm) : rtc EPar.R a b -> rtc ERPar.R a b.
 Proof.
   sfirstorder use:@relations.rtc_subrel.
 Qed.
 
 Module Type HindleyRosen.
-  Parameter A : nat -> Type.
-  Parameter R0 R1 : forall n, A n -> A n -> Prop.
-  Axiom diamond_R0 : forall n, relations.diamond (R0 n).
-  Axiom diamond_R1 : forall n, relations.diamond (R1 n).
-  Axiom commutativity : forall n,
-    forall a b c, R0 n a b -> R1 n a c -> exists d, R1 n b d /\ R0 n c d.
+  Parameter A : Type.
+  Parameter R0 R1 : A -> A -> Prop.
+  Axiom diamond_R0 : relations.diamond R0.
+  Axiom diamond_R1 : relations.diamond R1.
+  Axiom commutativity :
+    forall a b c, R0 a b -> R1 a c -> exists d, R1 b d /\ R0  c d.
 End HindleyRosen.
 
 Module HindleyRosenFacts (M : HindleyRosen).
   Import M.
   Lemma R0_comm :
-    forall n a b c, R0 n a b -> rtc (union (R0 n) (R1 n)) a c ->
-             exists d, rtc (union (R0 n) (R1 n)) b d /\ R0 n c d.
+    forall a b c, R0 a b -> rtc (union R0 R1) a c ->
+              exists d, rtc (union R0 R1) b d /\ R0 c d.
   Proof.
-    move => n a + c + h.
+    move => a + c + h.
     elim : a c /h.
     - sfirstorder.
     - move => a0 a1 a2 ha ha0 ih b h.
@@ -2011,10 +2023,10 @@ Module HindleyRosenFacts (M : HindleyRosen).
   Qed.
 
   Lemma R1_comm :
-    forall n a b c, R1 n a b -> rtc (union (R0 n) (R1 n)) a c ->
-             exists d, rtc (union (R0 n) (R1 n)) b d /\ R1 n c d.
+    forall a b c, R1 a b -> rtc (union (R0) (R1)) a c ->
+             exists d, rtc (union (R0) (R1)) b d /\ R1 c d.
   Proof.
-    move => n a + c + h.
+    move => a + c + h.
     elim : a c /h.
     - sfirstorder.
     - move => a0 a1 a2 ha ha0 ih b h.
@@ -2026,17 +2038,17 @@ Module HindleyRosenFacts (M : HindleyRosen).
   Qed.
 
   Lemma U_comm :
-    forall n a b c, (union (R0 n) (R1 n)) a b -> rtc (union (R0 n) (R1 n)) a c ->
-             exists d, rtc (union (R0 n) (R1 n)) b d /\ (union (R0 n) (R1 n)) c d.
+    forall a b c, (union R0 R1) a b -> rtc (union R0 R1) a c ->
+              exists d, rtc (union R0 R1) b d /\ (union R0 R1) c d.
   Proof.
     hauto lq:on use:R0_comm, R1_comm.
   Qed.
 
   Lemma U_comms :
-    forall n a b c, rtc (union (R0 n) (R1 n)) a b -> rtc (union (R0 n) (R1 n)) a c ->
-             exists d, rtc (union (R0 n) (R1 n)) b d /\ rtc (union (R0 n) (R1 n)) c d.
+    forall a b c, rtc (union R0 R1) a b -> rtc (union R0 R1) a c ->
+              exists d, rtc (union R0 R1) b d /\ rtc (union R0 R1) c d.
   Proof.
-    move => n a b + h.
+    move => a b + h.
     elim : a b /h.
     - sfirstorder.
     - hecrush ctrs:rtc use:U_comm.
@@ -2046,16 +2058,15 @@ End HindleyRosenFacts.
 
 Module HindleyRosenER <: HindleyRosen.
   Definition A := PTm.
-  Definition R0 n := rtc (@RPar.R n).
-  Definition R1 n := rtc (@EPar.R n).
-  Lemma diamond_R0 : forall n, relations.diamond (R0 n).
+  Definition R0 := rtc (@RPar.R ).
+  Definition R1 := rtc (@EPar.R ).
+  Lemma diamond_R0 : relations.diamond (R0).
     sfirstorder use:RPar_confluent.
   Qed.
-  Lemma diamond_R1 : forall n, relations.diamond (R1 n).
+  Lemma diamond_R1 : relations.diamond (R1).
     sfirstorder use:EPar_confluent.
   Qed.
-  Lemma commutativity : forall n,
-    forall a b c, R0 n a b -> R1 n a c -> exists d, R1 n b d /\ R0 n c d.
+  Lemma commutativity : forall a b c, R0 a b -> R1 a c -> exists d, R1 b d /\ R0 c d.
   Proof.
     hauto l:on use:commutativity.
   Qed.
@@ -2063,7 +2074,7 @@ End HindleyRosenER.
 
 Module ERFacts := HindleyRosenFacts HindleyRosenER.
 
-Lemma rtc_union n (a b : PTm n) :
+Lemma rtc_union (a b : PTm) :
   rtc (union RPar.R EPar.R) a b <->
     rtc (union (rtc RPar.R) (rtc EPar.R)) a b.
 Proof.
@@ -2085,7 +2096,7 @@ Proof.
       sfirstorder.
 Qed.
 
-Lemma prov_erpar n (u : PTm n) a b : prov u a -> ERPar.R a b -> prov u b.
+Lemma prov_erpar (u : PTm) a b : prov u a -> ERPar.R a b -> prov u b.
 Proof.
   move => h [].
   - sfirstorder use:prov_rpar.
@@ -2093,7 +2104,7 @@ Proof.
     sfirstorder use:prov_ereds.
 Qed.
 
-Lemma prov_pars n (u : PTm n) a b : prov u a -> rtc Par.R a b -> prov u b.
+Lemma prov_pars (u : PTm) a b : prov u a -> rtc Par.R a b -> prov u b.
 Proof.
   move => h /Pars_ERPar.
   move => h0.
@@ -2103,51 +2114,50 @@ Proof.
   - hauto lq:on use:prov_erpar.
 Qed.
 
-Lemma Par_confluent n (a b c : PTm n) :
+Lemma Par_confluent (a b c : PTm) :
   rtc Par.R a b ->
   rtc Par.R a c ->
   exists d, rtc Par.R b d /\ rtc Par.R c d.
 Proof.
-  move : n a b c.
-  suff : forall (n : nat) (a b c : PTm n),
+  move : a b c.
+  suff : forall (a b c : PTm),
       rtc ERPar.R a b ->
-      rtc ERPar.R a c -> exists d : PTm n, rtc ERPar.R b d /\ rtc ERPar.R c d.
-  move => h n a b c h0 h1.
+      rtc ERPar.R a c -> exists d : PTm, rtc ERPar.R b d /\ rtc ERPar.R c d.
+  move => h a b c h0 h1.
   apply Par_ERPar_iff in h0, h1.
   move : h h0 h1; repeat move/[apply].
   hauto lq:on use:Par_ERPar_iff.
   have h := ERFacts.U_comms.
-  move => n a b c.
+  move => a b c.
   rewrite /HindleyRosenER.R0 /HindleyRosenER.R1 in h.
-  specialize h with (n := n).
   rewrite /HindleyRosenER.A in h.
   rewrite /ERPar.R.
-  have eq : (fun a0 b0 : PTm n => union RPar.R EPar.R a0 b0) = union RPar.R EPar.R by reflexivity.
+  have eq : (fun a0 b0 : PTm => union RPar.R EPar.R a0 b0) = union RPar.R EPar.R by reflexivity.
   rewrite !{}eq.
   move /rtc_union => + /rtc_union.
   move : h; repeat move/[apply].
   hauto lq:on use:rtc_union.
 Qed.
 
-Lemma pars_univ_inv n i (c : PTm n) :
+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 n) by sfirstorder.
+  have : prov (PUniv i) (PUniv i : PTm) by sfirstorder.
   move : prov_pars. repeat move/[apply].
   apply prov_extract.
 Qed.
 
-Lemma pars_const_inv n i (c : PTm n) :
+Lemma pars_const_inv i (c : PTm) :
   rtc Par.R (PConst i) c ->
   extract c = PConst i.
 Proof.
-  have : prov (PConst i) (PConst i : PTm n) by sfirstorder.
+  have : prov (PConst i) (PConst i : PTm) by sfirstorder.
   move : prov_pars. repeat move/[apply].
   apply prov_extract.
 Qed.
 
-Lemma pars_var_inv n (i : fin n) C :
+Lemma pars_var_inv (i : nat) C :
   rtc Par.R (VarPTm i) C ->
   extract C = VarPTm i.
 Proof.
@@ -2156,7 +2166,7 @@ Proof.
   apply prov_extract.
 Qed.
 
-Lemma pars_univ_inj n i j (C : PTm n) :
+Lemma pars_univ_inj i j (C : PTm) :
   rtc Par.R (PUniv i) C ->
   rtc Par.R (PUniv j) C ->
   i = j.
@@ -2164,7 +2174,7 @@ Proof.
   sauto l:on use:pars_univ_inv.
 Qed.
 
-Lemma pars_const_inj n i j (C : PTm n) :
+Lemma pars_const_inj i j (C : PTm) :
   rtc Par.R (PConst i) C ->
   rtc Par.R (PConst j) C ->
   i = j.
@@ -2172,10 +2182,10 @@ Proof.
   sauto l:on use:pars_const_inv.
 Qed.
 
-Definition join {n} (a b : PTm n) :=
+Definition join (a b : PTm) :=
   exists c, rtc Par.R a c /\ rtc Par.R b c.
 
-Lemma join_transitive n (a b c : PTm n) :
+Lemma join_transitive (a b c : PTm) :
   join a b -> join b c -> join a c.
 Proof.
   rewrite /join.
@@ -2185,31 +2195,31 @@ Proof.
   eauto using relations.rtc_transitive.
 Qed.
 
-Lemma join_symmetric n (a b : PTm n) :
+Lemma join_symmetric (a b : PTm) :
   join a b -> join b a.
 Proof. sfirstorder unfold:join. Qed.
 
-Lemma join_refl n (a : PTm n) : join a a.
+Lemma join_refl (a : PTm) : join a a.
 Proof. hauto lq:on ctrs:rtc unfold:join. Qed.
 
-Lemma join_univ_inj n i j :
-  join (PUniv i : PTm n) (PUniv j) -> i = j.
+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 n i j :
-  join (PConst i : PTm n) (PConst j) -> i = j.
+Lemma join_const_inj i j :
+  join (PConst i : PTm) (PConst j) -> i = j.
 Proof.
   sfirstorder use:pars_const_inj.
 Qed.
 
-Lemma join_substing n m (a b : PTm n) (ρ : fin n -> PTm m) :
+Lemma join_substing (a b : PTm) (ρ : nat -> PTm) :
   join a b ->
   join (subst_PTm ρ a) (subst_PTm ρ b).
 Proof. hauto lq:on unfold:join use:Pars.substing. Qed.
 
-Fixpoint ne {n} (a : PTm n) :=
+Fixpoint ne (a : PTm) :=
   match a with
   | VarPTm i => true
   | PApp a b => ne a && nf b
@@ -2220,7 +2230,7 @@ Fixpoint ne {n} (a : PTm n) :=
   | PConst _ => false
   | PBot => true
   end
-with nf {n} (a : PTm n) :=
+with nf (a : PTm) :=
   match a with
   | VarPTm i => true
   | PApp a b => ne a && nf b
@@ -2232,53 +2242,53 @@ with nf {n} (a : PTm n) :=
   | PBot => true
 end.
 
-Lemma ne_nf n a : @ne n a -> nf a.
+Lemma ne_nf a : ne a -> nf a.
 Proof. elim : a => //=. Qed.
 
-Definition wn {n} (a : PTm n) := exists b, rtc RPar'.R a b /\ nf b.
-Definition wne {n} (a : PTm n) := exists b, rtc RPar'.R a b /\ ne b.
+Definition wn (a : PTm) := exists b, rtc RPar'.R a b /\ nf b.
+Definition wne (a : PTm) := exists b, rtc RPar'.R a b /\ ne b.
 
 (* Weakly neutral implies weakly normal *)
-Lemma wne_wn n a : @wne n a -> wn a.
+Lemma wne_wn a : @wne a -> wn a.
 Proof. sfirstorder use:ne_nf. Qed.
 
 (* Normal implies weakly normal *)
-Lemma nf_wn n v : @nf n v -> wn v.
+Lemma nf_wn v : @nf v -> wn v.
 Proof. sfirstorder ctrs:rtc. Qed.
 
-Lemma nf_refl n (a b : PTm n) (h : RPar'.R a b) : (nf a -> b = a) /\ (ne a -> b = a).
+Lemma nf_refl (a b : PTm) (h : RPar'.R a b) : (nf a -> b = a) /\ (ne a -> b = a).
 Proof.
   elim : a b /h => //=; solve [hauto b:on].
 Qed.
 
-Lemma ne_nf_ren n m (a : PTm n) (ξ : fin n -> fin m) :
+Lemma ne_nf_ren  (a : PTm) (ξ : nat -> nat) :
   (ne a <-> ne (ren_PTm ξ a)) /\ (nf a <-> nf (ren_PTm ξ a)).
 Proof.
-  move : m ξ. elim : n / a => //=; solve [hauto b:on].
+  move : ξ. elim : a => //=; solve [hauto b:on].
 Qed.
 
-Lemma wne_app n (a b : PTm n) :
+Lemma wne_app (a b : PTm) :
   wne a -> wn b -> wne (PApp a b).
 Proof.
   move => [a0 [? ?]] [b0 [? ?]].
   exists (PApp a0 b0). hauto b:on drew:off use:RPars'.AppCong.
 Qed.
 
-Lemma wn_abs n a (h : wn a) : @wn n (PAbs a).
+Lemma wn_abs a (h : wn a) : @wn (PAbs a).
 Proof.
   move : h => [v [? ?]].
   exists (PAbs v).
   eauto using RPars'.AbsCong.
 Qed.
 
-Lemma wn_pair n (a b : PTm n) : wn a -> wn b -> wn (PPair a b).
+Lemma wn_pair (a b : PTm) : wn a -> wn b -> wn (PPair a b).
 Proof.
   move => [a0 [? ?]] [b0 [? ?]].
   exists (PPair a0 b0).
   hauto lqb:on use:RPars'.PairCong.
 Qed.
 
-Lemma wne_proj n p (a : PTm n) : wne a -> wne (PProj p a).
+Lemma wne_proj p (a : PTm) : wne a -> wne (PProj p a).
 Proof.
   move => [a0 [? ?]].
   exists (PProj p a0). hauto lqb:on use:RPars'.ProjCong.
@@ -2287,15 +2297,15 @@ Qed.
 Create HintDb nfne.
 #[export]Hint Resolve nf_wn ne_nf wne_wn nf_refl : nfne.
 
-Lemma ne_nf_antiren n m (a : PTm n) (ρ : fin n -> PTm m) :
+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).
 Proof.
-  move : m ρ. elim : n / a => //;
+  move : ρ. elim : a => //;
    hauto b:on drew:off use:RPar.var_or_const_up.
 Qed.
 
-Lemma wn_antirenaming n m a (ρ : fin n -> PTm m) :
+Lemma wn_antirenaming a (ρ : nat -> PTm) :
   (forall i, var_or_const (ρ i)) ->
   wn (subst_PTm ρ a) -> wn a.
 Proof.
@@ -2308,7 +2318,7 @@ Proof.
   by eapply ne_nf_antiren.
 Qed.
 
-Lemma ext_wn n (a : PTm n) :
+Lemma ext_wn (a : PTm) :
     wn (PApp a PBot) ->
     wn a.
 Proof.
@@ -2333,41 +2343,41 @@ Proof.
 Qed.
 
 Module Join.
-  Lemma ProjCong p n (a0 a1 : PTm n) :
+  Lemma ProjCong p (a0 a1 : PTm) :
     join a0 a1 ->
     join (PProj p a0) (PProj p a1).
   Proof. hauto lq:on use:Pars.ProjCong unfold:join. Qed.
 
-  Lemma PairCong n (a0 a1 b0 b1 : PTm n) :
+  Lemma PairCong (a0 a1 b0 b1 : PTm) :
     join a0 a1 ->
     join b0 b1 ->
     join (PPair a0 b0) (PPair a1 b1).
   Proof. hauto lq:on use:Pars.PairCong unfold:join. Qed.
 
-  Lemma AppCong n (a0 a1 b0 b1 : PTm n) :
+  Lemma AppCong (a0 a1 b0 b1 : PTm) :
     join a0 a1 ->
     join b0 b1 ->
     join (PApp a0 b0) (PApp a1 b1).
   Proof. hauto lq:on use:Pars.AppCong. Qed.
 
-  Lemma AbsCong n (a b : PTm (S n)) :
+  Lemma AbsCong (a b : PTm) :
     join a b ->
     join (PAbs a) (PAbs b).
   Proof. hauto lq:on use:Pars.AbsCong. Qed.
 
-  Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) :
+  Lemma renaming (a b : PTm) (ξ : nat -> nat) :
     join a b -> join (ren_PTm ξ a) (ren_PTm ξ b).
   Proof.
     induction 1; hauto lq:on use:Pars.renaming.
   Qed.
 
-  Lemma weakening n (a b : PTm n)  :
+  Lemma weakening (a b : PTm)  :
     join a b -> join (ren_PTm shift a) (ren_PTm shift b).
   Proof.
     apply renaming.
   Qed.
 
-  Lemma FromPar n (a b : PTm n) :
+  Lemma FromPar (a b : PTm) :
     Par.R a b ->
     join a b.
   Proof.
@@ -2375,7 +2385,7 @@ Module Join.
   Qed.
 End Join.
 
-Lemma abs_eq n a (b : PTm n) :
+Lemma abs_eq a (b : PTm) :
   join (PAbs a) b <-> join a (PApp (ren_PTm shift b) (VarPTm var_zero)).
 Proof.
   split.
@@ -2385,13 +2395,13 @@ Proof.
     simpl.
     move => ?. apply : join_transitive; eauto.
     apply join_symmetric. apply Join.FromPar.
-    apply : Par.AppAbs'; eauto using Par.refl. by asimpl.
+    apply : Par.AppAbs'; eauto using Par.refl. by asimpl; rewrite subst_id.
   - move /Join.AbsCong.
     move /join_transitive. apply.
     apply join_symmetric. apply Join.FromPar. apply Par.AppEta. apply Par.refl.
 Qed.
 
-Lemma pair_eq n (a0 a1 b : PTm n) :
+Lemma pair_eq (a0 a1 b : PTm) :
   join (PPair a0 a1) b <-> join a0 (PProj PL b) /\ join a1 (PProj PR b).
 Proof.
   split.
@@ -2407,7 +2417,7 @@ Proof.
     apply Join.FromPar. hauto lq:on ctrs:Par.R use:Par.refl.
 Qed.
 
-Lemma join_pair_inj n (a0 a1 b0 b1 : PTm n) :
+Lemma join_pair_inj (a0 a1 b0 b1 : PTm) :
   join (PPair a0 a1) (PPair b0 b1) <-> join a0 b0 /\ join a1 b1.
 Proof.
   split; last by hauto lq:on use:Join.PairCong.