6 changed files with 1031 additions and 674 deletions
--- a/syntax.sig
+++ b/syntax.sig
@ -14,9 +14,11 @@ PAbs : (bind PTm in PTm) -> PTm
 PApp : PTm -> PTm -> PTm
 PPair : PTm -> PTm -> PTm
 PProj : PTag -> PTm -> PTm
-PConst : nat -> PTm
+PConst : TTag -> PTm
+PUniv : nat -> PTm
+PBot : PTm

-Abs : Tm -> (bind Tm in Tm) -> Tm
+Abs : (bind Tm in Tm) -> Tm
 App : Tm -> Tm -> Tm
 Pair : Tm -> Tm -> Tm
 Proj : PTag -> Tm -> Tm
--- a/theories/Autosubst2/syntax.v
+++ b/theories/Autosubst2/syntax.v
@ -19,13 +19,29 @@ Proof.
 exact (eq_refl).
 Qed.

+Inductive TTag : Type :=
+  | TPi : TTag
+  | TSig : TTag.
+
+Lemma congr_TPi : TPi = TPi.
+Proof.
+exact (eq_refl).
+Qed.
+
+Lemma congr_TSig : TSig = TSig.
+Proof.
+exact (eq_refl).
+Qed.
+
 Inductive PTm : Type :=
  | VarPTm : nat -> PTm
  | PAbs : PTm -> PTm
  | PApp : PTm -> PTm -> PTm
  | PPair : PTm -> PTm -> PTm
  | PProj : PTag -> PTm -> PTm
-  | PConst : nat -> PTm.
+  | PConst : TTag -> PTm
+  | PUniv : nat -> PTm
+  | PBot : PTm.

 Lemma congr_PAbs {s0 : PTm} {t0 : PTm} (H0 : s0 = t0) : PAbs s0 = PAbs t0.
 Proof.
@ -53,12 +69,22 @@ exact (eq_trans (eq_trans eq_refl (ap (fun x => PProj x s1) H0))
         (ap (fun x => PProj t0 x) H1)).
 Qed.

-Lemma congr_PConst {s0 : nat} {t0 : nat} (H0 : s0 = t0) :
+Lemma congr_PConst {s0 : TTag} {t0 : TTag} (H0 : s0 = t0) :
  PConst s0 = PConst t0.
 Proof.
 exact (eq_trans eq_refl (ap (fun x => PConst x) H0)).
 Qed.

+Lemma congr_PUniv {s0 : nat} {t0 : nat} (H0 : s0 = t0) : PUniv s0 = PUniv t0.
+Proof.
+exact (eq_trans eq_refl (ap (fun x => PUniv x) H0)).
+Qed.
+
+Lemma congr_PBot : PBot = PBot.
+Proof.
+exact (eq_refl).
+Qed.
+
 Lemma upRen_PTm_PTm (xi : nat -> nat) : nat -> nat.
 Proof.
 exact (up_ren xi).
@ -72,6 +98,8 @@ Fixpoint ren_PTm (xi_PTm : nat -> nat) (s : PTm) {struct s} : PTm :=
  | PPair s0 s1 => PPair (ren_PTm xi_PTm s0) (ren_PTm xi_PTm s1)
  | PProj s0 s1 => PProj s0 (ren_PTm xi_PTm s1)
  | PConst s0 => PConst s0
+  | PUniv s0 => PUniv s0
+  | PBot => PBot
  end.

 Lemma up_PTm_PTm (sigma : nat -> PTm) : nat -> PTm.
@ -87,6 +115,8 @@ Fixpoint subst_PTm (sigma_PTm : nat -> PTm) (s : PTm) {struct s} : PTm :=
  | PPair s0 s1 => PPair (subst_PTm sigma_PTm s0) (subst_PTm sigma_PTm s1)
  | PProj s0 s1 => PProj s0 (subst_PTm sigma_PTm s1)
  | PConst s0 => PConst s0
+  | PUniv s0 => PUniv s0
+  | PBot => PBot
  end.

 Lemma upId_PTm_PTm (sigma : nat -> PTm) (Eq : forall x, sigma x = VarPTm x) :
@ -115,6 +145,8 @@ subst_PTm sigma_PTm s = s :=
        (idSubst_PTm sigma_PTm Eq_PTm s1)
  | PProj s0 s1 => congr_PProj (eq_refl s0) (idSubst_PTm sigma_PTm Eq_PTm s1)
  | PConst s0 => congr_PConst (eq_refl s0)
+  | PUniv s0 => congr_PUniv (eq_refl s0)
+  | PBot => congr_PBot
  end.

 Lemma upExtRen_PTm_PTm (xi : nat -> nat) (zeta : nat -> nat)
@ -145,6 +177,8 @@ ren_PTm xi_PTm s = ren_PTm zeta_PTm s :=
  | PProj s0 s1 =>
      congr_PProj (eq_refl s0) (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1)
  | PConst s0 => congr_PConst (eq_refl s0)
+  | PUniv s0 => congr_PUniv (eq_refl s0)
+  | PBot => congr_PBot
  end.

 Lemma upExt_PTm_PTm (sigma : nat -> PTm) (tau : nat -> PTm)
@ -176,6 +210,8 @@ subst_PTm sigma_PTm s = subst_PTm tau_PTm s :=
  | PProj s0 s1 =>
      congr_PProj (eq_refl s0) (ext_PTm sigma_PTm tau_PTm Eq_PTm s1)
  | PConst s0 => congr_PConst (eq_refl s0)
+  | PUniv s0 => congr_PUniv (eq_refl s0)
+  | PBot => congr_PBot
  end.

 Lemma up_ren_ren_PTm_PTm (xi : nat -> nat) (zeta : nat -> nat)
