Finish all cases of type unique except for pair formation

syntax.sig

@@ -14,11 +14,9 @@ PAbs : (bind PTm in PTm) -> PTm
 PApp : PTm -> PTm -> PTm
 PPair : PTm -> PTm -> PTm
 PProj : PTag -> PTm -> PTm
-PConst : TTag -> PTm
+PConst : nat -> PTm
-PUniv : nat -> PTm
-PBot : PTm
 
-Abs : (bind Tm in Tm) -> Tm
+Abs : Tm -> (bind Tm in Tm) -> Tm
 App : Tm -> Tm -> Tm
 Pair : Tm -> Tm -> Tm
 Proj : PTag -> Tm -> Tm

theories/Autosubst2/syntax.v

@@ -19,29 +19,13 @@ Proof.
 exact (eq_refl).
 Qed.
 
-Inductive TTag : Type :=
-  | TPi : TTag
-  | TSig : TTag.
-
-Lemma congr_TPi : TPi = TPi.
-Proof.
-exact (eq_refl).
-Qed.
-
-Lemma congr_TSig : TSig = TSig.
-Proof.
-exact (eq_refl).
-Qed.
-
 Inductive PTm : Type :=
   | VarPTm : nat -> PTm
   | PAbs : PTm -> PTm
   | PApp : PTm -> PTm -> PTm
   | PPair : PTm -> PTm -> PTm
   | PProj : PTag -> PTm -> PTm
-  | PConst : TTag -> PTm
+  | PConst : nat -> PTm.
-  | PUniv : nat -> PTm
-  | PBot : PTm.
 
 Lemma congr_PAbs {s0 : PTm} {t0 : PTm} (H0 : s0 = t0) : PAbs s0 = PAbs t0.
 Proof.
@@ -69,22 +53,12 @@ exact (eq_trans (eq_trans eq_refl (ap (fun x => PProj x s1) H0))
          (ap (fun x => PProj t0 x) H1)).
 Qed.
 
-Lemma congr_PConst {s0 : TTag} {t0 : TTag} (H0 : s0 = t0) :
+Lemma congr_PConst {s0 : nat} {t0 : nat} (H0 : s0 = t0) :
   PConst s0 = PConst t0.
 Proof.
 exact (eq_trans eq_refl (ap (fun x => PConst x) H0)).
 Qed.
 
-Lemma congr_PUniv {s0 : nat} {t0 : nat} (H0 : s0 = t0) : PUniv s0 = PUniv t0.
-Proof.
-exact (eq_trans eq_refl (ap (fun x => PUniv x) H0)).
-Qed.
-
-Lemma congr_PBot : PBot = PBot.
-Proof.
-exact (eq_refl).
-Qed.
-
 Lemma upRen_PTm_PTm (xi : nat -> nat) : nat -> nat.
 Proof.
 exact (up_ren xi).
@@ -98,8 +72,6 @@ Fixpoint ren_PTm (xi_PTm : nat -> nat) (s : PTm) {struct s} : PTm :=
   | PPair s0 s1 => PPair (ren_PTm xi_PTm s0) (ren_PTm xi_PTm s1)
   | PProj s0 s1 => PProj s0 (ren_PTm xi_PTm s1)
   | PConst s0 => PConst s0
-  | PUniv s0 => PUniv s0
-  | PBot => PBot
   end.
 
 Lemma up_PTm_PTm (sigma : nat -> PTm) : nat -> PTm.
@@ -115,8 +87,6 @@ Fixpoint subst_PTm (sigma_PTm : nat -> PTm) (s : PTm) {struct s} : PTm :=
   | PPair s0 s1 => PPair (subst_PTm sigma_PTm s0) (subst_PTm sigma_PTm s1)
   | PProj s0 s1 => PProj s0 (subst_PTm sigma_PTm s1)
   | PConst s0 => PConst s0
-  | PUniv s0 => PUniv s0
-  | PBot => PBot
   end.
 
 Lemma upId_PTm_PTm (sigma : nat -> PTm) (Eq : forall x, sigma x = VarPTm x) :
@@ -145,8 +115,6 @@ subst_PTm sigma_PTm s = s :=
         (idSubst_PTm sigma_PTm Eq_PTm s1)
   | PProj s0 s1 => congr_PProj (eq_refl s0) (idSubst_PTm sigma_PTm Eq_PTm s1)
   | PConst s0 => congr_PConst (eq_refl s0)
