From b3bd75ad429cb400cb5a8ab38446dd63dc8c9fb9 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <yliu8e5f7@protonmail.com>
Date: Mon, 3 Mar 2025 01:38:22 -0500
Subject: [PATCH] Fix the typing rules

---
 theories/common.v     |   7 ++
 theories/structural.v |  77 ++++++++--------------
 theories/typing.v     | 145 +++++++++++++++++++++---------------------
 3 files changed, 103 insertions(+), 126 deletions(-)

diff --git a/theories/common.v b/theories/common.v
index a890edd..a3740ff 100644
--- a/theories/common.v
+++ b/theories/common.v
@@ -10,6 +10,13 @@ Inductive lookup : nat -> list PTm -> PTm -> Prop :=
   lookup i Γ A ->
   lookup (S i) (cons B Γ) (ren_PTm shift A).
 
+Lemma here' A Γ U : U = ren_PTm shift A -> lookup 0 (A :: Γ) U.
+Proof.  move => ->. apply here. Qed.
+
+Lemma there' i Γ A B U : U = ren_PTm shift A -> lookup i Γ A ->
+                       lookup (S i) (cons B Γ) U.
+Proof. move => ->. apply there. Qed.
+
 Derive Inversion lookup_inv with (forall i Γ A, lookup i Γ A).
 
 Definition renaming_ok (Γ : list PTm) (Δ : list PTm) (ξ : nat -> nat) :=
diff --git a/theories/structural.v b/theories/structural.v
index c25986c..39a573d 100644
--- a/theories/structural.v
+++ b/theories/structural.v
@@ -1,96 +1,69 @@
-Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax common typing.
+Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common typing.
 From Hammer Require Import Tactics.
 Require Import ssreflect.
 Require Import Psatz.
 
 Lemma wff_mutual :
-  (forall n (Γ : fin n -> PTm n), ⊢ Γ -> True) /\
-  (forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> ⊢ Γ)  /\
-  (forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> ⊢ Γ) /\
-  (forall n Γ (A B : PTm n), Γ ⊢ A ≲ B -> ⊢ Γ).
+  (forall Γ, ⊢ Γ -> True) /\
+  (forall Γ (a A : PTm), Γ ⊢ a ∈ A -> ⊢ Γ)  /\
+  (forall Γ (a b A : PTm), Γ ⊢ a ≡ b ∈ A -> ⊢ Γ) /\
+  (forall Γ (A B : PTm), Γ ⊢ A ≲ B -> ⊢ Γ).
 Proof. apply wt_mutual; eauto. Qed.
 
 #[export]Hint Constructors Wt Wff Eq : wt.
 
-Lemma T_Nat' n Γ :
+Lemma T_Nat' Γ :
   ⊢ Γ ->
-  Γ ⊢ PNat : PTm n ∈ PUniv 0.
+  Γ ⊢ PNat ∈ PUniv 0.
 Proof. apply T_Nat. Qed.
 
-Lemma renaming_up n m (ξ : fin n -> fin m) Δ Γ A :
+Lemma renaming_up (ξ : nat -> nat) Δ Γ A :
   renaming_ok Δ Γ ξ ->
-  renaming_ok (funcomp (ren_PTm shift) (scons (ren_PTm ξ A) Δ)) (funcomp (ren_PTm shift) (scons A Γ)) (upRen_PTm_PTm ξ) .
+  renaming_ok (cons (ren_PTm ξ A) Δ) (cons A Γ) (upRen_PTm_PTm ξ) .
 Proof.
-  move => h i.
-  destruct i as [i|].
-  asimpl. rewrite /renaming_ok in h.
-  rewrite /funcomp. rewrite -h.
-  by asimpl.
-  by asimpl.
+  move => h i A0.
+  elim /lookup_inv => //=_.
+  - move => A1 Γ0 ? [*]. subst. apply here'. by asimpl.
+  - move => i0 Γ0 A1 B h' ? [*]. subst.
+    apply : there'; eauto. by asimpl.
 Qed.
 
-Lemma Su_Wt n Γ a i :
-  Γ ⊢ a ∈ @PUniv n i ->
+Lemma Su_Wt Γ a i :
+  Γ ⊢ a ∈ PUniv i ->
   Γ ⊢ a ≲ a.
 Proof. hauto lq:on ctrs:LEq, Eq. Qed.
 