@ -206,6 +242,8 @@ Fixpoint compRenRen_PTm (xi_PTm : nat -> nat) (zeta_PTm : nat -> nat)
      congr_PProj (eq_refl s0)
        (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1)
  | PConst s0 => congr_PConst (eq_refl s0)
+  | PUniv s0 => congr_PUniv (eq_refl s0)
+  | PBot => congr_PBot
  end.

 Lemma up_ren_subst_PTm_PTm (xi : nat -> nat) (tau : nat -> PTm)
@ -240,6 +278,8 @@ Fixpoint compRenSubst_PTm (xi_PTm : nat -> nat) (tau_PTm : nat -> PTm)
      congr_PProj (eq_refl s0)
        (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1)
  | PConst s0 => congr_PConst (eq_refl s0)
+  | PUniv s0 => congr_PUniv (eq_refl s0)
+  | PBot => congr_PBot
  end.

 Lemma up_subst_ren_PTm_PTm (sigma : nat -> PTm) (zeta_PTm : nat -> nat)
@ -285,6 +325,8 @@ ren_PTm zeta_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s :=
      congr_PProj (eq_refl s0)
        (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1)
  | PConst s0 => congr_PConst (eq_refl s0)
+  | PUniv s0 => congr_PUniv (eq_refl s0)
+  | PBot => congr_PBot
  end.

 Lemma up_subst_subst_PTm_PTm (sigma : nat -> PTm) (tau_PTm : nat -> PTm)
@ -331,6 +373,8 @@ subst_PTm tau_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s :=
      congr_PProj (eq_refl s0)
        (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1)
  | PConst s0 => congr_PConst (eq_refl s0)
+  | PUniv s0 => congr_PUniv (eq_refl s0)
+  | PBot => congr_PBot
  end.

 Lemma renRen_PTm (xi_PTm : nat -> nat) (zeta_PTm : nat -> nat) (s : PTm) :
@ -420,6 +464,8 @@ Fixpoint rinst_inst_PTm (xi_PTm : nat -> nat) (sigma_PTm : nat -> PTm)
  | PProj s0 s1 =>
      congr_PProj (eq_refl s0) (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1)
  | PConst s0 => congr_PConst (eq_refl s0)
+  | PUniv s0 => congr_PUniv (eq_refl s0)
+  | PBot => congr_PBot
  end.

 Lemma rinstInst'_PTm (xi_PTm : nat -> nat) (s : PTm) :
@ -481,23 +527,9 @@ Proof.
 exact (fun x => eq_refl).
 Qed.

-Inductive TTag : Type :=
-  | TPi : TTag
-  | TSig : TTag.
-
-Lemma congr_TPi : TPi = TPi.
-Proof.
-exact (eq_refl).
-Qed.
-
-Lemma congr_TSig : TSig = TSig.
-Proof.
-exact (eq_refl).
-Qed.
-
 Inductive Tm : Type :=
  | VarTm : nat -> Tm
-  | Abs : Tm -> Tm -> Tm
+  | Abs : Tm -> Tm
  | App : Tm -> Tm -> Tm
  | Pair : Tm -> Tm -> Tm
  | Proj : PTag -> Tm -> Tm
@ -507,11 +539,9 @@ Inductive Tm : Type :=
  | Bool : Tm
  | If : Tm -> Tm -> Tm -> Tm.

-Lemma congr_Abs {s0 : Tm} {s1 : Tm} {t0 : Tm} {t1 : Tm} (H0 : s0 = t0)
-  (H1 : s1 = t1) : Abs s0 s1 = Abs t0 t1.
+Lemma congr_Abs {s0 : Tm} {t0 : Tm} (H0 : s0 = t0) : Abs s0 = Abs t0.
 Proof.
-exact (eq_trans (eq_trans eq_refl (ap (fun x => Abs x s1) H0))
-         (ap (fun x => Abs t0 x) H1)).
+exact (eq_trans eq_refl (ap (fun x => Abs x) H0)).
 Qed.

 Lemma congr_App {s0 : Tm} {s1 : Tm} {t0 : Tm} {t1 : Tm} (H0 : s0 = t0)
@ -576,7 +606,7 @@ Defined.
 Fixpoint ren_Tm (xi_Tm : nat -> nat) (s : Tm) {struct s} : Tm :=
  match s with
  | VarTm s0 => VarTm (xi_Tm s0)
-  | Abs s0 s1 => Abs (ren_Tm xi_Tm s0) (ren_Tm (upRen_Tm_Tm xi_Tm) s1)
+  | Abs s0 => Abs (ren_Tm (upRen_Tm_Tm xi_Tm) s0)
  | App s0 s1 => App (ren_Tm xi_Tm s0) (ren_Tm xi_Tm s1)
  | Pair s0 s1 => Pair (ren_Tm xi_Tm s0) (ren_Tm xi_Tm s1)
  | Proj s0 s1 => Proj s0 (ren_Tm xi_Tm s1)
@ -596,7 +626,7 @@ Defined.
 Fixpoint subst_Tm (sigma_Tm : nat -> Tm) (s : Tm) {struct s} : Tm :=
  match s with
  | VarTm s0 => sigma_Tm s0
-  | Abs s0 s1 => Abs (subst_Tm sigma_Tm s0) (subst_Tm (up_Tm_Tm sigma_Tm) s1)
+  | Abs s0 => Abs (subst_Tm (up_Tm_Tm sigma_Tm) s0)
  | App s0 s1 => App (subst_Tm sigma_Tm s0) (subst_Tm sigma_Tm s1)
  | Pair s0 s1 => Pair (subst_Tm sigma_Tm s0) (subst_Tm sigma_Tm s1)
  | Proj s0 s1 => Proj s0 (subst_Tm sigma_Tm s1)
@ -624,9 +654,8 @@ Fixpoint idSubst_Tm (sigma_Tm : nat -> Tm)
 subst_Tm sigma_Tm s = s :=
  match s with
  | VarTm s0 => Eq_Tm s0