-  | PUniv s0 => congr_PUniv (eq_refl s0)
-  | PBot => congr_PBot
   end.
 
 Lemma upExtRen_PTm_PTm (xi : nat -> nat) (zeta : nat -> nat)
@@ -177,8 +145,6 @@ ren_PTm xi_PTm s = ren_PTm zeta_PTm s :=
   | PProj s0 s1 =>
       congr_PProj (eq_refl s0) (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1)
   | PConst s0 => congr_PConst (eq_refl s0)
-  | PUniv s0 => congr_PUniv (eq_refl s0)
-  | PBot => congr_PBot
   end.
 
 Lemma upExt_PTm_PTm (sigma : nat -> PTm) (tau : nat -> PTm)
@@ -210,8 +176,6 @@ subst_PTm sigma_PTm s = subst_PTm tau_PTm s :=
   | PProj s0 s1 =>
       congr_PProj (eq_refl s0) (ext_PTm sigma_PTm tau_PTm Eq_PTm s1)
   | PConst s0 => congr_PConst (eq_refl s0)
-  | PUniv s0 => congr_PUniv (eq_refl s0)
-  | PBot => congr_PBot
   end.
 
 Lemma up_ren_ren_PTm_PTm (xi : nat -> nat) (zeta : nat -> nat)
@@ -242,8 +206,6 @@ Fixpoint compRenRen_PTm (xi_PTm : nat -> nat) (zeta_PTm : nat -> nat)
       congr_PProj (eq_refl s0)
         (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1)
   | PConst s0 => congr_PConst (eq_refl s0)
-  | PUniv s0 => congr_PUniv (eq_refl s0)
-  | PBot => congr_PBot
   end.
 
 Lemma up_ren_subst_PTm_PTm (xi : nat -> nat) (tau : nat -> PTm)
@@ -278,8 +240,6 @@ Fixpoint compRenSubst_PTm (xi_PTm : nat -> nat) (tau_PTm : nat -> PTm)
       congr_PProj (eq_refl s0)
         (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1)
   | PConst s0 => congr_PConst (eq_refl s0)
-  | PUniv s0 => congr_PUniv (eq_refl s0)
-  | PBot => congr_PBot
   end.
 
 Lemma up_subst_ren_PTm_PTm (sigma : nat -> PTm) (zeta_PTm : nat -> nat)
@@ -325,8 +285,6 @@ ren_PTm zeta_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s :=
       congr_PProj (eq_refl s0)
         (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1)
   | PConst s0 => congr_PConst (eq_refl s0)
-  | PUniv s0 => congr_PUniv (eq_refl s0)
-  | PBot => congr_PBot
   end.
 
 Lemma up_subst_subst_PTm_PTm (sigma : nat -> PTm) (tau_PTm : nat -> PTm)
@@ -373,8 +331,6 @@ subst_PTm tau_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s :=
       congr_PProj (eq_refl s0)
         (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1)
   | PConst s0 => congr_PConst (eq_refl s0)
-  | PUniv s0 => congr_PUniv (eq_refl s0)
-  | PBot => congr_PBot
   end.
 
 Lemma renRen_PTm (xi_PTm : nat -> nat) (zeta_PTm : nat -> nat) (s : PTm) :
@@ -464,8 +420,6 @@ Fixpoint rinst_inst_PTm (xi_PTm : nat -> nat) (sigma_PTm : nat -> PTm)
   | PProj s0 s1 =>
       congr_PProj (eq_refl s0) (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1)
   | PConst s0 => congr_PConst (eq_refl s0)
-  | PUniv s0 => congr_PUniv (eq_refl s0)
-  | PBot => congr_PBot
   end.
 
 Lemma rinstInst'_PTm (xi_PTm : nat -> nat) (s : PTm) :
@@ -527,9 +481,23 @@ 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
+  | Abs : Tm -> Tm -> Tm
   | App : Tm -> Tm -> Tm
   | Pair : Tm -> Tm -> Tm
   | Proj : PTag -> Tm -> Tm
@@ -539,9 +507,11 @@ Inductive Tm : Type :=
   | Bool : Tm
   | If : Tm -> Tm -> Tm -> Tm.
 
