Finish the conversion proof completely

Reviewed-on: #1

theories/admissible.v

@@ -0,0 +1,69 @@
+Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax common typing structural.
+From Hammer Require Import Tactics.
+Require Import ssreflect.
+Require Import Psatz.
+Require Import Coq.Logic.FunctionalExtensionality.
+
+Derive Dependent Inversion wff_inv with (forall n (Γ : fin n -> PTm n), ⊢ Γ) Sort Prop.
+
+Lemma Wff_Cons_Inv n Γ (A : PTm n) :
+  ⊢ funcomp (ren_PTm shift) (scons A Γ) ->
+  ⊢ Γ /\ exists i, Γ ⊢ A ∈ PUniv i.
+Proof.
+  elim /wff_inv => //= _.
+  move => n0 Γ0 A0 i0 hΓ0 hA0 [? _]. subst.
+  Equality.simplify_dep_elim.
+  have h : forall i, (funcomp (ren_PTm shift) (scons A0 Γ0)) i = (funcomp (ren_PTm shift) (scons A Γ)) i by scongruence.
+  move /(_ var_zero) : (h).
+  rewrite /funcomp. asimpl.
+  move /ren_injective. move /(_ ltac:(hauto lq:on rew:off inv:option)).
+  move => ?. subst.
+  have : Γ0 = Γ. extensionality i.
+  move /(_ (Some i)) : h.
+  rewrite /funcomp. asimpl.
+  move /ren_injective. move /(_ ltac:(hauto lq:on rew:off inv:option)).
+  done.
+  move => ?. subst. sfirstorder.
+Qed.
+
+Lemma T_Abs n Γ (a : PTm (S n)) A B :
+  funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B ->
+  Γ ⊢ PAbs a ∈ PBind PPi A B.
+Proof.
+  move => ha.
+  have [i hB] : exists i, funcomp (ren_PTm shift) (scons A Γ) ⊢ B ∈ PUniv i by sfirstorder use:regularity.
+  have hΓ : ⊢ funcomp (ren_PTm shift) (scons A Γ) by sfirstorder use:wff_mutual.
+  move /Wff_Cons_Inv : hΓ => [hΓ][j]hA.
+  hauto lq:on rew:off use:T_Bind', typing.T_Abs.
+Qed.
+
+Lemma E_Bind n Γ i p (A0 A1 : PTm n) B0 B1 :
+  Γ ⊢ A0 ≡ A1 ∈ PUniv i ->
+  funcomp (ren_PTm shift) (scons A0 Γ) ⊢ B0 ≡ B1 ∈ PUniv i ->
+  Γ ⊢ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv i.
+Proof.
+  move => h0 h1.
+  have : Γ ⊢ A0 ∈ PUniv i by hauto l:on use:regularity.
+  have : ⊢ Γ by sfirstorder use:wff_mutual.
+  move : E_Bind h0 h1; repeat move/[apply].
+  firstorder.
+Qed.
+
+Lemma E_App n Γ (b0 b1 a0 a1 : PTm n) A B :
+  Γ ⊢ b0 ≡ b1 ∈ PBind PPi A B ->
+  Γ ⊢ a0 ≡ a1 ∈ A ->
+  Γ ⊢ PApp b0 a0 ≡ PApp b1 a1 ∈ subst_PTm (scons a0 VarPTm) B.
+Proof.
+  move => h.
+  have [i] : exists i, Γ ⊢ PBind PPi A B ∈ PUniv i by hauto l:on use:regularity.
+  move : E_App h. by repeat move/[apply].
+Qed.
+
+Lemma E_Proj2 n Γ (a b : PTm n) A B :
+  Γ ⊢ a ≡ b ∈ PBind PSig A B ->
+  Γ ⊢ PProj PR a ≡ PProj PR b ∈ subst_PTm (scons (PProj PL a) VarPTm) B.
+Proof.
+  move => h.
+  have [i] : exists i, Γ ⊢ PBind PSig A B ∈ PUniv i by hauto l:on use:regularity.
+  move : E_Proj2 h; by repeat move/[apply].
+Qed.

theories/common.v

@@ -0,0 +1,97 @@
+Require Import Autosubst2.fintype Autosubst2.syntax ssreflect.
+From Ltac2 Require Ltac2.
+Import Ltac2.Notations.
+Import Ltac2.Control.
+From Hammer Require Import Tactics.
+
+Definition renaming_ok {n m} (Γ : fin n -> PTm n) (Δ : fin m -> PTm m) (ξ : fin m -> fin n) :=
+  forall (i : fin m), ren_PTm ξ (Δ i) = Γ (ξ i).
+
+Local Ltac2 rec solve_anti_ren () :=
+  let x := Fresh.in_goal (Option.get (Ident.of_string "x")) in
+  intro $x;
+  lazy_match! Constr.type (Control.hyp x) with
+  | fin _ -> _ _ => (ltac1:(case;hauto q:on depth:2))
+  | _ => solve_anti_ren ()
+  end.
+
+Local Ltac solve_anti_ren := ltac2:(Control.enter solve_anti_ren).
+
+Lemma up_injective n m (ξ : fin n -> fin m) :
+  (forall i j, ξ i = ξ j -> i = j) ->
+  forall i j, (upRen_PTm_PTm ξ)  i = (upRen_PTm_PTm ξ) j -> i = j.
+Proof.
+  sblast inv:option.
+Qed.
+
+Lemma ren_injective n m (a b : PTm n) (ξ : fin n -> fin m) :
+  (forall i j, ξ i = ξ j -> i = j) ->
+  ren_PTm ξ a = ren_PTm ξ b ->
+  a = b.
+Proof.
+  move : m ξ b.
+  elim : n / a => //; try solve_anti_ren.
+
+  move => n a iha m ξ []//=.
+  move => u hξ [h].
+  apply iha in h. by subst.
+  destruct i, j=>//=.
+  hauto l:on.
+
+  move => n p A ihA B ihB m ξ []//=.
+  move => b A0 B0  hξ [?]. subst.
+  move => ?. have ? : A0 = A by firstorder. subst.
+  move => ?. have : B = B0. apply : ihB; eauto.
+  sauto.
+  congruence.
+Qed.
+
+Definition ishf {n} (a : PTm n) :=
+  match a with
+  | PPair _ _ => true
+  | PAbs _ => true
+  | PUniv _ => true
+  | PBind _ _ _ => true
+  | _ => false
+  end.
+
+Fixpoint ishne {n} (a : PTm n) :=
+  match a with
+  | VarPTm _ => true
+  | PApp a _ => ishne a
+  | PProj _ a => ishne a
+  | PBot => true
+  | _ => false
+  end.
+
+Definition isbind {n} (a : PTm n) := if a is PBind _ _ _ then true else false.
+
+Definition isuniv {n} (a : PTm n) := if a is PUniv _ then true else false.
+
+Definition ispair {n} (a : PTm n) :=
+  match a with
+  | PPair _ _ => true
+  | _ => false
+  end.
+
+Definition isabs {n} (a : PTm n) :=
+  match a with
+  | PAbs _ => true
+  | _ => false
+  end.
+
+Definition ishf_ren n m (a : PTm n)  (ξ : fin n -> fin m) :
+  ishf (ren_PTm ξ a) = ishf a.
+Proof. case : a => //=. Qed.
+
+Definition isabs_ren n m (a : PTm n)  (ξ : fin n -> fin m) :
+  isabs (ren_PTm ξ a) = isabs a.
+Proof. case : a => //=. Qed.
+
+Definition ispair_ren n m (a : PTm n)  (ξ : fin n -> fin m) :
+  ispair (ren_PTm ξ a) = ispair a.
+Proof. case : a => //=. Qed.
+
+Definition ishne_ren n m (a : PTm n)  (ξ : fin n -> fin m) :
+  ishne (ren_PTm ξ a) = ishne a.
+Proof. move : m ξ. elim : n / a => //=. Qed.

theories/fp_red.v

@@ -8,7 +8,7 @@ Require Import Arith.Wf_nat (well_founded_lt_compat).
 Require Import Psatz.
 From stdpp Require Import relations (rtc (..), rtc_once, rtc_r, sn).
 From Hammer Require Import Tactics.
-Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax.
+Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax common.
 Require Import Btauto.
 Require Import Cdcl.Itauto.
 
@@ -20,7 +20,7 @@ Ltac2 spec_refl () :=
                try (specialize $h with (1 := eq_refl))
            end)  (Control.hyps ()).
 
-Ltac spec_refl := ltac2:(spec_refl ()).
+Ltac spec_refl := ltac2:(Control.enter spec_refl).
 
 Module EPar.
   Inductive R {n} : PTm n -> PTm n ->  Prop :=
@@ -166,41 +166,6 @@ with TRedSN {n} : PTm n -> PTm n -> Prop :=
 
 Derive Dependent Inversion tred_inv with (forall n (a b : PTm n), TRedSN a b) Sort Prop.
 
-Definition ishf {n} (a : PTm n) :=
-  match a with
-  | PPair _ _ => true
-  | PAbs _ => true
-  | PUniv _ => true
-  | PBind _ _ _ => true
-  | _ => false
-  end.
-Definition isbind {n} (a : PTm n) := if a is PBind _ _ _ then true else false.
-
-Definition isuniv {n} (a : PTm n) := if a is PUniv _ then true else false.
-
-Definition ispair {n} (a : PTm n) :=
-  match a with
-  | PPair _ _ => true
-  | _ => false
-  end.
-
-Definition isabs {n} (a : PTm n) :=
-  match a with
-  | PAbs _ => true
-  | _ => false
-  end.
-
-Definition ishf_ren n m (a : PTm n)  (ξ : fin n -> fin m) :
-  ishf (ren_PTm ξ a) = ishf a.
-Proof. case : a => //=. Qed.
-
-Definition isabs_ren n m (a : PTm n)  (ξ : fin n -> fin m) :
-  isabs (ren_PTm ξ a) = isabs a.
-Proof. case : a => //=. Qed.
-
-Definition ispair_ren n m (a : PTm n)  (ξ : fin n -> fin m) :
-  ispair (ren_PTm ξ a) = ispair a.
-Proof. case : a => //=. Qed.
 
 Lemma PProj_imp n p a :
   @ishf n a ->
@@ -297,6 +262,12 @@ end.
 Lemma ne_nf n a : @ne n a -> nf a.
 Proof. elim : a => //=. Qed.
 
+Lemma ne_nf_ren n m (a : PTm n) (ξ : fin n -> fin m) :
+  (ne a <-> ne (ren_PTm ξ a)) /\ (nf a <-> nf (ren_PTm ξ a)).
+Proof.
+  move : m ξ. elim : n / a => //=; solve [hauto b:on].
+Qed.
+
 Inductive TRedSN' {n} (a : PTm n) : PTm n -> Prop :=
 | T_Refl :
   TRedSN' a a
@@ -328,6 +299,12 @@ Proof.
   apply N_β'. by asimpl. eauto.
 Qed.
 
+Lemma ne_nf_embed n (a : PTm n) :
+  (ne a -> SNe a) /\ (nf a -> SN a).
+Proof.
+  elim : n  / a => //=; hauto qb:on ctrs:SNe, SN.
+Qed.
+
 #[export]Hint Constructors SN SNe TRedSN : sn.
 
 Ltac2 rec solve_anti_ren () :=
@@ -871,12 +848,6 @@ Module RReds.
 End RReds.
 
 
-Lemma ne_nf_ren n m (a : PTm n) (ξ : fin n -> fin m) :
-  (ne a <-> ne (ren_PTm ξ a)) /\ (nf a <-> nf (ren_PTm ξ a)).
-Proof.
-  move : m ξ. elim : n / a => //=; solve [hauto b:on].
-Qed.
-
 Module NeEPar.
   Inductive R_nonelim {n} : PTm n -> PTm n ->  Prop :=
   (****************** Eta ***********************)
@@ -1408,35 +1379,6 @@ Module ERed.
   (*   destruct a. *)
   (*   exact (ξ f). *)
 
-  Lemma up_injective n m (ξ : fin n -> fin m) :
-    (forall i j, ξ i = ξ j -> i = j) ->
-    forall i j, (upRen_PTm_PTm ξ)  i = (upRen_PTm_PTm ξ) j -> i = j.
-  Proof.
-    sblast inv:option.
-  Qed.
-
-  Lemma ren_injective n m (a b : PTm n) (ξ : fin n -> fin m) :
-    (forall i j, ξ i = ξ j -> i = j) ->
-    ren_PTm ξ a = ren_PTm ξ b ->
-    a = b.
-  Proof.
-    move : m ξ b.
-    elim : n / a => //; try solve_anti_ren.
-
-    move => n a iha m ξ []//=.
-    move => u hξ [h].
-    apply iha in h. by subst.
-    destruct i, j=>//=.
-    hauto l:on.
-
-    move => n p A ihA B ihB m ξ []//=.
-    move => b A0 B0  hξ [?]. subst.
-    move => ?. have ? : A0 = A by firstorder. subst.
-    move => ?. have : B = B0. apply : ihB; eauto.
-    sauto.
-    congruence.
-  Qed.
-
   Lemma AppEta' n a u :
     u = (@PApp (S n) (ren_PTm shift a) (VarPTm var_zero)) ->
     R (PAbs u) a.
@@ -1504,6 +1446,14 @@ Module ERed.
     all : hauto lq:on ctrs:R.
   Qed.
 
+  Lemma nf_preservation n (a b : PTm n) :
+    ERed.R a b -> (nf a -> nf b) /\ (ne a -> ne b).
+  Proof.
+    move => h.
+    elim : n a b /h => //=;
+                        hauto lqb:on use:ne_nf_ren,ne_nf.
+  Qed.
+
 End ERed.
 
 Module EReds.
@@ -1574,10 +1524,70 @@ Module EReds.
     induction 1; hauto lq:on ctrs:rtc use:ERed.substing.
   Qed.
 
+  Lemma app_inv n (a0 b0 C : PTm n) :
+    rtc ERed.R (PApp a0 b0) C ->
+    exists a1 b1, C = PApp a1 b1 /\
+               rtc ERed.R a0 a1 /\
+               rtc ERed.R b0 b1.
+  Proof.
+    move E : (PApp a0 b0) => u hu.
+    move : a0 b0 E.
+    elim : u C / hu.
+    - hauto lq:on ctrs:rtc.
+    - move => a b c ha ha' iha a0 b0 ?. subst.
+      hauto lq:on rew:off ctrs:rtc, ERed.R inv:ERed.R.
+  Qed.
+
+  Lemma proj_inv n p (a C : PTm n) :
+    rtc ERed.R (PProj p a) C ->
+    exists c, C = PProj p c /\ rtc ERed.R a c.
+  Proof.
+    move E : (PProj p a) => u hu.
+    move : p a E.
+    elim : u C /hu;
+      hauto q:on ctrs:rtc,ERed.R inv:ERed.R.
+  Qed.
+
+  Lemma bind_inv n p (A : PTm n) B C :
+    rtc ERed.R (PBind p A B) C ->
+    exists A0 B0, C = PBind p A0 B0 /\ rtc ERed.R A A0 /\ rtc ERed.R B B0.
+  Proof.
+    move E : (PBind p A B) => u hu.
+    move : p A B E.
+    elim : u C / hu.
+    hauto lq:on ctrs:rtc.
+    hauto lq:on rew:off ctrs:rtc, ERed.R inv:ERed.R, rtc.
+  Qed.
+
 End EReds.
 
 #[export]Hint Constructors ERed.R RRed.R EPar.R : red.
 
+Module EJoin.
+  Definition R {n} (a b : PTm n) := exists c, rtc ERed.R a c /\ rtc ERed.R b c.
+
+  Lemma hne_app_inj n (a0 b0 a1 b1 : PTm n) :
+    R (PApp a0 b0) (PApp a1 b1) ->
+    R a0 a1 /\ R b0 b1.
+  Proof.
+    hauto lq:on use:EReds.app_inv.
+  Qed.
+
+  Lemma hne_proj_inj n p0 p1 (a0 a1 : PTm n) :
+    R (PProj p0 a0) (PProj p1 a1) ->
+    p0 = p1 /\ R a0 a1.
+  Proof.
+    hauto lq:on rew:off use:EReds.proj_inv.
+  Qed.
+
+  Lemma bind_inj n p0 p1 (A0 A1 : PTm n) B0 B1 :
+    R (PBind p0 A0 B0) (PBind p1 A1 B1) ->
+    p0 = p1 /\ R A0 A1 /\ R B0 B1.
+  Proof.
+    hauto lq:on rew:off use:EReds.bind_inv.
+  Qed.
+
+End EJoin.
 
 Module RERed.
   Inductive R {n} : PTm n -> PTm n ->  Prop :=
@@ -1666,9 +1676,17 @@ Module RERed.
     hauto q:on use:ToBetaEta, FromBeta, FromEta, RRed.substing, ERed.substing.
   Qed.
 
+  Lemma hne_preservation n (a b : PTm n) :
+    RERed.R a b -> ishne a -> ishne b.
+  Proof.  induction 1; sfirstorder. Qed.
+
 End RERed.
 
 Module REReds.
+  Lemma hne_preservation n (a b : PTm n) :
+    rtc RERed.R a b -> ishne a -> ishne b.
+  Proof.  induction 1; eauto using RERed.hne_preservation, rtc_refl, rtc. Qed.
+
   Lemma sn_preservation n (a b : PTm n) :
     rtc RERed.R a b ->
     SN a ->
@@ -1750,12 +1768,83 @@ Module REReds.
     hauto lq:on rew:off ctrs:rtc inv:RERed.R.
   Qed.
 
+  Lemma var_inv n (i : fin n) C :
+    rtc RERed.R (VarPTm i) C ->
+    C = VarPTm i.
+  Proof.
+    move E : (VarPTm i) => u hu.
+    move : i E. elim : u C /hu; hauto lq:on rew:off inv:RERed.R.
+  Qed.
+
+  Lemma hne_app_inv n (a0 b0 C : PTm n) :
+    rtc RERed.R (PApp a0 b0) C ->
+    ishne a0 ->
+    exists a1 b1, C = PApp a1 b1 /\
+               rtc RERed.R a0 a1 /\
+               rtc RERed.R b0 b1.
+  Proof.
+    move E : (PApp a0 b0) => u hu.
+    move : a0 b0 E.
+    elim : u C / hu.
+    - hauto lq:on ctrs:rtc.
+    - move => a b c ha ha' iha a0 b0 ?. subst.
+      hauto lq:on rew:off ctrs:rtc, RERed.R use:RERed.hne_preservation inv:RERed.R.
+  Qed.
+
+  Lemma hne_proj_inv n p (a C : PTm n) :
+    rtc RERed.R (PProj p a) C ->
+    ishne a ->
+    exists c, C = PProj p c /\ rtc RERed.R a c.
+  Proof.
+    move E : (PProj p a) => u hu.
+    move : p a E.
+    elim : u C /hu;
+      hauto q:on ctrs:rtc,RERed.R use:RERed.hne_preservation inv:RERed.R.
+  Qed.
+
   Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) :
     rtc RERed.R a b -> rtc RERed.R (subst_PTm ρ a) (subst_PTm ρ b).
   Proof.
     induction 1; hauto lq:on ctrs:rtc use:RERed.substing.
   Qed.
 