-  | Abs s0 s1 =>
-      congr_Abs (idSubst_Tm sigma_Tm Eq_Tm s0)
-        (idSubst_Tm (up_Tm_Tm sigma_Tm) (upId_Tm_Tm _ Eq_Tm) s1)
+  | Abs s0 =>
+      congr_Abs (idSubst_Tm (up_Tm_Tm sigma_Tm) (upId_Tm_Tm _ Eq_Tm) s0)
  | App s0 s1 =>
      congr_App (idSubst_Tm sigma_Tm Eq_Tm s0) (idSubst_Tm sigma_Tm Eq_Tm s1)
  | Pair s0 s1 =>
@ -659,10 +688,10 @@ Fixpoint extRen_Tm (xi_Tm : nat -> nat) (zeta_Tm : nat -> nat)
 ren_Tm xi_Tm s = ren_Tm zeta_Tm s :=
  match s with
  | VarTm s0 => ap (VarTm) (Eq_Tm s0)
-  | Abs s0 s1 =>
-      congr_Abs (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0)
+  | Abs s0 =>
+      congr_Abs
        (extRen_Tm (upRen_Tm_Tm xi_Tm) (upRen_Tm_Tm zeta_Tm)
-           (upExtRen_Tm_Tm _ _ Eq_Tm) s1)
+           (upExtRen_Tm_Tm _ _ Eq_Tm) s0)
  | App s0 s1 =>
      congr_App (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0)
        (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1)
@ -698,10 +727,10 @@ Fixpoint ext_Tm (sigma_Tm : nat -> Tm) (tau_Tm : nat -> Tm)
 subst_Tm sigma_Tm s = subst_Tm tau_Tm s :=
  match s with
  | VarTm s0 => Eq_Tm s0
-  | Abs s0 s1 =>
-      congr_Abs (ext_Tm sigma_Tm tau_Tm Eq_Tm s0)
+  | Abs s0 =>
+      congr_Abs
        (ext_Tm (up_Tm_Tm sigma_Tm) (up_Tm_Tm tau_Tm) (upExt_Tm_Tm _ _ Eq_Tm)
-           s1)
+           s0)
  | App s0 s1 =>
      congr_App (ext_Tm sigma_Tm tau_Tm Eq_Tm s0)
        (ext_Tm sigma_Tm tau_Tm Eq_Tm s1)
@ -733,10 +762,10 @@ Fixpoint compRenRen_Tm (xi_Tm : nat -> nat) (zeta_Tm : nat -> nat)
 (s : Tm) {struct s} : ren_Tm zeta_Tm (ren_Tm xi_Tm s) = ren_Tm rho_Tm s :=
  match s with
  | VarTm s0 => ap (VarTm) (Eq_Tm s0)
-  | Abs s0 s1 =>
-      congr_Abs (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0)
+  | Abs s0 =>
+      congr_Abs
        (compRenRen_Tm (upRen_Tm_Tm xi_Tm) (upRen_Tm_Tm zeta_Tm)
-           (upRen_Tm_Tm rho_Tm) (up_ren_ren _ _ _ Eq_Tm) s1)
+           (upRen_Tm_Tm rho_Tm) (up_ren_ren _ _ _ Eq_Tm) s0)
  | App s0 s1 =>
      congr_App (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0)
        (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1)
@ -775,10 +804,10 @@ Fixpoint compRenSubst_Tm (xi_Tm : nat -> nat) (tau_Tm : nat -> Tm)
 subst_Tm tau_Tm (ren_Tm xi_Tm s) = subst_Tm theta_Tm s :=
  match s with
  | VarTm s0 => Eq_Tm s0
-  | Abs s0 s1 =>
-      congr_Abs (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0)
+  | Abs s0 =>
+      congr_Abs
        (compRenSubst_Tm (upRen_Tm_Tm xi_Tm) (up_Tm_Tm tau_Tm)
-           (up_Tm_Tm theta_Tm) (up_ren_subst_Tm_Tm _ _ _ Eq_Tm) s1)
+           (up_Tm_Tm theta_Tm) (up_ren_subst_Tm_Tm _ _ _ Eq_Tm) s0)
  | App s0 s1 =>
      congr_App (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0)
        (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s1)
@ -831,10 +860,10 @@ Fixpoint compSubstRen_Tm (sigma_Tm : nat -> Tm) (zeta_Tm : nat -> nat)
 ren_Tm zeta_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s :=
  match s with
  | VarTm s0 => Eq_Tm s0
-  | Abs s0 s1 =>
-      congr_Abs (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0)
+  | Abs s0 =>
+      congr_Abs
        (compSubstRen_Tm (up_Tm_Tm sigma_Tm) (upRen_Tm_Tm zeta_Tm)
-           (up_Tm_Tm theta_Tm) (up_subst_ren_Tm_Tm _ _ _ Eq_Tm) s1)
+           (up_Tm_Tm theta_Tm) (up_subst_ren_Tm_Tm _ _ _ Eq_Tm) s0)
  | App s0 s1 =>
      congr_App (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0)
        (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s1)
@ -887,10 +916,10 @@ Fixpoint compSubstSubst_Tm (sigma_Tm : nat -> Tm) (tau_Tm : nat -> Tm)
 subst_Tm tau_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s :=
  match s with
  | VarTm s0 => Eq_Tm s0
-  | Abs s0 s1 =>
-      congr_Abs (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0)
+  | Abs s0 =>
+      congr_Abs
        (compSubstSubst_Tm (up_Tm_Tm sigma_Tm) (up_Tm_Tm tau_Tm)
-           (up_Tm_Tm theta_Tm) (up_subst_subst_Tm_Tm _ _ _ Eq_Tm) s1)
+           (up_Tm_Tm theta_Tm) (up_subst_subst_Tm_Tm _ _ _ Eq_Tm) s0)
  | App s0 s1 =>
      congr_App (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0)
        (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s1)