-Lemma Wt_Univ n Γ a A i
+Lemma Wt_Univ Γ a A i
   (h : Γ ⊢ a ∈ A) :
-  Γ ⊢ @PUniv n i ∈ PUniv (S i).
+  Γ ⊢ @PUniv i ∈ PUniv (S i).
 Proof.
   hauto lq:on ctrs:Wt use:wff_mutual.
 Qed.
 
-Lemma Bind_Inv n Γ p (A : PTm n) B U :
+Lemma Bind_Inv Γ p (A : PTm) B U :
   Γ ⊢ PBind p A B ∈ U ->
   exists i, Γ ⊢ A ∈ PUniv i /\
-  funcomp (ren_PTm shift) (scons A Γ) ⊢ B ∈ PUniv i /\
+  (cons A Γ) ⊢ B ∈ PUniv i /\
   Γ ⊢ PUniv i ≲ U.
 Proof.
   move E :(PBind p A B) => T h.
   move : p A B E.
-  elim : n Γ T U / h => //=.
-  - move => n Γ i p A B hA _ hB _ p0 A0 B0 [*]. subst.
+  elim : Γ T U / h => //=.
+  - move => Γ i p A B hA _ hB _ p0 A0 B0 [*]. subst.
     exists i. repeat split => //=.
     eapply wff_mutual in hA.
     apply Su_Univ; eauto.
   - hauto lq:on rew:off ctrs:LEq.
 Qed.
 