+
+  Lemma cong_up n m (ρ0 ρ1 : fin n -> PTm m) :
+    (forall i, rtc RERed.R (ρ0 i) (ρ1 i)) ->
+    (forall i, rtc RERed.R (up_PTm_PTm ρ0 i) (up_PTm_PTm ρ1 i)).
+  Proof. move => h i. destruct i as [i|].
+         simpl. rewrite /funcomp.
+         substify. by apply substing.
+         apply rtc_refl.
+  Qed.
+
+  Lemma cong n m (a : PTm n) (ρ0 ρ1 : fin n -> PTm m) :
+    (forall i, rtc RERed.R (ρ0 i) (ρ1 i)) ->
+    rtc RERed.R (subst_PTm ρ0 a) (subst_PTm ρ1 a).
+  Proof.
+    move : m ρ0 ρ1. elim : n / a;
+      eauto using AppCong, AbsCong, BindCong, ProjCong, PairCong, cong_up, rtc_refl.
+  Qed.
+
+  Lemma cong' n m (a b : PTm n) (ρ0 ρ1 : fin n -> PTm m) :
+    rtc RERed.R a b ->
+    (forall i, rtc RERed.R (ρ0 i) (ρ1 i)) ->
+    rtc RERed.R (subst_PTm ρ0 a) (subst_PTm ρ1 b).
+  Proof.
+    move => h0 h1.
+    have : rtc RERed.R (subst_PTm ρ0 a) (subst_PTm ρ1 a) by eauto using cong.
+    move => ?. apply : relations.rtc_transitive; eauto.
+    hauto l:on use:substing.
+  Qed.
+
+  Lemma ToEReds n (a b : PTm n) :
+    nf a ->
+    rtc RERed.R a b -> rtc ERed.R a b.
+  Proof.
+    move => + h.
+    induction h; hauto lq:on rew:off ctrs:rtc use:RERed.ToBetaEta, RReds.nf_refl, @rtc_once, ERed.nf_preservation.
+  Qed.
+
 End REReds.
 
 Module LoRed.
@@ -1811,6 +1900,22 @@ Module LoRed.
     RRed.R a b.
   Proof. induction 1; hauto lq:on ctrs:RRed.R. Qed.
 
+  Lemma AppAbs' n a (b : PTm n) u :
+    u = (subst_PTm (scons b VarPTm) a) ->
+    R (PApp (PAbs a) b)  u.
+  Proof. move => ->. apply AppAbs. Qed.
+
+  Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) :
+    R a b -> R (ren_PTm ξ a) (ren_PTm ξ b).
+  Proof.
+    move => h. move : m ξ.
+    elim : n a b /h.
+
+    move => n a b m ξ /=.
+    apply AppAbs'. by asimpl.
+    all : try qauto ctrs:R use:ne_nf_ren, ishf_ren.
+  Qed.
+
 End LoRed.
 
 Module LoReds.
@@ -2142,6 +2247,12 @@ Module DJoin.
   Lemma refl n (a : PTm n) : R a a.
   Proof. sfirstorder use:@rtc_refl unfold:R. Qed.
 
+  Lemma FromEJoin n (a b : PTm n) : EJoin.R a b -> DJoin.R a b.
+  Proof. hauto q:on use:REReds.FromEReds. Qed.
+
+  Lemma ToEJoin n (a b : PTm n) : nf a -> nf b -> DJoin.R a b -> EJoin.R a b.
+  Proof. hauto q:on use:REReds.ToEReds. Qed.
+
   Lemma symmetric n (a b : PTm n) : R a b -> R b a.
   Proof. sfirstorder unfold:R. Qed.
 
@@ -2176,6 +2287,12 @@ Module DJoin.
     R (PProj p a0) (PProj p a1).
   Proof. hauto q:on use:REReds.ProjCong. Qed.
 
+  Lemma BindCong n p (A0 A1 : PTm n) B0 B1 :
+    R A0 A1 ->
+    R B0 B1 ->
+    R (PBind p A0 B0) (PBind p A1 B1).
+  Proof. hauto q:on use:REReds.BindCong. Qed.
+
   Lemma FromRedSNs n (a b : PTm n) :
     rtc TRedSN a b ->
     R a b.
@@ -2209,6 +2326,28 @@ Module DJoin.
     case : c => //=; itauto.
   Qed.
 
+  Lemma hne_univ_noconf n (a b : PTm n) :
+    R a b -> ishne a -> isuniv b -> False.
+  Proof.
+    move => [c [h0 h1]] h2 h3.
+    have {h0 h1 h2 h3} : ishne c /\ isuniv c by
+      hauto l:on use:REReds.hne_preservation,
+          REReds.univ_preservation.
+    move => [].
+    case : c => //=.
+  Qed.
+
+  Lemma hne_bind_noconf n (a b : PTm n) :
+    R a b -> ishne a -> isbind b -> False.
+  Proof.
+    move => [c [h0 h1]] h2 h3.
+    have {h0 h1 h2 h3} : ishne c /\ isbind c by
+      hauto l:on use:REReds.hne_preservation,
+          REReds.bind_preservation.
+    move => [].
+    case : c => //=.
+  Qed.
+
   Lemma bind_inj n p0 p1 (A0 A1 : PTm n) B0 B1 :
     DJoin.R (PBind p0 A0 B0) (PBind p1 A1 B1) ->
     p0 = p1 /\ DJoin.R A0 A1 /\ DJoin.R B0 B1.
@@ -2217,12 +2356,34 @@ Module DJoin.
     hauto lq:on rew:off use:REReds.bind_inv.
   Qed.
 
+  Lemma var_inj n (i j : fin n) :
+    R (VarPTm i) (VarPTm j) -> i = j.
+  Proof. sauto lq:on rew:off use:REReds.var_inv unfold:R. Qed.
+
   Lemma univ_inj n i j :
     @R n (PUniv i) (PUniv j)  -> i = j.
   Proof.
     sauto lq:on rew:off use:REReds.univ_inv.
   Qed.
 
+  Lemma hne_app_inj n (a0 b0 a1 b1 : PTm n) :
+    R (PApp a0 b0) (PApp a1 b1) ->
+    ishne a0 ->
+    ishne a1 ->
+    R a0 a1 /\ R b0 b1.
+  Proof.
+    hauto lq:on use:REReds.hne_app_inv.
+  Qed.
+
+  Lemma hne_proj_inj n p0 p1 (a0 a1 : PTm n) :
+    R (PProj p0 a0) (PProj p1 a1) ->
+    ishne a0 ->
+    ishne a1 ->
+    p0 = p1 /\ R a0 a1.
+  Proof.
+    sauto lq:on use:REReds.hne_proj_inv.
+  Qed.
+
   Lemma FromRRed0 n (a b : PTm n) :
     RRed.R a b -> R a b.
   Proof.
@@ -2253,4 +2414,456 @@ Module DJoin.
     hauto lq:on rew:off ctrs:rtc unfold:R use:REReds.substing.
   Qed.
 