-Lemma congr_Abs {s0 : Tm} {t0 : Tm} (H0 : s0 = t0) : Abs s0 = Abs t0.
+Lemma congr_Abs {s0 : Tm} {s1 : Tm} {t0 : Tm} {t1 : Tm} (H0 : s0 = t0)
+  (H1 : s1 = t1) : Abs s0 s1 = Abs t0 t1.
 Proof.
-exact (eq_trans eq_refl (ap (fun x => Abs x) H0)).
+exact (eq_trans (eq_trans eq_refl (ap (fun x => Abs x s1) H0))
+         (ap (fun x => Abs t0 x) H1)).
 Qed.
 
 Lemma congr_App {s0 : Tm} {s1 : Tm} {t0 : Tm} {t1 : Tm} (H0 : s0 = t0)
@@ -606,7 +576,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 => Abs (ren_Tm (upRen_Tm_Tm xi_Tm) s0)
+  | Abs s0 s1 => Abs (ren_Tm xi_Tm s0) (ren_Tm (upRen_Tm_Tm xi_Tm) s1)
   | 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)
@@ -626,7 +596,7 @@ Defined.
 Fixpoint subst_Tm (sigma_Tm : nat -> Tm) (s : Tm) {struct s} : Tm :=
   match s with
   | VarTm s0 => sigma_Tm s0
-  | Abs s0 => Abs (subst_Tm (up_Tm_Tm sigma_Tm) s0)
+  | Abs s0 s1 => Abs (subst_Tm sigma_Tm s0) (subst_Tm (up_Tm_Tm sigma_Tm) s1)
   | 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)
@@ -654,8 +624,9 @@ Fixpoint idSubst_Tm (sigma_Tm : nat -> Tm)
 subst_Tm sigma_Tm s = s :=
   match s with
   | VarTm s0 => Eq_Tm s0
-  | Abs s0 =>
+  | Abs s0 s1 =>
-      congr_Abs (idSubst_Tm (up_Tm_Tm sigma_Tm) (upId_Tm_Tm _ Eq_Tm) s0)
+      congr_Abs (idSubst_Tm sigma_Tm Eq_Tm s0)
+        (idSubst_Tm (up_Tm_Tm sigma_Tm) (upId_Tm_Tm _ Eq_Tm) s1)
   | App s0 s1 =>
       congr_App (idSubst_Tm sigma_Tm Eq_Tm s0) (idSubst_Tm sigma_Tm Eq_Tm s1)
   | Pair s0 s1 =>
@@ -688,10 +659,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 =>
+  | Abs s0 s1 =>
-      congr_Abs
+      congr_Abs (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0)
         (extRen_Tm (upRen_Tm_Tm xi_Tm) (upRen_Tm_Tm zeta_Tm)
-           (upExtRen_Tm_Tm _ _ Eq_Tm) s0)
+           (upExtRen_Tm_Tm _ _ Eq_Tm) s1)
   | App s0 s1 =>
       congr_App (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0)
         (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1)
@@ -727,10 +698,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 =>
+  | Abs s0 s1 =>
-      congr_Abs
+      congr_Abs (ext_Tm sigma_Tm tau_Tm Eq_Tm s0)
         (ext_Tm (up_Tm_Tm sigma_Tm) (up_Tm_Tm tau_Tm) (upExt_Tm_Tm _ _ Eq_Tm)
-           s0)
+           s1)
   | App s0 s1 =>
       congr_App (ext_Tm sigma_Tm tau_Tm Eq_Tm s0)
         (ext_Tm sigma_Tm tau_Tm Eq_Tm s1)
@@ -762,10 +733,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 =>
+  | Abs s0 s1 =>
-      congr_Abs
+      congr_Abs (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0)
         (compRenRen_Tm (upRen_Tm_Tm xi_Tm) (upRen_Tm_Tm zeta_Tm)
-           (upRen_Tm_Tm rho_Tm) (up_ren_ren _ _ _ Eq_Tm) s0)
+           (upRen_Tm_Tm rho_Tm) (up_ren_ren _ _ _ Eq_Tm) s1)
   | 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)
@@ -804,10 +775,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 =>
+  | Abs s0 s1 =>
-      congr_Abs
+      congr_Abs (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0)
         (compRenSubst_Tm (upRen_Tm_Tm xi_Tm) (up_Tm_Tm tau_Tm)
-           (up_Tm_Tm theta_Tm) (up_ren_subst_Tm_Tm _ _ _ Eq_Tm) s0)
+           (up_Tm_Tm theta_Tm) (up_ren_subst_Tm_Tm _ _ _ Eq_Tm) s1)
   | 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)