@ -984,10 +1013,10 @@ Fixpoint rinst_inst_Tm (xi_Tm : nat -> nat) (sigma_Tm : nat -> Tm)
   : ren_Tm xi_Tm s = subst_Tm sigma_Tm s :=
  match s with
  | VarTm s0 => Eq_Tm s0
-  | Abs s0 s1 =>
-      congr_Abs (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0)
+  | Abs s0 =>
+      congr_Abs
        (rinst_inst_Tm (upRen_Tm_Tm xi_Tm) (up_Tm_Tm sigma_Tm)
-           (rinstInst_up_Tm_Tm _ _ Eq_Tm) s1)
+           (rinstInst_up_Tm_Tm _ _ Eq_Tm) s0)
  | App s0 s1 =>
      congr_App (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0)
        (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1)
--- a/theories/compile.v
+++ b/theories/compile.v
@ -1,47 +1,47 @@
-Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax fp_red.
+Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax fp_red.
 Require Import ssreflect ssrbool.
 From Hammer Require Import Tactics.
 From stdpp Require Import relations (rtc(..)).

 Module Compile.
-  Definition compileTag p := if p is TPi then 0 else 1.
-
-  Fixpoint F (a : Tm) : PTm :=
+  Fixpoint F {n} (a : Tm n) : Tm n :=
    match a with
-    | TBind p A B => PPair (PPair (PConst (compileTag p)) (F A)) (PAbs (F B))
-    | Univ i => PConst (3 + i)
-    | Abs _ a => PAbs (F a)
-    | App a b => PApp (F a) (F b)
-    | VarTm i => VarPTm i
-    | Pair a b => PPair (F a) (F b)
-    | Proj t a => PProj t (F a)
-    | If a b c => PApp (PApp (F a) (F b)) (F c)
-    | BVal b => if b then (PAbs (PAbs (VarPTm (shift var_zero)))) else (PAbs (PAbs (VarPTm var_zero)))
-    | Bool => PConst 2
+    | TBind p A B => Pair (Pair (Const p) (F A)) (Abs (F B))
+    | Const k => Const k
+    | Univ i => Univ i
+    | Abs a => Abs (F a)
+    | App a b => App (F a) (F b)
+    | VarTm i => VarTm i
+    | Pair a b => Pair (F a) (F b)
+    | Proj t a => Proj t (F a)
+    | Bot => Bot
+    | If a b c => App (App (F a) (F b)) (F c)
+    | BVal b => if b then (Abs (Abs (VarTm (shift var_zero)))) else (Abs (Abs (VarTm var_zero)))
+    | Bool => Bool
    end.

-  Lemma renaming (a : Tm) (ξ : nat -> nat) :
-    F (ren_Tm ξ a)= ren_PTm ξ (F a).
-  Proof. move : ξ. elim : a => //=; hauto lq:on. Qed.
+  Lemma renaming n m (a : Tm n) (ξ : fin n -> fin m) :
+    F (ren_Tm ξ a)= ren_Tm ξ (F a).
+  Proof. move : m ξ. elim : n  / a => //=; hauto lq:on. Qed.

  #[local]Hint Rewrite Compile.renaming : compile.

-  Lemma morphing (a : Tm) ρ0 ρ1 :
+  Lemma morphing n m (a : Tm n) (ρ0 ρ1 : fin n -> Tm m) :
    (forall i, ρ0 i = F (ρ1 i)) ->
-    subst_PTm ρ0 (F a) = F (subst_Tm ρ1 a).
+    subst_Tm ρ0 (F a) = F (subst_Tm ρ1 a).
  Proof.
-    move : ρ0 ρ1. elim : a =>//=.
-    - hauto lq:on inv:nat rew:db:compile unfold:funcomp.
+    move : m ρ0 ρ1. elim : n / a => n//=.
+    - hauto lq:on inv:option rew:db:compile unfold:funcomp.
    - hauto lq:on rew:off.
    - hauto lq:on rew:off.
    - hauto lq:on.
-    - hauto lq:on inv:nat rew:db:compile unfold:funcomp.
+    - hauto lq:on inv:option rew:db:compile unfold:funcomp.
    - hauto lq:on rew:off.
    - hauto lq:on rew:off.
  Qed.

-  Lemma substing b (a : Tm) :
-    subst_PTm (scons (F b) VarPTm) (F a) = F (subst_Tm (scons b VarTm) a).
+  Lemma substing n b (a : Tm (S n)) :
+    subst_Tm (scons (F b) VarTm) (F a) = F (subst_Tm (scons b VarTm) a).
  Proof.
    apply morphing.
    case => //=.
@ -53,55 +53,38 @@ End Compile.


 Module Join.
-  Definition R (a b : Tm) := join (Compile.F a) (Compile.F b).
+  Definition R {n} (a b : Tm n) := join (Compile.F a) (Compile.F b).

-  Lemma compileTagInj p0 p1 :
-    Compile.compileTag p0 = Compile.compileTag p1 -> p0 = p1.
-  Proof.
-    case : p0 ; case : p1 => //.
-  Qed.
-
-  Lemma BindInj p0 p1 (A0 A1 : Tm) B0 B1  :
+  Lemma BindInj n p0 p1 (A0 A1 : Tm n) B0 B1  :
    R (TBind p0 A0 B0) (TBind p1 A1 B1) -> p0 = p1 /\ R A0 A1 /\ R B0 B1.
  Proof.
    rewrite /R /= !join_pair_inj.
-    move => [[/join_const_inj /compileTagInj h0 h1] h2].
+    move => [[/join_const_inj h0 h1] h2].
    apply abs_eq in h2.