-(* Lemma Pi_Inv n Γ (A : PTm n) B U : *)
-(*   Γ ⊢ PBind PPi A B ∈ U -> *)
-(*   exists i, Γ ⊢ A ∈ PUniv i /\ *)
-(*   funcomp (ren_PTm shift) (scons A Γ) ⊢ B ∈ PUniv i /\ *)
-(*   Γ ⊢ PUniv i ≲ U. *)
-(* Proof. *)
-(*   move E :(PBind PPi A B) => T h. *)
-(*   move : A B E. *)
-(*   elim : n Γ T U / h => //=. *)
-(*   - hauto lq:on ctrs:Wt,LEq,Eq use:Wt_Univ. *)
-(*   - hauto lq:on rew:off ctrs:LEq. *)
-(* Qed. *)
-
-(* Lemma Bind_Inv n Γ (A : PTm n) B U : *)
-(*   Γ ⊢ PBind PSig A B ∈ U -> *)
-(*   exists i, Γ ⊢ A ∈ PUniv i /\ *)
-(*   funcomp (ren_PTm shift) (scons A Γ) ⊢ B ∈ PUniv i /\ *)
-(*   Γ ⊢ PUniv i ≲ U. *)
-(* Proof. *)
-(*   move E :(PBind PSig A B) => T h. *)
-(*   move : A B E. *)
-(*   elim : n Γ T U / h => //=. *)
-(*   - hauto lq:on ctrs:Wt,LEq,Eq use:Wt_Univ. *)
-(*   - hauto lq:on rew:off ctrs:LEq. *)
-(* Qed. *)
-
-Lemma T_App' n Γ (b a : PTm n) A B U :
+Lemma T_App' Γ (b a : PTm) A B U :
   U = subst_PTm (scons a VarPTm) B ->
   Γ ⊢ b ∈ PBind PPi A B ->
   Γ ⊢ a ∈ A ->
   Γ ⊢ PApp b a ∈ U.
 Proof. move => ->. apply T_App. Qed.
 
-Lemma T_Pair' n Γ (a b : PTm n) A B i U :
+Lemma T_Pair' Γ (a b : PTm ) A B i U :
   U = subst_PTm (scons a VarPTm) B ->
   Γ ⊢ a ∈ A ->
   Γ ⊢ b ∈ U ->
@@ -100,7 +73,7 @@ Proof.
   move => ->. eauto using T_Pair.
 Qed.
 
-Lemma E_IndCong' n Γ P0 P1 (a0 a1 : PTm n) b0 b1 c0 c1 i U :
+Lemma E_IndCong' Γ P0 P1 (a0 a1 : PTm ) b0 b1 c0 c1 i U :
   U = subst_PTm (scons a0 VarPTm) P0 ->
   funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P0 ∈ PUniv i ->
   funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P0 ≡ P1 ∈ PUniv i ->
diff --git a/theories/typing.v b/theories/typing.v
index 818d6b5..ae78747 100644
--- a/theories/typing.v
+++ b/theories/typing.v
@@ -1,240 +1,237 @@
-Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax.
+Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax common.
 
 Reserved Notation "Γ ⊢ a ∈ A" (at level 70).
 Reserved Notation "Γ ⊢ a ≡ b ∈ A" (at level 70).
 Reserved Notation "Γ ⊢ A ≲ B" (at level 70).
 Reserved Notation "⊢ Γ" (at level 70).
-Inductive Wt : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> Prop :=
-| T_Var n Γ (i : fin n) :
+Inductive Wt : list PTm -> PTm -> PTm -> Prop :=
+| T_Var i Γ A :
   ⊢ Γ ->
-  Γ ⊢ VarPTm i ∈ Γ i
+  lookup i Γ A ->
+  Γ ⊢ VarPTm i ∈ A
 
-| T_Bind n Γ i p (A : PTm n) (B : PTm (S n)) :
+| T_Bind Γ i p (A : PTm) (B : PTm) :
   Γ ⊢ A ∈ PUniv i ->
-  funcomp (ren_PTm shift) (scons A Γ) ⊢ B ∈ PUniv i ->
+  cons A Γ ⊢ B ∈ PUniv i ->
   Γ ⊢ PBind p A B ∈ PUniv i
 
-| T_Abs n Γ (a : PTm (S n)) A B i :
+| T_Abs Γ (a : PTm) A B i :
   Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
-  funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B ->
+  (cons A Γ) ⊢ a ∈ B ->
   Γ ⊢ PAbs a ∈ PBind PPi A B
 
-| T_App n Γ (b a : PTm n) A B :
+| T_App Γ (b a : PTm) A B :
   Γ ⊢ b ∈ PBind PPi A B ->
   Γ ⊢ a ∈ A ->
   Γ ⊢ PApp b a ∈ subst_PTm (scons a VarPTm) B
 
-| T_Pair n Γ (a b : PTm n) A B i :
+| T_Pair Γ (a b : PTm) A B i :
   Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
   Γ ⊢ a ∈ A ->
   Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B ->
   Γ ⊢ PPair a b ∈ PBind PSig A B
 
-| T_Proj1 n Γ (a : PTm n) A B :
+| T_Proj1 Γ (a : PTm) A B :
   Γ ⊢ a ∈ PBind PSig A B ->
   Γ ⊢ PProj PL a ∈ A
 
-| T_Proj2 n Γ (a : PTm n) A B :
+| T_Proj2 Γ (a : PTm) A B :
   Γ ⊢ a ∈ PBind PSig A B ->
   Γ ⊢ PProj PR a ∈ subst_PTm (scons (PProj PL a) VarPTm) B
 
-| T_Univ n Γ i :
+| T_Univ Γ i :
   ⊢ Γ ->
-  Γ ⊢ PUniv i : PTm n ∈ PUniv (S i)
+  Γ ⊢ PUniv i ∈ PUniv (S i)
 
-| T_Nat n Γ i :
+| T_Nat Γ i :
   ⊢ Γ ->
-  Γ ⊢ PNat : PTm n ∈ PUniv i
+  Γ ⊢ PNat ∈ PUniv i
 
-| T_Zero n Γ :
+| T_Zero Γ :
   ⊢ Γ ->
-  Γ ⊢ PZero : PTm n ∈ PNat
+  Γ ⊢ PZero ∈ PNat
 
-| T_Suc n Γ (a : PTm n) :
+| T_Suc Γ (a : PTm) :
   Γ ⊢ a ∈ PNat ->
   Γ ⊢ PSuc a ∈ PNat
 
-| T_Ind s Γ P (a : PTm s) b c i :
-  funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P ∈ PUniv i ->
+| T_Ind Γ P (a : PTm) b c i :
+  cons PNat Γ ⊢ P ∈ PUniv i ->
   Γ ⊢ a ∈ PNat ->
   Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P ->
-  funcomp (ren_PTm shift)(scons P (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
+  (cons P (cons PNat Γ)) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
   Γ ⊢ PInd P a b c ∈ subst_PTm (scons a VarPTm) P
 
-| T_Conv n Γ (a : PTm n) A B :
+| T_Conv Γ (a : PTm) A B :
   Γ ⊢ a ∈ A ->
   Γ ⊢ A ≲ B ->
   Γ ⊢ a ∈ B
 
-with Eq : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> PTm n -> Prop :=
+with Eq : list PTm -> PTm -> PTm -> PTm -> Prop :=
 (* Structural *)
-| E_Refl n Γ (a : PTm n) A :
+| E_Refl Γ (a : PTm ) A :
   Γ ⊢ a ∈ A ->
   Γ ⊢ a ≡ a ∈ A
 
-| E_Symmetric n Γ (a b : PTm n) A :
+| E_Symmetric Γ (a b : PTm) A :
   Γ ⊢ a ≡ b ∈ A ->
   Γ ⊢ b ≡ a ∈ A
 
-| E_Transitive n Γ (a b c : PTm n) A :
+| E_Transitive Γ (a b c : PTm) A :
   Γ ⊢ a ≡ b ∈ A ->
   Γ ⊢ b ≡ c ∈ A ->
   Γ ⊢ a ≡ c ∈ A
 
 (* Congruence *)
-| E_Bind n Γ i p (A0 A1 : PTm n) B0 B1 :
-  ⊢ Γ ->
+| E_Bind Γ i p (A0 A1 : PTm) B0 B1 :
   Γ ⊢ A0 ∈ PUniv i ->
   Γ ⊢ A0 ≡ A1 ∈ PUniv i ->
-  funcomp (ren_PTm shift) (scons A0 Γ) ⊢ B0 ≡ B1 ∈ PUniv i ->
+  (cons A0 Γ) ⊢ B0 ≡ B1 ∈ PUniv i ->
   Γ ⊢ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv i
 
-| E_Abs n Γ (a b : PTm (S n)) A B i :
+| E_Abs Γ (a b : PTm) A B i :
   Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
-  funcomp (ren_PTm shift) (scons A Γ) ⊢ a ≡ b ∈ B ->
+  (cons A Γ) ⊢ a ≡ b ∈ B ->
   Γ ⊢ PAbs a ≡ PAbs b ∈ PBind PPi A B
 
-| E_App n Γ i (b0 b1 a0 a1 : PTm n) A B :
+| E_App Γ i (b0 b1 a0 a1 : PTm) A B :
   Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
   Γ ⊢ b0 ≡ b1 ∈ PBind PPi A B ->
   Γ ⊢ a0 ≡ a1 ∈ A ->
   Γ ⊢ PApp b0 a0 ≡ PApp b1 a1 ∈ subst_PTm (scons a0 VarPTm) B
 
-| E_Pair n Γ (a0 a1 b0 b1 : PTm n) A B i :
+| E_Pair Γ (a0 a1 b0 b1 : PTm) A B i :
   Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
   Γ ⊢ a0 ≡ a1 ∈ A ->
   Γ ⊢ b0 ≡ b1 ∈ subst_PTm (scons a0 VarPTm) B ->
   Γ ⊢ PPair a0 b0 ≡ PPair a1 b1 ∈ PBind PSig A B
 
-| E_Proj1 n Γ (a b : PTm n) A B :
+| E_Proj1 Γ (a b : PTm) A B :
   Γ ⊢ a ≡ b ∈ PBind PSig A B ->
   Γ ⊢ PProj PL a ≡ PProj PL b ∈ A
 
-| E_Proj2 n Γ i (a b : PTm n) A B :
+| E_Proj2 Γ i (a b : PTm) A B :
   Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
   Γ ⊢ a ≡ b ∈ PBind PSig A B ->
   Γ ⊢ PProj PR a ≡ PProj PR b ∈ subst_PTm (scons (PProj PL a) VarPTm) B
 
-| E_IndCong n Γ P0 P1 (a0 a1 : PTm n) b0 b1 c0 c1 i :
-  funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P0 ∈ PUniv i ->
-  funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P0 ≡ P1 ∈ PUniv i ->
+| E_IndCong Γ P0 P1 (a0 a1 : PTm) b0 b1 c0 c1 i :
+  (cons PNat Γ) ⊢ P0 ∈ PUniv i ->
+  (cons PNat Γ) ⊢ P0 ≡ P1 ∈ PUniv i ->
   Γ ⊢ a0 ≡ a1 ∈ PNat ->
   Γ ⊢ b0 ≡ b1 ∈ subst_PTm (scons PZero VarPTm) P0 ->
-  funcomp (ren_PTm shift) (scons P0 (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c0 ≡ c1 ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P0) ->
+  (cons P0 ((cons PNat Γ))) ⊢ c0 ≡ c1 ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P0) ->
   Γ ⊢ PInd P0 a0 b0 c0 ≡ PInd P1 a1 b1 c1 ∈ subst_PTm (scons a0 VarPTm) P0
 
-| E_SucCong n Γ (a b : PTm n) :
+| E_SucCong Γ (a b : PTm) :
   Γ ⊢ a ≡ b ∈ PNat ->
   Γ ⊢ PSuc a ≡ PSuc b ∈ PNat
 
-| E_Conv n Γ (a b : PTm n) A B :
+| E_Conv Γ (a b : PTm) A B :
   Γ ⊢ a ≡ b ∈ A ->
   Γ ⊢ A ≲ B ->
   Γ ⊢ a ≡ b ∈ B
 
 (* Beta *)
-| E_AppAbs n Γ (a : PTm (S n)) b A B i:
+| E_AppAbs Γ (a : PTm) b A B i:
   Γ ⊢ PBind PPi A B ∈ PUniv i ->
   Γ ⊢ b ∈ A ->
-  funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B ->
+  (cons A Γ) ⊢ a ∈ B ->
   Γ ⊢ PApp (PAbs a) b ≡ subst_PTm (scons b VarPTm) a ∈ subst_PTm (scons b VarPTm ) B
 
-| E_ProjPair1 n Γ (a b : PTm n) A B i :
+| E_ProjPair1 Γ (a b : PTm) A B i :
   Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
   Γ ⊢ a ∈ A ->
   Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B ->
   Γ ⊢ PProj PL (PPair a b) ≡ a ∈ A
 
-| E_ProjPair2 n Γ (a b : PTm n) A B i :
+| E_ProjPair2 Γ (a b : PTm) A B i :
   Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
   Γ ⊢ a ∈ A ->
   Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B ->
   Γ ⊢ PProj PR (PPair a b) ≡ b ∈ subst_PTm (scons a VarPTm) B
 
-| E_IndZero n Γ P i (b : PTm n) c :
-  funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P ∈ PUniv i ->
+| E_IndZero Γ P i (b : PTm) c :
+  (cons PNat Γ) ⊢ P ∈ PUniv i ->
   Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P ->
-  funcomp (ren_PTm shift)(scons P (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
+  (cons P (cons PNat Γ)) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
   Γ ⊢ PInd P PZero b c ≡ b ∈ subst_PTm (scons PZero VarPTm) P
 
-| E_IndSuc s Γ P (a : PTm s) b c i :
-  funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P ∈ PUniv i ->
+| E_IndSuc Γ P (a : PTm) b c i :
+  (cons PNat Γ) ⊢ P ∈ PUniv i ->
   Γ ⊢ a ∈ PNat ->
   Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P ->
-  funcomp (ren_PTm shift)(scons P (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
+  (cons P (cons PNat Γ)) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
   Γ ⊢ PInd P (PSuc a) b c ≡ (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c) ∈ subst_PTm (scons (PSuc a) VarPTm) P
 
 (* Eta *)
-| E_AppEta n Γ (b : PTm n) A B i :
-  ⊢ Γ ->
+| E_AppEta Γ (b : PTm) A B i :
   Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
   Γ ⊢ b ∈ PBind PPi A B ->
   Γ ⊢ PAbs (PApp (ren_PTm shift b) (VarPTm var_zero)) ≡ b ∈ PBind PPi A B
 
-| E_PairEta n Γ (a : PTm n) A B i :
+| E_PairEta Γ (a : PTm ) A B i :
   Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
   Γ ⊢ a ∈ PBind PSig A B ->
   Γ ⊢ a ≡ PPair (PProj PL a) (PProj PR a) ∈ PBind PSig A B
 
-with LEq : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> Prop :=
+with LEq : list PTm -> PTm -> PTm -> Prop :=
 (* Structural *)
-| Su_Transitive  n Γ (A B C : PTm n) :
+| Su_Transitive Γ (A B C : PTm) :
   Γ ⊢ A ≲ B ->
   Γ ⊢ B ≲ C ->
   Γ ⊢ A ≲ C
 
 (* Congruence *)
-| Su_Univ n Γ i j :
+| Su_Univ Γ i j :
   ⊢ Γ ->
   i <= j ->
-  Γ ⊢ PUniv i : PTm n ≲ PUniv j
+  Γ ⊢ PUniv i ≲ PUniv j
 
-| Su_Pi n Γ (A0 A1 : PTm n) B0 B1 i :
-  ⊢ Γ ->
+| Su_Pi Γ (A0 A1 : PTm) B0 B1 i :
   Γ ⊢ A0 ∈ PUniv i ->
   Γ ⊢ A1 ≲ A0 ->
-  funcomp (ren_PTm shift) (scons A0 Γ) ⊢ B0 ≲ B1 ->
+  (cons A0 Γ) ⊢ B0 ≲ B1 ->
   Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1
 
-| Su_Sig n Γ (A0 A1 : PTm n) B0 B1 i :
-  ⊢ Γ ->
+| Su_Sig Γ (A0 A1 : PTm) B0 B1 i :
   Γ ⊢ A1 ∈ PUniv i ->
   Γ ⊢ A0 ≲ A1 ->
-  funcomp (ren_PTm shift) (scons A1 Γ) ⊢ B0 ≲ B1 ->
+  (cons A1 Γ) ⊢ B0 ≲ B1 ->
   Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1
 
 (* Injecting from equalities *)
-| Su_Eq n Γ (A : PTm n) B i  :
+| Su_Eq Γ (A : PTm) B i  :
   Γ ⊢ A ≡ B ∈ PUniv i ->
   Γ ⊢ A ≲ B
 
 (* Projection axioms *)
-| Su_Pi_Proj1 n Γ (A0 A1 : PTm n) B0 B1 :
+| Su_Pi_Proj1 Γ (A0 A1 : PTm) B0 B1 :
   Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 ->
   Γ ⊢ A1 ≲ A0
 
-| Su_Sig_Proj1 n Γ (A0 A1 : PTm n) B0 B1 :
+| Su_Sig_Proj1 Γ (A0 A1 : PTm) B0 B1 :
   Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1 ->
   Γ ⊢ A0 ≲ A1
 
-| Su_Pi_Proj2 n Γ (a0 a1 A0 A1 : PTm n) B0 B1 :
+| Su_Pi_Proj2 Γ (a0 a1 A0 A1 : PTm ) B0 B1 :
   Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 ->
   Γ ⊢ a0 ≡ a1 ∈ A1 ->
   Γ ⊢ subst_PTm (scons a0 VarPTm) B0 ≲ subst_PTm (scons a1 VarPTm) B1
 
-| Su_Sig_Proj2 n Γ (a0 a1 A0 A1 : PTm n) B0 B1 :
+| Su_Sig_Proj2 Γ (a0 a1 A0 A1 : PTm) B0 B1 :
   Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1 ->
   Γ ⊢ a0 ≡ a1 ∈ A0 ->
   Γ ⊢ subst_PTm (scons a0 VarPTm) B0 ≲ subst_PTm (scons a1 VarPTm) B1
 
-with Wff : forall {n}, (fin n -> PTm n) -> Prop :=
+with Wff : list PTm -> Prop :=
 | Wff_Nil :
-  ⊢ null
-| Wff_Cons n Γ (A : PTm n) i :
+  ⊢ nil
+| Wff_Cons Γ (A : PTm) i :
   ⊢ Γ ->
   Γ ⊢ A ∈ PUniv i ->
   (* -------------------------------- *)
-  ⊢ funcomp (ren_PTm shift) (scons A Γ)
+  ⊢ (cons A Γ)
 
 where
 "Γ ⊢ a ∈ A" := (Wt Γ a A) and "⊢ Γ" := (Wff Γ) and "Γ ⊢ a ≡ b ∈ A" := (Eq Γ a b A) and "Γ ⊢ A ≲ B" := (LEq Γ A B).