@@ -860,10 +831,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 =>
+  | Abs s0 s1 =>
-      congr_Abs
+      congr_Abs (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0)
         (compSubstRen_Tm (up_Tm_Tm sigma_Tm) (upRen_Tm_Tm zeta_Tm)
-           (up_Tm_Tm theta_Tm) (up_subst_ren_Tm_Tm _ _ _ Eq_Tm) s0)
+           (up_Tm_Tm theta_Tm) (up_subst_ren_Tm_Tm _ _ _ Eq_Tm) s1)
   | 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)
@@ -916,10 +887,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 =>
+  | Abs s0 s1 =>
-      congr_Abs
+      congr_Abs (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0)
         (compSubstSubst_Tm (up_Tm_Tm sigma_Tm) (up_Tm_Tm tau_Tm)
-           (up_Tm_Tm theta_Tm) (up_subst_subst_Tm_Tm _ _ _ Eq_Tm) s0)
+           (up_Tm_Tm theta_Tm) (up_subst_subst_Tm_Tm _ _ _ Eq_Tm) s1)
   | 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)
@@ -1013,10 +984,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 =>
+  | Abs s0 s1 =>
-      congr_Abs
+      congr_Abs (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0)
         (rinst_inst_Tm (upRen_Tm_Tm xi_Tm) (up_Tm_Tm sigma_Tm)
-           (rinstInst_up_Tm_Tm _ _ Eq_Tm) s0)
+           (rinstInst_up_Tm_Tm _ _ Eq_Tm) s1)
   | 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)

theories/compile.v

@@ -1,47 +1,47 @@
-Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax fp_red.
+Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax fp_red.
 Require Import ssreflect ssrbool.
 From Hammer Require Import Tactics.
 From stdpp Require Import relations (rtc(..)).
 
 Module Compile.
-  Fixpoint F {n} (a : Tm n) : Tm n :=
+  Definition compileTag p := if p is TPi then 0 else 1.
+
+  Fixpoint F (a : Tm) : PTm :=
     match a with
-    | TBind p A B => Pair (Pair (Const p) (F A)) (Abs (F B))
+    | TBind p A B => PPair (PPair (PConst (compileTag p)) (F A)) (PAbs (F B))
-    | Const k => Const k
+    | Univ i => PConst (3 + i)
-    | Univ i => Univ i
+    | Abs _ a => PAbs (F a)
-    | Abs a => Abs (F a)
+    | App a b => PApp (F a) (F b)
-    | App a b => App (F a) (F b)
+    | VarTm i => VarPTm i
-    | VarTm i => VarTm i
+    | Pair a b => PPair (F a) (F b)
-    | Pair a b => Pair (F a) (F b)
+    | Proj t a => PProj t (F a)
-    | Proj t a => Proj t (F a)
+    | If a b c => PApp (PApp (F a) (F b)) (F c)
-    | Bot => Bot
+    | BVal b => if b then (PAbs (PAbs (VarPTm (shift var_zero)))) else (PAbs (PAbs (VarPTm var_zero)))
-    | If a b c => App (App (F a) (F b)) (F c)
+    | Bool => PConst 2
-    | BVal b => if b then (Abs (Abs (VarTm (shift var_zero)))) else (Abs (Abs (VarTm var_zero)))
-    | Bool => Bool
     end.
 
-  Lemma renaming n m (a : Tm n) (ξ : fin n -> fin m) :
+  Lemma renaming (a : Tm) (ξ : nat -> nat) :
-    F (ren_Tm ξ a)= ren_Tm ξ (F a).
+    F (ren_Tm ξ a)= ren_PTm ξ (F a).
-  Proof. move : m ξ. elim : n  / a => //=; hauto lq:on. Qed.
+  Proof. move : ξ. elim : a => //=; hauto lq:on. Qed.
 
   #[local]Hint Rewrite Compile.renaming : compile.
 
-  Lemma morphing n m (a : Tm n) (ρ0 ρ1 : fin n -> Tm m) :
+  Lemma morphing (a : Tm) ρ0 ρ1 :
     (forall i, ρ0 i = F (ρ1 i)) ->
-    subst_Tm ρ0 (F a) = F (subst_Tm ρ1 a).
+    subst_PTm ρ0 (F a) = F (subst_Tm ρ1 a).
   Proof.