-    evar (t : PTm ).
-    have : join (PApp (ren_PTm shift (PAbs (Compile.F B1))) (VarPTm var_zero)) t by
+    evar (t : Tm (S n)).
+    have : join (App (ren_Tm shift (Abs (Compile.F B1))) (VarTm var_zero)) t by
      apply Join.FromPar; apply Par.AppAbs; auto using Par.refl.
-    subst t. rewrite -/ren_PTm.
-    move : h2. move /join_transitive => /[apply]. asimpl; rewrite subst_id => h2.
+    subst t. rewrite -/ren_Tm.
+    move : h2. move /join_transitive => /[apply]. asimpl => h2.
    tauto.
  Qed.

-  Lemma BindCong p A0 A1 B0 B1 :
-    R A0 A1 ->
-    R B0 B1 ->
-    R (TBind p A0 B0) (TBind p A1 B1).
-  Proof.
-    move => h0 h1. rewrite /R /=.
-    apply join_pair_inj.
-    split. apply join_pair_inj. split. apply join_refl. done.
-    by apply Join.AbsCong.
-  Qed.
+  Lemma UnivInj n i j : R (Univ i : Tm n) (Univ j) -> i = j.
+  Proof. hauto l:on use:join_univ_inj. Qed.

-  Lemma UnivInj i j : R (Univ i : Tm) (Univ j) -> i = j.
-  Proof. hauto l:on use:join_const_inj. Qed.
-
-  Lemma transitive (a b c : Tm) :
+  Lemma transitive n (a b c : Tm n) :
    R a b -> R b c -> R a c.
  Proof. hauto l:on use:join_transitive unfold:R. Qed.

-  Lemma symmetric (a b : Tm) :
+  Lemma symmetric n (a b : Tm n) :
    R a b -> R b a.
  Proof. hauto l:on use:join_symmetric. Qed.

-  Lemma reflexive (a : Tm) :
+  Lemma reflexive n (a : Tm n) :
    R a a.
  Proof. hauto l:on use:join_refl. Qed.

-  Lemma substing (a b : Tm) (ρ : nat -> Tm) :
+  Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) :
    R a b -> R (subst_Tm ρ a) (subst_Tm ρ b).
  Proof.
    rewrite /R.
@ -112,3 +95,92 @@ Module Join.
  Qed.

 End Join.
+
+Module Equiv.
+  Inductive R {n} : Tm n -> Tm n ->  Prop :=
+  (***************** Beta ***********************)
+  | AppAbs a b :
+    R (App (Abs a) b)  (subst_Tm (scons b VarTm) a)
+  | ProjPair p a b :
+    R (Proj p (Pair a b)) (if p is PL then a else b)
+
+  (****************** Eta ***********************)
+  | AppEta a :
+    R a (Abs (App (ren_Tm shift a) (VarTm var_zero)))
+  | PairEta a :
+    R a (Pair (Proj PL a) (Proj PR a))
+
+  (*************** Congruence ********************)
+  | Var i : R (VarTm i) (VarTm i)
+  | AbsCong a b :
+    R a b ->
+    R (Abs a) (Abs b)
+  | AppCong a0 a1 b0 b1 :
+    R a0 a1 ->
+    R b0 b1 ->
+    R (App a0 b0) (App a1 b1)
+  | PairCong a0 a1 b0 b1 :
+    R a0 a1 ->
+    R b0 b1 ->
+    R (Pair a0 b0) (Pair a1 b1)
+  | ProjCong p a0 a1 :
+    R a0 a1 ->
+    R (Proj p a0) (Proj p a1)
+  | BindCong p A0 A1 B0 B1:
+    R A0 A1 ->
+    R B0 B1 ->
+    R (TBind p A0 B0) (TBind p A1 B1)
+  | UnivCong i :
+    R (Univ i) (Univ i).
+End Equiv.
+
+Module EquivJoin.
+  Lemma FromEquiv n (a b : Tm n) : Equiv.R a b -> Join.R a b.
+  Proof.
+    move => h. elim : n a b /h => n.
+    - move => a b.
+      rewrite /Join.R /join /=.
+      eexists. split. apply relations.rtc_once.
+      apply Par.AppAbs; auto using Par.refl.
+      rewrite Compile.substing.
+      apply relations.rtc_refl.
+    - move => p a b.
+      apply Join.FromPar.
+      simpl. apply : Par.ProjPair'; auto using Par.refl.
+      case : p => //=.
+    - move => a. apply Join.FromPar => /=.
+      apply : Par.AppEta'; auto using Par.refl.
+      by autorewrite with compile.
+    - move => a. apply Join.FromPar => /=.
+      apply : Par.PairEta; auto using Par.refl.
+    - hauto l:on use:Join.FromPar, Par.Var.
+    - hauto lq:on use:Join.AbsCong.
+    - qauto l:on use:Join.AppCong.
+    - qauto l:on use:Join.PairCong.
+    - qauto use:Join.ProjCong.
+    - rewrite /Join.R => p A0 A1 B0 B1 _ hA _ hB /=.
+      sfirstorder use:Join.PairCong,Join.AbsCong,Join.FromPar,Par.ConstCong.
+    - hauto l:on.
+  Qed.
+End EquivJoin.
+
+Lemma compile_rpar n (a b : Tm n) : RPar'.R a b -> RPar'.R (Compile.F a) (Compile.F b).
+Proof.
+  move => h. elim : n a b /h.
+  - move => n  a0 a1 b0 b1 ha iha hb ihb /=.
+    rewrite -Compile.substing.
+    apply RPar'.AppAbs => //.
+  - hauto q:on use:RPar'.ProjPair'.
+  - qauto ctrs:RPar'.R.
+  - hauto lq:on ctrs:RPar'.R.
+  - hauto lq:on ctrs:RPar'.R.
+  - hauto lq:on ctrs:RPar'.R.
+  - hauto lq:on ctrs:RPar'.R.
+  - hauto lq:on ctrs:RPar'.R.
+  - hauto lq:on ctrs:RPar'.R.
+  - hauto lq:on ctrs:RPar'.R.
+  - hauto lq:on ctrs:RPar'.R.
+Qed.
+
+Lemma compile_rpars n (a b : Tm n) : rtc RPar'.R a b -> rtc RPar'.R (Compile.F a) (Compile.F b).
+Proof. induction 1; hauto lq:on ctrs:rtc use:compile_rpar. Qed.
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
--- a/theories/typing.v
+++ b/theories/typing.v
@ -1,93 +1,251 @@
-Require Import Autosubst2.core Autosubst2.unscoped compile Autosubst2.syntax ssreflect.
-From Hammer Require Import Tactics.
+Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax.

 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 lookup : nat -> list Tm -> Tm -> Prop :=