+  Lemma renaming n m (a b : PTm n) (ρ : fin n -> fin m) :
+    R a b -> R (ren_PTm ρ a) (ren_PTm ρ b).
+  Proof. substify. apply substing. Qed.
+
+  Lemma weakening n (a b : PTm n)  :
+    R a b -> R (ren_PTm shift a) (ren_PTm shift b).
+  Proof. apply renaming. Qed.
+
+  Lemma cong n m (a : PTm (S n)) c d (ρ : fin n -> PTm m) :
+    R c d -> R (subst_PTm (scons c ρ) a) (subst_PTm (scons d ρ) a).
+  Proof.
+    rewrite /R. move => [cd [h0 h1]].
+    exists (subst_PTm (scons cd ρ) a).
+    hauto q:on ctrs:rtc inv:option use:REReds.cong.
+  Qed.
+
+  Lemma pair_inj n (a0 a1 b0 b1 : PTm n) :
+    SN (PPair a0 b0) ->
+    SN (PPair a1 b1) ->
+    R (PPair a0 b0) (PPair a1 b1) ->
+    R a0 a1 /\ R b0 b1.
+  Proof.
+    move => sn0 sn1.
+    have [? [? [? ?]]] : SN a0 /\ SN b0 /\ SN a1 /\ SN b1 by sfirstorder use:SN_NoForbid.P_PairInv.
+    have ? : SN (PProj PL (PPair a0 b0)) by hauto lq:on db:sn.
+    have ? : SN (PProj PR (PPair a0 b0)) by hauto lq:on db:sn.
+    have ? : SN (PProj PL (PPair a1 b1)) by hauto lq:on db:sn.
+    have ? : SN (PProj PR (PPair a1 b1)) by hauto lq:on db:sn.
+    have h0L : RRed.R (PProj PL (PPair a0 b0)) a0 by eauto with red.
+    have h0R : RRed.R (PProj PR (PPair a0 b0)) b0 by eauto with red.
+    have h1L : RRed.R (PProj PL (PPair a1 b1)) a1 by eauto with red.
+    have h1R : RRed.R (PProj PR (PPair a1 b1)) b1 by eauto with red.
+    move => h2.
+    move /ProjCong in h2.
+    have h2L := h2 PL.
+    have {h2}h2R := h2 PR.
+    move /FromRRed1 in h0L.
+    move /FromRRed0 in h1L.
+    move /FromRRed1 in h0R.
+    move /FromRRed0 in h1R.
+    split; eauto using transitive.
+  Qed.
+
+  Lemma ejoin_pair_inj n (a0 a1 b0 b1 : PTm n) :
+    nf a0 -> nf b0 -> nf a1 -> nf b1 ->
+    EJoin.R (PPair a0 b0) (PPair a1 b1) ->
+    EJoin.R a0 a1 /\ EJoin.R b0 b1.
+  Proof.
+    move => h0 h1 h2 h3 /FromEJoin.
+    have [? ?] : SN (PPair a0 b0) /\ SN (PPair a1 b1) by sauto lqb:on rew:off use:ne_nf_embed.
+    move => ?.
+    have : R a0 a1 /\ R b0 b1 by hauto l:on use:pair_inj.
+    hauto l:on use:ToEJoin.
+  Qed.
+
+  Lemma abs_inj n (a0 a1 : PTm (S n)) :
+    SN a0 -> SN a1 ->
+    R (PAbs a0) (PAbs a1) ->
+    R a0 a1.
+  Proof.
+    move => sn0 sn1.
+    move /weakening => /=.
+    move /AppCong. move /(_ (VarPTm var_zero) (VarPTm var_zero)).
+    move => /(_ ltac:(sfirstorder use:refl)).
+    move => h.
+    have /FromRRed1 h0 : RRed.R (PApp (PAbs (ren_PTm (upRen_PTm_PTm shift) a0)) (VarPTm var_zero)) a0 by apply RRed.AppAbs'; asimpl.
+    have /FromRRed0 h1 : RRed.R (PApp (PAbs (ren_PTm (upRen_PTm_PTm shift) a1)) (VarPTm var_zero)) a1 by apply RRed.AppAbs'; asimpl.
+    have sn0' := sn0.
+    have sn1' := sn1.
+    eapply sn_renaming with (ξ := (upRen_PTm_PTm shift)) in sn0.
+    eapply sn_renaming with (ξ := (upRen_PTm_PTm shift)) in sn1.
+    apply : transitive; try apply h0.
+    apply : N_Exp. apply N_β. sauto.
+    by asimpl.
+    apply : transitive; try apply h1.
+    apply : N_Exp. apply N_β. sauto.
+    by asimpl.
+    eauto.
+  Qed.
+
+  Lemma ejoin_abs_inj n (a0 a1 : PTm (S n)) :
+    nf a0 -> nf a1 ->
+    EJoin.R (PAbs a0) (PAbs a1) ->
+    EJoin.R a0 a1.
+  Proof.
+    move => h0 h1.
+    have [? [? [? ?]]] : SN a0 /\ SN a1 /\ SN (PAbs a0) /\ SN (PAbs a1) by sauto lqb:on rew:off use:ne_nf_embed.
+    move /FromEJoin.
+    move /abs_inj.
+    hauto l:on use:ToEJoin.
+  Qed.
+
+  Lemma standardization n (a b : PTm n) :
+    SN a -> SN b -> R a b ->
+    exists va vb, rtc RRed.R a va /\ rtc RRed.R b vb /\ nf va /\ nf vb /\ EJoin.R va vb.
+  Proof.
+    move => h0 h1 [ab [hv0 hv1]].
+    have hv : SN ab by sfirstorder use:REReds.sn_preservation.
+    have : exists v, rtc RRed.R ab v  /\ nf v by hauto q:on use:LoReds.FromSN, LoReds.ToRReds.
+    move => [v [hv2 hv3]].
+    have : rtc RERed.R a v by hauto q:on use:@relations.rtc_transitive, REReds.FromRReds.
+    have : rtc RERed.R b v by hauto q:on use:@relations.rtc_transitive, REReds.FromRReds.
+    move : h0 h1 hv3. clear.
+    move => h0 h1 hv hbv hav.
+    move : rered_standardization (h0) hav. repeat move/[apply].
+    move => [a1 [ha0 ha1]].
+    move : rered_standardization (h1) hbv. repeat move/[apply].
+    move => [b1 [hb0 hb1]].
+    have [*] : nf a1 /\ nf b1 by sfirstorder use:NeEPars.R_nonelim_nf.
+    hauto q:on use:NeEPars.ToEReds unfold:EJoin.R.
+  Qed.
+
+  Lemma standardization_lo n (a b : PTm n) :
+    SN a -> SN b -> R a b ->
+    exists va vb, rtc LoRed.R a va /\ rtc LoRed.R b vb /\ nf va /\ nf vb /\ EJoin.R va vb.
+  Proof.
+    move => /[dup] sna + /[dup] snb.
+    move : standardization; repeat move/[apply].
+    move => [va][vb][hva][hvb][nfva][nfvb]hj.
+    move /LoReds.FromSN : sna => [va' [hva' hva'0]].
+    move /LoReds.FromSN : snb => [vb' [hvb' hvb'0]].
+    exists va', vb'.
+    repeat split => //=.
+    have : va = va' /\ vb = vb' by sfirstorder use:red_uniquenf, LoReds.ToRReds.
+    case; congruence.
+  Qed.
 End DJoin.
+
+
+Module Sub1.
+  Inductive R {n} : PTm n -> PTm n -> Prop :=
+  | Refl a :
+    R a a
+  | Univ i j :
+    i <= j ->
+    R (PUniv i) (PUniv j)
+  | PiCong A0 A1 B0 B1 :
+    R A1 A0 ->
+    R B0 B1 ->
+    R (PBind PPi A0 B0) (PBind PPi A1 B1)
+  | SigCong A0 A1 B0 B1 :
+    R A0 A1 ->
+    R B0 B1 ->
+    R (PBind PSig A0 B0) (PBind PSig A1 B1).
+
+  Lemma transitive0 n (A B C : PTm n) :
+    R A B -> (R B C -> R A C) /\ (R C A -> R C B).
+  Proof.
+    move => h. move : C.
+    elim : n A B /h; hauto lq:on ctrs:R inv:R solve+:lia.
+  Qed.
+
+  Lemma transitive n (A B C : PTm n) :
+    R A B -> R B C -> R A C.
+  Proof. hauto q:on use:transitive0. Qed.
+
+  Lemma refl n (A : PTm n) : R A A.
+  Proof. sfirstorder. Qed.
+
+  Lemma commutativity0 n (A B C : PTm n) :
+    R A B ->
+    (RERed.R A C ->
+    exists D, RERed.R B D /\ R C D) /\
+    (RERed.R B C ->
+    exists D, RERed.R A D /\ R D C).
+  Proof.
+    move => h. move : C.
+    elim : n A B / h; hauto lq:on ctrs:RERed.R, R inv:RERed.R.
+  Qed.
+
+  Lemma commutativity_Ls n (A B C : PTm n) :
+    R A B ->
+    rtc RERed.R A C ->
+    exists D, rtc RERed.R B D /\ R C D.
+  Proof.
+    move => + h. move : B. induction h; sauto lq:on use:commutativity0.
+  Qed.
+
+  Lemma commutativity_Rs n (A B C : PTm n) :
+    R A B ->
+    rtc RERed.R B C ->
+    exists D, rtc RERed.R A D /\ R D C.
+  Proof.
+    move => + h. move : A. induction h; sauto lq:on use:commutativity0.
+  Qed.
+
+  Lemma sn_preservation  : forall n,
+  (forall (a : PTm n) (s : SNe a), forall b, R a b \/ R b a -> a = b) /\
+  (forall (a : PTm n) (s : SN a), forall b, R a b \/ R b a -> SN b) /\
+  (forall (a b : PTm n) (_ : TRedSN a b), forall c, R a c \/ R c a -> a = c).
+  Proof.
+    apply sn_mutual; hauto lq:on inv:R ctrs:SN.
+  Qed.
+
+  Lemma bind_preservation n (a b : PTm n) :
+    R a b -> isbind a = isbind b.
+  Proof. hauto q:on inv:R. Qed.
+
+  Lemma univ_preservation n (a b : PTm n) :
+    R a b -> isuniv a = isuniv b.
+  Proof. hauto q:on inv:R. Qed.
+
+  Lemma sne_preservation n (a b : PTm n) :
+    R a b -> SNe a <-> SNe b.
+  Proof. hfcrush use:sn_preservation. Qed.
+
+  Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) :
+    R a b -> R (ren_PTm ξ a) (ren_PTm ξ b).
+  Proof.
+    move => h. move : m ξ.
+    elim : n a b /h; hauto lq:on ctrs:R.
+  Qed.
+
+  Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) :
+    R a b -> R (subst_PTm ρ a) (subst_PTm ρ b).
+  Proof. move => h. move : m ρ. elim : n a b /h; hauto lq:on ctrs:R. Qed.
+
+  Lemma hne_refl n (a b : PTm n) :
+    ishne a \/ ishne b -> R a b -> a = b.
+  Proof. hauto q:on inv:R. Qed.
+
+End Sub1.
+
+Module ESub.
+  Definition R {n} (a b : PTm n) := exists c0 c1, rtc ERed.R a c0 /\ rtc ERed.R b c1 /\ Sub1.R c0 c1.
+
+  Lemma pi_inj n (A0 A1 : PTm n) B0 B1 :
+    R (PBind PPi A0 B0) (PBind PPi A1 B1) ->
+    R A1 A0 /\ R B0 B1.
+  Proof.
+    move => [u0 [u1 [h0 [h1 h2]]]].
+    move /EReds.bind_inv : h0 => [A2][B2][?][h3]h4. subst.
+    move /EReds.bind_inv : h1 => [A3][B3][?][h5]h6. subst.
+    sauto lq:on rew:off inv:Sub1.R.
+  Qed.
+
+  Lemma sig_inj n (A0 A1 : PTm n) B0 B1 :
+    R (PBind PSig A0 B0) (PBind PSig A1 B1) ->
+    R A0 A1 /\ R B0 B1.
+  Proof.
+    move => [u0 [u1 [h0 [h1 h2]]]].
+    move /EReds.bind_inv : h0 => [A2][B2][?][h3]h4. subst.
+    move /EReds.bind_inv : h1 => [A3][B3][?][h5]h6. subst.
+    sauto lq:on rew:off inv:Sub1.R.
+  Qed.
+
+End ESub.
+
+Module Sub.
+  Definition R {n} (a b : PTm n) := exists c d, rtc RERed.R a c /\ rtc RERed.R b d /\ Sub1.R c d.
+
+  Lemma refl n (a : PTm n) : R a a.
+  Proof. sfirstorder use:@rtc_refl unfold:R. Qed.
+
+  Lemma ToJoin n (a b : PTm n) :
+    ishne a \/ ishne b ->
+    R a b ->
+    DJoin.R a b.
+  Proof.
+    move => h [c][d][h0][h1]h2.
+    have : ishne c \/ ishne d by hauto q:on use:REReds.hne_preservation.
+    hauto lq:on rew:off use:Sub1.hne_refl.
+  Qed.
+
+  Lemma transitive n (a b c : PTm n) : SN b -> R a b -> R b c -> R a c.
+  Proof.
+    rewrite /R.
+    move => h  [a0][b0][ha][hb]ha0b0 [b1][c0][hb'][hc]hb1c0.
+    move : hb hb'.
+    move : rered_confluence h. repeat move/[apply].
+    move => [b'][hb0]hb1.
+    have [a' ?] : exists a', rtc RERed.R a0 a' /\ Sub1.R a' b' by hauto l:on use:Sub1.commutativity_Rs.
+    have [c' ?] : exists a', rtc RERed.R c0 a' /\ Sub1.R b' a' by hauto l:on use:Sub1.commutativity_Ls.
+    exists a',c'; hauto l:on use:Sub1.transitive, @relations.rtc_transitive.
+  Qed.
+
+  Lemma FromJoin n (a b : PTm n) : DJoin.R a b -> R a b.
+  Proof. sfirstorder. Qed.
+
+  Lemma PiCong n (A0 A1 : PTm n) B0 B1 :
+    R A1 A0 ->
+    R B0 B1 ->
+    R (PBind PPi A0 B0) (PBind PPi A1 B1).
+  Proof.
+    rewrite /R.
+    move => [A][A'][h0][h1]h2.
+    move => [B][B'][h3][h4]h5.
+    exists (PBind PPi A' B), (PBind PPi A B').
+    repeat split; eauto using REReds.BindCong, Sub1.PiCong.
+  Qed.
+
+  Lemma SigCong n (A0 A1 : PTm n) B0 B1 :
+    R A0 A1 ->
+    R B0 B1 ->
+    R (PBind PSig A0 B0) (PBind PSig A1 B1).
+  Proof.
+    rewrite /R.
+    move => [A][A'][h0][h1]h2.
+    move => [B][B'][h3][h4]h5.
+    exists (PBind PSig A B), (PBind PSig A' B').
+    repeat split; eauto using REReds.BindCong, Sub1.SigCong.
+  Qed.
+
+  Lemma UnivCong n i j :
+    i <= j ->
+    @R n (PUniv i) (PUniv j).
+  Proof. hauto lq:on ctrs:Sub1.R, rtc. Qed.
+
+  Lemma sne_bind_noconf n (a b : PTm n) :
+    R a b -> SNe a -> isbind b -> False.
+  Proof.
+    rewrite /R.
+    move => [c[d] [? []]] *.
+    have : SNe c /\ isbind c by
+      hauto l:on use:REReds.sne_preservation, REReds.bind_preservation, Sub1.sne_preservation, Sub1.bind_preservation.
+    qauto l:on inv:SNe.
+  Qed.
+
+  Lemma hne_bind_noconf n (a b : PTm n) :
+    R a b -> ishne a -> isbind b -> False.
+  Proof.
+    rewrite /R.
+    move => [c[d] [? []]] h0 h1 h2 h3.
+    have : ishne c by eauto using REReds.hne_preservation.
+    have : isbind d by eauto using REReds.bind_preservation.
+    move : h1. clear. inversion 1; subst => //=.
+    clear. case : d => //=.
+  Qed.
+
+  Lemma bind_sne_noconf n (a b : PTm n) :
+    R a b -> SNe b -> isbind a -> False.
+  Proof.
+    rewrite /R.
+    move => [c[d] [? []]] *.
+    have : SNe c /\ isbind c by
+      hauto l:on use:REReds.sne_preservation, REReds.bind_preservation, Sub1.sne_preservation, Sub1.bind_preservation.
+    qauto l:on inv:SNe.
+  Qed.
+
+  Lemma sne_univ_noconf n (a b : PTm n) :
+    R a b -> SNe a -> isuniv b -> False.
+  Proof.
+    hauto l:on use:REReds.sne_preservation,
+          REReds.univ_preservation, Sub1.sne_preservation, Sub1.univ_preservation inv:SNe.
+  Qed.
+
+  Lemma univ_sne_noconf n (a b : PTm n) :
+    R a b -> SNe b -> isuniv a -> False.
+  Proof.
+    move => [c[d] [? []]] *.
+    have ? : SNe d by eauto using REReds.sne_preservation.
+    have : SNe c by sfirstorder use:Sub1.sne_preservation.
+    have : isuniv c by sfirstorder use:REReds.univ_preservation.
+    clear. case : c => //=. inversion 2.
+  Qed.
+
+  Lemma bind_univ_noconf n (a b : PTm n) :
+    R a b -> isbind a -> isuniv b -> False.
+  Proof.
+    move => [c[d] [h0 [h1 h1']]] h2 h3.
+    have : isbind c /\ isuniv c by
+      hauto l:on use:REReds.bind_preservation,
+            REReds.univ_preservation, Sub1.bind_preservation, Sub1.univ_preservation.
+    move : h2 h3. clear.
+    case : c => //=; itauto.
+  Qed.
+
+  Lemma univ_bind_noconf n (a b : PTm n) :
+    R a b -> isbind b -> isuniv a -> False.
+  Proof.
+    move => [c[d] [h0 [h1 h1']]] h2 h3.
+    have : isbind c /\ isuniv c by
+      hauto l:on use:REReds.bind_preservation,
+            REReds.univ_preservation, Sub1.bind_preservation, Sub1.univ_preservation.
+    move : h2 h3. clear.
+    case : c => //=; itauto.
+  Qed.
+
+  Lemma bind_inj n p0 p1 (A0 A1 : PTm n) B0 B1 :
+    R (PBind p0 A0 B0) (PBind p1 A1 B1) ->
+    p0 = p1 /\ (if p0 is PPi then R A1 A0 else R A0 A1) /\ R B0 B1.
+  Proof.
+    rewrite /R.
+    move => [u][v][h0][h1]h.
+    move /REReds.bind_inv : h0 => [A2][B2][?][h00]h01. subst.
+    move /REReds.bind_inv : h1 => [A3][B3][?][h10]h11. subst.
+    inversion h; subst; sauto lq:on.
+  Qed.
+
+  Lemma univ_inj n i j :
+    @R n (PUniv i) (PUniv j)  -> i <= j.
+  Proof.
+    sauto lq:on rew:off use:REReds.univ_inv.
+  Qed.
+
+  Lemma cong n m (a b : PTm (S n)) c d (ρ : fin n -> PTm m) :
+    R a b -> DJoin.R c d -> R (subst_PTm (scons c ρ) a) (subst_PTm (scons d ρ) b).
+  Proof.
+    rewrite /R.
+    move => [a0][b0][h0][h1]h2.
+    move => [cd][h3]h4.
+    exists (subst_PTm (scons cd ρ) a0), (subst_PTm (scons cd ρ) b0).
+    repeat split.
+    hauto l:on use:REReds.cong' inv:option.
+    hauto l:on use:REReds.cong' inv:option.
+    eauto using Sub1.substing.
+  Qed.
+
+  Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) :
+    R a b -> R (subst_PTm ρ a) (subst_PTm ρ b).
+  Proof.
+    rewrite /R.
+    move => [a0][b0][h0][h1]h2.
+    hauto ctrs:rtc use:REReds.cong', Sub1.substing.
+  Qed.
+
+  Lemma ToESub n (a b : PTm n) : nf a -> nf b -> R a b -> ESub.R a b.
+  Proof. hauto q:on use:REReds.ToEReds. Qed.
+
+  Lemma standardization n (a b : PTm n) :
+    SN a -> SN b -> R a b ->
+    exists va vb, rtc RRed.R a va /\ rtc RRed.R b vb /\ nf va /\ nf vb /\ ESub.R va vb.
+  Proof.
+    move => h0 h1 hS.
+    have : exists v, rtc RRed.R a v  /\ nf v by sfirstorder use:LoReds.FromSN, LoReds.ToRReds.
+    move => [v [hv2 hv3]].
+    have : exists v, rtc RRed.R b v  /\ nf v by sfirstorder use:LoReds.FromSN, LoReds.ToRReds.
+    move => [v' [hv2' hv3']].
+    move : (hv2) (hv2') => *.
+    apply DJoin.FromRReds in hv2, hv2'.
+    move/DJoin.symmetric in hv2'.
+    apply FromJoin in hv2, hv2'.
+    have hv : R v v' by eauto using transitive.
+    have {}hv : ESub.R v v' by hauto l:on use:ToESub.
+    hauto lq:on.
+  Qed.
+
+  Lemma standardization_lo n (a b : PTm n) :
+    SN a -> SN b -> R a b ->
+    exists va vb, rtc LoRed.R a va /\ rtc LoRed.R b vb /\ nf va /\ nf vb /\ ESub.R va vb.
+  Proof.
+    move => /[dup] sna + /[dup] snb.
+    move : standardization; repeat move/[apply].
+    move => [va][vb][hva][hvb][nfva][nfvb]hj.
+    move /LoReds.FromSN : sna => [va' [hva' hva'0]].
+    move /LoReds.FromSN : snb => [vb' [hvb' hvb'0]].
+    exists va', vb'.
+    repeat split => //=.
+    have : va = va' /\ vb = vb' by sfirstorder use:red_uniquenf, LoReds.ToRReds.
+    case; congruence.
+  Qed.
+
+End Sub.

theories/logrel.v

@@ -1,5 +1,5 @@
 Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax.
-Require Import fp_red.
+Require Import common fp_red.
 From Hammer Require Import Tactics.
 From Equations Require Import Equations.
 Require Import ssreflect ssrbool.
@@ -24,6 +24,7 @@ Inductive InterpExt {n} i (I : nat -> PTm n -> Prop) : PTm n -> (PTm n -> Prop)
 | InterpExt_Ne A :
   SNe A ->
   ⟦ A ⟧ i ;; I ↘ (fun a => exists v, rtc TRedSN a v /\ SNe v)
+
 | InterpExt_Bind p A B PA PF :
   ⟦ A ⟧ i ;; I ↘ PA ->
   (forall a, PA a -> exists PB, PF a PB) ->
@@ -40,7 +41,6 @@ Inductive InterpExt {n} i (I : nat -> PTm n -> Prop) : PTm n -> (PTm n -> Prop)
   ⟦ A ⟧ i ;; I ↘ PA
 where "⟦ A ⟧ i ;; I ↘ S" := (InterpExt i I A S).
 
-
 Lemma InterpExt_Univ' n i  I j (PF : PTm n -> Prop) :
   PF = I j ->
   j < i ->
@@ -261,7 +261,8 @@ Qed.
 Lemma redsns_preservation : forall n a b, @SN n a -> rtc TRedSN a b -> SN b.
 Proof. induction 2; sfirstorder use:redsn_preservation_mutual ctrs:rtc. Qed.
 
-#[export]Hint Resolve DJoin.sne_bind_noconf DJoin.sne_univ_noconf DJoin.bind_univ_noconf : noconf.
+#[export]Hint Resolve Sub.sne_bind_noconf Sub.sne_univ_noconf Sub.bind_univ_noconf
+  Sub.bind_sne_noconf Sub.univ_sne_noconf Sub.univ_bind_noconf: noconf.
 
 Lemma InterpUniv_SNe_inv n i (A : PTm n) PA :
   SNe A ->
@@ -294,26 +295,150 @@ Proof.
   subst. hauto lq:on inv:TRedSN.
 Qed.
 
-Lemma bindspace_iff n p (PA : PTm n -> Prop) PF PF0 b  :
-  (forall (a : PTm n) (PB PB0 : PTm n -> Prop), PA a -> PF a PB -> PF0 a PB0 -> PB = PB0) ->
+Lemma bindspace_impl n p (PA PA0 : PTm n -> Prop) PF PF0 b  :
+  (forall x, if p is PPi then (PA0 x -> PA x) else (PA x -> PA0 x)) ->
+  (forall (a : PTm n) (PB PB0 : PTm n -> Prop), PA0 a -> PF a PB -> PF0 a PB0 -> (forall x, PB x ->  PB0 x)) ->
   (forall a, PA a -> exists PB, PF a PB) ->
-  (forall a, PA a -> exists PB0, PF0 a PB0) ->
-  (BindSpace p PA PF b <-> BindSpace p PA PF0 b).
+  (forall a, PA0 a -> exists PB0, PF0 a PB0) ->
+  (BindSpace p PA PF b -> BindSpace p PA0 PF0 b).
 Proof.
-  rewrite /BindSpace => h hPF hPF0.
-  case : p => /=.
+  rewrite /BindSpace => hSA h hPF hPF0.
+  case : p hSA => /= hSA.
   - rewrite /ProdSpace.
-    split.
     move => h1 a PB ha hPF'.
-    specialize hPF with (1 := ha).
+    have {}/hPF : PA a by sfirstorder.
     specialize hPF0 with (1 := ha).
-    sblast.
-    move => ? a PB ha.
-    specialize hPF with (1 := ha).
-    specialize hPF0 with (1 := ha).
-    sblast.
+    hauto lq:on.
   - rewrite /SumSpace.
-    hauto lq:on rew:off.
+    case. sfirstorder.
+    move => [a0][b0][h0][h1]h2. right.
+    hauto lq:on.
+Qed.
+
+Lemma InterpUniv_Sub' n i (A B : PTm n) PA PB :
+  ⟦ A ⟧ i ↘ PA ->
+  ⟦ B ⟧ i ↘ PB ->
+  ((Sub.R A B -> forall x, PA x -> PB x) /\
+  (Sub.R B A -> forall x, PB x -> PA x)).
+Proof.
+  move => hA.
+  move : i A PA hA B PB.
+  apply : InterpUniv_ind.
+  - move => i A hA B PB hPB. split.
+    + move => hAB a ha.
+      have [? ?] : SN B /\ SN A by hauto l:on use:adequacy.
+      move /InterpUniv_case : hPB.
+      move => [H [/DJoin.FromRedSNs h [h1 h0]]].
+      have {h}{}hAB : Sub.R A H by qauto l:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
+      have {}h0 : SNe H.
+      suff : ~ isbind H /\ ~ isuniv H by itauto.
+      move : hA hAB. clear. hauto lq:on db:noconf.
+      move : InterpUniv_SNe_inv h1 h0. repeat move/[apply]. move => ?. subst.
+      tauto.
+    + move => hAB a ha.
+      have [? ?] : SN B /\ SN A by hauto l:on use:adequacy.
+      move /InterpUniv_case : hPB.
+      move => [H [/DJoin.FromRedSNs h [h1 h0]]].
+      have {h}{}hAB : Sub.R H A by qauto l:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
+      have {}h0 : SNe H.
+      suff : ~ isbind H /\ ~ isuniv H by itauto.
+      move : hAB hA h0. clear. hauto lq:on db:noconf.
+      move : InterpUniv_SNe_inv h1 h0. repeat move/[apply]. move => ?. subst.
+      tauto.
+  - move => i p A B PA PF hPA ihPA hTot hRes ihPF U PU hU. split.
+    + have hU' : SN U by hauto l:on use:adequacy.
+      move /InterpUniv_case : hU => [H [/DJoin.FromRedSNs h [h1 h0]]] hU.
+      have {hU} {}h : Sub.R (PBind p A B) H
+        by move : hU hU' h; clear; hauto q:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
+      have{h0} : isbind H.
+      suff : ~ SNe H /\ ~ isuniv H by itauto.
+      have : isbind (PBind p A B) by scongruence.
+      move : h. clear. hauto l:on db:noconf.
+      case : H h1 h => //=.
+      move => p0 A0 B0 h0 /Sub.bind_inj.
+      move => [? [hA hB]] _. subst.
+      move /InterpUniv_Bind_inv : h0.
+      move => [PA0][PF0][hPA0][hTot0][hRes0 ?]. subst.
+      move => x. apply bindspace_impl; eauto;[idtac|idtac]. hauto l:on.
+      move => a PB PB' ha hPB hPB'.
+      move : hRes0 hPB'. repeat move/[apply].
+      move : ihPF hPB. repeat move/[apply].
+      move => h. eapply h.
+      apply Sub.cong => //=; eauto using DJoin.refl.
+    + have hU' : SN U by hauto l:on use:adequacy.
+      move /InterpUniv_case : hU => [H [/DJoin.FromRedSNs h [h1 h0]]] hU.
+      have {hU} {}h : Sub.R H (PBind p A B)
+        by move : hU hU' h; clear; hauto q:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
+      have{h0} : isbind H.
+      suff : ~ SNe H /\ ~ isuniv H by itauto.
+      have : isbind (PBind p A B) by scongruence.
+      move : h. clear. move : (PBind p A B). hauto lq:on db:noconf.
+      case : H h1 h => //=.
+      move => p0 A0 B0 h0 /Sub.bind_inj.
+      move => [? [hA hB]] _. subst.
+      move /InterpUniv_Bind_inv : h0.
+      move => [PA0][PF0][hPA0][hTot0][hRes0 ?]. subst.
+      move => x. apply bindspace_impl; eauto;[idtac|idtac]. hauto l:on.
+      move => a PB PB' ha hPB hPB'.
+      eapply ihPF; eauto.
+      apply Sub.cong => //=; eauto using DJoin.refl.
+  - move => i j jlti ih B PB hPB. split.
+    + have ? : SN B by hauto l:on use:adequacy.
+      move /InterpUniv_case : hPB => [H [/DJoin.FromRedSNs h [h1 h0]]].
+      move => hj.
+      have {hj}{}h : Sub.R (PUniv j) H by eauto using Sub.transitive, Sub.FromJoin.
+      have {h0} : isuniv H.
+      suff : ~ SNe H /\ ~ isbind H by tauto. move : h. clear. hauto lq:on db:noconf.
+      case : H h1 h => //=.
+      move => j' hPB h _.
+      have {}h : j <= j' by hauto lq:on use: Sub.univ_inj. subst.
+      move /InterpUniv_Univ_inv : hPB => [? ?]. subst.
+      have ? : j <= i by lia.
+      move => A. hauto l:on use:InterpUniv_cumulative.
+    + have ? : SN B by hauto l:on use:adequacy.
+      move /InterpUniv_case : hPB => [H [/DJoin.FromRedSNs h [h1 h0]]].
+      move => hj.
+      have {hj}{}h : Sub.R H (PUniv j) by eauto using Sub.transitive, Sub.FromJoin, DJoin.symmetric.
+      have {h0} : isuniv H.
+      suff : ~ SNe H /\ ~ isbind H by tauto. move : h. clear. hauto lq:on db:noconf.
+      case : H h1 h => //=.
+      move => j' hPB h _.
+      have {}h : j' <= j by hauto lq:on use: Sub.univ_inj.
+      move /InterpUniv_Univ_inv : hPB => [? ?]. subst.
+      move => A. hauto l:on use:InterpUniv_cumulative.
+  - move => i A A0 PA hr hPA ihPA B PB hPB.
+    have ? : SN A by sauto lq:on use:adequacy.
+    split.
+    + move => ?.
+      have {}hr : Sub.R A0 A by hauto lq:on  ctrs:rtc use:DJoin.FromRedSNs, DJoin.symmetric, Sub.FromJoin.
+      have : Sub.R A0 B by eauto using Sub.transitive.
+      qauto l:on.
+    + move => ?.
+      have {}hr : Sub.R A A0 by hauto lq:on  ctrs:rtc use:DJoin.FromRedSNs, DJoin.symmetric, Sub.FromJoin.
+      have : Sub.R B A0 by eauto using Sub.transitive.
+      qauto l:on.
+Qed.
+
+Lemma InterpUniv_Sub0 n i (A B : PTm n) PA PB :
+  ⟦ A ⟧ i ↘ PA ->
+  ⟦ B ⟧ i ↘ PB ->
+  Sub.R A B -> forall x, PA x -> PB x.
+Proof.
+  move : InterpUniv_Sub'. repeat move/[apply].
+  move => [+ _]. apply.
+Qed.
+
+Lemma InterpUniv_Sub n i j (A B : PTm n) PA PB :
+  ⟦ A ⟧ i ↘ PA ->
+  ⟦ B ⟧ j ↘ PB ->
+  Sub.R A B -> forall x, PA x -> PB x.
+Proof.
+  have [? ?] : i <= max i j /\ j <= max i j by lia.
+  move => hPA hPB.
+  have : ⟦ B ⟧ (max i j) ↘ PB by eauto using InterpUniv_cumulative.
+  have : ⟦ A ⟧ (max i j) ↘ PA by eauto using InterpUniv_cumulative.
+  move : InterpUniv_Sub0. repeat move/[apply].
+  apply.
 Qed.
 
 Lemma InterpUniv_Join n i (A B : PTm n) PA PB :
@@ -322,69 +447,19 @@ Lemma InterpUniv_Join n i (A B : PTm n) PA PB :
   DJoin.R A B ->
   PA = PB.
 Proof.
-  move => hA.
-  move : i A PA hA B PB.
-  apply : InterpUniv_ind.
-  - move => i A hA B PB hPB hAB.
-    have [*] : SN B /\ SN A by hauto l:on use:adequacy.
-    move /InterpUniv_case : hPB.
-    move => [H [/DJoin.FromRedSNs h [h1 h0]]].
-    have {hAB} {}h : DJoin.R A H by eauto using DJoin.transitive.
-    have {}h0 : SNe H.
-    suff : ~ isbind H /\ ~ isuniv H by itauto.
-    move : h hA. clear. hauto lq:on db:noconf.
-    hauto lq:on use:InterpUniv_SNe_inv.
-  - move => i p A B PA PF hPA ihPA hTot hRes ihPF U PU hU.
-    have hU' : SN U by hauto l:on use:adequacy.
-    move /InterpUniv_case : hU => [H [/DJoin.FromRedSNs h [h1 h0]]] hU.
-    have {hU} {}h : DJoin.R (PBind p A B) H by eauto using DJoin.transitive.
-    have{h0} : isbind H.
-    suff : ~ SNe H /\ ~ isuniv H by itauto.
-    have : isbind (PBind p A B) by scongruence.
-    hauto l:on use: DJoin.sne_bind_noconf, DJoin.bind_univ_noconf, DJoin.symmetric.
-    case : H h1 h => //=.
-    move => p0 A0 B0 h0 /DJoin.bind_inj.
-    move => [? [hA hB]] _. subst.
-    move /InterpUniv_Bind_inv : h0.
-    move => [PA0][PF0][hPA0][hTot0][hRes0 ?]. subst.
-    have ? : PA0 = PA by qauto l:on. subst.
-    have : forall a PB PB', PA a -> PF a PB -> PF0 a PB' -> PB = PB'.
-    move => a PB PB' ha hPB hPB'. apply : ihPF; eauto.
-    have hj0 : DJoin.R (PAbs B) (PAbs B0) by eauto using DJoin.AbsCong.
-    have {}hj0 : DJoin.R (PApp (PAbs B) a) (PApp (PAbs B0) a) by eauto using DJoin.AppCong, DJoin.refl.
-    have [? ?] : SN (PApp (PAbs B) a) /\ SN (PApp (PAbs B0) a) by
-      hauto lq:on rew:off use:N_Exp, N_β, adequacy.
-    have [? ?] : DJoin.R (PApp (PAbs B0) a) (subst_PTm (scons a VarPTm) B0) /\
-           DJoin.R (subst_PTm (scons a VarPTm) B) (PApp (PAbs B) a)
-      by hauto lq:on ctrs:RRed.R use:DJoin.FromRRed0, DJoin.FromRRed1.
-    eauto using DJoin.transitive.
-    move => h. extensionality b. apply propositional_extensionality.
-    hauto l:on use:bindspace_iff.
-  - move => i j jlti ih B PB hPB.
-    have ? : SN B by hauto l:on use:adequacy.
-    move /InterpUniv_case : hPB => [H [/DJoin.FromRedSNs h [h1 h0]]].
-    move => hj.
-    have {hj}{}h : DJoin.R (PUniv j) H by eauto using DJoin.transitive.
-    have {h0} : isuniv H.
-    suff : ~ SNe H /\ ~ isbind H by tauto.
-    hauto l:on use: DJoin.sne_univ_noconf, DJoin.bind_univ_noconf, DJoin.symmetric.
-    case : H h1 h => //=.
-    move => j' hPB h _.
-    have {}h : j' = j by hauto lq:on use: DJoin.univ_inj. subst.
-    hauto lq:on use:InterpUniv_Univ_inv.
-  - move => i A A0 PA hr hPA ihPA B PB hPB hAB.
-    have /DJoin.symmetric ? : DJoin.R A A0 by hauto lq:on rew:off ctrs:rtc use:DJoin.FromRedSNs.
-    have ? : SN A0 by hauto l:on use:adequacy.
-    have ? : SN A by eauto using N_Exp.
-    have : DJoin.R A0 B by eauto using DJoin.transitive.
-    eauto.
+  move => + + /[dup] /Sub.FromJoin + /DJoin.symmetric /Sub.FromJoin.
+  move : InterpUniv_Sub'; repeat move/[apply]. move => h.
+  move => h1 h2.
+  extensionality x.
+  apply propositional_extensionality.
+  firstorder.
 Qed.
 
 Lemma InterpUniv_Functional n i  (A : PTm n) PA PB :
   ⟦ A ⟧ i ↘ PA ->
   ⟦ A ⟧ i ↘ PB ->
   PA = PB.
-Proof. hauto use:InterpUniv_Join, DJoin.refl. Qed.
+Proof. hauto l:on use:InterpUniv_Join, DJoin.refl. Qed.
 
 Lemma InterpUniv_Join' n i j (A B : PTm n) PA PB :
   ⟦ A ⟧ i ↘ PA ->
@@ -441,6 +516,61 @@ Definition ρ_ok {n} (Γ : fin n -> PTm n) (ρ : fin n -> PTm 0) := forall i k P
 Definition SemWt {n} Γ (a A : PTm n) := forall ρ, ρ_ok Γ ρ -> exists k PA, ⟦ subst_PTm ρ A ⟧ k ↘ PA /\ PA (subst_PTm ρ a).
 Notation "Γ ⊨ a ∈ A" := (SemWt Γ a A) (at level 70).
 
+Definition SemEq {n} Γ (a b A : PTm n) := DJoin.R a b /\ forall ρ, ρ_ok Γ ρ -> exists k PA, ⟦ subst_PTm ρ A ⟧ k ↘ PA /\ PA (subst_PTm ρ a) /\ PA (subst_PTm ρ b).
+Notation "Γ ⊨ a ≡ b ∈ A" := (SemEq Γ a b A) (at level 70).
+
+Definition SemLEq {n} Γ (A B : PTm n) := Sub.R A B /\ exists i, forall ρ, ρ_ok Γ ρ -> exists S0 S1, ⟦ subst_PTm ρ A ⟧ i ↘ S0 /\ ⟦ subst_PTm ρ B ⟧ i ↘ S1.
+Notation "Γ ⊨ a ≲ b" := (SemLEq Γ a b) (at level 70).
+
+Lemma SemWt_Univ n Γ (A : PTm n) i  :
+  Γ ⊨ A ∈ PUniv i <->
+  forall ρ, ρ_ok Γ ρ -> exists S, ⟦ subst_PTm ρ A ⟧ i ↘ S.
+Proof.
+  rewrite /SemWt.
+  split.
+  - hauto lq:on rew:off use:InterpUniv_Univ_inv.
+  - move => /[swap] ρ /[apply].
+    move => [PA hPA].
+    exists (S i). eexists.
+    split.
+    + simp InterpUniv. apply InterpExt_Univ. lia.
+    + simpl. eauto.
+Qed.
+
+Lemma SemEq_SemWt n Γ (a b A : PTm n) : Γ ⊨ a ≡ b ∈ A -> Γ ⊨ a ∈ A /\ Γ ⊨ b ∈ A /\ DJoin.R a b.
+Proof. hauto lq:on rew:off unfold:SemEq, SemWt. Qed.
+
+Lemma SemLEq_SemWt n Γ (A B : PTm n) : Γ ⊨ A ≲ B -> Sub.R A B /\ exists i, Γ ⊨ A ∈ PUniv i /\ Γ ⊨ B ∈ PUniv i.
+Proof. hauto q:on use:SemWt_Univ. Qed.
+
+Lemma SemWt_SemEq n Γ (a b A : PTm n) : Γ ⊨ a ∈ A -> Γ ⊨ b ∈ A -> (DJoin.R a b) -> Γ ⊨ a ≡ b ∈ A.
+Proof.
+  move => ha hb heq. split => //= ρ hρ.
+  have {}/ha := hρ.
+  have {}/hb := hρ.
+  move => [k][PA][hPA]hpb.
+  move => [k0][PA0][hPA0]hpa.
+  have : PA = PA0 by hauto l:on use:InterpUniv_Functional'.
+  hauto lq:on.
+Qed.
+
+Lemma SemWt_SemLEq n Γ (A B : PTm n) i j :
+  Γ ⊨ A ∈ PUniv i -> Γ ⊨ B ∈ PUniv j -> Sub.R A B -> Γ ⊨ A ≲ B.
+Proof.
+  move => ha hb heq. split => //.
+  exists (Nat.max i j).
+  have [? ?] : i <= Nat.max i j /\ j <= Nat.max i j by lia.
+  move => ρ hρ.
+  have {}/ha := hρ.
+  have {}/hb := hρ.
+  move => [k][PA][/= /InterpUniv_Univ_inv [? hPA]]hpb.
+  move => [k0][PA0][/= /InterpUniv_Univ_inv [? hPA0]]hpa. subst.
+  move : hpb => [PA]hPA'.
+  move : hpa => [PB]hPB'.
+  exists PB, PA.
+  split; apply : InterpUniv_cumulative; eauto.
+Qed.
+
 (* Semantic context wellformedness *)
 Definition SemWff {n} Γ := forall (i : fin n), exists j, Γ ⊨ Γ i ∈ PUniv j.
 Notation "⊨ Γ" := (SemWff Γ) (at level 70).
@@ -469,8 +599,12 @@ Proof.
     by subst.
 Qed.
 
-Definition renaming_ok {n m} (Γ : fin n -> PTm n) (Δ : fin m -> PTm m) (ξ : fin m -> fin n) :=
-  forall (i : fin m), ren_PTm ξ (Δ i) = Γ (ξ i).
+Lemma ρ_ok_cons' n i (Γ : fin n -> PTm n) ρ a PA A  Δ :
+  Δ = (funcomp (ren_PTm shift) (scons A Γ)) ->
+  ⟦ subst_PTm ρ A ⟧ i ↘ PA -> PA a ->
+  ρ_ok Γ ρ ->
+  ρ_ok Δ (scons a ρ).
+Proof. move => ->. apply ρ_ok_cons. Qed.
 
 Lemma ρ_ok_renaming n m (Γ : fin n -> PTm n) ρ :
   forall (Δ : fin m -> PTm m) ξ,
@@ -520,20 +654,15 @@ Proof.
   move {h}. hauto l:on use:sn_unmorphing.
 Qed.
 
-Lemma SemWt_Univ n Γ (A : PTm n) i  :
-  Γ ⊨ A ∈ PUniv i <->
-  forall ρ, ρ_ok Γ ρ -> exists S, ⟦ subst_PTm ρ A ⟧ i ↘ S.
-Proof.
-  rewrite /SemWt.
-  split.
-  - hauto lq:on rew:off use:InterpUniv_Univ_inv.
-  - move => /[swap] ρ /[apply].
-    move => [PA hPA].
-    exists (S i). eexists.
-    split.
-    + simp InterpUniv. apply InterpExt_Univ. lia.
-    + simpl. eauto.
-Qed.
+Lemma SemEq_SN_Join n Γ (a b A : PTm n) :
+  Γ ⊨ a ≡ b ∈ A ->
+  SN a /\ SN b /\ SN A /\ DJoin.R a b.
+Proof. hauto l:on use:SemEq_SemWt, SemWt_SN. Qed.
+
+Lemma SemLEq_SN_Sub n Γ (a b : PTm n) :
+  Γ ⊨ a ≲ b ->
+  SN a /\ SN b /\ Sub.R a b.
+Proof. hauto l:on use:SemLEq_SemWt, SemWt_SN. Qed.
 
 (* Structural laws for Semantic context wellformedness *)
 Lemma SemWff_nil : SemWff null.
@@ -573,7 +702,7 @@ Proof.
 Qed.
 
 
-Lemma ST_Bind n Γ i j p (A : PTm n) (B : PTm (S n)) :
+Lemma ST_Bind' n Γ i j p (A : PTm n) (B : PTm (S n)) :
   Γ ⊨ A ∈ PUniv i ->
   funcomp (ren_PTm shift) (scons A Γ) ⊨ B ∈ PUniv j ->
   Γ ⊨ PBind p A B ∈ PUniv (max i j).
@@ -588,6 +717,17 @@ Proof.
   - move => *. asimpl. hauto l:on use:InterpUniv_cumulative, ρ_ok_cons.
 Qed.
 
+Lemma ST_Bind n Γ i p (A : PTm n) (B : PTm (S n)) :
+  Γ ⊨ A ∈ PUniv i ->
+  funcomp (ren_PTm shift) (scons A Γ) ⊨ B ∈ PUniv i ->
+  Γ ⊨ PBind p A B ∈ PUniv i.
+Proof.
+  move => h0 h1.
+  replace i with (max i i) by lia.
+  move : h0 h1.
+  apply ST_Bind'.
+Qed.
+
 Lemma ST_Abs n Γ (a : PTm (S n)) A B i :
   Γ ⊨ PBind PPi A B ∈ (PUniv i) ->
   funcomp (ren_PTm shift) (scons A Γ) ⊨ a ∈ B ->
@@ -626,6 +766,13 @@ Proof.
   asimpl. hauto lq:on.
 Qed.
 
+Lemma ST_App' n Γ (b a : PTm n) A B U :
+  U = subst_PTm (scons a VarPTm) B ->
+  Γ ⊨ b ∈ PBind PPi A B ->
+  Γ ⊨ a ∈ A ->
+  Γ ⊨ PApp b a ∈ U.
+Proof. move => ->. apply ST_App. Qed.
+
 Lemma ST_Pair n Γ (a b : PTm n) A B i :
   Γ ⊨ PBind PSig A B ∈ (PUniv i) ->
   Γ ⊨ a ∈ A ->
@@ -718,35 +865,471 @@ Proof.
       move : hPB. asimpl => hPB.
       suff : DJoin.R (subst_PTm (scons (PProj PL (subst_PTm ρ a)) ρ) B) (subst_PTm (scons a0 ρ) B).
       move : InterpUniv_Join hPB0 hPB; repeat move/[apply]. done.
-      suff : BJoin.R (subst_PTm (scons (PProj PL (subst_PTm ρ a)) ρ) B) (subst_PTm (scons a0 ρ) B)
-        by hauto q:on use:DJoin.FromBJoin.
-      have : BJoin.R (PApp (PAbs (subst_PTm (up_PTm_PTm ρ) B)) (PProj PL (subst_PTm ρ a)))
-               (subst_PTm (scons (PProj PL (subst_PTm ρ a)) ρ) B).
-      eexists. split. apply relations.rtc_once. apply RRed.AppAbs.
-      asimpl. apply rtc_refl.
-      have /BJoin.symmetric : BJoin.R (PApp (PAbs (subst_PTm (up_PTm_PTm ρ)B)) a0)
-                                (subst_PTm (scons a0 ρ) B).
-      eexists. split. apply relations.rtc_once. apply RRed.AppAbs.
-      asimpl. apply rtc_refl.
-      suff : BJoin.R (PApp (PAbs (subst_PTm (up_PTm_PTm ρ) B)) (PProj PL (subst_PTm ρ a)))
-               (PApp (PAbs (subst_PTm (up_PTm_PTm ρ)B)) a0) by eauto using BJoin.transitive, BJoin.symmetric.
-      apply BJoin.AppCong. apply BJoin.refl.
-      move /RReds.FromRedSNs : hr'.
+      apply DJoin.cong.
+      apply DJoin.FromRedSNs.
       hauto lq:on ctrs:rtc unfold:BJoin.R.
     + hauto lq:on use:@relations.rtc_r, InterpUniv_back_closs.
 Qed.
 
-Lemma ST_Conv n Γ (a : PTm n) A B i :
+Lemma ST_Conv' n Γ (a : PTm n) A B i :
+  Γ ⊨ a ∈ A ->
+  Γ ⊨ B ∈ PUniv i ->
+  Sub.R A B ->
+  Γ ⊨ a ∈ B.
+Proof.
+  move => ha /SemWt_Univ h h0.
+  move => ρ hρ.
+  have {}h0 : Sub.R (subst_PTm ρ A) (subst_PTm ρ B) by
+    eauto using Sub.substing.
+  move /ha : (hρ){ha} => [m [PA [h1 h2]]].
+  move /h : (hρ){h} => [S hS].
+  have h3 : forall x, PA x -> S x.
+  move : InterpUniv_Sub h0 h1 hS; by repeat move/[apply].
+  hauto lq:on.
+Qed.
+
+Lemma ST_Conv_E n Γ (a : PTm n) A B i :
   Γ ⊨ a ∈ A ->
   Γ ⊨ B ∈ PUniv i ->
   DJoin.R A B ->
   Γ ⊨ a ∈ B.
 Proof.
-  move => ha /SemWt_Univ h h0.
-  move => ρ hρ.
-  have {}h0 : DJoin.R (subst_PTm ρ A) (subst_PTm ρ B) by eauto using DJoin.substing.
-  move /ha : (hρ){ha} => [m [PA [h1 h2]]].
-  move /h : (hρ){h} => [S hS].
-  have ? : PA = S by eauto using InterpUniv_Join'. subst.
-  eauto.
+  hauto l:on use:ST_Conv', Sub.FromJoin.
 Qed.
+
+Lemma ST_Conv n Γ (a : PTm n) A B :
+  Γ ⊨ a ∈ A ->
+  Γ ⊨ A ≲ B ->
+  Γ ⊨ a ∈ B.
+Proof. hauto l:on use:ST_Conv', SemLEq_SemWt. Qed.
+
+Lemma SE_Refl n Γ (a : PTm n) A :
+  Γ ⊨ a ∈ A ->
+  Γ ⊨ a ≡ a ∈ A.
+Proof. hauto lq:on unfold:SemWt,SemEq use:DJoin.refl. Qed.
+
+Lemma SE_Symmetric n Γ (a b : PTm n) A :
+  Γ ⊨ a ≡ b ∈ A ->
+  Γ ⊨ b ≡ a ∈ A.
+Proof. hauto q:on unfold:SemEq. Qed.
+
+Lemma SE_Transitive n Γ (a b c : PTm n) A :
+  Γ ⊨ a ≡ b ∈ A ->
+  Γ ⊨ b ≡ c ∈ A ->
+  Γ ⊨ a ≡ c ∈ A.
+Proof.
+  move => ha hb.
+  apply SemEq_SemWt in ha, hb.
+  have ? : SN b by hauto l:on use:SemWt_SN.
+  apply SemWt_SemEq; try tauto.
+  hauto l:on use:DJoin.transitive.
+Qed.
+
+Definition Γ_eq {n} (Γ Δ : fin n -> PTm n)  := forall i, DJoin.R (Γ i) (Δ i).
+
+Lemma Γ_eq_ρ_ok n Γ Δ (ρ : fin n -> PTm 0) : Γ_eq Γ Δ -> ⊨ Γ -> ρ_ok Γ ρ -> ρ_ok Δ ρ.
+Proof.
+  move => hΓΔ hΓ h.
+  move => i k PA hPA.
+  move : hΓ. rewrite /SemWff. move /(_ i) => [j].
+  move => hΓ.
+  rewrite SemWt_Univ in hΓ.
+  have {}/hΓ  := h.
+  move => [S hS].
+  move /(_ i) in h. suff : PA = S by qauto l:on.
+  move : InterpUniv_Join' hPA hS. repeat move/[apply].
+  apply. move /(_ i) /DJoin.symmetric in hΓΔ.
+  hauto l:on use: DJoin.substing.
+Qed.
+
+Definition Γ_sub {n} (Γ Δ : fin n -> PTm n)  := forall i, Sub.R (Γ i) (Δ i).
+
+Lemma Γ_sub_ρ_ok n Γ Δ (ρ : fin n -> PTm 0) : Γ_sub Γ Δ -> ⊨ Γ -> ρ_ok Γ ρ -> ρ_ok Δ ρ.
+Proof.
+  move => hΓΔ hΓ h.
+  move => i k PA hPA.
+  move : hΓ. rewrite /SemWff. move /(_ i) => [j].
+  move => hΓ.
+  rewrite SemWt_Univ in hΓ.
+  have {}/hΓ  := h.
+  move => [S hS].
+  move /(_ i) in h. suff : forall x, S x -> PA x by qauto l:on.
+  move : InterpUniv_Sub hS hPA. repeat move/[apply].
+  apply. by apply Sub.substing.
+Qed.
+
+Lemma Γ_sub_refl n (Γ : fin n -> PTm n) :
+  Γ_sub Γ Γ.
+Proof. sfirstorder use:Sub.refl. Qed.
+
+Lemma Γ_sub_cons n (Γ Δ : fin n -> PTm n) A B :
+  Sub.R A B ->
+  Γ_sub Γ Δ ->
+  Γ_sub (funcomp (ren_PTm shift) (scons A Γ)) (funcomp (ren_PTm shift) (scons B Δ)).
+Proof.
+  move => h h0.
+  move => i.
+  destruct i as [i|].
+  rewrite /funcomp. substify. apply Sub.substing. by asimpl.
+  rewrite /funcomp.
+  asimpl. substify. apply Sub.substing. by asimpl.
+Qed.
+
+Lemma Γ_sub_cons' n (Γ : fin n -> PTm n) A B :
+  Sub.R A B ->
+  Γ_sub (funcomp (ren_PTm shift) (scons A Γ)) (funcomp (ren_PTm shift) (scons B Γ)).
+Proof. eauto using Γ_sub_refl ,Γ_sub_cons. Qed.
+
+Lemma Γ_eq_refl n (Γ : fin n -> PTm n) :
+  Γ_eq Γ Γ.
+Proof. sfirstorder use:DJoin.refl. Qed.
+
+Lemma Γ_eq_cons n (Γ Δ : fin n -> PTm n) A B :
+  DJoin.R A B ->
+  Γ_eq Γ Δ ->
+  Γ_eq (funcomp (ren_PTm shift) (scons A Γ)) (funcomp (ren_PTm shift) (scons B Δ)).
+Proof.
+  move => h h0.
+  move => i.
+  destruct i as [i|].
+  rewrite /funcomp. substify. apply DJoin.substing. by asimpl.
+  rewrite /funcomp.
+  asimpl. substify. apply DJoin.substing. by asimpl.
+Qed.
+Lemma Γ_eq_cons' n (Γ : fin n -> PTm n) A B :
+  DJoin.R A B ->
+  Γ_eq (funcomp (ren_PTm shift) (scons A Γ)) (funcomp (ren_PTm shift) (scons B Γ)).
+Proof. eauto using Γ_eq_refl ,Γ_eq_cons. Qed.
+
+Lemma SE_Bind' n Γ i j p (A0 A1 : PTm n) B0 B1 :
+  ⊨ Γ ->
+  Γ ⊨ A0 ≡ A1 ∈ PUniv i ->
+  funcomp (ren_PTm shift) (scons A0 Γ) ⊨ B0 ≡ B1 ∈ PUniv j ->
+  Γ ⊨ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv (max i j).
+Proof.
+  move => hΓ hA hB.
+  apply SemEq_SemWt in hA, hB.
+  apply SemWt_SemEq; last by hauto l:on use:DJoin.BindCong.
+  hauto l:on use:ST_Bind'.
+  apply ST_Bind'; first by tauto.
+  have hΓ' : ⊨ funcomp (ren_PTm shift) (scons A1 Γ) by hauto l:on use:SemWff_cons.
+  move => ρ hρ.
+  suff : ρ_ok (funcomp (ren_PTm shift) (scons A0 Γ)) ρ by hauto l:on.
+  move : Γ_eq_ρ_ok hΓ' hρ; repeat move/[apply]. apply.
+  hauto lq:on use:Γ_eq_cons'.
+Qed.
+
+Lemma SE_Bind n Γ i p (A0 A1 : PTm n) B0 B1 :
+  ⊨ Γ ->
+  Γ ⊨ A0 ≡ A1 ∈ PUniv i ->
+  funcomp (ren_PTm shift) (scons A0 Γ) ⊨ B0 ≡ B1 ∈ PUniv i ->
+  Γ ⊨ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv i.
+Proof.
+  move => *. replace i with (max i i) by lia. auto using SE_Bind'.
+Qed.
+
+Lemma SE_Abs n Γ (a b : PTm (S n)) A B i :
+  Γ ⊨ PBind PPi A B ∈ (PUniv i) ->
+  funcomp (ren_PTm shift) (scons A Γ) ⊨ a ≡ b ∈ B ->
+  Γ ⊨ PAbs a ≡ PAbs b ∈ PBind PPi A B.
+Proof.
+  move => hPi /SemEq_SemWt [ha][hb]he.
+  apply SemWt_SemEq; eauto using DJoin.AbsCong, ST_Abs.
+Qed.
+
+Lemma SBind_inv1 n Γ i p (A : PTm n) B :
+  Γ ⊨ PBind p A B ∈ PUniv i ->
+  Γ ⊨ A ∈ PUniv i.
+  move /SemWt_Univ => h. apply SemWt_Univ.
+  hauto lq:on rew:off  use:InterpUniv_Bind_inv.
+Qed.
+
+Lemma SE_AppEta n Γ (b : PTm n) 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.
+Proof.
+  move => hΓ h0 h1. apply SemWt_SemEq; eauto.
+  apply : ST_Abs; eauto.
+  have hA : Γ ⊨ A ∈ PUniv i by eauto using SBind_inv1.
+  eapply ST_App' with (A := ren_PTm shift A)(B:= ren_PTm (upRen_PTm_PTm shift) B). by asimpl.
+  2 : {
+    apply ST_Var.
+    eauto using SemWff_cons.
+  }
+  change (PBind PPi (ren_PTm shift A) (ren_PTm (upRen_PTm_PTm shift) B)) with
+    (ren_PTm shift (PBind PPi A B)).
+  apply : weakening_Sem; eauto.
+  hauto q:on ctrs:rtc,RERed.R.
+Qed.
+
+Lemma SE_AppAbs n Γ (a : PTm (S n)) b A B i:
+  Γ ⊨ PBind PPi A B ∈ PUniv i ->
+  Γ ⊨ b ∈ A ->
+  funcomp (ren_PTm shift) (scons A Γ) ⊨ a ∈ B ->
+  Γ ⊨ PApp (PAbs a) b ≡ subst_PTm (scons b VarPTm) a ∈ subst_PTm (scons b VarPTm ) B.
+Proof.
+  move => h h0 h1. apply SemWt_SemEq; eauto using ST_App, ST_Abs.
+  move => ρ hρ.
+  have {}/h0 := hρ.
+  move => [k][PA][hPA]hb.
+  move : ρ_ok_cons hPA hb (hρ); repeat move/[apply].
+  move => {}/h1.
+  by asimpl.
+  apply DJoin.FromRRed0.
+  apply RRed.AppAbs.
+Qed.
+
+Lemma SE_Conv' n Γ (a b : PTm n) A B i :
+  Γ ⊨ a ≡ b ∈ A ->
+  Γ ⊨ B ∈ PUniv i ->
+  Sub.R A B ->
+  Γ ⊨ a ≡ b ∈ B.
+Proof.
+  move /SemEq_SemWt => [ha][hb]he hB hAB.
+  apply SemWt_SemEq; eauto using ST_Conv'.
+Qed.
+
+Lemma SE_Conv n Γ (a b : PTm n) A B :
+  Γ ⊨ a ≡ b ∈ A ->
+  Γ ⊨ A ≲ B ->
+  Γ ⊨ a ≡ b ∈ B.
+Proof.
+  move => h /SemLEq_SemWt [h0][h1][ha]hb.
+  eauto using SE_Conv'.
+Qed.
+
+Lemma SBind_inst n Γ p i (A : PTm n) B (a : PTm n) :
+  Γ ⊨ a ∈ A ->
+  Γ ⊨ PBind p A B ∈ PUniv i ->
+  Γ ⊨ subst_PTm (scons a VarPTm) B ∈ PUniv i.
+Proof.
+  move => ha /SemWt_Univ hb.
+  apply SemWt_Univ.
+  move => ρ hρ.
+  have {}/hb := hρ.
+  asimpl. move => /= [S hS].
+  move /InterpUniv_Bind_inv_nopf : hS.
+  move => [PA][hPA][hPF]?. subst.
+  have {}/ha := hρ.
+  move => [k][PA0][hPA0]ha.
+  have ? : PA0 = PA by hauto l:on use:InterpUniv_Functional'. subst.
+  have {}/hPF := ha.
+  move => [PB]. asimpl.
+  hauto lq:on.
+Qed.
+
+Lemma SE_Pair n Γ (a0 a1 b0 b1 : PTm n) 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.
+Proof.
+  move => h /SemEq_SemWt [ha0][ha1]hae /SemEq_SemWt [hb0][hb1]hbe.
+  apply SemWt_SemEq; eauto using ST_Pair, DJoin.PairCong, SBind_inst, DJoin.cong, ST_Conv_E, ST_Pair.
+Qed.
+
+Lemma SE_Proj1 n Γ (a b : PTm n) A B :
+  Γ ⊨ a ≡ b ∈ PBind PSig A B ->
+  Γ ⊨ PProj PL a ≡ PProj PL b ∈ A.
+Proof.
+  move => /SemEq_SemWt [ha][hb]he.
+  apply SemWt_SemEq; eauto using DJoin.ProjCong, ST_Proj1.
+Qed.
+
+Lemma SE_Proj2 n Γ i (a b : PTm n) 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.
+Proof.
+  move => hS.
+  move => /SemEq_SemWt [ha][hb]he.
+  apply SemWt_SemEq; eauto using DJoin.ProjCong, ST_Proj2.
+  have h : Γ ⊨ PProj PR b ∈ subst_PTm (scons (PProj PL b) VarPTm) B by eauto using ST_Proj2.
+  apply : ST_Conv_E. apply h.
+  apply : SBind_inst. eauto using ST_Proj1.
+  eauto.
+  hauto lq:on use: DJoin.cong,  DJoin.ProjCong.
+Qed.
+
+Lemma SE_ProjPair1 n Γ (a b : PTm n) 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.
+Proof.
+  move => h0 h1 h2.
+  apply SemWt_SemEq; eauto using ST_Proj1, ST_Pair.
+  apply DJoin.FromRRed0. apply RRed.ProjPair.
+Qed.
+
+Lemma SE_ProjPair2 n Γ (a b : PTm n) 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.
+Proof.
+  move => h0 h1 h2.
+  apply SemWt_SemEq; eauto using ST_Proj2, ST_Pair.
+  apply : ST_Conv_E. apply : ST_Proj2; eauto. apply : ST_Pair; eauto.
+  hauto l:on use:SBind_inst.
+  apply DJoin.cong. apply DJoin.FromRRed0. apply RRed.ProjPair.
+  apply DJoin.FromRRed0. apply RRed.ProjPair.
+Qed.
+
+Lemma SE_PairEta n Γ (a : PTm n) 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.
+Proof.
+  move => h0 h. apply SemWt_SemEq; eauto.
+  apply : ST_Pair; eauto using ST_Proj1, ST_Proj2.
+  rewrite /DJoin.R. hauto lq:on ctrs:rtc,RERed.R.
+Qed.
+
+Lemma SE_App n Γ i (b0 b1 a0 a1 : PTm n) 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.
+Proof.
+  move => hPi.
+  move => /SemEq_SemWt [hb0][hb1]hb /SemEq_SemWt [ha0][ha1]ha.
+  apply SemWt_SemEq; eauto using DJoin.AppCong, ST_App.
+  apply : ST_Conv_E; eauto using ST_App, DJoin.cong, DJoin.symmetric, SBind_inst.
+Qed.
+
+Lemma SSu_Eq n Γ (A B : PTm n) i :
+  Γ ⊨ A ≡ B ∈ PUniv i ->
+  Γ ⊨ A ≲ B.
+Proof. move /SemEq_SemWt => h.
+       qauto l:on use:SemWt_SemLEq, Sub.FromJoin.
+Qed.
+
+Lemma SSu_Transitive n Γ (A B C : PTm n) :
+  Γ ⊨ A ≲ B ->
+  Γ ⊨ B ≲ C ->
+  Γ ⊨ A ≲ C.
+Proof.
+  move => ha hb.
+  apply SemLEq_SemWt in ha, hb.
+  have ? : SN B by hauto l:on use:SemWt_SN.
+  move : ha => [ha0 [i [ha1 ha2]]]. move : hb => [hb0 [j [hb1 hb2]]].
+  qauto l:on use:SemWt_SemLEq, Sub.transitive.
+Qed.
+
+Lemma ST_Univ' n Γ i j :
+  i < j ->
+  Γ ⊨ PUniv i : PTm n ∈ PUniv j.
+Proof.
+  move => ?.
+  apply SemWt_Univ. move => ρ hρ. eexists. by apply InterpUniv_Univ.
+Qed.
+
+Lemma ST_Univ n Γ i :
+  Γ ⊨ PUniv i : PTm n ∈ PUniv (S i).
+Proof.
+  apply ST_Univ'. lia.
+Qed.
+
+Lemma SSu_Univ n Γ i j :
+  i <= j ->
+  Γ ⊨ PUniv i : PTm n ≲ PUniv j.
+Proof.
+  move => h. apply : SemWt_SemLEq; eauto using ST_Univ.
+  sauto lq:on.
+Qed.
+
+Lemma SSu_Pi n Γ (A0 A1 : PTm n) B0 B1 :
+  ⊨ Γ ->
+  Γ ⊨ A1 ≲ A0 ->
+  funcomp (ren_PTm shift) (scons A0 Γ) ⊨ B0 ≲ B1 ->
+  Γ ⊨ PBind PPi A0 B0 ≲ PBind PPi A1 B1.
+Proof.
+  move => hΓ hA hB.
+  have ? : SN A0 /\ SN A1 /\ SN B0 /\ SN B1
+    by hauto l:on use:SemLEq_SN_Sub.
+  apply SemLEq_SemWt in hA, hB.
+  move : hA => [hA0][i][hA1]hA2.
+  move : hB => [hB0][j][hB1]hB2.
+  apply : SemWt_SemLEq; last by hauto l:on use:Sub.PiCong.
+  hauto l:on use:ST_Bind'.
+  apply ST_Bind'; eauto.
+  have hΓ' : ⊨ funcomp (ren_PTm shift) (scons A1 Γ) by hauto l:on use:SemWff_cons.
+  move => ρ hρ.
+  suff : ρ_ok (funcomp (ren_PTm shift) (scons A0 Γ)) ρ by hauto l:on.
+  move : Γ_sub_ρ_ok hΓ' hρ; repeat move/[apply]. apply.
+  hauto lq:on use:Γ_sub_cons'.
+Qed.
+
+Lemma SSu_Sig n Γ (A0 A1 : PTm n) B0 B1 :
+  ⊨ Γ ->
+  Γ ⊨ A0 ≲ A1 ->
+  funcomp (ren_PTm shift) (scons A1 Γ) ⊨ B0 ≲ B1 ->
+  Γ ⊨ PBind PSig A0 B0 ≲ PBind PSig A1 B1.
+Proof.
+  move => hΓ hA hB.
+  have ? : SN A0 /\ SN A1 /\ SN B0 /\ SN B1
+    by hauto l:on use:SemLEq_SN_Sub.
+  apply SemLEq_SemWt in hA, hB.
+  move : hA => [hA0][i][hA1]hA2.
+  move : hB => [hB0][j][hB1]hB2.
+  apply : SemWt_SemLEq; last by hauto l:on use:Sub.SigCong.
+  2 : { hauto l:on use:ST_Bind'. }
+  apply ST_Bind'; eauto.
+  have hΓ' : ⊨ funcomp (ren_PTm shift) (scons A1 Γ) by hauto l:on use:SemWff_cons.
+  have hΓ'' : ⊨ funcomp (ren_PTm shift) (scons A0 Γ) by hauto l:on use:SemWff_cons.
+  move => ρ hρ.
+  suff : ρ_ok (funcomp (ren_PTm shift) (scons A1 Γ)) ρ by hauto l:on.
+  apply : Γ_sub_ρ_ok; eauto.
+  hauto lq:on use:Γ_sub_cons'.
+Qed.
+
+Lemma SSu_Pi_Proj1 n Γ (A0 A1 : PTm n) B0 B1 :
+  Γ ⊨ PBind PPi A0 B0 ≲ PBind PPi A1 B1 ->
+  Γ ⊨ A1 ≲ A0.
+Proof.
+  move /SemLEq_SemWt => [h0][h1][h2]he.
+  apply : SemWt_SemLEq; eauto using SBind_inv1.
+  hauto lq:on rew:off use:Sub.bind_inj.
+Qed.
+
+Lemma SSu_Sig_Proj1 n Γ (A0 A1 : PTm n) B0 B1 :
+  Γ ⊨ PBind PSig A0 B0 ≲ PBind PSig A1 B1 ->
+  Γ ⊨ A0 ≲ A1.
+Proof.
+  move /SemLEq_SemWt => [h0][h1][h2]he.
+  apply : SemWt_SemLEq; eauto using SBind_inv1.
+  hauto lq:on rew:off use:Sub.bind_inj.
+Qed.
+
+Lemma SSu_Pi_Proj2 n Γ (a0 a1 A0 A1 : PTm n) 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.
+Proof.
+  move /SemLEq_SemWt => [/Sub.bind_inj [_ [h1 h2]]].
+  move => [i][hP0]hP1 /SemEq_SemWt [ha0][ha1]ha.
+  apply : SemWt_SemLEq; eauto using SBind_inst;
+    last by hauto l:on use:Sub.cong.
+  apply SBind_inst with (p := PPi) (A := A0); eauto.
+  apply : ST_Conv'; eauto. hauto l:on use:SBind_inv1.
+Qed.
+
+Lemma SSu_Sig_Proj2 n Γ (a0 a1 A0 A1 : PTm n) 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.
+Proof.
+  move /SemLEq_SemWt => [/Sub.bind_inj [_ [h1 h2]]].
+  move => [i][hP0]hP1 /SemEq_SemWt [ha0][ha1]ha.
+  apply : SemWt_SemLEq; eauto using SBind_inst;
+    last by hauto l:on use:Sub.cong.
+  apply SBind_inst with (p := PSig) (A := A1); eauto.
+  apply : ST_Conv'; eauto. hauto l:on use:SBind_inv1.
+Qed.
+
+#[export]Hint Resolve ST_Var ST_Bind ST_Abs ST_App ST_Pair ST_Proj1 ST_Proj2 ST_Univ ST_Conv
+  SE_Refl SE_Symmetric SE_Transitive SE_Bind SE_Abs SE_App SE_Proj1 SE_Proj2
+  SE_Conv SSu_Pi_Proj1 SSu_Pi_Proj2 SSu_Sig_Proj1 SSu_Sig_Proj2 SSu_Eq SSu_Transitive SSu_Pi SSu_Sig SemWff_nil SemWff_cons SSu_Univ SE_AppAbs SE_ProjPair1 SE_ProjPair2 SE_AppEta SE_PairEta : sem.

theories/preservation.v

@@ -0,0 +1,179 @@
+Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax common typing structural fp_red.
+From Hammer Require Import Tactics.
+Require Import ssreflect.
+Require Import Psatz.
+Require Import Coq.Logic.FunctionalExtensionality.
+
+Lemma App_Inv n Γ (b a : PTm n) U :
+  Γ ⊢ PApp b a ∈ U ->
+  exists A B, Γ ⊢ b ∈ PBind PPi A B /\ Γ ⊢ a ∈ A /\ Γ ⊢ subst_PTm (scons a VarPTm) B ≲ U.
+Proof.
+  move E : (PApp b a) => u hu.
+  move : b a E. elim : n Γ u U / hu => n //=.
+  - move => Γ b a A B hb _ ha _ b0 a0 [*]. subst.
+    exists A,B.
+    repeat split => //=.
+    have [i] : exists i, Γ ⊢ PBind PPi A B ∈  PUniv i by sfirstorder use:regularity.
+    hauto lq:on use:bind_inst, E_Refl.
+  - hauto lq:on rew:off ctrs:LEq.
+Qed.
+
+Lemma Abs_Inv n Γ (a : PTm (S n)) U :
+  Γ ⊢ PAbs a ∈ U ->
+  exists A B, funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B /\ Γ ⊢ PBind PPi A B ≲ U.
+Proof.
+  move E : (PAbs a) => u hu.
+  move : a E. elim : n Γ u U / hu => n //=.
+  - move => Γ a A B i hP _ ha _ a0 [*]. subst.
+    exists A, B. repeat split => //=.
+    hauto lq:on use:E_Refl, Su_Eq.
+  - hauto lq:on rew:off ctrs:LEq.
+Qed.
+
+Lemma Proj1_Inv n Γ (a : PTm n) U :
+  Γ ⊢ PProj PL a ∈ U ->
+  exists A B, Γ ⊢ a ∈ PBind PSig A B /\ Γ ⊢ A ≲ U.
+Proof.
+  move E : (PProj PL a) => u hu.
+  move :a E. elim : n Γ u U / hu => n //=.
+  - move => Γ a A B ha _ a0 [*]. subst.
+    exists A, B. split => //=.
+    eapply regularity in ha.
+    move : ha => [i].
+    move /Bind_Inv => [j][h _].
+    by move /E_Refl /Su_Eq in h.
+  - hauto lq:on rew:off ctrs:LEq.
+Qed.
+
+Lemma Proj2_Inv n Γ (a : PTm n) U :
+  Γ ⊢ PProj PR a ∈ U ->
+  exists A B, Γ ⊢ a ∈ PBind PSig A B /\ Γ ⊢ subst_PTm (scons (PProj PL a) VarPTm) B ≲ U.
+Proof.
+  move E : (PProj PR a) => u hu.
+  move :a E. elim : n Γ u U / hu => n //=.
+  - move => Γ a A B ha _ a0 [*]. subst.
+    exists A, B. split => //=.
+    have ha' := ha.
+    eapply regularity in ha.
+    move : ha => [i ha].
+    move /T_Proj1 in ha'.
+    apply : bind_inst; eauto.
+    apply : E_Refl ha'.
+  - hauto lq:on rew:off ctrs:LEq.
+Qed.
+
+Lemma Pair_Inv n Γ (a b : PTm n) U :
+  Γ ⊢ PPair a b ∈ U ->
+  exists A B, Γ ⊢ a ∈ A /\
+         Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B /\
+         Γ ⊢ PBind PSig A B ≲ U.
+Proof.
+  move E : (PPair a b) => u hu.
+  move : a b E. elim : n Γ u U / hu => n //=.
+  - move => Γ a b A B i hS _ ha _ hb _ a0 b0 [*]. subst.
+    exists A,B. repeat split => //=.
+    move /E_Refl /Su_Eq : hS. apply.
+  - hauto lq:on rew:off ctrs:LEq.
+Qed.
+
+Lemma E_AppAbs : forall n (a : PTm (S n)) (b : PTm n) (Γ : fin n -> PTm n) (A : PTm n),
+  Γ ⊢ PApp (PAbs a) b ∈ A -> Γ ⊢ PApp (PAbs a) b ≡ subst_PTm (scons b VarPTm) a ∈ A.
+Proof.
+  move => n a b Γ A ha.
+  move /App_Inv : ha.
+  move => [A0][B0][ha][hb]hS.
+  move /Abs_Inv : ha => [A1][B1][ha]hS0.
+  have hb' := hb.
+  move /E_Refl in hb.
+  have hS1 : Γ ⊢ A0 ≲ A1 by sfirstorder use:Su_Pi_Proj1.
+  have [i hPi] : exists i, Γ ⊢ PBind PPi A1 B1 ∈ PUniv i by sfirstorder use:regularity_sub0.
+  move : Su_Pi_Proj2 hS0 hb; repeat move/[apply].
+  move : hS => /[swap]. move : Su_Transitive. repeat move/[apply].
+  move => h.
+  apply : E_Conv; eauto.
+  apply : E_AppAbs; eauto.
+  eauto using T_Conv.
+Qed.
+
+Lemma E_ProjPair1 : forall n (a b : PTm n) (Γ : fin n -> PTm n) (A : PTm n),
+    Γ ⊢ PProj PL (PPair a b) ∈ A -> Γ ⊢ PProj PL (PPair a b) ≡ a ∈ A.
+Proof.
+  move => n a b Γ A.
+  move /Proj1_Inv. move => [A0][B0][hab]hA0.
+  move /Pair_Inv : hab => [A1][B1][ha][hb]hS.
+  have [i ?]  : exists i, Γ ⊢ PBind PSig A1 B1 ∈ PUniv i by sfirstorder use:regularity_sub0.
+  move /Su_Sig_Proj1 in hS.
+  have {hA0} {}hS : Γ ⊢ A1 ≲ A by eauto using Su_Transitive.
+  apply : E_Conv; eauto.
+  apply : E_ProjPair1; eauto.
+Qed.
+
+Lemma RRed_Eq n Γ (a b : PTm n) A :
+  Γ ⊢ a ∈ A ->
+  RRed.R a b ->
+  Γ ⊢ a ≡ b ∈ A.
+Proof.
+  move => + h. move : Γ A. elim : n a b /h => n.
+  - apply E_AppAbs.
+  - move => p a b Γ A.
+    case : p => //=.
+    + apply E_ProjPair1.
+    + move /Proj2_Inv. move => [A0][B0][hab]hA0.
+      move /Pair_Inv : hab => [A1][B1][ha][hb]hS.
+      have [i ?]  : exists i, Γ ⊢ PBind PSig A1 B1 ∈ PUniv i by sfirstorder use:regularity_sub0.
+      have : Γ ⊢ PPair a b ∈ PBind PSig A1 B1 by hauto lq:on ctrs:Wt.
+      move /T_Proj1.
+      move /E_ProjPair1 /E_Symmetric => h.
+      have /Su_Sig_Proj1 hSA := hS.
+      have : Γ ⊢ subst_PTm (scons a VarPTm) B1 ≲ subst_PTm (scons (PProj PL (PPair a b)) VarPTm) B0 by
+        apply : Su_Sig_Proj2; eauto.
+      move : hA0 => /[swap]. move : Su_Transitive. repeat move/[apply].
+      move {hS}.
+      move => ?. apply : E_Conv; eauto. apply : E_ProjPair2; eauto.
+  - qauto l:on use:Abs_Inv, E_Conv, regularity_sub0, E_Abs.
+  - move => a0 a1 b ha iha Γ A /App_Inv [A0][B0][ih0][ih1]hU.
+    have {}/iha iha := ih0.
+    have [i hP] : exists i, Γ ⊢ PBind PPi A0 B0 ∈ PUniv i by sfirstorder use:regularity.
+    apply : E_Conv; eauto.
+    apply : E_App; eauto using E_Refl.
+  - move => a0 b0 b1 ha iha Γ A /App_Inv [A0][B0][ih0][ih1]hU.
+    have {}/iha iha := ih1.
+    have [i hP] : exists i, Γ ⊢ PBind PPi A0 B0 ∈ PUniv i by sfirstorder use:regularity.
+    apply : E_Conv; eauto.
+    apply : E_App; eauto.
+    sfirstorder use:E_Refl.
+  - move => a0 a1 b ha iha Γ A /Pair_Inv.
+    move => [A0][B0][h0][h1]hU.
+    have [i hP] : exists i, Γ ⊢ PBind PSig A0 B0 ∈ PUniv i by eauto using regularity_sub0.
+    have {}/iha iha := h0.
+    apply : E_Conv; eauto.
+    apply : E_Pair; eauto using E_Refl.
+  - move => a b0 b1 ha iha Γ A /Pair_Inv.
+    move => [A0][B0][h0][h1]hU.
+    have [i hP] : exists i, Γ ⊢ PBind PSig A0 B0 ∈ PUniv i by eauto using regularity_sub0.
+    have {}/iha iha := h1.
+    apply : E_Conv; eauto.
+    apply : E_Pair; eauto using E_Refl.
+  - case.
+    + move => a0 a1 ha iha Γ A /Proj1_Inv [A0][B0][h0]hU.
+      apply : E_Conv; eauto.
+      qauto l:on ctrs:Eq,Wt.
+    + move => a0 a1 ha iha Γ A /Proj2_Inv [A0][B0][h0]hU.
+      have [i hP] : exists i, Γ ⊢ PBind PSig A0 B0 ∈ PUniv i by sfirstorder use:regularity.
+      apply : E_Conv; eauto.
+      apply : E_Proj2; eauto.
+  - move => p A0 A1 B hA ihA Γ U /Bind_Inv [i][h0][h1]hU.
+    have {}/ihA ihA := h0.
+    apply : E_Conv; eauto.
+    apply E_Bind'; eauto using E_Refl.
+  - move => p A0 A1 B hA ihA Γ U /Bind_Inv [i][h0][h1]hU.
+    have {}/ihA ihA := h1.
+    apply : E_Conv; eauto.
+    apply E_Bind'; eauto using E_Refl.
+Qed.
+
+Theorem subject_reduction n Γ (a b A : PTm n) :
+  Γ ⊢ a ∈ A ->
+  RRed.R a b ->
+  Γ ⊢ b ∈ A.
+Proof. hauto lq:on use:RRed_Eq, regularity. Qed.

theories/soundness.v

@@ -0,0 +1,15 @@
+Require Import Autosubst2.fintype Autosubst2.syntax.
+Require Import fp_red logrel typing.
+From Hammer Require Import Tactics.
+
+Theorem fundamental_theorem :
+  (forall n (Γ : fin n -> PTm n), ⊢ Γ -> ⊨ Γ) /\
+  (forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> Γ ⊨ a ∈ A)  /\
+  (forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> Γ ⊨ a ≡ b ∈ A) /\
+  (forall n Γ (a b : PTm n), Γ ⊢ a ≲ b -> Γ ⊨ a ≲ b).
+  apply wt_mutual; eauto with sem; [hauto l:on use:SE_Pair].
+  Unshelve. all : exact 0.
+Qed.
+
+Lemma synsub_to_usub : forall n Γ (a b : PTm n), Γ ⊢ a ≲ b -> SN a /\ SN b /\ Sub.R a b.
+Proof. hauto lq:on rew:off use:fundamental_theorem, SemLEq_SN_Sub. Qed.

theories/structural.v

@@ -0,0 +1,676 @@
+Require Import Autosubst2.core Autosubst2.fintype 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 -> ⊢ Γ).
+Proof. apply wt_mutual; eauto. Qed.
+
+#[export]Hint Constructors Wt Wff Eq : wt.
+
+Lemma renaming_up n m (ξ : fin n -> fin m) Δ Γ A :
+  renaming_ok Δ Γ ξ ->
+  renaming_ok (funcomp (ren_PTm shift) (scons (ren_PTm ξ A) Δ)) (funcomp (ren_PTm shift) (scons 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.
+Qed.
+
+Lemma Su_Wt n Γ a i :
+  Γ ⊢ a ∈ @PUniv n i ->
+  Γ ⊢ a ≲ a.
+Proof. hauto lq:on ctrs:LEq, Eq. Qed.
+
+Lemma Wt_Univ n Γ a A i
+  (h : Γ ⊢ a ∈ A) :
+  Γ ⊢ @PUniv n i ∈ PUniv (S i).
+Proof.
+  hauto lq:on ctrs:Wt use:wff_mutual.
+Qed.
+
+Lemma Bind_Inv n Γ p (A : PTm n) B U :
+  Γ ⊢ PBind p A B ∈ U ->
+  exists i, Γ ⊢ A ∈ PUniv i /\
+  funcomp (ren_PTm shift) (scons 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 => //=.
+  - hauto lq:on ctrs:Wt,LEq,Eq use:Wt_Univ.
+  - 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 :
+  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 :
+  U = subst_PTm (scons a VarPTm) B ->
+  Γ ⊢ a ∈ A ->
+  Γ ⊢ b ∈ U ->
+  Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
+  Γ ⊢ PPair a b ∈ PBind PSig A B.
+Proof.
+  move => ->. eauto using T_Pair.
+Qed.
+
+Lemma T_Proj2' n Γ (a : PTm n) A B U :
+  U = subst_PTm (scons (PProj PL a) VarPTm) B ->
+  Γ ⊢ a ∈ PBind PSig A B ->
+  Γ ⊢ PProj PR a ∈ U.
+Proof. move => ->. apply T_Proj2. Qed.
+
+Lemma E_Proj2' n Γ i (a b : PTm n) A B U :
+  U = subst_PTm (scons (PProj PL a) VarPTm) B ->
+  Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
+  Γ ⊢ a ≡ b ∈ PBind PSig A B ->
+  Γ ⊢ PProj PR a ≡ PProj PR b ∈ U.
+Proof.
+  move => ->. apply E_Proj2.
+Qed.
+
+Lemma E_Bind' n Γ i p (A0 A1 : PTm n) B0 B1 :
+  Γ ⊢ A0 ∈ PUniv i ->
+  Γ ⊢ A0 ≡ A1 ∈ PUniv i ->
+  funcomp (ren_PTm shift) (scons A0 Γ) ⊢ B0 ≡ B1 ∈ PUniv i ->
+  Γ ⊢ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv i.
+Proof. hauto lq:on use:E_Bind, wff_mutual. Qed.
+
+Lemma E_App' n Γ i (b0 b1 a0 a1 : PTm n) A B U :
+  U = subst_PTm (scons a0 VarPTm) B ->
+  Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
+  Γ ⊢ b0 ≡ b1 ∈ PBind PPi A B ->
+  Γ ⊢ a0 ≡ a1 ∈ A ->
+  Γ ⊢ PApp b0 a0 ≡ PApp b1 a1 ∈ U.
+Proof. move => ->. apply E_App. Qed.
+
+Lemma E_AppAbs' n Γ (a : PTm (S n)) b A B i u U :
+  u = subst_PTm (scons b VarPTm) a ->
+  U = subst_PTm (scons b VarPTm ) B ->
+  Γ ⊢ PBind PPi A B ∈ PUniv i ->
+  Γ ⊢ b ∈ A ->
+  funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B ->
+  Γ ⊢ PApp (PAbs a) b ≡ u ∈ U.
+  move => -> ->. apply E_AppAbs. Qed.
+
+Lemma E_ProjPair2' n Γ (a b : PTm n) A B i U :
+  U = subst_PTm (scons a VarPTm) B ->
+  Γ ⊢ PBind PSig A B ∈ (PUniv i) ->
+  Γ ⊢ a ∈ A ->
+  Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B ->
+  Γ ⊢ PProj PR (PPair a b) ≡ b ∈ U.
+Proof. move => ->. apply E_ProjPair2. Qed.
+
+Lemma E_AppEta' n Γ (b : PTm n) A B i u :
+  u = (PApp (ren_PTm shift b) (VarPTm var_zero)) ->
+  Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
+  Γ ⊢ b ∈ PBind PPi A B ->
+  Γ ⊢ PAbs u ≡ b ∈ PBind PPi A B.
+Proof. qauto l:on use:wff_mutual, E_AppEta. Qed.
+
+Lemma Su_Pi_Proj2' n Γ (a0 a1 A0 A1 : PTm n) B0 B1 U T :
+  U = subst_PTm (scons a0 VarPTm) B0 ->
+  T = subst_PTm (scons a1 VarPTm) B1 ->
+  Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 ->
+  Γ ⊢ a0 ≡ a1 ∈ A1 ->
+  Γ ⊢ U ≲ T.
+Proof. move => -> ->. apply Su_Pi_Proj2. Qed.
+
+Lemma Su_Sig_Proj2' n Γ (a0 a1 A0 A1 : PTm n) B0 B1 U T :
+  U = subst_PTm (scons a0 VarPTm) B0 ->
+  T = subst_PTm (scons a1 VarPTm) B1 ->
+  Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1 ->
+  Γ ⊢ a0 ≡ a1 ∈ A0 ->
+  Γ ⊢ U ≲ T.
+Proof. move => -> ->. apply Su_Sig_Proj2. Qed.
+
+Lemma renaming :
+  (forall n (Γ : fin n -> PTm n), ⊢ Γ -> True) /\
+  (forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> forall m Δ (ξ : fin n -> fin m), ⊢ Δ -> renaming_ok Δ Γ ξ ->
+     Δ ⊢ ren_PTm ξ a ∈ ren_PTm ξ A) /\
+  (forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> forall m Δ (ξ : fin n -> fin m), ⊢ Δ -> renaming_ok Δ Γ ξ ->
+     Δ ⊢ ren_PTm ξ a ≡ ren_PTm ξ b ∈ ren_PTm ξ A) /\
+  (forall n Γ (A B : PTm n), Γ ⊢ A ≲ B -> forall  m Δ (ξ : fin n -> fin m), ⊢ Δ -> renaming_ok Δ Γ ξ ->
+    Δ ⊢ ren_PTm ξ A ≲ ren_PTm ξ B).
+Proof.
+  apply wt_mutual => //=; eauto 3 with wt.
+  - move => n Γ i hΓ _ m Δ ξ hΔ hξ.
+    rewrite hξ.
+    by apply T_Var.
+  - hauto lq:on rew:off ctrs:Wt, Wff  use:renaming_up.
+  - move => n Γ a A B i hP ihP ha iha m Δ ξ hΔ hξ.
+    apply : T_Abs; eauto.
+    move : ihP(hΔ) (hξ); repeat move/[apply]. move/Bind_Inv.
+    hauto lq:on rew:off ctrs:Wff,Wt use:renaming_up.
+  - move => *. apply : T_App'; eauto. by asimpl.
+  - move => n Γ a A b B i hA ihA hB ihB hS ihS m Δ ξ hξ hΔ.
+    eapply T_Pair' with (U := ren_PTm ξ (subst_PTm (scons a VarPTm) B));eauto. by asimpl.
+  - move => n Γ a A B ha iha m Δ ξ hΔ hξ. apply : T_Proj2'; eauto. by asimpl.
+  - hauto lq:on ctrs:Wt,LEq.
+  - hauto lq:on ctrs:Eq.
+  - hauto lq:on rew:off use:E_Bind', Wff_Cons, renaming_up.
+  - move => n Γ a b A B i hPi ihPi ha iha m Δ ξ hΔ hξ.
+    move : ihPi (hΔ) (hξ). repeat move/[apply].
+    move => /Bind_Inv [j][h0][h1]h2.
+    have ? : Δ ⊢ PBind PPi (ren_PTm ξ A) (ren_PTm (upRen_PTm_PTm ξ) B) ∈ PUniv j by qauto l:on ctrs:Wt.
+    move {hPi}.
+    apply : E_Abs; eauto. qauto l:on ctrs:Wff use:renaming_up.
+  - move => *. apply : E_App'; eauto. by asimpl.
+  - move => n Γ a0 a1 b0 b1 A B i hA ihA ha iha hb ihb m Δ ξ hΔ hξ.
+    apply : E_Pair; eauto.
+    move : ihb hΔ hξ. repeat move/[apply].
+    by asimpl.
+  - move => *. apply : E_Proj2'; eauto. by asimpl.
+  - qauto l:on ctrs:Eq, LEq.
+  - move => n Γ a b A B i hP ihP hb ihb ha iha m Δ ξ hΔ hξ.
+    move : ihP (hξ) (hΔ). repeat move/[apply].
+    move /Bind_Inv.
+    move => [j][h0][h1]h2.
+    have ? : Δ ⊢ PBind PPi (ren_PTm ξ A) (ren_PTm (upRen_PTm_PTm ξ) B) ∈ PUniv j by qauto l:on ctrs:Wt.
+    apply : E_AppAbs'; eauto. by asimpl. by asimpl.
+    hauto lq:on ctrs:Wff use:renaming_up.
+  - move => n Γ a b A B i hP ihP ha iha hb ihb m Δ ξ hΔ hξ.
+    move : {hP} ihP (hξ) (hΔ). repeat move/[apply].
+    move /Bind_Inv => [i0][h0][h1]h2.
+    have ? : Δ ⊢ PBind PSig (ren_PTm ξ A) (ren_PTm (upRen_PTm_PTm ξ) B) ∈ PUniv i0 by qauto l:on ctrs:Wt.
+    apply : E_ProjPair1; eauto.
+    move : ihb hξ hΔ. repeat move/[apply]. by asimpl.
+  - move => n Γ a b A B i hP ihP ha iha hb ihb m Δ ξ hΔ hξ.
+    apply : E_ProjPair2'; eauto. by asimpl.
+    move : ihb hξ hΔ; repeat move/[apply]. by asimpl.
+  - move => *.
+    apply : E_AppEta'; eauto. by asimpl.
+  - qauto l:on use:E_PairEta.
+  - hauto lq:on ctrs:LEq.
+  - qauto l:on ctrs:LEq.
+  - hauto lq:on ctrs:Wff use:renaming_up, Su_Pi.
+  - hauto lq:on ctrs:Wff use:Su_Sig, renaming_up.
+  - hauto q:on ctrs:LEq.
+  - hauto lq:on ctrs:LEq.
+  - qauto l:on ctrs:LEq.
+  - move => *; apply : Su_Pi_Proj2'; eauto; by asimpl.
+  - move => *. apply : Su_Sig_Proj2'; eauto; by asimpl.
+Qed.
+
+Definition morphing_ok {n m} Δ Γ (ρ : fin n -> PTm m) :=
+  forall i, Δ ⊢ ρ i ∈ subst_PTm ρ (Γ i).
+
+Lemma morphing_ren n m p Ξ Δ Γ
+  (ρ : fin n -> PTm m) (ξ : fin m -> fin p) :
+  ⊢ Ξ ->
+  renaming_ok Ξ Δ ξ -> morphing_ok Δ Γ ρ ->
+  morphing_ok Ξ Γ (funcomp (ren_PTm ξ) ρ).
+Proof.
+  move => hΞ hξ hρ.
+  move => i.
+  rewrite {1}/funcomp.
+  have -> :
+    subst_PTm (funcomp (ren_PTm ξ) ρ) (Γ i) =
+    ren_PTm ξ (subst_PTm ρ (Γ i)) by asimpl.
+  eapply renaming; eauto.
+Qed.
+
+Lemma morphing_ext n m Δ Γ (ρ : fin n -> PTm m) (a : PTm m) (A : PTm n)  :
+  morphing_ok Δ Γ ρ ->
+  Δ ⊢ a ∈ subst_PTm ρ A ->
+  morphing_ok
+  Δ (funcomp (ren_PTm shift) (scons A Γ)) (scons a ρ).
+Proof.
+  move => h ha i. destruct i as [i|]; by asimpl.
+Qed.
+
+Lemma T_Var' n Γ (i : fin n) U :
+  U = Γ i ->
+  ⊢ Γ ->
+  Γ ⊢ VarPTm i ∈ U.
+Proof. move => ->. apply T_Var. Qed.
+
+Lemma renaming_wt : forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> forall m Δ (ξ : fin n -> fin m), ⊢ Δ -> renaming_ok Δ Γ ξ -> Δ ⊢ ren_PTm ξ a ∈ ren_PTm ξ A.
+Proof. sfirstorder use:renaming. Qed.
+
+Lemma renaming_wt' : forall n m Δ Γ a A (ξ : fin n -> fin m) u U,
+    u = ren_PTm ξ a -> U = ren_PTm ξ A ->
+    Γ ⊢ a ∈ A -> ⊢ Δ ->
+    renaming_ok Δ Γ ξ -> Δ ⊢ u ∈ U.
+Proof. hauto use:renaming_wt. Qed.
+
+Lemma renaming_shift n m Γ (ρ : fin n -> PTm m) A :
+  renaming_ok (funcomp (ren_PTm shift) (scons (subst_PTm ρ A) Γ)) Γ shift.
+Proof. sfirstorder. Qed.
+
+Lemma morphing_up n m Γ Δ (ρ : fin n -> PTm m) (A : PTm n) k :
+  morphing_ok Γ Δ ρ ->
+  Γ ⊢ subst_PTm ρ A ∈ PUniv k ->
+  morphing_ok (funcomp (ren_PTm shift) (scons (subst_PTm ρ A) Γ)) (funcomp (ren_PTm shift) (scons A Δ)) (up_PTm_PTm ρ).
+Proof.
+  move => h h1 [:hp]. apply morphing_ext.
+  rewrite /morphing_ok.
+  move => i.
+  rewrite {2}/funcomp.
+  apply : renaming_wt'; eauto. by asimpl.
+  abstract : hp. qauto l:on ctrs:Wff use:wff_mutual.
+  eauto using renaming_shift.
+  apply : T_Var';eauto. rewrite /funcomp. by asimpl.
+Qed.
+
+Lemma Wff_Cons' n Γ (A : PTm n) i :
+  Γ ⊢ A ∈ PUniv i ->
+  (* -------------------------------- *)
+  ⊢ funcomp (ren_PTm shift) (scons A Γ).
+Proof. hauto lq:on rew:off use:Wff_Cons, wff_mutual. Qed.
+
+Lemma weakening_wt : forall n Γ (a A B : PTm n) i,
+    Γ ⊢ B ∈ PUniv i ->
+    Γ ⊢ a ∈ A ->
+    funcomp (ren_PTm shift) (scons B Γ) ⊢ ren_PTm shift a ∈ ren_PTm shift A.
+Proof.
+  move => n Γ a A B i hB ha.
+  apply : renaming_wt'; eauto.
+  apply : Wff_Cons'; eauto.
+  apply : renaming_shift; eauto.
+Qed.
+
+Lemma weakening_wt' : forall n Γ (a A B : PTm n) i U u,
+    u = ren_PTm shift a ->
+    U = ren_PTm shift A ->
+    Γ ⊢ B ∈ PUniv i ->
+    Γ ⊢ a ∈ A ->
+    funcomp (ren_PTm shift) (scons B Γ) ⊢ u ∈ U.
+Proof. move => > -> ->. apply weakening_wt. Qed.
+
+Lemma morphing :
+  (forall n (Γ : fin n -> PTm n), ⊢ Γ -> True) /\
+  (forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> forall m Δ (ρ : fin n -> PTm m), ⊢ Δ -> morphing_ok Δ Γ ρ ->
+     Δ ⊢ subst_PTm ρ a ∈ subst_PTm ρ A) /\
+  (forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> forall m Δ (ρ : fin n -> PTm m), ⊢ Δ -> morphing_ok Δ Γ ρ ->
+     Δ ⊢ subst_PTm ρ a ≡ subst_PTm ρ b ∈ subst_PTm ρ A) /\
+  (forall n Γ (A B : PTm n), Γ ⊢ A ≲ B -> forall  m Δ (ρ : fin n -> PTm m), ⊢ Δ -> morphing_ok Δ Γ ρ ->
+    Δ ⊢ subst_PTm ρ A ≲ subst_PTm ρ B).
+Proof.
+  apply wt_mutual => //=.
+  - hauto lq:on use:morphing_up, Wff_Cons', T_Bind.
+  - move => n Γ a A B i hP ihP ha iha m Δ ρ hΔ hρ.
+    move : ihP (hΔ) (hρ); repeat move/[apply].
+    move /Bind_Inv => [j][h0][h1]h2. move {hP}.
+    have ? : Δ ⊢ PBind PPi (subst_PTm ρ A) (subst_PTm (up_PTm_PTm ρ) B) ∈ PUniv i by hauto lq:on ctrs:Wt.
+    apply : T_Abs; eauto.
+    apply : iha.
+    hauto lq:on use:Wff_Cons', Bind_Inv.
+    apply : morphing_up; eauto.
+  - move => *; apply : T_App'; eauto; by asimpl.
+  - move => n Γ a A b B i hA ihA hB ihB hS ihS m Δ ρ hρ hΔ.
+    eapply T_Pair' with (U := subst_PTm ρ (subst_PTm (scons a VarPTm) B));eauto. by asimpl.
+  - hauto lq:on use:T_Proj1.
+  - move => *. apply : T_Proj2'; eauto. by asimpl.
+  - hauto lq:on ctrs:Wt,LEq.
+  - qauto l:on ctrs:Wt.
+  - hauto lq:on ctrs:Eq.
+  - hauto lq:on ctrs:Eq.
+  - hauto lq:on ctrs:Eq.
+  - hauto lq:on rew:off use:E_Bind', Wff_Cons, morphing_up.
+  - move => n Γ a b A B i hPi ihPi ha iha m Δ ρ hΔ hρ.
+    move : ihPi (hΔ) (hρ). repeat move/[apply].
+    move => /Bind_Inv [j][h0][h1]h2.
+    have ? : Δ ⊢ PBind PPi (subst_PTm ρ A) (subst_PTm (up_PTm_PTm ρ) B) ∈ PUniv j by qauto l:on ctrs:Wt.
+    move {hPi}.
+    apply : E_Abs; eauto. qauto l:on ctrs:Wff use:morphing_up.
+  - move => *. apply : E_App'; eauto. by asimpl.
+  - move => n Γ a0 a1 b0 b1 A B i hA ihA ha iha hb ihb m Δ ρ hΔ hρ.
+    apply : E_Pair; eauto.
+    move : ihb hΔ hρ. repeat move/[apply].
+    by asimpl.
+  - hauto q:on ctrs:Eq.
+  - move => *. apply : E_Proj2'; eauto. by asimpl.
+  - qauto l:on ctrs:Eq, LEq.
+  - move => n Γ a b A B i hP ihP hb ihb ha iha m Δ ρ hΔ hρ.
+    move : ihP (hρ) (hΔ). repeat move/[apply].
+    move /Bind_Inv.
+    move => [j][h0][h1]h2.
+    have ? : Δ ⊢ PBind PPi (subst_PTm ρ A) (subst_PTm (up_PTm_PTm ρ) B) ∈ PUniv j by qauto l:on ctrs:Wt.
+    apply : E_AppAbs'; eauto. by asimpl. by asimpl.
+    hauto lq:on ctrs:Wff use:morphing_up.
+  - move => n Γ a b A B i hP ihP ha iha hb ihb m Δ ρ hΔ hρ.
+    move : {hP} ihP (hρ) (hΔ). repeat move/[apply].
+    move /Bind_Inv => [i0][h0][h1]h2.
+    have ? : Δ ⊢ PBind PSig (subst_PTm ρ A) (subst_PTm (up_PTm_PTm ρ) B) ∈ PUniv i0 by qauto l:on ctrs:Wt.
+    apply : E_ProjPair1; eauto.
+    move : ihb hρ hΔ. repeat move/[apply]. by asimpl.
+  - move => n Γ a b A B i hP ihP ha iha hb ihb m Δ ρ hΔ hρ.
+    apply : E_ProjPair2'; eauto. by asimpl.
+    move : ihb hρ hΔ; repeat move/[apply]. by asimpl.
+  - move => *.
+    apply : E_AppEta'; eauto. by asimpl.
+  - qauto l:on use:E_PairEta.
+  - hauto lq:on ctrs:LEq.
+  - qauto l:on ctrs:LEq.
+  - hauto lq:on ctrs:Wff use:morphing_up, Su_Pi.
+  - hauto lq:on ctrs:Wff use:Su_Sig, morphing_up.
+  - hauto q:on ctrs:LEq.
+  - hauto lq:on ctrs:LEq.
+  - qauto l:on ctrs:LEq.
+  - move => *; apply : Su_Pi_Proj2'; eauto; by asimpl.
+  - move => *. apply : Su_Sig_Proj2'; eauto; by asimpl.
+Qed.
+
+Lemma morphing_wt : forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> forall m Δ (ρ : fin n -> PTm m), ⊢ Δ -> morphing_ok Δ Γ ρ -> Δ ⊢ subst_PTm ρ a ∈ subst_PTm ρ A.
+Proof. sfirstorder use:morphing. Qed.
+
+Lemma morphing_wt' : forall n m Δ Γ a A (ρ : fin n -> PTm m) u U,
+    u = subst_PTm ρ a -> U = subst_PTm ρ A ->
+    Γ ⊢ a ∈ A -> ⊢ Δ ->
+    morphing_ok Δ Γ ρ -> Δ ⊢ u ∈ U.
+Proof. hauto use:morphing_wt. Qed.
+
+Lemma morphing_id : forall n (Γ : fin n -> PTm n), ⊢ Γ -> morphing_ok Γ Γ VarPTm.
+Proof.
+  move => n Γ hΓ.
+  rewrite /morphing_ok.
+  move => i. asimpl. by apply T_Var.
+Qed.
+
+Lemma substing_wt : forall n Γ (a : PTm (S n)) (b A : PTm n) B,
+    funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B ->
+    Γ ⊢ b ∈ A ->
+    Γ ⊢ subst_PTm (scons b VarPTm) a ∈ subst_PTm (scons b VarPTm) B.
+Proof.
+  move => n Γ a b A B ha hb [:hΓ]. apply : morphing_wt; eauto.
+  abstract : hΓ. sfirstorder use:wff_mutual.
+  apply morphing_ext; last by asimpl.
+  by apply morphing_id.
+Qed.
+
+(* Could generalize to all equal contexts *)
+Lemma ctx_eq_subst_one n (A0 A1 : PTm n) i j Γ a A :
+  funcomp (ren_PTm shift) (scons A0 Γ) ⊢ a ∈ A ->
+  Γ ⊢ A0 ∈ PUniv i ->
+  Γ ⊢ A1 ∈ PUniv j ->
+  Γ ⊢ A1 ≲ A0 ->
+  funcomp (ren_PTm shift) (scons A1 Γ) ⊢ a ∈ A.
+Proof.
+  move => h0 h1 h2 h3.
+  replace a with (subst_PTm VarPTm a); last by asimpl.
+  replace A with (subst_PTm VarPTm A); last by asimpl.
+  have ? : ⊢ Γ by sfirstorder use:wff_mutual.
+  apply : morphing_wt; eauto.
+  apply : Wff_Cons'; eauto.
+  move => k. destruct k as [k|].
+  - asimpl.
+    eapply weakening_wt' with (a := VarPTm k);eauto using T_Var.
+    by substify.
+  - move => [:hΓ'].
+    apply : T_Conv.
+    apply T_Var.
+    abstract : hΓ'.
+    eauto using Wff_Cons'.
+    rewrite /funcomp. asimpl. substify. asimpl.
+    renamify.
+    eapply renaming; eauto.
+    apply : renaming_shift; eauto.
+Qed.
+
+Lemma bind_inst n Γ p (A : PTm n) B i a0 a1 :
+  Γ ⊢ PBind p A B ∈ PUniv i ->
+  Γ ⊢ a0 ≡ a1 ∈ A ->
+  Γ ⊢ subst_PTm (scons a0 VarPTm) B ≲ subst_PTm (scons a1 VarPTm) B.
+Proof.
+  move => h h0.
+  have {}h : Γ ⊢ PBind p A B ≲ PBind p A B by eauto using E_Refl, Su_Eq.
+  case : p h => //=; hauto l:on use:Su_Pi_Proj2, Su_Sig_Proj2.
+Qed.
+
+Lemma Cumulativity n Γ (a : PTm n) i j :
+  i <= j ->
+  Γ ⊢ a ∈ PUniv i ->
+  Γ ⊢ a ∈ PUniv j.
+Proof.
+  move => h0 h1. apply : T_Conv; eauto.
+  apply Su_Univ => //=.
+  sfirstorder use:wff_mutual.
+Qed.
+
+Lemma T_Bind' n Γ i j p (A : PTm n) (B : PTm (S n)) :
+  Γ ⊢ A ∈ PUniv i ->
+  funcomp (ren_PTm shift) (scons A Γ) ⊢ B ∈ PUniv j ->
+  Γ ⊢ PBind p A B ∈ PUniv (max i j).
+Proof.
+  move => h0 h1.
+  have [*] : i <= max i j /\ j <= max i j by lia.
+  qauto l:on ctrs:Wt use:Cumulativity.
+Qed.
+
+Hint Resolve T_Bind' : wt.
+
+Lemma regularity :
+  (forall n (Γ : fin n -> PTm n), ⊢ Γ -> forall i, exists j, Γ ⊢ Γ i ∈ PUniv j) /\
+  (forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> exists i, Γ ⊢ A ∈ PUniv i)  /\
+  (forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> Γ ⊢ a ∈ A /\ Γ ⊢ b ∈ A /\ exists i, Γ ⊢ A ∈ PUniv i) /\
+  (forall n Γ (A B : PTm n), Γ ⊢ A ≲ B -> exists i, Γ ⊢ A ∈ PUniv i /\ Γ ⊢ B ∈ PUniv i).
+Proof.
+  apply wt_mutual => //=; eauto with wt.
+  - move => n Γ A i hΓ ihΓ hA _ j.
+    destruct j as [j|].
+    have := ihΓ j.
+    move => [j0 hj].
+    exists j0. apply : renaming_wt' => //=; eauto using renaming_shift.
+    reflexivity. econstructor; eauto.
+    exists i. rewrite {2}/funcomp. simpl.
+    apply : renaming_wt'; eauto. reflexivity.
+    econstructor; eauto.
+    apply : renaming_shift; eauto.
+  - move => n Γ b a A B hb [i ihb] ha [j iha].
+    move /Bind_Inv : ihb => [k][h0][h1]h2.
+    move : substing_wt ha h1; repeat move/[apply].
+    move => h. exists k.
+    move : h. by asimpl.
+  - hauto lq:on use:Bind_Inv.
+  - move => n Γ a A B ha [i /Bind_Inv[j][h0][h1]h2].
+    exists j. have : Γ ⊢ PProj PL a ∈ A by qauto use:T_Proj1.
+    move : substing_wt h1; repeat move/[apply].
+    by asimpl.
+  - sfirstorder.
+  - sfirstorder.
+  - sfirstorder.
+  - move => n Γ i p A0 A1 B0 B1 hΓ ihΓ hA0
+             [i0 ihA0] hA [ihA [ihA' [i1 ihA'']]].
+    move => hB [ihB0 [ihB1 [i2 ihB2]]].
+    repeat split => //=.
+    qauto use:T_Bind.
+    apply T_Bind; eauto.
+    apply : ctx_eq_subst_one; eauto using Su_Eq, E_Symmetric.
+    eauto using T_Univ.
+  - hauto lq:on ctrs:Wt,Eq.
+  - move => n Γ i b0 b1 a0 a1 A B hP _ hb [ihb0 [ihb1 [i0 ihb2]]]
+             ha [iha0 [iha1 [i1 iha2]]].
+    repeat split.
+    qauto use:T_App.
+    apply : T_Conv; eauto.
+    qauto use:T_App.
+    move /E_Symmetric in ha.
+    by eauto using bind_inst.
+    hauto lq:on ctrs:Wt,Eq,LEq lq:on use:Bind_Inv, substing_wt.
+  - hauto lq:on use:bind_inst db:wt.
+  - hauto lq:on use:Bind_Inv db:wt.
+  - move => n Γ i a b A B hS _ hab [iha][ihb][j]ihs.
+    repeat split => //=; eauto with wt.
+    apply : T_Conv; eauto with wt.
+    move /E_Symmetric /E_Proj1 in hab.
+    eauto using bind_inst.
+    move /T_Proj1 in iha.
+    hauto lq:on ctrs:Wt,Eq,LEq use:Bind_Inv, substing_wt.
+  - hauto lq:on ctrs:Wt.
+  - hauto q:on use:substing_wt db:wt.
+  - hauto l:on use:bind_inst db:wt.
+  - move => n Γ b A B i hΓ ihΓ hP _ hb [i0 ihb].
+    repeat split => //=; eauto with wt.
+    have {}hb : funcomp (ren_PTm shift) (scons A Γ) ⊢ ren_PTm shift b ∈ ren_PTm shift (PBind PPi A B)
+                        by hauto lq:on use:weakening_wt, Bind_Inv.
+    apply : T_Abs; eauto.
+    apply : T_App'; eauto; rewrite-/ren_PTm.
+    by asimpl.
+    apply T_Var. sfirstorder use:wff_mutual.
+  - hauto lq:on ctrs:Wt.
+  - move => n Γ A B C hA [i [ihA0 ihA1]] hC [j [ihC0 ihC1]].
+    have ? : ⊢ Γ by sfirstorder use:wff_mutual.
+    exists (max i j).
+    have [? ?] : i <= Nat.max i j /\ j <= Nat.max i j by lia.
+    qauto l:on use:T_Conv, Su_Univ.
+  - move => n Γ i j hΓ *. exists (S (max i j)).
+    have [? ?] : S i <= S (Nat.max i j) /\ S j <= S (Nat.max i j) by lia.
+    hauto lq:on ctrs:Wt,LEq.
+  - move => n Γ A0 A1 B0 B1 i hΓ ihΓ hA0 _ hA1 [i0][ih0]ih1 hB[j0][ihB0]ihB1.
+    exists (max i0 j0).
+    split; eauto with wt.
+    apply T_Bind'; eauto.
+    sfirstorder use:ctx_eq_subst_one.
+  - move => n Γ A0 A1 B0 B1 i hΓ ihΓ hA1 _ hA0 [i0][ihA0]ihA1 hB[i1][ihB0]ihB1.
+    exists (max i0 i1). repeat split; eauto with wt.
+    apply T_Bind'; eauto.
+    sfirstorder use:ctx_eq_subst_one.
+  - sfirstorder.
+  - move => n Γ A0 A1 B0 B1 _ [i][ih0 ih1].
+    move /Bind_Inv : ih0 => [i0][h _].
+    move /Bind_Inv : ih1 => [i1][h' _].
+    exists (max i0 i1).
+    have [? ?] : i0 <= Nat.max i0 i1 /\ i1 <= Nat.max i0 i1 by lia.
+    eauto using Cumulativity.
+  - move => n Γ A0 A1 B0 B1 _ [i][ih0 ih1].
+    move /Bind_Inv : ih0 => [i0][h _].
+    move /Bind_Inv : ih1 => [i1][h' _].
+    exists (max i0 i1).
+    have [? ?] : i0 <= Nat.max i0 i1 /\ i1 <= Nat.max i0 i1 by lia.
+    eauto using Cumulativity.
+  - move => n Γ a0 a1 A0 A1 B0 B1 /Su_Pi_Proj1 hA1.
+    move => [i][ihP0]ihP1.
+    move => ha [iha0][iha1][j]ihA1.
+    move /Bind_Inv :ihP0 => [i0][ih0][ih0' _].
+    move /Bind_Inv :ihP1 => [i1][ih1][ih1' _].
+    have [*] : i0 <= max i0 i1 /\ i1 <= max i0 i1 by lia.
+    exists (max i0 i1).
+    split.
+    + apply Cumulativity with (i := i0); eauto.
+      have : Γ ⊢ a0 ∈ A0 by eauto using T_Conv.
+      move : substing_wt ih0';repeat move/[apply]. by asimpl.
+    + apply Cumulativity with (i := i1); eauto.
+      move : substing_wt ih1' iha1;repeat move/[apply]. by asimpl.
+  - move => n Γ a0 a1 A0 A1 B0 B1 /Su_Sig_Proj1 hA1.
+    move => [i][ihP0]ihP1.
+    move => ha [iha0][iha1][j]ihA1.
+    move /Bind_Inv :ihP0 => [i0][ih0][ih0' _].
+    move /Bind_Inv :ihP1 => [i1][ih1][ih1' _].
+    have [*] : i0 <= max i0 i1 /\ i1 <= max i0 i1 by lia.
+    exists (max i0 i1).
+    split.
+    + apply Cumulativity with (i := i0); eauto.
+      move : substing_wt iha0 ih0';repeat move/[apply]. by asimpl.
+    + apply Cumulativity with (i := i1); eauto.
+      have : Γ ⊢ a1 ∈ A1 by eauto using T_Conv.
+      move : substing_wt ih1';repeat move/[apply]. by asimpl.
+Qed.
+
+Lemma Var_Inv n Γ (i : fin n) A :
+  Γ ⊢ VarPTm i ∈ A ->
+  ⊢ Γ /\ Γ ⊢ Γ i ≲ A.
+Proof.
+  move E : (VarPTm i) => u hu.
+  move : i E.
+  elim : n Γ u A / hu=>//=.
+  - move => n Γ i hΓ i0 [?]. subst.
+    repeat split => //=.
+    have h : Γ ⊢ VarPTm i ∈ Γ i by eauto using T_Var.
+    eapply regularity in h.
+    move : h => [i0]?.
+    apply : Su_Eq. apply E_Refl; eassumption.
+  - sfirstorder use:Su_Transitive.
+Qed.
+
+Lemma renaming_su' : forall n m Δ Γ (ξ : fin n -> fin m) (A B : PTm n) u U ,
+    u = ren_PTm ξ A ->
+    U = ren_PTm ξ B ->
+    Γ ⊢ A ≲ B ->
+    ⊢ Δ -> renaming_ok Δ Γ ξ ->
+    Δ ⊢ u ≲ U.
+Proof. move => > -> ->. hauto l:on use:renaming. Qed.
+
+Lemma weakening_su : forall n Γ (A0 A1 B : PTm n) i,
+    Γ ⊢ B ∈ PUniv i ->
+    Γ ⊢ A0 ≲ A1 ->
+    funcomp (ren_PTm shift) (scons B Γ) ⊢ ren_PTm shift A0 ≲ ren_PTm shift A1.
+Proof.
+  move => n Γ A0 A1 B i hB hlt.
+  apply : renaming_su'; eauto.
+  apply : Wff_Cons'; eauto.
+  apply : renaming_shift; eauto.
+Qed.
+
+Lemma regularity_sub0 : forall n Γ (A B : PTm n), Γ ⊢ A ≲ B -> exists i, Γ ⊢ A ∈ PUniv i.
+Proof. hauto lq:on use:regularity. Qed.
+
+Lemma Su_Pi_Proj2_Var n Γ (A0 A1 : PTm n) B0 B1 :
+  Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 ->
+  funcomp (ren_PTm shift) (scons A1 Γ) ⊢ B0 ≲ B1.
+Proof.
+  move => h.
+  have /Su_Pi_Proj1 h1 := h.
+  have /regularity_sub0 [i h2] := h1.
+  move /weakening_su : (h) h2. move => /[apply].
+  move => h2.
+  apply : Su_Pi_Proj2'; try eassumption; rewrite -?/ren_PTm; cycle 2.
+  apply E_Refl. apply T_Var' with (i := var_zero); eauto.
+  sfirstorder use:wff_mutual.
+  by asimpl.
+  by asimpl.
+Qed.
+
+Lemma Su_Sig_Proj2_Var n Γ (A0 A1 : PTm n) B0 B1 :
+  Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1 ->
+  funcomp (ren_PTm shift) (scons A0 Γ) ⊢ B0 ≲ B1.
+Proof.
+  move => h.
+  have /Su_Sig_Proj1 h1 := h.
+  have /regularity_sub0 [i h2] := h1.
+  move /weakening_su : (h) h2. move => /[apply].
+  move => h2.
+  apply : Su_Sig_Proj2'; try eassumption; rewrite -?/ren_PTm; cycle 2.
+  apply E_Refl. apply T_Var' with (i := var_zero); eauto.
+  sfirstorder use:wff_mutual.
+  by asimpl.
+  by asimpl.
+Qed.

theories/typing.v

@@ -0,0 +1,210 @@
+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 Wt : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> Prop :=
+| T_Var n Γ (i : fin n) :
+  ⊢ Γ ->
+  Γ ⊢ VarPTm i ∈ Γ i
+
+| T_Bind n Γ i p (A : PTm n) (B : PTm (S n)) :
+  Γ ⊢ A ∈ PUniv i ->
+  funcomp (ren_PTm shift) (scons A Γ) ⊢ B ∈ PUniv i ->
+  Γ ⊢ PBind p A B ∈ PUniv i
+
+| T_Abs n Γ (a : PTm (S n)) A B i :
+  Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
+  funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B ->
+  Γ ⊢ PAbs a ∈ PBind PPi A B
+
+| T_App n Γ (b a : PTm n) 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 :
+  Γ ⊢ 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 :
+  Γ ⊢ a ∈ PBind PSig A B ->
+  Γ ⊢ PProj PL a ∈ A
+
+| T_Proj2 n Γ (a : PTm n) A B :
+  Γ ⊢ a ∈ PBind PSig A B ->
+  Γ ⊢ PProj PR a ∈ subst_PTm (scons (PProj PL a) VarPTm) B
+
+| T_Univ n Γ i :
+  ⊢ Γ ->
+  Γ ⊢ PUniv i : PTm n ∈ PUniv (S i)
+
+| T_Conv n Γ (a : PTm n) A B :
+  Γ ⊢ a ∈ A ->
+  Γ ⊢ A ≲ B ->
+  Γ ⊢ a ∈ B
+
+with Eq : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> PTm n -> Prop :=
+(* Structural *)
+| E_Refl n Γ (a : PTm n) A :
+  Γ ⊢ a ∈ A ->
+  Γ ⊢ a ≡ a ∈ A
+
+| E_Symmetric n Γ (a b : PTm n) A :
+  Γ ⊢ a ≡ b ∈ A ->
+  Γ ⊢ b ≡ a ∈ A
+
+| E_Transitive n Γ (a b c : PTm n) A :
+  Γ ⊢ a ≡ b ∈ A ->
+  Γ ⊢ b ≡ c ∈ A ->
+  Γ ⊢ a ≡ c ∈ A
+
+(* Congruence *)
+| E_Bind n Γ i p (A0 A1 : PTm n) B0 B1 :
+  ⊢ Γ ->
+  Γ ⊢ A0 ∈ PUniv i ->
+  Γ ⊢ A0 ≡ A1 ∈ PUniv i ->
+  funcomp (ren_PTm shift) (scons 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 :
+  Γ ⊢ PBind PPi A B ∈ (PUniv i) ->
+  funcomp (ren_PTm shift) (scons A Γ) ⊢ a ≡ b ∈ B ->
+  Γ ⊢ PAbs a ≡ PAbs b ∈ PBind PPi A B
+
+| E_App n Γ i (b0 b1 a0 a1 : PTm n) 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 :
+  Γ ⊢ 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 :
+  Γ ⊢ a ≡ b ∈ PBind PSig A B ->
+  Γ ⊢ PProj PL a ≡ PProj PL b ∈ A
+
+| E_Proj2 n Γ i (a b : PTm n) 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_Conv n Γ (a b : PTm n) A B :
+  Γ ⊢ a ≡ b ∈ A ->
+  Γ ⊢ A ≲ B ->
+  Γ ⊢ a ≡ b ∈ B
+
+(* Beta *)
+| E_AppAbs n Γ (a : PTm (S n)) b A B i:
+  Γ ⊢ PBind PPi A B ∈ PUniv i ->
+  Γ ⊢ b ∈ A ->
+  funcomp (ren_PTm shift) (scons 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 :
+  Γ ⊢ 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 :
+  Γ ⊢ 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
+
+(* Eta *)
+| E_AppEta n Γ (b : PTm n) 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 :
+  Γ ⊢ 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 :=
+(* Structural *)
+| Su_Transitive  n Γ (A B C : PTm n) :
+  Γ ⊢ A ≲ B ->
+  Γ ⊢ B ≲ C ->
+  Γ ⊢ A ≲ C
+
+(* Congruence *)
+| Su_Univ n Γ i j :
+  ⊢ Γ ->
+  i <= j ->
+  Γ ⊢ PUniv i : PTm n ≲ PUniv j
+
+| Su_Pi n Γ (A0 A1 : PTm n) B0 B1 i :
+  ⊢ Γ ->
+  Γ ⊢ A0 ∈ PUniv i ->
+  Γ ⊢ A1 ≲ A0 ->
+  funcomp (ren_PTm shift) (scons A0 Γ) ⊢ B0 ≲ B1 ->
+  Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1
+
+| Su_Sig n Γ (A0 A1 : PTm n) B0 B1 i :
+  ⊢ Γ ->
+  Γ ⊢ A1 ∈ PUniv i ->
+  Γ ⊢ A0 ≲ A1 ->
+  funcomp (ren_PTm shift) (scons A1 Γ) ⊢ B0 ≲ B1 ->
+  Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1
+
+(* Injecting from equalities *)
+| Su_Eq n Γ (A : PTm n) B i  :
+  Γ ⊢ A ≡ B ∈ PUniv i ->
+  Γ ⊢ A ≲ B
+
+(* Projection axioms *)
+| Su_Pi_Proj1 n Γ (A0 A1 : PTm n) B0 B1 :
+  Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 ->
+  Γ ⊢ A1 ≲ A0
+
+| Su_Sig_Proj1 n Γ (A0 A1 : PTm n) B0 B1 :
+  Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1 ->
+  Γ ⊢ A0 ≲ A1
+
+| Su_Pi_Proj2 n Γ (a0 a1 A0 A1 : PTm n) 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 :
+  Γ ⊢ 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 :=
+| Wff_Nil :
+  ⊢ null
+| Wff_Cons n Γ (A : PTm n) i :
+  ⊢ Γ ->
+  Γ ⊢ A ∈ PUniv i ->
+  (* -------------------------------- *)
+  ⊢ funcomp (ren_PTm shift) (scons A Γ)
+
+where
+"Γ ⊢ 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 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.
+
+(* Lemma lem : *)
+(*   (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. ... *)