-    move : m ρ0 ρ1. elim : n / a => n//=.
+    move : ρ0 ρ1. elim : a =>//=.
-    - hauto lq:on inv:option rew:db:compile unfold:funcomp.
+    - hauto lq:on inv:nat rew:db:compile unfold:funcomp.
     - hauto lq:on rew:off.
     - hauto lq:on rew:off.
     - hauto lq:on.
-    - hauto lq:on inv:option rew:db:compile unfold:funcomp.
+    - hauto lq:on inv:nat rew:db:compile unfold:funcomp.
     - hauto lq:on rew:off.
     - hauto lq:on rew:off.
   Qed.
 
-  Lemma substing n b (a : Tm (S n)) :
+  Lemma substing b (a : Tm) :
-    subst_Tm (scons (F b) VarTm) (F a) = F (subst_Tm (scons b VarTm) a).
+    subst_PTm (scons (F b) VarPTm) (F a) = F (subst_Tm (scons b VarTm) a).
   Proof.
     apply morphing.
     case => //=.
@@ -53,38 +53,55 @@ End Compile.
 
 
 Module Join.
-  Definition R {n} (a b : Tm n) := join (Compile.F a) (Compile.F b).
+  Definition R (a b : Tm) := join (Compile.F a) (Compile.F b).
 
-  Lemma BindInj n p0 p1 (A0 A1 : Tm n) B0 B1  :
+  Lemma compileTagInj p0 p1 :
+    Compile.compileTag p0 = Compile.compileTag p1 -> p0 = p1.
+  Proof.
+    case : p0 ; case : p1 => //.
+  Qed.
+
+  Lemma BindInj p0 p1 (A0 A1 : Tm) B0 B1  :
     R (TBind p0 A0 B0) (TBind p1 A1 B1) -> p0 = p1 /\ R A0 A1 /\ R B0 B1.
   Proof.
     rewrite /R /= !join_pair_inj.
-    move => [[/join_const_inj h0 h1] h2].
+    move => [[/join_const_inj /compileTagInj h0 h1] h2].
     apply abs_eq in h2.
-    evar (t : Tm (S n)).
+    evar (t : PTm ).
-    have : join (App (ren_Tm shift (Abs (Compile.F B1))) (VarTm var_zero)) t by
+    have : join (PApp (ren_PTm shift (PAbs (Compile.F B1))) (VarPTm var_zero)) t by
       apply Join.FromPar; apply Par.AppAbs; auto using Par.refl.
-    subst t. rewrite -/ren_Tm.
+    subst t. rewrite -/ren_PTm.
-    move : h2. move /join_transitive => /[apply]. asimpl => h2.
+    move : h2. move /join_transitive => /[apply]. asimpl; rewrite subst_id => h2.
     tauto.
   Qed.
 
-  Lemma UnivInj n i j : R (Univ i : Tm n) (Univ j) -> i = j.
+  Lemma BindCong p A0 A1 B0 B1 :
-  Proof. hauto l:on use:join_univ_inj. Qed.
+    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 transitive n (a b c : Tm n) :
+  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) :
     R a b -> R b c -> R a c.
   Proof. hauto l:on use:join_transitive unfold:R. Qed.
 
-  Lemma symmetric n (a b : Tm n) :
+  Lemma symmetric (a b : Tm) :
     R a b -> R b a.
   Proof. hauto l:on use:join_symmetric. Qed.
 
-  Lemma reflexive n (a : Tm n) :
+  Lemma reflexive (a : Tm) :
     R a a.
   Proof. hauto l:on use:join_refl. Qed.
 
-  Lemma substing n m (a b : Tm n) (ρ : fin n -> Tm m) :
+  Lemma substing (a b : Tm) (ρ : nat -> Tm) :
     R a b -> R (subst_Tm ρ a) (subst_Tm ρ b).
   Proof.
     rewrite /R.
@@ -95,92 +112,3 @@ Module Join.
   Qed.
 
 End Join.