-| here A Γ : lookup 0 (cons A Γ) (ren_Tm shift A)
-| there i Γ A B :
-  lookup i Γ A ->
-  lookup (S i) (cons B Γ) (ren_Tm shift A).
-
-Lemma lookup_deter i Γ A B :
-  lookup i Γ A ->
-  lookup i Γ B ->
-  A = B.
-Proof. move => h. move : B. induction h; hauto lq:on inv:lookup. Qed.
-
-Lemma here' A Γ U : U = ren_Tm shift A -> lookup 0 (A :: Γ) U.
-Proof.  move => ->. apply here. Qed.
-
-Lemma there' i Γ A B U : U = ren_Tm 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).
-
-
-Inductive Wt : list Tm -> Tm -> Tm -> Prop :=
+Inductive Wt : list PTm -> PTm -> PTm -> Prop :=
 | T_Var i Γ A :
  ⊢ Γ ->
  lookup i Γ A ->
-  Γ ⊢ VarTm i ∈ A
+  Γ ⊢ VarPTm i ∈ A

-| T_Bind Γ i p A B :
-  Γ ⊢ A ∈ Univ i ->
-  cons A Γ ⊢ B ∈ Univ i ->
-  Γ ⊢ TBind p A B ∈ Univ i
+| T_Bind Γ i p (A : PTm) (B : PTm) :
+  Γ ⊢ A ∈ PUniv i ->
+  cons A Γ ⊢ B ∈ PUniv i ->
+  Γ ⊢ PBind p A B ∈ PUniv i

-| T_Abs Γ a A B i :
-  Γ ⊢ TBind TPi A B ∈ (Univ i) ->
+| T_Abs Γ (a : PTm) A B i :
+  Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
  (cons A Γ) ⊢ a ∈ B ->
-  Γ ⊢ Abs A a ∈ TBind TPi A B
+  Γ ⊢ PAbs a ∈ PBind PPi A B

-| T_App Γ b a A B :
-  Γ ⊢ b ∈ TBind TPi A B ->
+| T_App Γ (b a : PTm) A B :
+  Γ ⊢ b ∈ PBind PPi A B ->
  Γ ⊢ a ∈ A ->
-  Γ ⊢ App b a ∈ subst_Tm (scons a VarTm) B
+  Γ ⊢ PApp b a ∈ subst_PTm (scons a VarPTm) B

-| T_Pair Γ (a b : Tm) A B i :
-  Γ ⊢ TBind TSig A B ∈ (Univ i) ->
+| T_Pair Γ (a b : PTm) A B i :
+  Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
  Γ ⊢ a ∈ A ->
-  Γ ⊢ b ∈ subst_Tm (scons a VarTm) B ->
-  Γ ⊢ Pair a b ∈ TBind TSig A B
+  Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B ->
+  Γ ⊢ PPair a b ∈ PBind PSig A B

-| T_Proj1 Γ (a : Tm) A B :
-  Γ ⊢ a ∈ TBind TSig A B ->
-  Γ ⊢ Proj PL a ∈ A
+| T_Proj1 Γ (a : PTm) A B :
+  Γ ⊢ a ∈ PBind PSig A B ->
+  Γ ⊢ PProj PL a ∈ A

-| T_Proj2 Γ (a : Tm) A B :
-  Γ ⊢ a ∈ TBind TSig A B ->
-  Γ ⊢ Proj PR a ∈ subst_Tm (scons (Proj PL a) VarTm) 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 Γ i :
  ⊢ Γ ->
-  Γ ⊢ Univ i ∈ Univ (S i)
+  Γ ⊢ PUniv i ∈ PUniv (S i)

-| T_Conv Γ (a : Tm) A B i :
+| T_Nat Γ i :
+  ⊢ Γ ->
+  Γ ⊢ PNat ∈ PUniv i
+
+| T_Zero Γ :
+  ⊢ Γ ->
+  Γ ⊢ PZero ∈ PNat
+
+| T_Suc Γ (a : PTm) :
+  Γ ⊢ a ∈ PNat ->
+  Γ ⊢ PSuc a ∈ PNat
+
+| T_Ind Γ P (a : PTm) b c i :
+  cons PNat Γ ⊢ P ∈ PUniv i ->
+  Γ ⊢ a ∈ PNat ->
+  Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) 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 Γ (a : PTm) A B :
  Γ ⊢ a ∈ A ->
-  Γ ⊢ B ∈ Univ i ->
-  Join.R A B ->
+  Γ ⊢ A ≲ B ->
  Γ ⊢ a ∈ B