-
-Module Equiv.
-  Inductive R {n} : Tm n -> Tm n ->  Prop :=
-  (***************** Beta ***********************)
-  | AppAbs a b :
-    R (App (Abs a) b)  (subst_Tm (scons b VarTm) a)
-  | ProjPair p a b :
-    R (Proj p (Pair a b)) (if p is PL then a else b)
-
-  (****************** Eta ***********************)
-  | AppEta a :
-    R a (Abs (App (ren_Tm shift a) (VarTm var_zero)))
-  | PairEta a :
-    R a (Pair (Proj PL a) (Proj PR a))
-
-  (*************** Congruence ********************)
-  | Var i : R (VarTm i) (VarTm i)
-  | AbsCong a b :
-    R a b ->
-    R (Abs a) (Abs b)
-  | AppCong a0 a1 b0 b1 :
-    R a0 a1 ->
-    R b0 b1 ->
-    R (App a0 b0) (App a1 b1)
-  | PairCong a0 a1 b0 b1 :
-    R a0 a1 ->
-    R b0 b1 ->
-    R (Pair a0 b0) (Pair a1 b1)
-  | ProjCong p a0 a1 :
-    R a0 a1 ->
-    R (Proj p a0) (Proj p a1)
-  | BindCong p A0 A1 B0 B1:
-    R A0 A1 ->
-    R B0 B1 ->
-    R (TBind p A0 B0) (TBind p A1 B1)
-  | UnivCong i :
-    R (Univ i) (Univ i).
-End Equiv.
-
-Module EquivJoin.
-  Lemma FromEquiv n (a b : Tm n) : Equiv.R a b -> Join.R a b.
-  Proof.
-    move => h. elim : n a b /h => n.
-    - move => a b.
-      rewrite /Join.R /join /=.
-      eexists. split. apply relations.rtc_once.
-      apply Par.AppAbs; auto using Par.refl.
-      rewrite Compile.substing.
-      apply relations.rtc_refl.
-    - move => p a b.
-      apply Join.FromPar.
-      simpl. apply : Par.ProjPair'; auto using Par.refl.
-      case : p => //=.
-    - move => a. apply Join.FromPar => /=.
-      apply : Par.AppEta'; auto using Par.refl.
-      by autorewrite with compile.
-    - move => a. apply Join.FromPar => /=.
-      apply : Par.PairEta; auto using Par.refl.
-    - hauto l:on use:Join.FromPar, Par.Var.
-    - hauto lq:on use:Join.AbsCong.
-    - qauto l:on use:Join.AppCong.
-    - qauto l:on use:Join.PairCong.
-    - qauto use:Join.ProjCong.
-    - rewrite /Join.R => p A0 A1 B0 B1 _ hA _ hB /=.
-      sfirstorder use:Join.PairCong,Join.AbsCong,Join.FromPar,Par.ConstCong.
-    - hauto l:on.
-  Qed.
-End EquivJoin.
-
-Lemma compile_rpar n (a b : Tm n) : RPar'.R a b -> RPar'.R (Compile.F a) (Compile.F b).
-Proof.
-  move => h. elim : n a b /h.
-  - move => n  a0 a1 b0 b1 ha iha hb ihb /=.
-    rewrite -Compile.substing.
-    apply RPar'.AppAbs => //.
-  - hauto q:on use:RPar'.ProjPair'.
-  - qauto ctrs:RPar'.R.
-  - hauto lq:on ctrs:RPar'.R.
-  - hauto lq:on ctrs:RPar'.R.
-  - hauto lq:on ctrs:RPar'.R.
-  - hauto lq:on ctrs:RPar'.R.
-  - hauto lq:on ctrs:RPar'.R.
-  - hauto lq:on ctrs:RPar'.R.
-  - hauto lq:on ctrs:RPar'.R.
-  - hauto lq:on ctrs:RPar'.R.
-Qed.
-
-Lemma compile_rpars n (a b : Tm n) : rtc RPar'.R a b -> rtc RPar'.R (Compile.F a) (Compile.F b).
-Proof. induction 1; hauto lq:on ctrs:rtc use:compile_rpar. Qed.

theories/typing.v

@@ -1,251 +1,93 @@
-Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax.
+Require Import Autosubst2.core Autosubst2.unscoped compile Autosubst2.syntax ssreflect.
+From Hammer Require Import Tactics.
 
 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 : list PTm -> PTm -> PTm -> Prop :=
+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 :=
 | T_Var i Γ A :
   ⊢ Γ ->
   lookup i Γ A ->
-  Γ ⊢ VarPTm i ∈ A
+  Γ ⊢ VarTm i ∈ A
 
-| T_Bind Γ i p (A : PTm) (B : PTm) :
+| T_Bind Γ i p A B :
-  Γ ⊢ A ∈ PUniv i ->
+  Γ ⊢ A ∈ Univ i ->
-  cons A Γ ⊢ B ∈ PUniv i ->
+  cons A Γ ⊢ B ∈ Univ i ->
-  Γ ⊢ PBind p A B ∈ PUniv i
+  Γ ⊢ TBind p A B ∈ Univ i
 
-| T_Abs Γ (a : PTm) A B i :
+| T_Abs Γ a A B i :
-  Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
+  Γ ⊢ TBind TPi A B ∈ (Univ i) ->
   (cons A Γ) ⊢ a ∈ B ->
-  Γ ⊢ PAbs a ∈ PBind PPi A B
+  Γ ⊢ Abs A a ∈ TBind TPi A B
 
-| T_App Γ (b a : PTm) A B :
+| T_App Γ b a A B :
-  Γ ⊢ b ∈ PBind PPi A B ->
+  Γ ⊢ b ∈ TBind TPi A B ->
   Γ ⊢ a ∈ A ->
-  Γ ⊢ PApp b a ∈ subst_PTm (scons a VarPTm) B
+  Γ ⊢ App b a ∈ subst_Tm (scons a VarTm) B
 
-| T_Pair Γ (a b : PTm) A B i :
+| T_Pair Γ (a b : Tm) A B i :
-  Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
+  Γ ⊢ TBind TSig A B ∈ (Univ i) ->
   Γ ⊢ a ∈ A ->
-  Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B ->
+  Γ ⊢ b ∈ subst_Tm (scons a VarTm) B ->
-  Γ ⊢ PPair a b ∈ PBind PSig A B
+  Γ ⊢ Pair a b ∈ TBind TSig A B
 
-| T_Proj1 Γ (a : PTm) A B :
+| T_Proj1 Γ (a : Tm) A B :
-  Γ ⊢ a ∈ PBind PSig A B ->
+  Γ ⊢ a ∈ TBind TSig A B ->
-  Γ ⊢ PProj PL a ∈ A
+  Γ ⊢ Proj PL a ∈ A
 
-| T_Proj2 Γ (a : PTm) A B :
+| T_Proj2 Γ (a : Tm) A B :
-  Γ ⊢ a ∈ PBind PSig A B ->
+  Γ ⊢ a ∈ TBind TSig A B ->
-  Γ ⊢ PProj PR a ∈ subst_PTm (scons (PProj PL a) VarPTm) B
+  Γ ⊢ Proj PR a ∈ subst_Tm (scons (Proj PL a) VarTm) B
 
 | T_Univ Γ i :
   ⊢ Γ ->
-  Γ ⊢ PUniv i ∈ PUniv (S i)
+  Γ ⊢ Univ i ∈ Univ (S i)
 
-| T_Nat Γ i :
+| T_Conv Γ (a : Tm) A B 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 ->
-  Γ ⊢ A ≲ B ->
+  Γ ⊢ B ∈ Univ i ->
+  Join.R A B ->
   Γ ⊢ a ∈ B
 
-with Eq : list PTm -> PTm -> PTm -> PTm -> Prop :=
+with Wff : list Tm -> 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 : PTm) i :
+| Wff_Cons Γ (A : Tm) i :
   ⊢ Γ ->
-  Γ ⊢ A ∈ PUniv i ->
+  Γ ⊢ A ∈ Univ i ->
   (* -------------------------------- *)
   ⊢ (cons A Γ)
 
 where
-"Γ ⊢ a ∈ A" := (Wt Γ a A) and "⊢ Γ" := (Wff Γ) and "Γ ⊢ a ≡ b ∈ A" := (Eq Γ a b A) and "Γ ⊢ A ≲ B" := (LEq Γ A B).
+"Γ ⊢ a ∈ A" := (Wt Γ a A) and "⊢ Γ" := (Wff Γ).
 
 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, eq_ind, le_ind.
+Combined Scheme wt_mutual from wf_ind, wt_ind.
 
 (* Lemma lem : *)
-(*   (forall n (Γ : fin n -> PTm n), ⊢ Γ -> ...) /\ *)
+(*   (forall n (Γ : fin n -> Tm n), ⊢ Γ -> ...) /\ *)
-(*   (forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> ...)  /\ *)
+(*   (forall n Γ (a A : Tm 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. ... *)

theories/typing_properties.v

@@ -0,0 +1,134 @@
+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.