-with Wff : list Tm -> Prop :=
+with Eq : list PTm -> PTm -> PTm -> PTm -> Prop :=
+(* Structural *)
+| E_Refl Γ (a : PTm ) A :
+  Γ ⊢ a ∈ A ->
+  Γ ⊢ a ≡ a ∈ A
+
+| E_Symmetric Γ (a b : PTm) A :
+  Γ ⊢ a ≡ b ∈ A ->
+  Γ ⊢ b ≡ a ∈ A
+
+| E_Transitive Γ (a b c : PTm) A :
+  Γ ⊢ a ≡ b ∈ A ->
+  Γ ⊢ b ≡ c ∈ A ->
+  Γ ⊢ a ≡ c ∈ A
+
+(* Congruence *)
+| E_Bind Γ i p (A0 A1 : PTm) B0 B1 :
+  Γ ⊢ A0 ∈ PUniv i ->
+  Γ ⊢ A0 ≡ A1 ∈ PUniv i ->
+  (cons A0 Γ) ⊢ B0 ≡ B1 ∈ PUniv i ->
+  Γ ⊢ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv i
+
+| E_Abs Γ (a b : PTm) A B i :
+  Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
+  (cons A Γ) ⊢ a ≡ b ∈ B ->
+  Γ ⊢ PAbs a ≡ PAbs b ∈ PBind PPi 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 Γ (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 Γ (a b : PTm) A B :
+  Γ ⊢ a ≡ b ∈ PBind PSig A B ->
+  Γ ⊢ PProj PL a ≡ PProj PL b ∈ A
+
+| 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 Γ 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 ->
+  (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 Γ (a b : PTm) :
+  Γ ⊢ a ≡ b ∈ PNat ->
+  Γ ⊢ PSuc a ≡ PSuc b ∈ PNat
+
+| E_Conv Γ (a b : PTm) A B :
+  Γ ⊢ a ≡ b ∈ A ->
+  Γ ⊢ A ≲ B ->
+  Γ ⊢ a ≡ b ∈ B
+
+(* Beta *)
+| E_AppAbs Γ (a : PTm) b A B i:
+  Γ ⊢ PBind PPi A B ∈ PUniv i ->
+  Γ ⊢ b ∈ A ->
+  (cons A Γ) ⊢ a ∈ B ->
+  Γ ⊢ PApp (PAbs a) b ≡ subst_PTm (scons b VarPTm) a ∈ subst_PTm (scons b VarPTm ) B
+
+| 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 Γ (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 Γ P i (b : PTm) c :
+  (cons PNat Γ) ⊢ P ∈ PUniv i ->
+  Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) 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 Γ P (a : PTm) b c i :
+  (cons PNat Γ) ⊢ P ∈ PUniv i ->
+  Γ ⊢ a ∈ PNat ->
+  Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) 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 Γ (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 Γ (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 : list PTm -> PTm -> PTm -> Prop :=
+(* Structural *)
+| Su_Transitive Γ (A B C : PTm) :
+  Γ ⊢ A ≲ B ->
+  Γ ⊢ B ≲ C ->
+  Γ ⊢ A ≲ C
+
+(* Congruence *)
+| Su_Univ Γ i j :
+  ⊢ Γ ->
+  i <= j ->
+  Γ ⊢ PUniv i ≲ PUniv j
+
+| Su_Pi Γ (A0 A1 : PTm) B0 B1 i :
+  Γ ⊢ A0 ∈ PUniv i ->
+  Γ ⊢ A1 ≲ A0 ->
+  (cons A0 Γ) ⊢ B0 ≲ B1 ->
+  Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1
+
+| Su_Sig Γ (A0 A1 : PTm) B0 B1 i :
+  Γ ⊢ A1 ∈ PUniv i ->
+  Γ ⊢ A0 ≲ A1 ->
+  (cons A1 Γ) ⊢ B0 ≲ B1 ->
+  Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1
+
+(* Injecting from equalities *)
+| Su_Eq Γ (A : PTm) B i  :
+  Γ ⊢ A ≡ B ∈ PUniv i ->
+  Γ ⊢ A ≲ B
+
+(* Projection axioms *)
+| Su_Pi_Proj1 Γ (A0 A1 : PTm) B0 B1 :
+  Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 ->
+  Γ ⊢ A1 ≲ A0
+
+| Su_Sig_Proj1 Γ (A0 A1 : PTm) B0 B1 :
+  Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1 ->
+  Γ ⊢ A0 ≲ A1
+
+| 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 Γ (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 : list PTm -> Prop :=
 | Wff_Nil :
  ⊢ nil
-| Wff_Cons Γ (A : Tm) i :
+| Wff_Cons Γ (A : PTm) i :
  ⊢ Γ ->
-  Γ ⊢ A ∈ Univ i ->
+  Γ ⊢ A ∈ PUniv i ->
  (* -------------------------------- *)
  ⊢ (cons A Γ)

 where
-"Γ ⊢ a ∈ A" := (Wt Γ a A) and "⊢ Γ" := (Wff Γ).
+"Γ ⊢ a ∈ A" := (Wt Γ a A) and "⊢ Γ" := (Wff Γ) and "Γ ⊢ a ≡ b ∈ A" := (Eq Γ a b A) and "Γ ⊢ A ≲ B" := (LEq Γ A B).

 Scheme wf_ind := Induction for Wff Sort Prop
-  with wt_ind := Induction for Wt Sort Prop.
+  with wt_ind := Induction for Wt Sort Prop
+  with eq_ind := Induction for Eq Sort Prop
+  with le_ind := Induction for LEq Sort Prop.

-Combined Scheme wt_mutual from wf_ind, wt_ind.
+Combined Scheme wt_mutual from wf_ind, wt_ind, eq_ind, le_ind.

 (* Lemma lem : *)
-(*   (forall n (Γ : fin n -> Tm n), ⊢ Γ -> ...) /\ *)
-(*   (forall n Γ (a A : Tm n), Γ ⊢ a ∈ A -> ...)  /\ *)
+(*   (forall n (Γ : fin n -> PTm n), ⊢ Γ -> ...) /\ *)
+(*   (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 -> ...). *)
 (* Proof. apply wt_mutual. ... *)
--- a/theories/typing_properties.v
+++ b/theories/typing_properties.v
@ -1,134 +0,0 @@
-Require Import Autosubst2.core Autosubst2.unscoped compile Autosubst2.syntax ssreflect typing.
-From Hammer Require Import Tactics.
-
-Lemma Bind_Inv Γ p A B U :
-  Γ ⊢ TBind p A B ∈ U ->
-  exists i, Γ ⊢ A ∈ Univ i /\ cons A Γ ⊢ B ∈ Univ i /\ Join.R (Univ i) U.
-Proof.
-  move E : (TBind p A B) => u hu.
-  move : p A B E.
-  elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive.
-Qed.
-
-Lemma Univ_Inv Γ i  U :
-  Γ ⊢ Univ i ∈ U ->
-  Γ ⊢ Univ i ∈ Univ (S i) /\ Join.R (Univ (S i)) U.
-Proof.
-  move E : (Univ i) => u hu.
-  move : i E.
-  elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive.
-Qed.
-
-Lemma App_Inv Γ b a U :
-  Γ ⊢ App b a ∈ U ->
-  exists A B, Γ ⊢ b ∈ TBind TPi A B /\ Γ ⊢ a ∈ A /\ Join.R (subst_Tm (scons a VarTm) B) U.
-Proof.
-  move E : (App b a) => u hu.
-  move : b a E.
-  elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive.
-Qed.
-
-Lemma Abs_Inv Γ A a U :
-  Γ ⊢ Abs A a ∈ U ->
-  exists B, cons A Γ ⊢ a ∈ B /\ Join.R (TBind TPi A B) U.
-Proof.
-  move E : (Abs A a) => u hu.
-  move : A a E.
-  elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive.
-Qed.
-
-Lemma Var_Inv Γ i U :
-  Γ ⊢ VarTm i ∈ U ->
-  exists A, lookup i Γ A /\ Join.R A U.
-Proof.
-  move E : (VarTm i) => u hu.
-  move : i E.
-  elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive.
-Qed.
-
-Lemma Pair_Inv Γ a b U :
-  Γ ⊢ Pair a b ∈ U ->
-  exists A B, Γ ⊢ a ∈ A /\ Γ ⊢ b ∈ subst_Tm (scons a VarTm) B /\ Join.R (TBind TSig A B) U.
-Proof.
-  move E : (Pair a b ) => u hu.
-  move : a b E.
-  elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive.
-Qed.
-
-Lemma ProjL_Inv Γ a U :
-  Γ ⊢ Proj PL a ∈ U ->
-  exists A B, Γ ⊢ a ∈ TBind TSig A B /\ Join.R A U.
-Proof.
-  move E : (Proj PL a) => u hu.
-  move : a E.
-  elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive.
-Qed.
-
-Lemma ProjR_Inv Γ a U :
-  Γ ⊢ Proj PR a ∈ U ->
-  exists A B, Γ ⊢ a ∈ TBind TSig A B /\ Join.R (subst_Tm (scons (Proj PL a) VarTm) B) U.
-Proof.
-  move E : (Proj PR a) => u hu.
-  move : a E.
-  elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive.
-Qed.
-
-Lemma ctx_wff_mutual :
-  (forall Γ, ⊢ Γ -> True) /\
-  (forall Γ a A, Γ ⊢ a ∈ A -> ⊢ Γ).
-Proof. apply wt_mutual => //=. Qed.
-
-Lemma lookup_deter i Γ A A0 :
-  lookup i Γ A ->
-  lookup i Γ A0 -> A = A0.
-Proof.
-  move => h. move : A0. elim : i Γ A / h; hauto lq:on inv:lookup.
-Qed.
-
-Lemma wt_unique :
-  (forall Γ, ⊢ Γ -> True) /\
-  (forall Γ a A, Γ ⊢ a ∈ A -> forall B, Γ ⊢ a ∈ B -> Join.R A B).
-Proof.
-  apply wt_mutual => //=.
-  - move => i Γ A hΓ _ hl B.
-    move /Var_Inv.
-    move => [A0 [h0 h1]].
-    move : hl h0.
-    move : lookup_deter; repeat move/[apply]. move => ?. by subst.
-  - move => Γ i p A B hA ihA hB ihB U.
-    move /Bind_Inv => [j][ih0][ih1]ih2.
-    apply ihB in ih1.
-    move /Join.UnivInj in ih1. by subst.
-  - move => Γ a A B i hP ihP ha iha U.
-    move /Abs_Inv => [B0][ha']hJ.
-    move /iha in ha' => {iha}.
-    apply : Join.transitive; eauto.
-    apply Join.BindCong; eauto using Join.reflexive.
-  - move => Γ b a A B hb ihb ha iha U.
-    move /App_Inv. move => [A0][B0][hb'][ha']hU.
-    apply ihb in hb' => {ihb}.
-    move /Join.BindInj : hb'.
-    move => [_][hJ0]hJ1.
-    apply : Join.transitive; eauto.
-    by apply Join.substing.
-  - move => Γ a b A B i hS ihS ha iha hb ihb U.
-    move /Pair_Inv.
-    move => [A0][B0][{}/iha ha'][{}/ihb hb']hJ.
-    apply : Join.transitive; eauto.
-    apply Join.BindCong; eauto.
-    admit.
-  - move => Γ a A B ha iha U.
-    move /ProjL_Inv.
-    move => [A0][B0][{}/iha ha0]hU.
-    apply Join.BindInj in ha0.
-    decompose record ha0.
-    eauto using Join.transitive.
-  - move => Γ a A B ha iha U /ProjR_Inv [A0][B0][{}/iha /Join.BindInj ha'].
-    decompose record ha'.
-    move => h. apply : Join.transitive; eauto.
-    by apply Join.substing.
-  - move => Γ i hΓ _ B /Univ_Inv. tauto.
-  - move => Γ a A B i ha iha hb ihb.
-    move => h0 B0 {}/iha ha'.
-    eauto using Join.symmetric, Join.transitive.
-Admitted.