10 changed files with 195 additions and 2523 deletions
--- a/syntax.sig
+++ b/syntax.sig
@ -16,8 +16,4 @@ PPair : PTm -> PTm -> PTm
 PProj : PTag -> PTm -> PTm
 PBind : BTag -> PTm -> (bind PTm in PTm) -> PTm
 PUniv : nat -> PTm
-PBot : PTm
+PBot : PTm
 PNat : PTm
 PZero : PTm
 PSuc : PTm -> PTm
 PInd : (bind PTm in PTm) -> PTm -> PTm -> (bind PTm,PTm in PTm) -> PTm
--- a/theories/Autosubst2/syntax.v
+++ b/theories/Autosubst2/syntax.v
@ -41,13 +41,7 @@ Inductive PTm (n_PTm : nat) : Type :=
  | PProj : PTag -> PTm n_PTm -> PTm n_PTm
  | PBind : BTag -> PTm n_PTm -> PTm (S n_PTm) -> PTm n_PTm
  | PUniv : nat -> PTm n_PTm
-  | PBot : PTm n_PTm
+  | PBot : PTm n_PTm.
  | PNat : PTm n_PTm
  | PZero : PTm n_PTm
  | PSuc : PTm n_PTm -> PTm n_PTm
  | PInd :
      PTm (S n_PTm) ->
      PTm n_PTm -> PTm n_PTm -> PTm (S (S n_PTm)) -> PTm n_PTm.
 Lemma congr_PAbs {m_PTm : nat} {s0 : PTm (S m_PTm)} {t0 : PTm (S m_PTm)}
  (H0 : s0 = t0) : PAbs m_PTm s0 = PAbs m_PTm t0.
@ -101,37 +95,6 @@ Proof.
 exact (eq_refl).
 Qed.
 Lemma congr_PNat {m_PTm : nat} : PNat m_PTm = PNat m_PTm.
 Proof.
 exact (eq_refl).
 Qed.
 Lemma congr_PZero {m_PTm : nat} : PZero m_PTm = PZero m_PTm.
 Proof.
 exact (eq_refl).
 Qed.
 Lemma congr_PSuc {m_PTm : nat} {s0 : PTm m_PTm} {t0 : PTm m_PTm}
  (H0 : s0 = t0) : PSuc m_PTm s0 = PSuc m_PTm t0.
 Proof.
 exact (eq_trans eq_refl (ap (fun x => PSuc m_PTm x) H0)).
 Qed.
 Lemma congr_PInd {m_PTm : nat} {s0 : PTm (S m_PTm)} {s1 : PTm m_PTm}
  {s2 : PTm m_PTm} {s3 : PTm (S (S m_PTm))} {t0 : PTm (S m_PTm)}
  {t1 : PTm m_PTm} {t2 : PTm m_PTm} {t3 : PTm (S (S m_PTm))} (H0 : s0 = t0)
  (H1 : s1 = t1) (H2 : s2 = t2) (H3 : s3 = t3) :
  PInd m_PTm s0 s1 s2 s3 = PInd m_PTm t0 t1 t2 t3.
 Proof.
 exact (eq_trans
         (eq_trans
            (eq_trans
               (eq_trans eq_refl (ap (fun x => PInd m_PTm x s1 s2 s3) H0))
               (ap (fun x => PInd m_PTm t0 x s2 s3) H1))
            (ap (fun x => PInd m_PTm t0 t1 x s3) H2))
         (ap (fun x => PInd m_PTm t0 t1 t2 x) H3)).
 Qed.
 Lemma upRen_PTm_PTm {m : nat} {n : nat} (xi : fin m -> fin n) :
  fin (S m) -> fin (S n).
 Proof.
@ -156,13 +119,6 @@ Fixpoint ren_PTm {m_PTm : nat} {n_PTm : nat}
      PBind n_PTm s0 (ren_PTm xi_PTm s1) (ren_PTm (upRen_PTm_PTm xi_PTm) s2)
  | PUniv _ s0 => PUniv n_PTm s0
  | PBot _ => PBot n_PTm
  | PNat _ => PNat n_PTm
  | PZero _ => PZero n_PTm
  | PSuc _ s0 => PSuc n_PTm (ren_PTm xi_PTm s0)
  | PInd _ s0 s1 s2 s3 =>
      PInd n_PTm (ren_PTm (upRen_PTm_PTm xi_PTm) s0) (ren_PTm xi_PTm s1)
        (ren_PTm xi_PTm s2)
        (ren_PTm (upRen_PTm_PTm (upRen_PTm_PTm xi_PTm)) s3)
  end.
 Lemma up_PTm_PTm {m : nat} {n_PTm : nat} (sigma : fin m -> PTm n_PTm) :
@ -194,13 +150,6 @@ Fixpoint subst_PTm {m_PTm : nat} {n_PTm : nat}
        (subst_PTm (up_PTm_PTm sigma_PTm) s2)
  | PUniv _ s0 => PUniv n_PTm s0
  | PBot _ => PBot n_PTm
  | PNat _ => PNat n_PTm
  | PZero _ => PZero n_PTm
  | PSuc _ s0 => PSuc n_PTm (subst_PTm sigma_PTm s0)
  | PInd _ s0 s1 s2 s3 =>
      PInd n_PTm (subst_PTm (up_PTm_PTm sigma_PTm) s0)
        (subst_PTm sigma_PTm s1) (subst_PTm sigma_PTm s2)
        (subst_PTm (up_PTm_PTm (up_PTm_PTm sigma_PTm)) s3)
  end.
 Lemma upId_PTm_PTm {m_PTm : nat} (sigma : fin m_PTm -> PTm m_PTm)
@ -244,15 +193,6 @@ Fixpoint idSubst_PTm {m_PTm : nat} (sigma_PTm : fin m_PTm -> PTm m_PTm)
        (idSubst_PTm (up_PTm_PTm sigma_PTm) (upId_PTm_PTm _ Eq_PTm) s2)
  | PUniv _ s0 => congr_PUniv (eq_refl s0)
  | PBot _ => congr_PBot
  | PNat _ => congr_PNat
  | PZero _ => congr_PZero
  | PSuc _ s0 => congr_PSuc (idSubst_PTm sigma_PTm Eq_PTm s0)
  | PInd _ s0 s1 s2 s3 =>
      congr_PInd
        (idSubst_PTm (up_PTm_PTm sigma_PTm) (upId_PTm_PTm _ Eq_PTm) s0)
        (idSubst_PTm sigma_PTm Eq_PTm s1) (idSubst_PTm sigma_PTm Eq_PTm s2)
        (idSubst_PTm (up_PTm_PTm (up_PTm_PTm sigma_PTm))
           (upId_PTm_PTm _ (upId_PTm_PTm _ Eq_PTm)) s3)
  end.
 Lemma upExtRen_PTm_PTm {m : nat} {n : nat} (xi : fin m -> fin n)
@ -299,18 +239,6 @@ ren_PTm xi_PTm s = ren_PTm zeta_PTm s :=
           (upExtRen_PTm_PTm _ _ Eq_PTm) s2)
  | PUniv _ s0 => congr_PUniv (eq_refl s0)
  | PBot _ => congr_PBot
  | PNat _ => congr_PNat
  | PZero _ => congr_PZero
  | PSuc _ s0 => congr_PSuc (extRen_PTm xi_PTm zeta_PTm Eq_PTm s0)
  | PInd _ s0 s1 s2 s3 =>
      congr_PInd
        (extRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm)
           (upExtRen_PTm_PTm _ _ Eq_PTm) s0)
        (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1)
        (extRen_PTm xi_PTm zeta_PTm Eq_PTm s2)
        (extRen_PTm (upRen_PTm_PTm (upRen_PTm_PTm xi_PTm))
           (upRen_PTm_PTm (upRen_PTm_PTm zeta_PTm))
           (upExtRen_PTm_PTm _ _ (upExtRen_PTm_PTm _ _ Eq_PTm)) s3)
  end.
 Lemma upExt_PTm_PTm {m : nat} {n_PTm : nat} (sigma : fin m -> PTm n_PTm)
@ -358,18 +286,6 @@ subst_PTm sigma_PTm s = subst_PTm tau_PTm s :=
           (upExt_PTm_PTm _ _ Eq_PTm) s2)
  | PUniv _ s0 => congr_PUniv (eq_refl s0)
  | PBot _ => congr_PBot
  | PNat _ => congr_PNat
  | PZero _ => congr_PZero
  | PSuc _ s0 => congr_PSuc (ext_PTm sigma_PTm tau_PTm Eq_PTm s0)
  | PInd _ s0 s1 s2 s3 =>
      congr_PInd
        (ext_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm)
           (upExt_PTm_PTm _ _ Eq_PTm) s0)
        (ext_PTm sigma_PTm tau_PTm Eq_PTm s1)
        (ext_PTm sigma_PTm tau_PTm Eq_PTm s2)
        (ext_PTm (up_PTm_PTm (up_PTm_PTm sigma_PTm))
           (up_PTm_PTm (up_PTm_PTm tau_PTm))
           (upExt_PTm_PTm _ _ (upExt_PTm_PTm _ _ Eq_PTm)) s3)
  end.
 Lemma up_ren_ren_PTm_PTm {k : nat} {l : nat} {m : nat} (xi : fin k -> fin l)
@ -418,20 +334,6 @@ Fixpoint compRenRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
           (upRen_PTm_PTm rho_PTm) (up_ren_ren _ _ _ Eq_PTm) s2)
  | PUniv _ s0 => congr_PUniv (eq_refl s0)
  | PBot _ => congr_PBot
  | PNat _ => congr_PNat
  | PZero _ => congr_PZero
  | PSuc _ s0 =>
      congr_PSuc (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s0)
  | PInd _ s0 s1 s2 s3 =>
      congr_PInd
        (compRenRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm)
           (upRen_PTm_PTm rho_PTm) (up_ren_ren _ _ _ Eq_PTm) s0)
        (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1)
        (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s2)
        (compRenRen_PTm (upRen_PTm_PTm (upRen_PTm_PTm xi_PTm))
           (upRen_PTm_PTm (upRen_PTm_PTm zeta_PTm))
           (upRen_PTm_PTm (upRen_PTm_PTm rho_PTm))
           (up_ren_ren _ _ _ (up_ren_ren _ _ _ Eq_PTm)) s3)
  end.
 Lemma up_ren_subst_PTm_PTm {k : nat} {l : nat} {m_PTm : nat}
@ -489,21 +391,6 @@ Fixpoint compRenSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
           (up_PTm_PTm theta_PTm) (up_ren_subst_PTm_PTm _ _ _ Eq_PTm) s2)
  | PUniv _ s0 => congr_PUniv (eq_refl s0)
  | PBot _ => congr_PBot
  | PNat _ => congr_PNat
  | PZero _ => congr_PZero
  | PSuc _ s0 =>
      congr_PSuc (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s0)
  | PInd _ s0 s1 s2 s3 =>
      congr_PInd
        (compRenSubst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm tau_PTm)
           (up_PTm_PTm theta_PTm) (up_ren_subst_PTm_PTm _ _ _ Eq_PTm) s0)
        (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1)
        (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s2)
        (compRenSubst_PTm (upRen_PTm_PTm (upRen_PTm_PTm xi_PTm))
           (up_PTm_PTm (up_PTm_PTm tau_PTm))
           (up_PTm_PTm (up_PTm_PTm theta_PTm))
           (up_ren_subst_PTm_PTm _ _ _ (up_ren_subst_PTm_PTm _ _ _ Eq_PTm))
           s3)
  end.
 Lemma up_subst_ren_PTm_PTm {k : nat} {l_PTm : nat} {m_PTm : nat}
@ -581,21 +468,6 @@ ren_PTm zeta_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s :=
           (up_PTm_PTm theta_PTm) (up_subst_ren_PTm_PTm _ _ _ Eq_PTm) s2)
  | PUniv _ s0 => congr_PUniv (eq_refl s0)
  | PBot _ => congr_PBot
  | PNat _ => congr_PNat
  | PZero _ => congr_PZero
  | PSuc _ s0 =>
      congr_PSuc (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s0)
  | PInd _ s0 s1 s2 s3 =>
      congr_PInd
        (compSubstRen_PTm (up_PTm_PTm sigma_PTm) (upRen_PTm_PTm zeta_PTm)
           (up_PTm_PTm theta_PTm) (up_subst_ren_PTm_PTm _ _ _ Eq_PTm) s0)
        (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1)
        (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s2)
        (compSubstRen_PTm (up_PTm_PTm (up_PTm_PTm sigma_PTm))
           (upRen_PTm_PTm (upRen_PTm_PTm zeta_PTm))
           (up_PTm_PTm (up_PTm_PTm theta_PTm))
           (up_subst_ren_PTm_PTm _ _ _ (up_subst_ren_PTm_PTm _ _ _ Eq_PTm))
           s3)
  end.
 Lemma up_subst_subst_PTm_PTm {k : nat} {l_PTm : nat} {m_PTm : nat}
@ -675,21 +547,6 @@ subst_PTm tau_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s :=
           (up_PTm_PTm theta_PTm) (up_subst_subst_PTm_PTm _ _ _ Eq_PTm) s2)
  | PUniv _ s0 => congr_PUniv (eq_refl s0)
  | PBot _ => congr_PBot
  | PNat _ => congr_PNat
  | PZero _ => congr_PZero
  | PSuc _ s0 =>
      congr_PSuc (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s0)
  | PInd _ s0 s1 s2 s3 =>
      congr_PInd
        (compSubstSubst_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm)
           (up_PTm_PTm theta_PTm) (up_subst_subst_PTm_PTm _ _ _ Eq_PTm) s0)
        (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1)
        (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s2)
        (compSubstSubst_PTm (up_PTm_PTm (up_PTm_PTm sigma_PTm))
           (up_PTm_PTm (up_PTm_PTm tau_PTm))
           (up_PTm_PTm (up_PTm_PTm theta_PTm))
           (up_subst_subst_PTm_PTm _ _ _
              (up_subst_subst_PTm_PTm _ _ _ Eq_PTm)) s3)
  end.
 Lemma renRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat}
@ -808,18 +665,6 @@ Fixpoint rinst_inst_PTm {m_PTm : nat} {n_PTm : nat}
           (rinstInst_up_PTm_PTm _ _ Eq_PTm) s2)
  | PUniv _ s0 => congr_PUniv (eq_refl s0)
  | PBot _ => congr_PBot
  | PNat _ => congr_PNat
  | PZero _ => congr_PZero
  | PSuc _ s0 => congr_PSuc (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s0)
  | PInd _ s0 s1 s2 s3 =>
      congr_PInd
        (rinst_inst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm sigma_PTm)
           (rinstInst_up_PTm_PTm _ _ Eq_PTm) s0)
        (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1)
        (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s2)
        (rinst_inst_PTm (upRen_PTm_PTm (upRen_PTm_PTm xi_PTm))
           (up_PTm_PTm (up_PTm_PTm sigma_PTm))
           (rinstInst_up_PTm_PTm _ _ (rinstInst_up_PTm_PTm _ _ Eq_PTm)) s3)
  end.
 Lemma rinstInst'_PTm {m_PTm : nat} {n_PTm : nat}
@ -1026,14 +871,6 @@ Core.
 Arguments VarPTm {n_PTm}.
 Arguments PInd {n_PTm}.
 Arguments PSuc {n_PTm}.
 Arguments PZero {n_PTm}.
 Arguments PNat {n_PTm}.
 Arguments PBot {n_PTm}.
 Arguments PUniv {n_PTm}.
@ -1048,9 +885,9 @@ Arguments PApp {n_PTm}.
 Arguments PAbs {n_PTm}.
-#[global]Hint Opaque subst_PTm: rewrite.
+#[global] Hint Opaque subst_PTm: rewrite.
-#[global]Hint Opaque ren_PTm: rewrite.
+#[global] Hint Opaque ren_PTm: rewrite.
 End Extra.
--- a/theories/algorithmic.v
+++ b/theories/algorithmic.v
@ -16,22 +16,13 @@ Module HRed.
  | ProjPair p a b :
    R (PProj p (PPair a b)) (if p is PL then a else b)
  | IndZero P b c :
    R (PInd P PZero b c) b
  | IndSuc P a b c :
    R (PInd P (PSuc a) b c) (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c)
  (*************** Congruence ********************)
  | AppCong a0 a1 b :
    R a0 a1 ->
    R (PApp a0 b) (PApp a1 b)
  | ProjCong p a0 a1 :
    R a0 a1 ->
-    R (PProj p a0) (PProj p a1)
+    R (PProj p a0) (PProj p a1).
  | IndCong P a0 a1 b c :
    R a0 a1 ->
    R (PInd P a0 b c) (PInd P a1 b c).
  Lemma ToRRed n (a b : PTm n) : HRed.R a b -> RRed.R a b.
  Proof. induction 1; hauto lq:on ctrs:RRed.R. Qed.
@ -91,17 +82,6 @@ Lemma T_Bot_Imp n Γ (A : PTm n) :
  induction hu => //=.
 Qed.
 Lemma Zero_Inv n Γ U :
  Γ ⊢ @PZero n ∈ U ->
  Γ ⊢ PNat ≲ U.
 Proof.
  move E : PZero => u hu.
  move : E.
  elim : n Γ u U /hu=>//=.
  by eauto using Su_Eq, E_Refl, T_Nat'.
  hauto lq:on rew:off ctrs:LEq.
 Qed.
 Lemma Sub_Bind_InvR n Γ p (A : PTm n) B C :
  Γ ⊢ PBind p A B ≲ C ->
  exists i A0 B0, Γ ⊢ C ≡ PBind p A0 B0 ∈ PUniv i.
@ -141,21 +121,6 @@ Proof.
    eauto.
  - hauto lq:on use:synsub_to_usub, Sub.bind_univ_noconf.
  - hauto lq:on use:regularity, T_Bot_Imp.
  - move => _ _ /synsub_to_usub [_ [_ h]]. exfalso.
    apply Sub.nat_bind_noconf in h => //=.
  - move => h.
    have {}h : Γ ⊢ PZero ∈ PUniv i by hauto l:on use:regularity.
    exfalso. move : h. clear.
    move /Zero_Inv /synsub_to_usub.
    hauto l:on use:Sub.univ_nat_noconf.
  - move => a h.
    have {}h : Γ ⊢ PSuc a  ∈ PUniv i by hauto l:on use:regularity.
    exfalso. move /Suc_Inv : h => [_ /synsub_to_usub].
    hauto lq:on use:Sub.univ_nat_noconf.
  - move => P0 a0 b0 c0 h0 h1 /synsub_to_usub [_ [_ h2]].
    set u := PInd _ _ _ _ in h0.
    have hne : SNe u by sfirstorder use:ne_nf_embed.
    exfalso. move : h2 hne. hauto l:on use:Sub.bind_sne_noconf.
 Qed.
 Lemma Sub_Univ_InvR n (Γ : fin n -> PTm n) i C :
@ -189,20 +154,6 @@ Proof.
  - hauto lq:on use:synsub_to_usub, Sub.univ_bind_noconf.
  - sfirstorder.
  - hauto lq:on use:regularity, T_Bot_Imp.
  - hauto q:on use:synsub_to_usub, Sub.nat_univ_noconf.
  - move => h.
    have {}h : Γ ⊢ PZero ∈ PUniv j by hauto l:on use:regularity.
    exfalso. move : h. clear.
    move /Zero_Inv /synsub_to_usub.
    hauto l:on use:Sub.univ_nat_noconf.
  - move => a h.
    have {}h : Γ ⊢ PSuc a  ∈ PUniv j by hauto l:on use:regularity.
    exfalso. move /Suc_Inv : h => [_ /synsub_to_usub].
    hauto lq:on use:Sub.univ_nat_noconf.
  - move => P0 a0 b0 c0 h0 h1 /synsub_to_usub [_ [_ h2]].
    set u := PInd _ _ _ _ in h0.
    have hne : SNe u by sfirstorder use:ne_nf_embed.
    exfalso. move : h2 hne. hauto l:on use:Sub.univ_sne_noconf.
 Qed.
 Lemma Sub_Bind_InvL n Γ p (A : PTm n) B C :
@ -244,22 +195,6 @@ Proof.
    eauto using E_Symmetric.
  - hauto lq:on use:synsub_to_usub, Sub.univ_bind_noconf.
  - hauto lq:on use:regularity, T_Bot_Imp.
  - move => _ _ /synsub_to_usub [_ [_ h]]. exfalso.
    apply Sub.bind_nat_noconf in h => //=.
  - move => h.
    have {}h : Γ ⊢ PZero ∈ PUniv i by hauto l:on use:regularity.
    exfalso. move : h. clear.
    move /Zero_Inv /synsub_to_usub.
    hauto l:on use:Sub.univ_nat_noconf.
  - move => a h.
    have {}h : Γ ⊢ PSuc a  ∈ PUniv i by hauto l:on use:regularity.
    exfalso. move /Suc_Inv : h => [_ /synsub_to_usub].
    hauto lq:on use:Sub.univ_nat_noconf.
  - move => P0 a0 b0 c0 h0 h1 /synsub_to_usub [_ [_ h2]].
    set u := PInd _ _ _ _ in h0.
    have hne : SNe u by sfirstorder use:ne_nf_embed.
    exfalso. move : h2 hne. subst u.
    hauto l:on use:Sub.sne_bind_noconf.
 Qed.
 Lemma T_Abs_Inv n Γ (a0 a1 : PTm (S n)) U :
@ -287,73 +222,11 @@ Proof.
    apply : ctx_eq_subst_one; eauto.
 Qed.
 Lemma T_Univ_Raise n Γ (a : PTm n) i j :
  Γ ⊢ a ∈ PUniv i ->
  i <= j ->
  Γ ⊢ a ∈ PUniv j.
 Proof. hauto lq:on rew:off use:T_Conv, Su_Univ, wff_mutual. Qed.
 Lemma Bind_Univ_Inv n Γ p (A : PTm n) B i :
  Γ ⊢ PBind p A B ∈ PUniv i ->
  Γ ⊢ A ∈ PUniv i /\ funcomp (ren_PTm shift) (scons A Γ) ⊢ B ∈ PUniv i.
 Proof.
  move /Bind_Inv.
  move => [i0][hA][hB]h.
  move /synsub_to_usub : h => [_ [_ /Sub.univ_inj ? ]].
  sfirstorder use:T_Univ_Raise.
 Qed.
 Lemma Abs_Pi_Inv n Γ (a : PTm (S n)) A B :
  Γ ⊢ PAbs a ∈ PBind PPi A B ->
  funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B.
 Proof.
  move => h.
  have [i hi] : exists i, Γ ⊢ PBind PPi A B ∈ PUniv i by hauto use:regularity.
  have  [{}i {}hi] : exists i, Γ ⊢ A ∈ PUniv i by hauto use:Bind_Inv.
  apply : subject_reduction; last apply RRed.AppAbs'.
  apply : T_App'; cycle 1.
  apply : weakening_wt'; cycle 2. apply hi.
  apply h. reflexivity. reflexivity. rewrite -/ren_PTm.
  apply T_Var' with (i := var_zero).  by asimpl.
  by eauto using Wff_Cons'.
  rewrite -/ren_PTm.
  by asimpl.
  rewrite -/ren_PTm.
  by asimpl.
 Qed.
 Lemma Pair_Sig_Inv n Γ (a b : PTm n) A B :
  Γ ⊢ PPair a b ∈ PBind PSig A B ->
  Γ ⊢ a ∈ A /\ Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B.
 Proof.
  move => /[dup] h0 h1.
  have [i hr] : exists i, Γ ⊢ PBind PSig A B ∈ PUniv i by sfirstorder use:regularity.
  move /T_Proj1 in h0.
  move /T_Proj2 in h1.
  split.
  hauto lq:on use:subject_reduction ctrs:RRed.R.
  have hE : Γ ⊢ PProj PL (PPair a b) ≡ a ∈ A by
    hauto lq:on use:RRed_Eq ctrs:RRed.R.
  apply : T_Conv.
  move /subject_reduction : h1. apply.
  apply RRed.ProjPair.
  apply : bind_inst; eauto.
 Qed.
 (* Coquand's algorithm with subtyping *)
 Reserved Notation "a ∼ b" (at level 70).
 Reserved Notation "a ↔ b" (at level 70).
 Reserved Notation "a ⇔ b" (at level 70).
 Inductive CoqEq {n} : PTm n -> PTm n -> Prop :=
 | CE_ZeroZero :
  PZero ↔ PZero
 | CE_SucSuc a b :
  a ⇔ b ->
  (* ------------- *)
  PSuc a ↔ PSuc b
 | CE_AbsAbs a b :
  a ⇔ b ->
  (* --------------------- *)
@ -401,10 +274,6 @@ Inductive CoqEq {n} : PTm n -> PTm n -> Prop :=
  (* ---------------------------- *)
  PBind p A0 B0 ↔ PBind p A1 B1
 | CE_NatCong :
  (* ------------------ *)
  PNat ↔ PNat
 | CE_NeuNeu a0 a1 :
  a0 ∼ a1 ->
  a0 ↔ a1
@ -429,16 +298,6 @@ with CoqEq_Neu  {n} : PTm n -> PTm n -> Prop :=
  (* ------------------------- *)
  PApp u0 a0 ∼ PApp u1 a1
 | CE_IndCong P0 P1 u0 u1 b0 b1 c0 c1 :
  ishne u0 ->
  ishne u1 ->
  P0 ⇔ P1 ->
  u0 ∼ u1 ->
  b0 ⇔ b1 ->
  c0 ⇔ c1 ->
  (* ----------------------------------- *)
  PInd P0 u0 b0 c0 ∼ PInd P1 u1 b1 c1
 with CoqEq_R {n} : PTm n -> PTm n -> Prop :=
 | CE_HRed a a' b b'  :
  rtc HRed.R a a' ->
@ -469,6 +328,9 @@ Lemma coqeq_symmetric_mutual : forall n,
    (forall (a b : PTm n), a ⇔ b -> b ⇔ a).
 Proof. apply coqeq_mutual; qauto l:on ctrs:CoqEq,CoqEq_R, CoqEq_Neu. Qed.
 (* Lemma Sub_Univ_InvR *)
 Lemma coqeq_sound_mutual : forall n,
    (forall (a b : PTm n), a ∼ b -> forall Γ A B, Γ ⊢ a ∈ A -> Γ ⊢ b ∈ B -> exists C,
       Γ ⊢ C ≲ A /\ Γ ⊢ C ≲ B /\ Γ ⊢ a ≡ b ∈ C) /\
@ -539,37 +401,6 @@ Proof.
      first by sfirstorder use:bind_inst.
    apply : Su_Pi_Proj2';  eauto using E_Refl.
    apply E_App with (A := A2); eauto using E_Conv_E.
  - move {hAppL hPairL} => n P0 P1 u0 u1 b0 b1 c0 c1 neu0 neu1 hP ihP hu ihu hb ihb hc ihc Γ A B.
    move /Ind_Inv => [i0][hP0][hu0][hb0][hc0]hSu0.
    move /Ind_Inv => [i1][hP1][hu1][hb1][hc1]hSu1.
    move : ihu hu0 hu1; do!move/[apply]. move => ihu.
    have {}ihu : Γ ⊢ u0 ≡ u1 ∈ PNat by hauto l:on use:E_Conv.
    have wfΓ : ⊢ Γ by hauto use:wff_mutual.
    have wfΓ' : ⊢ funcomp (ren_PTm shift) (scons PNat Γ) by hauto lq:on use:Wff_Cons', T_Nat'.
    move => [:sigeq].
    have sigeq' : Γ ⊢ PBind PSig PNat P0 ≡ PBind PSig PNat P1 ∈ PUniv (max i0 i1).
    apply E_Bind. by eauto using T_Nat, E_Refl.
    abstract : sigeq. hauto lq:on use:T_Univ_Raise solve+:lia.
    have sigleq : Γ ⊢ PBind PSig PNat P0 ≲ PBind PSig PNat P1.
    apply Su_Sig with (i := 0)=>//. by apply T_Nat'. by eauto using Su_Eq, T_Nat', E_Refl.
    apply Su_Eq with (i := max i0 i1).  apply sigeq.
    exists (subst_PTm (scons u0 VarPTm) P0). repeat split => //.
    suff : Γ ⊢ subst_PTm (scons u0 VarPTm) P0 ≲ subst_PTm (scons u1 VarPTm) P1 by eauto using Su_Transitive.
    by eauto using Su_Sig_Proj2.
    apply E_IndCong with (i := max i0 i1); eauto. move :sigeq; clear; hauto q:on use:regularity.
    apply ihb; eauto. apply : T_Conv; eauto. eapply morphing. apply : Su_Eq. apply E_Symmetric. apply sigeq.
    done. apply morphing_ext. apply morphing_id. done. by apply T_Zero.
    apply ihc; eauto.
    eapply T_Conv; eauto.
    eapply ctx_eq_subst_one; eauto. apply : Su_Eq; apply sigeq.
    eapply weakening_su; eauto.
    eapply morphing; eauto. apply : Su_Eq. apply E_Symmetric. apply sigeq.
    apply morphing_ext. set x := {1}(funcomp _ shift).
    have -> : x = funcomp (ren_PTm shift) VarPTm by asimpl.
    apply : morphing_ren; eauto. apply : renaming_shift; eauto. by apply morphing_id.
    apply T_Suc. by apply T_Var.
  - hauto lq:on use:Zero_Inv db:wt.
  - hauto lq:on use:Suc_Inv db:wt.
  - move => n a b ha iha Γ A h0 h1.
    move /Abs_Inv : h0 => [A0][B0][h0]h0'.
    move /Abs_Inv : h1 => [A1][B1][h1]h1'.
@ -702,7 +533,6 @@ Proof.
    apply : ctx_eq_subst_one; eauto. apply : Su_Eq; apply eqA.
    move : weakening_su hjk hA0. by repeat move/[apply].
  - hauto lq:on ctrs:Eq,LEq,Wt.
  - hauto lq:on ctrs:Eq,LEq,Wt.
  - move => n a a' b b' ha hb hab ihab Γ A ha0 hb0.
    have [*] : Γ ⊢ a' ∈ A /\ Γ ⊢ b' ∈ A by eauto using HReds.preservation.
    hauto lq:on use:HReds.ToEq, E_Symmetric, E_Transitive.
@ -723,14 +553,8 @@ Proof.
  - hauto l:on use:HRed.AppAbs.
  - hauto l:on use:HRed.ProjPair.
  - hauto lq:on ctrs:HRed.R.
  - hauto lq:on ctrs:HRed.R.
  - hauto lq:on ctrs:HRed.R.
  - sfirstorder use:ne_hne.
  - hauto lq:on ctrs:HRed.R.
  - sfirstorder use:ne_hne.
  - hauto q:on ctrs:HRed.R.
  - hauto lq:on use:ne_hne.
  - hauto lq:on use:ne_hne.
 Qed.
 Lemma algo_metric_case n k (a b : PTm n) :
@ -750,15 +574,6 @@ Proof.
    inversion E; subst => /=.
    + hauto lq:on use:HRed.ProjPair unfold:algo_metric solve+:lia.
    + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:algo_metric solve+:lia.
  - inversion h0 as [|A B C D E F]; subst.
    hauto qb:on use:ne_hne.
    inversion E; subst => /=.
    + hauto lq:on use:HRed.IndZero unfold:algo_metric solve+:lia.
    + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:algo_metric solve+:lia.
    + sfirstorder use:ne_hne.
    + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:algo_metric solve+:lia.
    + sfirstorder use:ne_hne.
    + sfirstorder use:ne_hne.
 Qed.
 Lemma algo_metric_sym n k (a b : PTm n) :
@ -794,53 +609,6 @@ Proof.
  clear. move /synsub_to_usub. hauto l:on use:Sub.bind_inj.
 Qed.
 Lemma T_AbsZero_Imp n Γ a (A : PTm n) :
  Γ ⊢ PAbs a ∈ A ->
  Γ ⊢ PZero ∈ A ->
  False.
 Proof.
  move /Abs_Inv => [A0][B0][_]haU.
  move /Zero_Inv => hbU.
  move /Sub_Bind_InvR : haU => [i][A2][B2]h2.
  have : Γ ⊢ PNat ≲ PBind PPi A2 B2 by eauto using Su_Transitive, Su_Eq.
  clear. hauto lq:on use:synsub_to_usub, Sub.bind_nat_noconf.
 Qed.
 Lemma T_AbsSuc_Imp n Γ a b (A : PTm n) :
  Γ ⊢ PAbs a ∈ A ->
  Γ ⊢ PSuc b ∈ A ->
  False.
 Proof.
  move /Abs_Inv => [A0][B0][_]haU.
  move /Suc_Inv => [_ hbU].
  move /Sub_Bind_InvR : haU => [i][A2][B2]h2.
  have {hbU h2} : Γ ⊢ PNat ≲ PBind PPi A2 B2 by eauto using Su_Transitive, Su_Eq.
  hauto lq:on use:Sub.bind_nat_noconf, synsub_to_usub.
 Qed.
 Lemma Nat_Inv n Γ A:
  Γ ⊢ @PNat n ∈ A ->
  exists i, Γ ⊢ PUniv i ≲ A.
 Proof.
  move E : PNat => u hu.
  move : E.
  elim : n Γ u A / hu=>//=.
  - hauto lq:on use:E_Refl, T_Univ, Su_Eq.
  - hauto lq:on ctrs:LEq.
 Qed.
 Lemma T_AbsNat_Imp n Γ a (A : PTm n) :
  Γ ⊢ PAbs a ∈ A ->
  Γ ⊢ PNat ∈ A ->
  False.
 Proof.
  move /Abs_Inv => [A0][B0][_]haU.
  move /Nat_Inv => [i hA].
  move /Sub_Univ_InvR : hA => [j][k]hA.
  have : Γ ⊢ PBind PPi A0 B0 ≲ PUniv j by eauto using Su_Transitive, Su_Eq.
  hauto lq:on use:Sub.bind_univ_noconf, synsub_to_usub.
 Qed.
 Lemma T_PairBind_Imp n Γ (a0 a1 : PTm n) p A0 B0 U :
  Γ ⊢ PPair a0 a1 ∈ U ->
  Γ ⊢ PBind p A0 B0  ∈ U ->
@ -853,39 +621,6 @@ Proof.
  clear. move /synsub_to_usub. hauto l:on use:Sub.bind_univ_noconf.
 Qed.
 Lemma T_PairNat_Imp n Γ (a0 a1 : PTm n) U :
  Γ ⊢ PPair a0 a1 ∈ U ->
  Γ ⊢ PNat ∈ U ->
  False.
 Proof.
  move/Pair_Inv => [A1][B1][_][_]hbU.
  move /Nat_Inv => [i]/Sub_Univ_InvR[j][k]hU.
  have : Γ ⊢ PBind PSig A1 B1 ≲ PUniv j by eauto using Su_Transitive, Su_Eq.
  clear. move /synsub_to_usub. hauto l:on use:Sub.bind_univ_noconf.
 Qed.
 Lemma T_PairZero_Imp n Γ (a0 a1 : PTm n) U :
  Γ ⊢ PPair a0 a1 ∈ U ->
  Γ ⊢ PZero ∈ U ->
  False.
 Proof.
  move/Pair_Inv=>[A1][B1][_][_]hbU.
  move/Zero_Inv. move/Sub_Bind_InvR : hbU=>[i][A0][B0]*.
  have : Γ ⊢ PNat ≲ PBind PSig A0 B0 by eauto using Su_Transitive, Su_Eq.
  clear. move /synsub_to_usub. hauto l:on use:Sub.bind_nat_noconf.
 Qed.
 Lemma T_PairSuc_Imp n Γ (a0 a1 : PTm n) b U :
  Γ ⊢ PPair a0 a1 ∈ U ->
  Γ ⊢ PSuc b ∈ U ->
  False.
 Proof.
  move/Pair_Inv=>[A1][B1][_][_]hbU.
  move/Suc_Inv=>[_ hU]. move/Sub_Bind_InvR : hbU=>[i][A0][B0]*.
  have : Γ ⊢ PNat ≲ PBind PSig A0 B0 by eauto using Su_Transitive, Su_Eq.
  clear. move /synsub_to_usub. hauto l:on use:Sub.bind_nat_noconf.
 Qed.
 Lemma Univ_Inv n Γ i U :
  Γ ⊢ @PUniv n i ∈ U ->
  Γ ⊢ PUniv i ∈ PUniv (S i)  /\ Γ ⊢ PUniv (S i) ≲ U.
@ -947,16 +682,6 @@ Proof.
  hauto lq:on use:Sub.bind_univ_noconf.
 Qed.
 Lemma lored_nsteps_suc_inv k n (a : PTm n) b :
  nsteps LoRed.R k (PSuc a) b -> exists b', nsteps LoRed.R k a b' /\ b = PSuc b'.
 Proof.
  move E : (PSuc a) => u hu.
  move : a E.
  elim : u b /hu.
  - hauto l:on.
  - scrush ctrs:nsteps inv:LoRed.R.
 Qed.
 Lemma lored_nsteps_abs_inv k n (a : PTm (S n)) b :
  nsteps LoRed.R k (PAbs a) b -> exists b', nsteps LoRed.R k a b' /\ b = PAbs b'.
 Proof.
@ -964,7 +689,7 @@ Proof.
  move : a E.
  elim : u b /hu.
  - hauto l:on.
-  - scrush ctrs:nsteps inv:LoRed.R.
+  - hauto lq:on ctrs:nsteps inv:LoRed.R.
 Qed.
 Lemma lored_hne_preservation n (a b : PTm n) :
@ -995,37 +720,6 @@ Proof.
    exists i,(S j),a1,b1. sauto lq:on solve+:lia.
 Qed.
 Lemma lored_nsteps_ind_inv k n P0 (a0 : PTm n) b0 c0 U :
  nsteps LoRed.R k (PInd P0 a0 b0 c0) U ->
  ishne a0 ->
  exists iP ia ib ic P1 a1 b1 c1,
    iP <= k /\ ia <= k /\ ib <= k /\ ic <= k /\
      U = PInd P1 a1 b1 c1 /\
      nsteps LoRed.R iP P0 P1 /\
      nsteps LoRed.R ia a0 a1 /\
      nsteps LoRed.R ib b0 b1 /\
      nsteps LoRed.R ic c0 c1.
 Proof.
  move E : (PInd P0 a0 b0 c0) => u hu.
  move : P0 a0 b0 c0 E.
  elim : k u U / hu.
  - sauto lq:on.
  - move => k t0 t1 t2 ht01 ht12 ih P0 a0 b0 c0 ? nea0. subst.
    inversion ht01; subst => //=; spec_refl.
    * move /(_ ltac:(done)) : ih.
      move => [iP][ia][ib][ic].
      exists (S iP), ia, ib, ic. sauto lq:on solve+:lia.
    * move /(_ ltac:(sfirstorder use:lored_hne_preservation)) : ih.
      move => [iP][ia][ib][ic].
      exists iP, (S ia), ib, ic. sauto lq:on solve+:lia.
    * move /(_ ltac:(done)) : ih.
      move => [iP][ia][ib][ic].
      exists iP, ia, (S ib), ic. sauto lq:on solve+:lia.
    * move /(_ ltac:(done)) : ih.
      move => [iP][ia][ib][ic].
      exists iP, ia, ib, (S ic). sauto lq:on solve+:lia.
 Qed.
 Lemma lored_nsteps_app_inv k n (a0 b0 C : PTm n) :
    nsteps LoRed.R k (PApp a0 b0) C ->
    ishne a0 ->
@ -1091,7 +785,6 @@ Proof.
  lia.
 Qed.
 Lemma lored_nsteps_app_cong k n (a0 a1 b : PTm n) :
  nsteps LoRed.R k a0 a1 ->
  ishne a0 ->
@ -1224,24 +917,6 @@ Proof.
  eapply DJoin.ejoin_pair_inj; hauto qb:on ctrs:rtc, ERed.R.
 Qed.
 Lemma algo_metric_ind n k P0 (a0 : PTm n) b0 c0 P1 a1 b1 c1 :
  algo_metric k (PInd P0 a0 b0 c0) (PInd P1 a1 b1 c1) ->
  ishne a0 ->
  ishne a1 ->
  exists j, j < k /\ algo_metric j P0 P1 /\ algo_metric j a0 a1 /\
         algo_metric j b0 b1 /\ algo_metric j c0 c1.
 Proof.
  move => [i][j][va][vb][h0][h1][h2][h3][h4]h5 hne0 hne1.
  move /lored_nsteps_ind_inv /(_ hne0) : h0.
  move =>[iP][ia][ib][ic][P2][a2][b2][c2][?][?][?][?][?][?][?][?]?. subst.
  move /lored_nsteps_ind_inv /(_ hne1) : h1.
  move =>[iP0][ia0][ib0][ic0][P3][a3][b3][c3][?][?][?][?][?][?][?][?]?. subst.
  move /EJoin.ind_inj : h4.
  move => [?][?][?]?.
  exists (k -1). simpl in *.
  hauto lq:on rew:off use:ne_nf b:on solve+:lia.
 Qed.
 Lemma algo_metric_app n k (a0 b0 a1 b1 : PTm n) :
  algo_metric k (PApp a0 b0) (PApp a1 b1) ->
  ishne a0 ->
@ -1271,20 +946,6 @@ Proof.
    repeat split => //=; sfirstorder b:on use:ne_nf.
 Qed.
 Lemma algo_metric_suc n k (a0 a1 : PTm n) :
  algo_metric k (PSuc a0) (PSuc a1) ->
  exists j, j < k /\ algo_metric j a0 a1.
 Proof.
  move => [i][j][va][vb][h0][h1][h2][h3][h4]h5.
  exists (k - 1).
  move /lored_nsteps_suc_inv : h0.
  move => [a0'][ha0]?. subst.
  move /lored_nsteps_suc_inv : h1.
  move => [b0'][hb0]?. subst. simpl in *.
  split; first by lia.
  rewrite /algo_metric.
  hauto lq:on rew:off use:EJoin.suc_inj solve+:lia.
 Qed.
 Lemma algo_metric_bind n k p0 (A0 : PTm n) B0 p1 A1 B1  :
  algo_metric k (PBind p0 A0 B0) (PBind p1 A1 B1) ->
@ -1305,6 +966,58 @@ Proof.
  - exists i1,j1,b2,b3. sfirstorder b:on solve+:lia.
 Qed.
 Lemma T_Univ_Raise n Γ (a : PTm n) i j :
  Γ ⊢ a ∈ PUniv i ->
  i <= j ->
  Γ ⊢ a ∈ PUniv j.
 Proof. hauto lq:on rew:off use:T_Conv, Su_Univ, wff_mutual. Qed.
 Lemma Bind_Univ_Inv n Γ p (A : PTm n) B i :
  Γ ⊢ PBind p A B ∈ PUniv i ->
  Γ ⊢ A ∈ PUniv i /\ funcomp (ren_PTm shift) (scons A Γ) ⊢ B ∈ PUniv i.
 Proof.
  move /Bind_Inv.
  move => [i0][hA][hB]h.
  move /synsub_to_usub : h => [_ [_ /Sub.univ_inj ? ]].
  sfirstorder use:T_Univ_Raise.
 Qed.
 Lemma Abs_Pi_Inv n Γ (a : PTm (S n)) A B :
  Γ ⊢ PAbs a ∈ PBind PPi A B ->
  funcomp (ren_PTm shift) (scons A Γ) ⊢ a ∈ B.
 Proof.
  move => h.
  have [i hi] : exists i, Γ ⊢ PBind PPi A B ∈ PUniv i by hauto use:regularity.
  have  [{}i {}hi] : exists i, Γ ⊢ A ∈ PUniv i by hauto use:Bind_Inv.
  apply : subject_reduction; last apply RRed.AppAbs'.
  apply : T_App'; cycle 1.
  apply : weakening_wt'; cycle 2. apply hi.
  apply h. reflexivity. reflexivity. rewrite -/ren_PTm.
  apply T_Var' with (i := var_zero).  by asimpl.
  by eauto using Wff_Cons'.
  rewrite -/ren_PTm.
  by asimpl.
  rewrite -/ren_PTm.
  by asimpl.
 Qed.
 Lemma Pair_Sig_Inv n Γ (a b : PTm n) A B :
  Γ ⊢ PPair a b ∈ PBind PSig A B ->
  Γ ⊢ a ∈ A /\ Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B.
 Proof.
  move => /[dup] h0 h1.
  have [i hr] : exists i, Γ ⊢ PBind PSig A B ∈ PUniv i by sfirstorder use:regularity.
  move /T_Proj1 in h0.
  move /T_Proj2 in h1.
  split.
  hauto lq:on use:subject_reduction ctrs:RRed.R.
  have hE : Γ ⊢ PProj PL (PPair a b) ≡ a ∈ A by
    hauto lq:on use:RRed_Eq ctrs:RRed.R.
  apply : T_Conv.
  move /subject_reduction : h1. apply.
  apply RRed.ProjPair.
  apply : bind_inst; eauto.
 Qed.
 Lemma coqeq_complete' n k (a b : PTm n) :
  algo_metric k a b ->
@ -1333,7 +1046,7 @@ Proof.
  - split; last by sfirstorder use:hf_not_hne.
    move {hnfneu}.
    case : a h fb fa => //=.
-    + case : b => //=; try qauto depth:1 use:T_AbsPair_Imp, T_AbsBind_Imp, T_AbsUniv_Imp, T_AbsZero_Imp, T_AbsSuc_Imp, T_AbsNat_Imp.
+    + case : b => //=; try qauto depth:1 use:T_AbsPair_Imp, T_AbsBind_Imp, T_AbsUniv_Imp.
      move => a0 a1 ha0 _ _ Γ A wt0 wt1.
      move : T_Abs_Inv wt0 wt1; repeat move/[apply]. move  => [Δ [V [wt1 wt0]]].
      apply : CE_HRed; eauto using rtc_refl.
@ -1364,7 +1077,7 @@ Proof.
      simpl in *.
      have [*] : va' = va /\ vb' = vb by eauto using red_uniquenf. subst.
      sfirstorder.
-    + case : b => //=; try qauto depth:1 use:T_AbsPair_Imp, T_PairBind_Imp, T_PairUniv_Imp, T_PairNat_Imp, T_PairSuc_Imp, T_PairZero_Imp.
+    + case : b => //=; try qauto depth:1 use:T_AbsPair_Imp, T_PairBind_Imp, T_PairUniv_Imp.
      move => a1 b1 a0 b0 h _ _ Γ A hu0 hu1.
      have [sn0 sn1] : SN (PPair a0 b0) /\ SN (PPair a1 b1)
        by qauto l:on use:fundamental_theorem, logrel.SemWt_SN.
@ -1432,12 +1145,6 @@ Proof.
        eauto using Su_Eq.
      * move => > /algo_metric_join.
        hauto lq:on use:DJoin.bind_univ_noconf.
      * move => > /algo_metric_join.
        hauto lq:on use:Sub.nat_bind_noconf, Sub.FromJoin.
      * move => > /algo_metric_join.
        clear. hauto lq:on rew:off use:REReds.bind_inv, REReds.zero_inv.
      * move => > /algo_metric_join. clear.
        hauto lq:on rew:off use:REReds.bind_inv, REReds.suc_inv.
    + case : b => //=.
      * hauto lq:on use:T_AbsUniv_Imp.
      * hauto lq:on use:T_PairUniv_Imp.
@ -1445,55 +1152,6 @@ Proof.
      * move => i j /algo_metric_join /DJoin.univ_inj ? _ _ Γ A hi hj.
        subst.
        hauto l:on.
      * move => > /algo_metric_join.
        hauto lq:on use:Sub.nat_univ_noconf, Sub.FromJoin.
      * move => > /algo_metric_join.
        clear. hauto lq:on rew:off use:REReds.univ_inv, REReds.zero_inv.
      * move => > /algo_metric_join.
        clear. hauto lq:on rew:off use:REReds.univ_inv, REReds.suc_inv.
    + case : b => //=.
      * qauto l:on use:T_AbsNat_Imp.
      * qauto l:on use:T_PairNat_Imp.
      * move => > /algo_metric_join /Sub.FromJoin. hauto l:on use:Sub.bind_nat_noconf.
      * move => > /algo_metric_join /Sub.FromJoin. hauto lq:on use:Sub.univ_nat_noconf.
      * hauto l:on.
      * move /algo_metric_join.
        hauto lq:on rew:off use:REReds.nat_inv, REReds.zero_inv.
      * move => > /algo_metric_join.
        hauto lq:on rew:off use:REReds.nat_inv, REReds.suc_inv.
    (* Zero *)
    + case : b => //=.
      * hauto lq:on rew:off use:T_AbsZero_Imp.
      * hauto lq: on use: T_PairZero_Imp.
      * move =>> /algo_metric_join.
        hauto lq:on rew:off use:REReds.zero_inv, REReds.bind_inv.
      * move =>> /algo_metric_join.
        hauto lq:on rew:off use:REReds.zero_inv, REReds.univ_inv.
      * move =>> /algo_metric_join.
        hauto lq:on rew:off use:REReds.zero_inv, REReds.nat_inv.
      * hauto l:on.
      * move =>> /algo_metric_join.
        hauto lq:on rew:off use:REReds.zero_inv, REReds.suc_inv.
    (* Suc *)
    + case : b => //=.
      * hauto lq:on rew:off use:T_AbsSuc_Imp.
      * hauto lq:on use:T_PairSuc_Imp.
      * move => > /algo_metric_join.
        hauto lq:on rew:off use:REReds.suc_inv, REReds.bind_inv.
      * move => > /algo_metric_join.
        hauto lq:on rew:off use:REReds.suc_inv, REReds.univ_inv.
      * move => > /algo_metric_join.
        hauto lq:on rew:off use:REReds.suc_inv, REReds.nat_inv.
      * move => > /algo_metric_join.
        hauto lq:on rew:off use:REReds.suc_inv, REReds.zero_inv.
      * move => a0 a1 h _ _.
        move /algo_metric_suc : h => [j [h4 h5]].
        move => Γ A /Suc_Inv [h0 h1] /Suc_Inv [h2 h3].
        move : ih h4 h5;do!move/[apply].
        move => [ih _].
        move : ih h0 h2;do!move/[apply].
        move => h. apply : CE_HRed; eauto using rtc_refl.
        by constructor.
  - move : k a b h fb fa. abstract : hnfneu.
    move => k.
    move => + b.
@ -1550,27 +1208,6 @@ Proof.
      hauto l:on use:Sub.hne_bind_noconf.
    (* NeuUniv: Impossible *)
    + hauto lq:on rew:off use:DJoin.hne_univ_noconf, algo_metric_join.
    + hauto lq:on rew:off use:DJoin.hne_nat_noconf, algo_metric_join.
    (* Zero *)
    + case => //=.
      * move => i /algo_metric_join. clear.
        hauto lq:on rew:off use:REReds.var_inv, REReds.zero_inv.
      * move => >/algo_metric_join. clear.
        hauto lq:on rew:off use:REReds.hne_app_inv, REReds.zero_inv.
      * move => >/algo_metric_join. clear.
        hauto lq:on rew:off use:REReds.hne_proj_inv, REReds.zero_inv.
      * sfirstorder use:T_Bot_Imp.
      * move => >/algo_metric_join. clear.
        move => h _ h2. exfalso.
        hauto q:on use:REReds.hne_ind_inv, REReds.zero_inv.
    (* Suc *)
    + move => a0.
      case => //=; move => >/algo_metric_join; clear.
      * hauto lq:on rew:off use:REReds.var_inv, REReds.suc_inv.
      * hauto lq:on rew:off use:REReds.hne_app_inv, REReds.suc_inv.
      * hauto lq:on rew:off use:REReds.hne_proj_inv, REReds.suc_inv.
      * sfirstorder use:T_Bot_Imp.
      * hauto q:on use:REReds.hne_ind_inv, REReds.suc_inv.
  - move {ih}.
    move /algo_metric_sym in h.
    qauto l:on use:coqeq_symmetric_mutual.
@ -1583,22 +1220,20 @@ Proof.
    by firstorder.
    case : a h fb fa => //=.
-    + case : b => //=; move => > /algo_metric_join.
+    + case : b => //=.
-      * move /DJoin.var_inj => ?. subst. qauto l:on use:Var_Inv, T_Var,CE_VarCong.
+      move => i j hi _ _.
-      * clear => ? ? _. exfalso.
+      * have ? : j = i by hauto lq:on use:algo_metric_join, DJoin.var_inj. subst.
        move => Γ A B hA hB.
        split. apply CE_VarCong.
        exists (Γ i). hauto l:on use:Var_Inv, T_Var.
      * move => p p0 f /algo_metric_join. clear => ? ? _. exfalso.
        hauto l:on use:REReds.var_inv, REReds.hne_app_inv.
-      * clear => ? ? _. exfalso.
+      * move => a0 a1 i /algo_metric_join. clear => ? ? _. exfalso.
        hauto l:on use:REReds.var_inv, REReds.hne_proj_inv.
      * sfirstorder use:T_Bot_Imp.
-      * clear => ? ? _. exfalso.
+    + case : b => //=.
-        hauto q:on use:REReds.var_inv, REReds.hne_ind_inv.
+      * clear. move => i a a0 /algo_metric_join h _ ?. exfalso.
-    + case : b => //=;
+        hauto l:on use:REReds.hne_app_inv, REReds.var_inv.
                   lazymatch goal with
                   | [|- context[algo_metric _ (PApp _ _) (PApp _ _)]] => idtac
                   | _ => move => > /algo_metric_join
                   end.
      * clear => *. exfalso.
        hauto lq:on rew:off use:REReds.hne_app_inv, REReds.var_inv.
      (* real case *)
      * move => b1 a1 b0 a0 halg hne1 hne0 Γ A B wtA wtB.
        move /App_Inv : wtA => [A0][B0][hb0][ha0]hS0.
@ -1624,7 +1259,7 @@ Proof.
        move => [ih _].
        move : ih (ha0') (ha1'); repeat move/[apply].
        move => iha.
-        split. qblast.
+        split. sauto lq:on.
        exists (subst_PTm (scons a0 VarPTm) B2).
        split.
        apply : Su_Transitive; eauto.
@ -1644,11 +1279,9 @@ Proof.
        move /E_Symmetric in h01.
        move /regularity_sub0 : hSu20 => [i0].
        sfirstorder use:bind_inst.
-      * clear => ? ? ?. exfalso.
+      * move => p p0 p1 p2 /algo_metric_join. clear => ? ? ?. exfalso.
        hauto q:on use:REReds.hne_app_inv, REReds.hne_proj_inv.
      * sfirstorder use:T_Bot_Imp.
      * clear => ? ? ?. exfalso.
        hauto q:on use:REReds.hne_app_inv, REReds.hne_ind_inv.
    + case : b => //=.
      * move => i p h /algo_metric_join. clear => ? _ ?. exfalso.
        hauto l:on use:REReds.hne_proj_inv, REReds.var_inv.
@ -1709,66 +1342,7 @@ Proof.
               move /regularity_sub0 in hSu21.
               sfirstorder use:bind_inst.
      * sfirstorder use:T_Bot_Imp.
      * move => > /algo_metric_join; clear => ? ? ?. exfalso.
        hauto q:on use:REReds.hne_proj_inv, REReds.hne_ind_inv.
    + sfirstorder use:T_Bot_Imp.
    (* ind ind case *)
    + move => P a0 b0 c0.
      case : b => //=;
                   lazymatch goal with
                   | [|- context[algo_metric _ (PInd _ _ _ _) (PInd _ _ _ _)]] => idtac
                   | _ => move => > /algo_metric_join; clear => *; exfalso
                   end.
      * hauto q:on use:REReds.hne_ind_inv, REReds.var_inv.
      * hauto q:on use:REReds.hne_ind_inv, REReds.hne_app_inv.
      * hauto q:on use:REReds.hne_ind_inv, REReds.hne_proj_inv.
      * sfirstorder use:T_Bot_Imp.
      * move => P1 a1 b1 c1 /[dup] halg /algo_metric_ind + h0 h1.
        move /(_ h1 h0).
        move => [j][hj][hP][ha][hb]hc Γ A B hL hR.
        move /Ind_Inv : hL => [iP0][wtP0][wta0][wtb0][wtc0]hSu0.
        move /Ind_Inv : hR => [iP1][wtP1][wta1][wtb1][wtc1]hSu1.
        have {}iha : a0 ∼ a1 by qauto l:on.
        have []  : iP0 <= max iP0 iP1 /\ iP1 <= max iP0 iP1 by lia.
        move : T_Univ_Raise wtP0; do!move/[apply]. move => wtP0.
        move : T_Univ_Raise wtP1; do!move/[apply]. move => wtP1.
        have {}ihP : P ⇔ P1 by qauto l:on.
        set Δ := funcomp _ _ in wtP0, wtP1, wtc0, wtc1.
        have wfΔ :⊢ Δ by hauto l:on use:wff_mutual.
        have hPE : Δ ⊢ P ≡ P1 ∈ PUniv (max iP0 iP1)
          by hauto l:on use:coqeq_sound_mutual.
        have haE : Γ ⊢ a0 ≡ a1 ∈ PNat
          by hauto l:on use:coqeq_sound_mutual.
        have wtΓ : ⊢ Γ by hauto l:on use:wff_mutual.
        have hE : Γ ⊢ subst_PTm (scons PZero VarPTm) P ≡ subst_PTm (scons PZero VarPTm) P1 ∈ subst_PTm (scons PZero VarPTm) (PUniv (Nat.max iP0 iP1)).
        eapply morphing; eauto. apply morphing_ext. by apply morphing_id. by apply T_Zero.
        have {}wtb1 : Γ ⊢ b1 ∈ subst_PTm (scons PZero VarPTm) P
          by eauto using T_Conv_E.
        have {}ihb : b0 ⇔ b1 by hauto l:on.
        have hPSig : Γ ⊢ PBind PSig PNat P ≡ PBind PSig PNat P1 ∈ PUniv (Nat.max iP0 iP1) by eauto with wt.
        set T := ren_PTm shift _ in wtc0.
        have : funcomp (ren_PTm shift) (scons P Δ) ⊢ c1 ∈ T.
        apply : T_Conv; eauto. apply : ctx_eq_subst_one; eauto with wt.
        apply : Su_Eq; eauto.
        subst T. apply : weakening_su; eauto.
        eapply morphing. apply : Su_Eq. apply E_Symmetric. by eauto.
        hauto l:on use:wff_mutual.
        apply morphing_ext. set x := funcomp _ _.
        have -> : x = funcomp (ren_PTm shift) VarPTm by asimpl.
        apply : morphing_ren; eauto using renaming_shift.
        apply : renaming_shift; eauto. by apply morphing_id.
        apply T_Suc. by apply T_Var. subst T => {}wtc1.
        have {}ihc : c0 ⇔ c1 by qauto l:on.
        move => [:ih].
        split. abstract : ih. move : h0 h1 ihP iha ihb ihc. clear. sauto lq:on.
        have hEInd : Γ ⊢ PInd P a0 b0 c0 ≡ PInd P1 a1 b1 c1 ∈ subst_PTm (scons a0 VarPTm) P by hfcrush use:coqeq_sound_mutual.
        exists (subst_PTm (scons a0 VarPTm) P).
        repeat split => //=; eauto with wt.
        apply : Su_Transitive.
        apply : Su_Sig_Proj2; eauto. apply : Su_Sig; eauto using T_Nat' with wt.
        apply : Su_Eq. apply E_Refl. by apply T_Nat'.
        apply : Su_Eq. apply hPE. by eauto.
        move : hEInd. clear. hauto l:on use:regularity.
 Qed.
 Lemma coqeq_sound : forall n Γ (a b : PTm n) A,
@ -1815,9 +1389,6 @@ Inductive CoqLEq {n} : PTm n -> PTm n -> Prop :=
  (* ---------------------------- *)
  PBind PSig A0 B0 ⋖ PBind PSig A1 B1
 | CLE_NatCong :
  PNat ⋖ PNat
 | CLE_NeuNeu a0 a1 :
  a0 ∼ a1 ->
  a0 ⋖ a1
@ -1880,7 +1451,6 @@ Proof.
    apply : ihB; by eauto using ctx_eq_subst_one.
    apply : Su_Sig; eauto using E_Refl, Su_Eq.
  - sauto lq:on use:coqeq_sound_mutual, Su_Eq.
  - sauto lq:on use:coqeq_sound_mutual, Su_Eq.
  - move => n a a' b b' ? ? ? ih Γ i ha hb.
    have /Su_Eq ? : Γ ⊢ a ≡ a' ∈ PUniv i by sfirstorder use:HReds.ToEq.
    have /E_Symmetric /Su_Eq ? : Γ ⊢ b ≡ b' ∈ PUniv i by sfirstorder use:HReds.ToEq.
@ -1905,15 +1475,6 @@ Proof.
    inversion E; subst => /=.
    + hauto lq:on use:HRed.ProjPair unfold:algo_metric solve+:lia.
    + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:algo_metric solve+:lia.
  - inversion h0 as [|A B C D E F]; subst.
    hauto qb:on use:ne_hne.
    inversion E; subst => /=.
    + hauto lq:on use:HRed.IndZero unfold:algo_metric solve+:lia.
    + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:algo_metric solve+:lia.
    + sfirstorder use:ne_hne.
    + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:algo_metric solve+:lia.
    + sfirstorder use:ne_hne.
    + sfirstorder use:ne_hne.
 Qed.
 Lemma CLE_HRedL n (a a' b : PTm n)  :
@ -1950,15 +1511,6 @@ Proof.
    inversion E; subst => /=.
    + hauto lq:on use:HRed.ProjPair unfold:algo_metric solve+:lia.
    + hauto q:on ctrs:HRed.R use: hf_hred_lored unfold:algo_metric solve+:lia.
  - inversion 1 as [|A B C D E F]; subst.
    hauto qb:on use:ne_hne.
    inversion E; subst => /=.
    + hauto lq:on use:HRed.IndZero unfold:algo_metric solve+:lia.
    + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:algo_metric solve+:lia.
    + sfirstorder use:ne_hne.
    + hauto lq:on ctrs:HRed.R use:hf_hred_lored unfold:algo_metric solve+:lia.
    + sfirstorder use:ne_hne.
    + sfirstorder use:ne_hne.
 Qed.
 Lemma salgo_metric_sub n k (a b : PTm n) :
@ -2043,55 +1595,21 @@ Proof.
             by hauto l:on.
           eauto using ctx_eq_subst_one.
      * hauto lq:on use:salgo_metric_sub, Sub.bind_univ_noconf.
      * hauto lq:on use:salgo_metric_sub, Sub.nat_bind_noconf.
      * move => _ > _ /salgo_metric_sub.
        hauto lq:on rew:off use:REReds.bind_inv, REReds.zero_inv inv:Sub1.R.
      * hauto lq:on rew:off use:REReds.bind_inv, REReds.suc_inv, salgo_metric_sub inv:Sub1.R.
    + case : b fb => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'.
      * hauto lq:on use:salgo_metric_sub, Sub.univ_bind_noconf.
      * move => *. econstructor; eauto using rtc_refl.
        hauto lq:on use:salgo_metric_sub, Sub.univ_inj, CLE_UnivCong.
      * hauto lq:on rew:off use:REReds.univ_inv, REReds.nat_inv, salgo_metric_sub inv:Sub1.R.
      * hauto lq:on rew:off use:REReds.univ_inv, REReds.zero_inv, salgo_metric_sub inv:Sub1.R.
      * hauto lq:on rew:off use:REReds.suc_inv, REReds.univ_inv, salgo_metric_sub inv:Sub1.R.
  (* Both cases are impossible *)
    + case : b fb => //=.
      * hauto lq:on use:T_AbsNat_Imp.
      * hauto lq:on use:T_PairNat_Imp.
      * hauto lq:on rew:off use:REReds.nat_inv, REReds.bind_inv, salgo_metric_sub inv:Sub1.R.
      * hauto lq:on rew:off use:REReds.nat_inv, REReds.univ_inv, salgo_metric_sub inv:Sub1.R.
      * hauto l:on.
      * hauto lq:on rew:off use:REReds.nat_inv, REReds.zero_inv, salgo_metric_sub inv:Sub1.R.
      * hauto lq:on rew:off use:REReds.nat_inv, REReds.suc_inv, salgo_metric_sub inv:Sub1.R.
    + move => ? ? Γ i /Zero_Inv.
      clear.
      move /synsub_to_usub => [_ [_ ]].
      hauto lq:on rew:off use:REReds.nat_inv, REReds.univ_inv inv:Sub1.R.
    + move => ? _ _ Γ i /Suc_Inv => [[_]].
      move /synsub_to_usub.
      hauto lq:on rew:off use:REReds.nat_inv, REReds.univ_inv inv:Sub1.R.
  - have {}h : DJoin.R a b by
       hauto lq:on use:salgo_metric_algo_metric, algo_metric_join.
    case : b fb h => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'.
    + hauto lq:on use:DJoin.hne_bind_noconf.
    + hauto lq:on use:DJoin.hne_univ_noconf.
    + hauto lq:on use:DJoin.hne_nat_noconf.
    + move => _ _ Γ i _.
      move /Zero_Inv.
      hauto q:on use:REReds.nat_inv, REReds.univ_inv, synsub_to_usub inv:Sub1.R.
    + move => p _ _ Γ i _ /Suc_Inv.
      hauto q:on use:REReds.nat_inv, REReds.univ_inv, synsub_to_usub inv:Sub1.R.
  - have {}h : DJoin.R b a by
      hauto lq:on use:salgo_metric_algo_metric, algo_metric_join, DJoin.symmetric.
    case : a fa h => //=; try hauto depth:1 lq:on use:T_AbsUniv_Imp', T_PairUniv_Imp'.
    + hauto lq:on use:DJoin.hne_bind_noconf.
    + hauto lq:on use:DJoin.hne_univ_noconf.
    + hauto lq:on use:DJoin.hne_nat_noconf.
    + move => _ _ Γ i.
      move /Zero_Inv.
      hauto q:on use:REReds.nat_inv, REReds.univ_inv, synsub_to_usub inv:Sub1.R.
    + move => p _ _ Γ i /Suc_Inv.
      hauto q:on use:REReds.nat_inv, REReds.univ_inv, synsub_to_usub inv:Sub1.R.
  - move => Γ i ha hb.
    econstructor; eauto using rtc_refl.
    apply CLE_NeuNeu. move {ih}.
--- a/theories/common.v
+++ b/theories/common.v
@ -1,4 +1,4 @@
-Require Import Autosubst2.fintype Autosubst2.syntax Autosubst2.core ssreflect.
+Require Import Autosubst2.fintype Autosubst2.syntax ssreflect.
 From Ltac2 Require Ltac2.
 Import Ltac2.Notations.
 Import Ltac2.Control.
@ -7,6 +7,16 @@ 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.
@ -14,26 +24,27 @@ Proof.
  sblast inv:option.
 Qed.
 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 lq:on rew:off use:up_injective))
  | _ => solve_anti_ren ()
  end.
 Local Ltac solve_anti_ren := ltac2:(Control.enter solve_anti_ren).
 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 : m ξ b.
-Qed.
+  elim : n / a => //; try solve_anti_ren.
-Inductive HF : Set :=
+  move => n a iha m ξ []//=.
-| H_Pair | H_Abs | H_Univ | H_Bind (p : BTag) | H_Nat | H_Suc | H_Zero | H_Bot.
+  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
@ -41,31 +52,15 @@ Definition ishf {n} (a : PTm n) :=
  | PAbs _ => true
  | PUniv _ => true
  | PBind _ _ _ => true
  | PNat => true
  | PSuc _ => true
  | PZero => true
  | _ => false
  end.
 Definition toHF {n} (a : PTm n) :=
  match a with
  | PPair _ _ => H_Pair
  | PAbs _ => H_Abs
  | PUniv _ => H_Univ
  | PBind p _ _ => H_Bind p
  | PNat => H_Nat
  | PSuc _ => H_Suc
  | PZero => H_Zero
  | _ => H_Bot
  end.
 Fixpoint ishne {n} (a : PTm n) :=
  match a with
  | VarPTm _ => true
  | PApp a _ => ishne a
  | PProj _ a => ishne a
  | PBot => true
  | PInd _ n _ _ => ishne n
  | _ => false
  end.
@ -79,12 +74,6 @@ Definition ispair {n} (a : PTm n) :=
  | _ => false
  end.
 Definition isnat {n} (a : PTm n) := if a is PNat then true else false.
 Definition iszero {n} (a : PTm n) := if a is PZero then true else false.
 Definition issuc {n} (a : PTm n) := if a is PSuc _ then true else false.
 Definition isabs {n} (a : PTm n) :=
  match a with
  | PAbs _ => true
@ -106,7 +95,3 @@ 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.
 Lemma renaming_shift n m Γ (ρ : fin n -> PTm m) A :
  renaming_ok (funcomp (ren_PTm shift) (scons (subst_PTm ρ A) Γ)) Γ shift.
 Proof. sfirstorder. Qed.
--- a/theories/executable.v
+++ b/theories/executable.v
@ -1,145 +0,0 @@
 From Equations Require Import Equations.
 Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax
  common typing preservation admissible fp_red structural soundness.
 Require Import algorithmic.
 From stdpp Require Import relations (rtc(..), nsteps(..)).
 Require Import ssreflect ssrbool.
 Inductive algo_dom {n} : PTm n -> PTm n -> Prop :=
 | A_AbsAbs a b :
  algo_dom a b ->
  (* --------------------- *)
  algo_dom (PAbs a) (PAbs b)
 | A_AbsNeu a u :
  ishne u ->
  algo_dom a (PApp (ren_PTm shift u) (VarPTm var_zero)) ->
  (* --------------------- *)
  algo_dom (PAbs a) u
 | A_NeuAbs a u :
  ishne u ->
  algo_dom (PApp (ren_PTm shift u) (VarPTm var_zero)) a ->
  (* --------------------- *)
  algo_dom u (PAbs a)
 | A_PairPair a0 a1 b0 b1 :
  algo_dom a0 a1 ->
  algo_dom b0 b1 ->
  (* ---------------------------- *)
  algo_dom (PPair a0 b0) (PPair a1 b1)
 | A_PairNeu a0 a1 u :
  ishne u ->
  algo_dom a0 (PProj PL u) ->
  algo_dom a1 (PProj PR u) ->
  (* ----------------------- *)
  algo_dom (PPair a0 a1) u
 | A_NeuPair a0 a1 u :
  ishne u ->
  algo_dom (PProj PL u) a0 ->
  algo_dom (PProj PR u) a1 ->
  (* ----------------------- *)
  algo_dom u (PPair a0 a1)
 | A_UnivCong i j :
  (* -------------------------- *)
  algo_dom (PUniv i) (PUniv j)
 | A_BindCong p0 p1 A0 A1 B0 B1 :
  algo_dom A0 A1 ->
  algo_dom B0 B1 ->
  (* ---------------------------- *)
  algo_dom (PBind p0 A0 B0) (PBind p1 A1 B1)
 | A_VarCong i j :
  (* -------------------------- *)
  algo_dom (VarPTm i) (VarPTm j)
 | A_ProjCong p0 p1 u0 u1 :
  ishne u0 ->
  ishne u1 ->
  algo_dom u0 u1 ->
  (* ---------------------  *)
  algo_dom (PProj p0 u0) (PProj p1 u1)
 | A_AppCong u0 u1 a0 a1 :
  ishne u0 ->
  ishne u1 ->
  algo_dom u0 u1 ->
  algo_dom a0 a1 ->
  (* ------------------------- *)
  algo_dom (PApp u0 a0) (PApp u1 a1)
 | A_HRedL a a' b  :
  HRed.R a a' ->
  algo_dom a' b ->
  (* ----------------------- *)
  algo_dom a b
 | A_HRedR a b b'  :
  ishne a \/ ishf a ->
  HRed.R b b' ->
  algo_dom a b' ->
  (* ----------------------- *)
  algo_dom a b.
 Definition fin_eq {n} (i j : fin n) : bool.
 Proof.
  induction n.
  - by exfalso.
  - refine (match i , j with
            | None, None => true
            | Some i, Some j => IHn i j
            | _, _ => false
            end).
 Defined.
 Lemma fin_eq_dec {n} (i j : fin n) :
  Bool.reflect (i = j) (fin_eq i j).
 Proof.
  revert i j. induction n.
  - destruct i.
  - destruct i; destruct j.
    + specialize (IHn f f0).
      inversion IHn; subst.
      simpl. rewrite -H.
      apply ReflectT.
      reflexivity.
      simpl. rewrite -H.
      apply ReflectF.
      injection. tauto.
    + by apply ReflectF.
    + by apply ReflectF.
    + by apply ReflectT.
 Defined.
 Equations check_equal {n} (a b : PTm n) (h : algo_dom a b) :
  bool by struct h :=
  check_equal a b h with (@idP (ishne a || ishf a)) := {
    | Bool.ReflectT _ _ => _
    | Bool.ReflectF _ _ => _
    }.
  (* check_equal (VarPTm i) (VarPTm j) h := fin_eq i j; *)
  (* check_equal (PAbs a) (PAbs b) h := check_equal a b _; *)
  (* check_equal (PPair a0 b0) (PPair a1 b1) h := *)
  (*   check_equal a0 b0 _ && check_equal a1 b1 _; *)
  (* check_equal (PUniv i) (PUniv j) _ := _; *)
 Next Obligation.
  simpl.
  intros ih.
 Admitted.
 Search (Bool.reflect (is_true _) _).
 Check idP.
 Definition metric {n} k (a b : PTm n) :=
  exists i j va vb, nsteps LoRed.R i a va /\ nsteps LoRed.R j b vb /\
  nf va /\ nf vb /\ size_PTm va + size_PTm vb + i + j <= k.
 Search (nat -> nat -> bool).
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
--- a/theories/logrel.v
+++ b/theories/logrel.v
@ -31,9 +31,6 @@ Inductive InterpExt {n} i (I : nat -> PTm n -> Prop) : PTm n -> (PTm n -> Prop)
  (forall a PB, PF a PB -> ⟦ subst_PTm (scons a VarPTm) B ⟧ i ;; I ↘ PB) ->
  ⟦ PBind p A B ⟧ i ;; I ↘ BindSpace p PA PF
 | InterpExt_Nat :
  ⟦ PNat ⟧ i ;; I ↘ SNat
 | InterpExt_Univ j :
  j < i ->
  ⟦ PUniv j ⟧ i ;; I ↘ (I j)
@ -71,7 +68,6 @@ Proof.
  - hauto q:on ctrs:InterpExt.
  - hauto lq:on rew:off ctrs:InterpExt.
  - hauto q:on ctrs:InterpExt.
  - hauto q:on ctrs:InterpExt.
  - hauto lq:on ctrs:InterpExt.
 Qed.
@ -92,14 +88,14 @@ Lemma InterpUnivN_nolt n i :
 Proof.
  simp InterpUnivN.
  extensionality A. extensionality PA.
  set I0 := (fun _ => _).
  set I1 := (fun _ => _).
  apply InterpExt_lt_eq.
  hauto q:on.
 Qed.
 #[export]Hint Rewrite @InterpUnivN_nolt : InterpUniv.
 Check InterpExt_ind.
 Lemma InterpUniv_ind
  : forall n (P : nat -> PTm n -> (PTm n -> Prop) -> Prop),
       (forall i (A : PTm n), SNe A -> P i A (fun a : PTm n => exists v : PTm n, rtc TRedSN a v /\ SNe v)) ->
@ -111,12 +107,11 @@ Lemma InterpUniv_ind
        (forall (a : PTm n) (PB : PTm n -> Prop), PF a PB -> ⟦ subst_PTm (scons a VarPTm) B ⟧ i ↘ PB) ->
        (forall (a : PTm n) (PB : PTm n -> Prop), PF a PB -> P i (subst_PTm (scons a VarPTm) B) PB) ->
        P i (PBind p A B) (BindSpace p PA PF)) ->
       (forall i, P i PNat SNat) ->
       (forall i j : nat, j < i ->  (forall A PA, ⟦ A ⟧ j ↘ PA -> P j A PA) -> P i (PUniv j) (fun A => exists PA, ⟦ A ⟧ j ↘ PA)) ->
       (forall i (A A0 : PTm n) (PA : PTm n -> Prop), TRedSN A A0 -> ⟦ A0 ⟧ i ↘ PA -> P i A0 PA -> P i A PA) ->
       forall i (p : PTm n) (P0 : PTm n -> Prop), ⟦ p ⟧ i ↘ P0 -> P i p P0.
 Proof.
-  move => n P  hSN hBind hNat hUniv hRed.
+  move => n P  hSN hBind hUniv hRed.
  elim /Wf_nat.lt_wf_ind => i ih . simp InterpUniv.
  move => A PA. move => h. set I := fun _ => _ in h.
  elim : A PA / h; rewrite -?InterpUnivN_nolt; eauto.
@ -149,9 +144,6 @@ Lemma InterpUniv_Step i n A A0 PA :
  ⟦ A ⟧ i ↘ PA.
 Proof. simp InterpUniv. apply InterpExt_Step. Qed.
 Lemma InterpUniv_Nat i n :
  ⟦ PNat : PTm n ⟧ i ↘ SNat.
 Proof. simp InterpUniv. apply InterpExt_Nat. Qed.
 #[export]Hint Resolve InterpUniv_Bind InterpUniv_Step InterpUniv_Ne InterpUniv_Univ : InterpUniv.
@ -184,14 +176,6 @@ Proof.
  induction 1; eauto using N_Exp.
 Qed.
 Lemma CR_SNat : forall n,  @CR n SNat.
 Proof.
  move => n. rewrite /CR.
  split.
  induction 1; hauto q:on ctrs:SN,SNe.
  hauto lq:on ctrs:SNat.
 Qed.
 Lemma adequacy : forall i n A PA,
   ⟦ A : PTm n ⟧ i ↘ PA ->
  CR PA /\ SN A.
@ -218,7 +202,6 @@ Proof.
      apply : N_Exp; eauto using N_β.
      hauto lq:on.
      qauto l:on use:SN_AppInv, SN_NoForbid.P_AbsInv.
  - qauto use:CR_SNat.
  - hauto l:on ctrs:InterpExt rew:db:InterpUniv.
  - hauto l:on ctrs:SN unfold:CR.
 Qed.
@ -244,7 +227,6 @@ Proof.
    apply N_AppL => //=.
    hauto q:on use:adequacy.
    + hauto lq:on ctrs:rtc unfold:SumSpace.
  - hauto lq:on ctrs:SNat.
  - hauto l:on use:InterpUniv_Step.
 Qed.
@ -256,14 +238,14 @@ Proof.
  induction 2; hauto lq:on ctrs:rtc use:InterpUniv_back_clos.
 Qed.
 Lemma InterpUniv_case n i (A : PTm n) PA :
  ⟦ A ⟧ i ↘ PA ->
-  exists H, rtc TRedSN A H /\  ⟦ H ⟧ i ↘ PA /\ (SNe H \/ isbind H \/ isuniv H \/ isnat H).
+  exists H, rtc TRedSN A H /\  ⟦ H ⟧ i ↘ PA /\ (SNe H \/ isbind H \/ isuniv H).
 Proof.
  move : i A PA. apply InterpUniv_ind => //=.
  hauto lq:on ctrs:rtc use:InterpUniv_Ne.
  hauto l:on use:InterpUniv_Bind.
  hauto l:on use:InterpUniv_Nat.
  hauto l:on use:InterpUniv_Univ.
  hauto lq:on ctrs:rtc.
 Qed.
@ -280,7 +262,7 @@ 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 Sub.sne_bind_noconf Sub.sne_univ_noconf Sub.bind_univ_noconf
-  Sub.bind_sne_noconf Sub.univ_sne_noconf Sub.univ_bind_noconf Sub.nat_bind_noconf Sub.bind_nat_noconf Sub.sne_nat_noconf Sub.nat_sne_noconf Sub.univ_nat_noconf Sub.nat_univ_noconf: 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 ->
@ -303,14 +285,6 @@ Proof. simp InterpUniv.
       sauto lq:on.
 Qed.
 Lemma InterpUniv_Nat_inv n i S :
  ⟦ PNat : PTm n ⟧ i ↘ S -> S = SNat.
 Proof.
  simp InterpUniv.
       inversion 1; try hauto inv:SNe q:on use:redsn_preservation_mutual.
       sauto lq:on.
 Qed.
 Lemma InterpUniv_Univ_inv n i j S :
  ⟦ PUniv j : PTm n ⟧ i ↘ S ->
  S = (fun A => exists PA, ⟦ A ⟧ j ↘ PA) /\ j < i.
@ -357,7 +331,7 @@ Proof.
      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 /\ ~ isnat H by itauto.
+      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.
@ -367,7 +341,7 @@ Proof.
      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 /\ ~ isnat H by itauto.
+      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.
@ -377,7 +351,7 @@ Proof.
      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 /\ ~ isnat H by itauto.
+      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 => //=.
@ -396,7 +370,7 @@ Proof.
      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 /\ ~ isnat H by itauto.
+      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 => //=.
@ -408,36 +382,13 @@ Proof.
      move => a PB PB' ha hPB hPB'.
      eapply ihPF; eauto.
      apply Sub.cong => //=; eauto using DJoin.refl.
  - move =>  i B PB h. split.
    + move => hAB a ha.
      have ? : SN B by hauto l:on use:adequacy.
      move /InterpUniv_case : h.
      move => [H [/DJoin.FromRedSNs h [h1 h0]]].
      have {h}{}hAB : Sub.R PNat H by qauto l:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
      have {}h0 : isnat H.
      suff : ~ isbind H /\ ~ isuniv H /\ ~ SNe H by itauto.
      have : @isnat n PNat by simpl.
      move : h0 hAB. clear. qauto l:on db:noconf.
      case : H h1 hAB h0 => //=.
      move /InterpUniv_Nat_inv. scongruence.
    + move => hAB a ha.
      have ? : SN B by hauto l:on use:adequacy.
      move /InterpUniv_case : h.
      move => [H [/DJoin.FromRedSNs h [h1 h0]]].
      have {h}{}hAB : Sub.R H PNat by qauto l:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
      have {}h0 : isnat H.
      suff : ~ isbind H /\ ~ isuniv H /\ ~ SNe H by itauto.
      have : @isnat n PNat by simpl.
      move : h0 hAB. clear. qauto l:on db:noconf.
      case : H h1 hAB h0 => //=.
      move /InterpUniv_Nat_inv. scongruence.
  - 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 /\ ~ isnat H by tauto. move : h. clear. hauto lq:on db:noconf.
+      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.
@ -449,7 +400,7 @@ Proof.
      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 /\ ~ isnat H by tauto. move : h. clear. hauto lq:on db:noconf.
+      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.
@ -683,70 +634,6 @@ Proof.
  hauto q:on solve+:(by asimpl).
 Qed.
 Definition smorphing_ok {n m} (Δ : fin m -> PTm m) Γ (ρ : fin n -> PTm m) :=
  forall ξ, ρ_ok Δ ξ -> ρ_ok Γ (funcomp (subst_PTm ξ) ρ).
 Lemma smorphing_ok_refl n (Δ : fin n -> PTm n) : smorphing_ok Δ Δ VarPTm.
  rewrite /smorphing_ok => ξ. apply.
 Qed.
 Lemma smorphing_ren n m p Ξ Δ Γ
  (ρ : fin n -> PTm m) (ξ : fin m -> fin p) :
  renaming_ok Ξ Δ ξ -> smorphing_ok Δ Γ ρ ->
  smorphing_ok Ξ Γ (funcomp (ren_PTm ξ) ρ).
 Proof.
  move => hξ hρ τ.
  move /ρ_ok_renaming : hξ => /[apply].
  move => h.
  rewrite /smorphing_ok in hρ.
  asimpl.
  Check (funcomp τ ξ).
  set u := funcomp _ _.
  have : u = funcomp (subst_PTm (funcomp τ ξ)) ρ.
  subst u. extensionality i. by asimpl.
  move => ->. by apply hρ.
 Qed.
 Lemma smorphing_ext n m Δ Γ (ρ : fin n -> PTm m) (a : PTm m) (A : PTm n)  :
  smorphing_ok Δ Γ ρ ->
  Δ ⊨ a ∈ subst_PTm ρ A ->
  smorphing_ok
  Δ (funcomp (ren_PTm shift) (scons A Γ)) (scons a ρ).
 Proof.
  move => h ha τ. move => /[dup] hτ.
  move : ha => /[apply].
  move => [k][PA][h0]h1.
  apply h in hτ.
  move => i.
  destruct i as [i|].
  - move => k0 PA0. asimpl. rewrite {2}/funcomp. asimpl.
    move : hτ => /[apply].
    by asimpl.
  - move => k0 PA0. asimpl. rewrite {2}/funcomp. asimpl.
    move => *. suff : PA0 = PA by congruence.
    move : h0. asimpl.
    eauto using InterpUniv_Functional'.
 Qed.
 Lemma morphing_SemWt : forall n Γ (a A : PTm n),
    Γ ⊨ a ∈ A -> forall m Δ (ρ : fin n -> PTm m),
      smorphing_ok Δ Γ ρ -> Δ ⊨ subst_PTm ρ a ∈ subst_PTm ρ A.
 Proof.
  move => n Γ a A ha m Δ ρ hρ τ hτ.
  have {}/hρ {}/ha := hτ.
  asimpl. eauto.
 Qed.
 Lemma morphing_SemWt_Univ : forall n Γ (a : PTm n) i,
    Γ ⊨ a ∈ PUniv i -> forall m Δ (ρ : fin n -> PTm m),
      smorphing_ok Δ Γ ρ -> Δ ⊨ subst_PTm ρ a ∈ PUniv i.
 Proof.
  move => n Γ a i ha.
  move => m Δ ρ.
  have -> : PUniv i = subst_PTm ρ (PUniv i) by reflexivity.
  by apply morphing_SemWt.
 Qed.
 Lemma weakening_Sem n Γ (a : PTm n) A B i
  (h0 : Γ ⊨ B ∈ PUniv i)
  (h1 : Γ ⊨ a ∈ A) :
@ -796,20 +683,15 @@ Proof.
 Qed.
 (* Semantic typing rules *)
 Lemma ST_Var' n Γ (i : fin n) j :
  Γ ⊨ Γ i ∈ PUniv j ->
  Γ ⊨ VarPTm i ∈ Γ i.
 Proof.
  move => /SemWt_Univ h.
  rewrite /SemWt => ρ /[dup] hρ {}/h [S hS].
  exists j,S.
  asimpl. firstorder.
 Qed.
 Lemma ST_Var n Γ (i : fin n) :
  ⊨ Γ ->
  Γ ⊨ VarPTm i ∈ Γ i.
-Proof. hauto l:on use:ST_Var' unfold:SemWff. Qed.
+Proof.
  move /(_ i) => [j /SemWt_Univ h].
  rewrite /SemWt => ρ /[dup] hρ {}/h [S hS].
  exists j, S.
  asimpl. firstorder.
 Qed.
 Lemma InterpUniv_Bind_nopf n p i (A : PTm n) B PA :
  ⟦ A ⟧ i ↘ PA ->
@ -1043,59 +925,6 @@ Proof.
  hauto l:on use:DJoin.transitive.
 Qed.
 Definition Γ_sub' {n} (Γ Δ : fin n -> PTm n) := forall ρ, ρ_ok Δ ρ -> ρ_ok Γ ρ.
 Definition Γ_eq' {n} (Γ Δ : fin n -> PTm n) := forall ρ, ρ_ok Δ ρ <-> ρ_ok Γ ρ.
 Lemma Γ_sub'_refl n (Γ : fin n -> PTm n) : Γ_sub' Γ Γ.
  rewrite /Γ_sub'. itauto. Qed.
 Lemma Γ_sub'_cons n (Γ Δ : fin n -> PTm n) A B i j :
  Sub.R B A ->
  Γ_sub' Γ Δ ->
  Γ ⊨ A ∈ PUniv i ->
  Δ ⊨ B ∈ PUniv j ->
  Γ_sub' (funcomp (ren_PTm shift) (scons A Γ)) (funcomp (ren_PTm shift) (scons B Δ)).
 Proof.
  move => hsub hsub' hA hB ρ hρ.
  move => k.
  move => k0 PA.
  have : ρ_ok Δ (funcomp ρ shift).
  move : hρ. clear.
  move => hρ i.
  specialize (hρ (shift i)).
  move => k PA. move /(_ k PA) in hρ.
  move : hρ. asimpl. by eauto.
  move => hρ_inv.
  destruct k as [k|].
  - rewrite /Γ_sub' in hsub'.
    asimpl.
    move /(_ (funcomp ρ shift) hρ_inv) in hsub'.
    sfirstorder simp+:asimpl.
  - asimpl.
    move => h.
    have {}/hsub' hρ' := hρ_inv.
    move /SemWt_Univ : (hA) (hρ')=> /[apply].
    move => [S]hS.
    move /SemWt_Univ : (hB) (hρ_inv)=>/[apply].
    move => [S1]hS1.
    move /(_ None) : hρ (hS1). asimpl => /[apply].
    suff : forall x, S1 x -> PA x by firstorder.
    apply : InterpUniv_Sub; eauto.
    by apply Sub.substing.
 Qed.
 Lemma Γ_sub'_SemWt n (Γ Δ : fin n -> PTm n) a A  :
  Γ_sub' Γ Δ ->
  Γ ⊨ a ∈ A ->
  Δ ⊨ a ∈ A.
 Proof.
  move => hs  ha ρ hρ.
  have {}/hs hρ' := hρ.
  hauto l:on.
 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 Δ ρ.
@ -1113,25 +942,6 @@ Proof.
  hauto l:on use: DJoin.substing.
 Qed.
 Lemma Γ_eq_sub n (Γ Δ : fin n -> PTm n) : Γ_eq' Γ Δ <-> Γ_sub' Γ Δ /\ Γ_sub' Δ Γ.
 Proof. rewrite /Γ_eq' /Γ_sub'. hauto l:on. Qed.
 Lemma Γ_eq'_cons n (Γ Δ : fin n -> PTm n) A B i j :
  DJoin.R B A ->
  Γ_eq' Γ Δ ->
  Γ ⊨ A ∈ PUniv i ->
  Δ ⊨ B ∈ PUniv j ->
  Γ_eq' (funcomp (ren_PTm shift) (scons A Γ)) (funcomp (ren_PTm shift) (scons B Δ)).
 Proof.
  move => h.
  have {h} [h0 h1] : Sub.R A B /\ Sub.R B A by hauto lq:on use:Sub.FromJoin, DJoin.symmetric.
  repeat rewrite ->Γ_eq_sub.
  hauto l:on use:Γ_sub'_cons.
 Qed.
 Lemma Γ_eq'_refl n (Γ : fin n -> PTm n) : Γ_eq' Γ Γ.
 Proof. rewrite /Γ_eq'. firstorder. 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 Δ ρ.
@ -1343,206 +1153,6 @@ Proof.
  hauto lq:on use: DJoin.cong,  DJoin.ProjCong.
 Qed.
 Lemma ST_Nat n Γ i :
  Γ ⊨ PNat : PTm n ∈ PUniv i.
 Proof.
  move => ?. apply SemWt_Univ. move => ρ hρ.
  eexists. by apply InterpUniv_Nat.
 Qed.
 Lemma ST_Zero n Γ :
  Γ ⊨ PZero : PTm n ∈ PNat.
 Proof.
  move => ρ hρ. exists 0, SNat. simpl. split.
  apply InterpUniv_Nat.
  apply S_Zero.
 Qed.
 Lemma ST_Suc n Γ (a : PTm n) :
  Γ ⊨ a ∈ PNat ->
  Γ ⊨ PSuc a ∈ PNat.
 Proof.
  move => ha ρ.
  move : ha => /[apply] /=.
  move => [k][PA][h0 h1].
  move /InterpUniv_Nat_inv : h0 => ?. subst.
  exists 0, SNat. split. apply InterpUniv_Nat.
  eauto using S_Suc.
 Qed.
 Lemma sn_unmorphing' n : (forall (a : PTm n) (s : SN a), forall m (ρ : fin m -> PTm n) b, a = subst_PTm ρ b -> SN b).
 Proof. hauto l:on use:sn_unmorphing. Qed.
 Lemma sn_bot_up n m (a : PTm (S n)) (ρ : fin n -> PTm m) :
  SN (subst_PTm (scons PBot ρ) a) -> SN (subst_PTm (up_PTm_PTm ρ) a).
  rewrite /up_PTm_PTm.
  move => h. eapply sn_unmorphing' with (ρ := (scons PBot VarPTm)); eauto.
  by asimpl.
 Qed.
 Lemma sn_bot_up2 n m (a : PTm (S (S n))) (ρ : fin n -> PTm m) :
  SN ((subst_PTm (scons PBot (scons PBot ρ)) a)) -> SN (subst_PTm (up_PTm_PTm (up_PTm_PTm ρ)) a).
  rewrite /up_PTm_PTm.
  move => h. eapply sn_unmorphing' with (ρ := (scons PBot (scons PBot VarPTm))); eauto.
  by asimpl.
 Qed.
 Lemma SNat_SN n (a : PTm n) : SNat a -> SN a.
  induction 1; hauto lq:on ctrs:SN. Qed.
 Lemma ST_Ind s Γ P (a : PTm s) b c i :
  funcomp (ren_PTm shift) (scons PNat Γ) ⊨ P ∈ PUniv i ->
  Γ ⊨ a ∈ PNat ->
  Γ ⊨ b ∈ subst_PTm (scons PZero VarPTm) P ->
  funcomp (ren_PTm shift)(scons P (funcomp (ren_PTm shift) (scons PNat Γ))) ⊨ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
  Γ ⊨ PInd P a b c ∈ subst_PTm (scons a VarPTm) P.
 Proof.
  move => hA hc ha hb ρ hρ.
  move /(_ ρ hρ) : ha => [m][PA][ha0]ha1.
  move /(_ ρ hρ) : hc => [n][PA0][/InterpUniv_Nat_inv ->].
  simpl.
  (* Use localiaztion to block asimpl from simplifying pind *)
  set x := PInd _ _ _ _. asimpl. subst x. move : {a} (subst_PTm ρ a) .
  move : (subst_PTm ρ b) ha1 => {}b ha1.
  move => u hu.
  have hρb : ρ_ok (funcomp (ren_PTm shift) (scons PNat Γ)) (scons PBot ρ) by apply : ρ_ok_cons; hauto lq:on ctrs:SNat, SNe use:(@InterpUniv_Nat 0).
  have hρbb : ρ_ok (funcomp (ren_PTm shift) (scons P (funcomp (ren_PTm shift) (scons PNat Γ)))) (scons PBot (scons PBot ρ)).
  move /SemWt_Univ /(_ _ hρb) : hA => [S ?].
  apply : ρ_ok_cons; eauto. sauto lq:on use:adequacy.
  (* have snP : SN P by hauto l:on use:SemWt_SN. *)
  have snb : SN b by hauto q:on use:adequacy.
  have snP : SN (subst_PTm (up_PTm_PTm ρ) P)
    by apply sn_bot_up; move : hA hρb => /[apply]; hauto lq:on use:adequacy.
  have snc : SN (subst_PTm (up_PTm_PTm (up_PTm_PTm ρ)) c)
    by apply sn_bot_up2; move : hb hρbb => /[apply]; hauto lq:on use:adequacy.
  elim : u /hu.
  + exists m, PA. split.
    * move : ha0. by asimpl.
    * apply : InterpUniv_back_clos; eauto.
      apply N_IndZero; eauto.
  + move => a snea.
    have hρ' : ρ_ok (funcomp (ren_PTm shift) (scons PNat Γ)) (scons a ρ)by
      apply : ρ_ok_cons; eauto using (InterpUniv_Nat 0); hauto ctrs:SNat.
    move /SemWt_Univ : (hA) hρ' => /[apply].
    move => [S0 hS0].
    exists i, S0. split=>//.
    eapply adequacy; eauto.
    apply N_Ind; eauto.
  + move => a ha [j][S][h0]h1.
    have hρ' : ρ_ok (funcomp (ren_PTm shift) (scons PNat Γ)) (scons (PSuc a) ρ)by
      apply : ρ_ok_cons; eauto using (InterpUniv_Nat 0); hauto ctrs:SNat.
    move /SemWt_Univ : (hA) (hρ') => /[apply].
    move => [S0 hS0].
    exists i, S0. split => //.
    apply : InterpUniv_back_clos; eauto.
    apply N_IndSuc; eauto using SNat_SN.
    move : (PInd (subst_PTm (up_PTm_PTm ρ) P) a b
              (subst_PTm (up_PTm_PTm (up_PTm_PTm ρ)) c))  h1.
    move => r hr.
    have hρ'' :  ρ_ok
                   (funcomp (ren_PTm shift) (scons P (funcomp (ren_PTm shift) (scons PNat Γ)))) (scons r (scons a ρ)) by
      eauto using ρ_ok_cons, (InterpUniv_Nat 0).
    move : hb hρ'' => /[apply].
    move => [k][PA1][h2]h3.
    move : h2. asimpl => ?.
    have ? : PA1 = S0 by  eauto using InterpUniv_Functional'.
    by subst.
  + move => a a' hr ha' [k][PA1][h0]h1.
    have : ρ_ok (funcomp (ren_PTm shift) (scons PNat Γ)) (scons a ρ)
      by apply : ρ_ok_cons; hauto l:on use:S_Red,(InterpUniv_Nat 0).
    move /SemWt_Univ : hA => /[apply]. move => [PA2]h2.
    exists i, PA2. split => //.
    apply : InterpUniv_back_clos; eauto.
    apply N_IndCong; eauto.
    suff : PA1 = PA2 by congruence.
    move : h0 h2. move : InterpUniv_Join'; repeat move/[apply]. apply.
    apply DJoin.FromRReds.
    apply RReds.FromRPar.
    apply RPar.morphing; last by apply RPar.refl.
    eapply LoReds.FromSN_mutual in hr.
    move /LoRed.ToRRed /RPar.FromRRed in hr.
    hauto lq:on inv:option use:RPar.refl.
 Qed.
 Lemma SE_SucCong n Γ (a b : PTm n) :
  Γ ⊨ a ≡ b ∈ PNat ->
  Γ ⊨ PSuc a ≡ PSuc b ∈ PNat.
 Proof.
  move /SemEq_SemWt => [ha][hb]he.
  apply SemWt_SemEq; eauto using ST_Suc.
  hauto q:on use:REReds.suc_inv, REReds.SucCong.
 Qed.
 Lemma SE_IndCong n Γ P0 P1 (a0 a1 : PTm n) b0 b1 c0 c1 i :
  funcomp (ren_PTm shift) (scons PNat Γ) ⊨ P0 ≡ P1 ∈ PUniv i ->
  Γ ⊨ a0 ≡ a1 ∈ PNat ->
  Γ ⊨ b0 ≡ b1 ∈ subst_PTm (scons PZero VarPTm) P0 ->
  funcomp (ren_PTm shift) (scons P0 (funcomp (ren_PTm shift) (scons PNat Γ))) ⊨ c0 ≡ c1 ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P0) ->
  Γ ⊨ PInd P0 a0 b0 c0 ≡ PInd P1 a1 b1 c1 ∈ subst_PTm (scons a0 VarPTm) P0.
 Proof.
  move /SemEq_SemWt=>[hP0][hP1]hPe.
  move /SemEq_SemWt=>[ha0][ha1]hae.
  move /SemEq_SemWt=>[hb0][hb1]hbe.
  move /SemEq_SemWt=>[hc0][hc1]hce.
  apply SemWt_SemEq; eauto using ST_Ind, DJoin.IndCong.
  apply ST_Conv_E with (A := subst_PTm (scons a1 VarPTm) P1) (i := i);
    last by eauto using DJoin.cong', DJoin.symmetric.
  apply : ST_Ind; eauto. eapply ST_Conv_E with (i := i); eauto.
  apply : morphing_SemWt_Univ; eauto.
  apply smorphing_ext. rewrite /smorphing_ok.
  move => ξ. rewrite /funcomp. by asimpl.
  by apply ST_Zero.
  by apply DJoin.substing.
  eapply ST_Conv_E with (i := i); eauto.
  apply : Γ_sub'_SemWt; eauto.
  apply : Γ_sub'_cons; eauto using DJoin.symmetric, Sub.FromJoin.
  apply : Γ_sub'_cons; eauto using Sub.refl, Γ_sub'_refl, (@ST_Nat _ _ 0).
  change (PUniv i) with (ren_PTm shift (@PUniv (S n) i)).
  apply : weakening_Sem; eauto. move : hP1.
  move /morphing_SemWt. apply. apply smorphing_ext.
  have -> : (funcomp VarPTm shift) = funcomp (ren_PTm shift) (@VarPTm n) by asimpl.
  apply : smorphing_ren; eauto using smorphing_ok_refl. hauto l:on inv:option.
  apply ST_Suc. apply ST_Var' with (j := 0). apply ST_Nat.
  apply DJoin.renaming. by apply DJoin.substing.
  apply : morphing_SemWt_Univ; eauto.
  apply smorphing_ext; eauto using smorphing_ok_refl.
 Qed.
 Lemma SE_IndZero n Γ P i (b : PTm n) c :
  funcomp (ren_PTm shift) (scons PNat Γ) ⊨ P ∈ PUniv i ->
  Γ ⊨ b ∈ subst_PTm (scons PZero VarPTm) P ->
  funcomp (ren_PTm shift)(scons P (funcomp (ren_PTm shift) (scons PNat Γ))) ⊨ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
  Γ ⊨ PInd P PZero b c ≡ b ∈ subst_PTm (scons PZero VarPTm) P.
 Proof.
  move => hP hb hc.
  apply SemWt_SemEq; eauto using ST_Zero, ST_Ind.
  apply DJoin.FromRRed0. apply RRed.IndZero.
 Qed.
 Lemma SE_IndSuc s Γ P (a : PTm s) b c i :
  funcomp (ren_PTm shift) (scons PNat Γ) ⊨ P ∈ PUniv i ->
  Γ ⊨ a ∈ PNat ->
  Γ ⊨ b ∈ subst_PTm (scons PZero VarPTm) P ->
  funcomp (ren_PTm shift)(scons P (funcomp (ren_PTm shift) (scons PNat Γ))) ⊨ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
  Γ ⊨ PInd P (PSuc a) b c ≡ (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c) ∈ subst_PTm (scons (PSuc a) VarPTm) P.
 Proof.
  move => hP ha hb hc.
  apply SemWt_SemEq; eauto using ST_Suc, ST_Ind.
  set Δ := (X in X ⊨ _ ∈ _) in hc.
  have : smorphing_ok Γ Δ (scons (PInd P a b c) (scons a VarPTm)).
  apply smorphing_ext. apply smorphing_ext. apply smorphing_ok_refl.
  done. eauto using ST_Ind.
  move : morphing_SemWt hc; repeat move/[apply].
  by asimpl.
  apply DJoin.FromRRed0.
  apply RRed.IndSuc.
 Qed.
 Lemma SE_ProjPair1 n Γ (a b : PTm n) A B i :
  Γ ⊨ PBind PSig A B ∈ (PUniv i) ->
  Γ ⊨ a ∈ A ->
@ -1578,15 +1188,6 @@ Proof.
  rewrite /DJoin.R. hauto lq:on ctrs:rtc,RERed.R.
 Qed.
 Lemma SE_Nat n Γ (a b : PTm n) :
  Γ ⊨ a ≡ b ∈ PNat ->
  Γ ⊨ PSuc a ≡ PSuc b ∈ PNat.
 Proof.
  move /SemEq_SemWt => [ha][hb]hE.
  apply SemWt_SemEq; eauto using ST_Suc.
  eauto using DJoin.SucCong.
 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 ->
@ -1731,4 +1332,4 @@ 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 ST_Nat ST_Ind ST_Suc ST_Zero SE_IndCong SE_SucCong SE_IndZero SE_IndSuc SE_SucCong : sem.
+  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.
--- a/theories/preservation.v
+++ b/theories/preservation.v
@ -76,23 +76,6 @@ Proof.
  - hauto lq:on rew:off ctrs:LEq.
 Qed.
 Lemma Ind_Inv n Γ P (a : PTm n) b c U :
  Γ ⊢ PInd P a b c ∈ U ->
  exists i, funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P ∈ PUniv i /\
       Γ ⊢ a ∈ PNat /\
       Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P /\
      funcomp (ren_PTm shift)(scons P (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) /\
       Γ ⊢ subst_PTm (scons a VarPTm) P ≲ U.
 Proof.
  move E : (PInd P a b c)=> u hu.
  move : P a b c E. elim : n Γ u U / hu => n //=.
  - move => Γ P a b c i hP _ ha _ hb _ hc _ P0 a0 b0 c0 [*]. subst.
    exists i. repeat split => //=.
    have : Γ ⊢ subst_PTm (scons a VarPTm) P ∈ subst_PTm (scons a VarPTm) (PUniv i) by hauto l:on use:substing_wt.
    eauto using E_Refl, Su_Eq.
  - 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.
@ -125,19 +108,6 @@ Proof.
  apply : E_ProjPair1; eauto.
 Qed.
 Lemma Suc_Inv n Γ (a : PTm n) A :
  Γ ⊢ PSuc a ∈ A -> Γ ⊢ a ∈ PNat /\ Γ ⊢ PNat ≲ A.
 Proof.
  move E : (PSuc a) => u hu.
  move : a E.
  elim : n Γ u A /hu => //=.
  - move => n Γ a ha iha a0 [*]. subst.
    split => //=. eapply wff_mutual in ha.
    apply : Su_Eq.
    apply E_Refl. by apply T_Nat'.
  - hauto lq:on rew:off ctrs:LEq.
 Qed.
 Lemma RRed_Eq n Γ (a b : PTm n) A :
  Γ ⊢ a ∈ A ->
  RRed.R a b ->
@ -160,13 +130,6 @@ Proof.
      move : hA0 => /[swap]. move : Su_Transitive. repeat move/[apply].
      move {hS}.
      move => ?. apply : E_Conv; eauto. apply : E_ProjPair2; eauto.
  - hauto lq:on use:Ind_Inv, E_Conv, E_IndZero.
  - move => P a b c Γ A.
    move /Ind_Inv.
    move => [i][hP][ha][hb][hc]hSu.
    apply : E_Conv; eauto.
    apply : E_IndSuc'; eauto.
    hauto l:on use:Suc_Inv.
  - 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.
@ -207,11 +170,6 @@ Proof.
    have {}/ihA ihA := h1.
    apply : E_Conv; eauto.
    apply E_Bind'; eauto using E_Refl.
  - hauto lq:on rew:off use:Ind_Inv, E_Conv, E_IndCong db:wt.
  - hauto lq:on rew:off use:Ind_Inv, E_Conv, E_IndCong db:wt.
  - hauto lq:on rew:off use:Ind_Inv, E_Conv, E_IndCong db:wt.
  - hauto lq:on rew:off use:Ind_Inv, E_Conv, E_IndCong db:wt.
  - hauto lq:on use:Suc_Inv, E_Conv, E_SucCong.
 Qed.
 Theorem subject_reduction n Γ (a b A : PTm n) :
--- a/theories/structural.v
+++ b/theories/structural.v
@ -12,11 +12,6 @@ Proof. apply wt_mutual; eauto. Qed.
 #[export]Hint Constructors Wt Wff Eq : wt.
 Lemma T_Nat' n Γ :
  ⊢ Γ ->
  Γ ⊢ PNat : PTm n ∈ PUniv 0.
 Proof. apply T_Nat. Qed.
 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 ξ) .
@ -50,10 +45,7 @@ Proof.
  move E :(PBind p A B) => T h.
  move : p A B E.
  elim : n Γ T U / h => //=.
-  - move => n Γ i p A B hA _ hB _ p0 A0 B0 [*]. subst.
+  - hauto lq:on ctrs:Wt,LEq,Eq use:Wt_Univ.
    exists i. repeat split => //=.
    eapply wff_mutual in hA.
    apply Su_Univ; eauto.
  - hauto lq:on rew:off ctrs:LEq.
 Qed.
@ -100,25 +92,6 @@ Proof.
  move => ->. eauto using T_Pair.
 Qed.
 Lemma E_IndCong' n Γ P0 P1 (a0 a1 : PTm n) b0 b1 c0 c1 i U :
  U = subst_PTm (scons a0 VarPTm) P0 ->
  funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P0 ∈ PUniv i ->
  funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P0 ≡ P1 ∈ PUniv i ->
  Γ ⊢ a0 ≡ a1 ∈ PNat ->
  Γ ⊢ b0 ≡ b1 ∈ subst_PTm (scons PZero VarPTm) P0 ->
  funcomp (ren_PTm shift) (scons P0 (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c0 ≡ c1 ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P0) ->
  Γ ⊢ PInd P0 a0 b0 c0 ≡ PInd P1 a1 b1 c1 ∈ U.
 Proof. move => ->. apply E_IndCong. Qed.
 Lemma T_Ind' s Γ P (a : PTm s) b c i U :
  U = subst_PTm (scons a VarPTm) P ->
  funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P ∈ PUniv i ->
  Γ ⊢ a ∈ PNat ->
  Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P ->
  funcomp (ren_PTm shift)(scons P (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
  Γ ⊢ PInd P a b c ∈ U.
 Proof. move =>->. apply T_Ind. 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 ->
@ -130,7 +103,9 @@ Lemma E_Proj2' n Γ i (a b : PTm n) A B U :
  Γ ⊢ 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.
+Proof.
  move => ->. apply E_Proj2.
 Qed.
 Lemma E_Bind' n Γ i p (A0 A1 : PTm n) B0 B1 :
  Γ ⊢ A0 ∈ PUniv i ->
@ -187,30 +162,6 @@ Lemma Su_Sig_Proj2' n Γ (a0 a1 A0 A1 : PTm n) B0 B1 U T :
  Γ ⊢ U ≲ T.
 Proof. move => -> ->. apply Su_Sig_Proj2. Qed.
 Lemma E_IndZero' n Γ P i (b : PTm n) c U :
  U = subst_PTm (scons PZero VarPTm) P ->
  funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P ∈ PUniv i ->
  Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P ->
  funcomp (ren_PTm shift)(scons P (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
  Γ ⊢ PInd P PZero b c ≡ b ∈ U.
 Proof. move => ->. apply E_IndZero. 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 E_IndSuc' s Γ P (a : PTm s) b c i u U :
  u = subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c ->
  U = subst_PTm (scons (PSuc a) VarPTm) P ->
  funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P ∈ PUniv i ->
  Γ ⊢ a ∈ PNat ->
  Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P ->
  funcomp (ren_PTm shift)(scons P (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
  Γ ⊢ PInd P (PSuc a) b c ≡ u ∈ U.
 Proof. move => ->->. apply E_IndSuc. 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 Δ Γ ξ ->
@ -233,22 +184,6 @@ Proof.
  - 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.
  - move => s Γ P a b c i hP ihP ha iha hb ihb hc ihc m Δ ξ hΔ hξ.
    move => [:hP].
    apply : T_Ind'; eauto. by asimpl.
    abstract :hP. apply ihP. by eauto using Wff_Cons', T_Nat'.
    hauto l:on use:renaming_up.
    set x := subst_PTm _ _. have -> : x = ren_PTm ξ (subst_PTm (scons PZero VarPTm) P) by subst x; asimpl.
    by subst x; eauto.
    set Ξ := funcomp _ _.
    have  hΞ : ⊢ Ξ. subst Ξ.
    apply : Wff_Cons'; eauto. apply hP.
    move /(_ _ Ξ (upRen_PTm_PTm (upRen_PTm_PTm ξ)) hΞ) : ihc.
    set Ξ' := (funcomp _ _ : fin (S (S _)) -> _) .
    have : renaming_ok Ξ Ξ' (upRen_PTm_PTm (upRen_PTm_PTm ξ)).
    by do 2 apply renaming_up.
    move /[swap] /[apply].
    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.
@ -264,27 +199,6 @@ Proof.
    move : ihb hΔ hξ. repeat move/[apply].
    by asimpl.
  - move => *. apply : E_Proj2'; eauto. by asimpl.
  - move => n Γ P0 P1 a0 a1 b0 b1 c0 c1 i hP0 ihP0 hP ihP ha iha hb ihb hc ihc.
    move => m Δ ξ hΔ hξ [:hP'].
    apply E_IndCong' with (i := i).
    by asimpl.
    abstract : hP'.
    qauto l:on use:renaming_up, Wff_Cons', T_Nat'.
    qauto l:on use:renaming_up, Wff_Cons', T_Nat'.
    by eauto with wt.
    move : ihb (hΔ) (hξ); do! move/[apply]. by asimpl.
    set Ξ := funcomp _ _.
    have hΞ : ⊢ Ξ.
    subst Ξ. apply :Wff_Cons'; eauto. apply hP'.
    move /(_ _ Ξ  (upRen_PTm_PTm (upRen_PTm_PTm ξ)) hΞ) : ihc.
    move /(_ ltac:(qauto l:on use:renaming_up)).
    suff : ren_PTm (upRen_PTm_PTm (upRen_PTm_PTm ξ))
      (ren_PTm shift
         (subst_PTm
            (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift)) P0)) = ren_PTm shift
      (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift))
         (ren_PTm (upRen_PTm_PTm ξ) P0)) by scongruence.
    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].
@ -302,32 +216,6 @@ Proof.
  - 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 => n Γ P i b c hP ihP hb ihb hc ihc m Δ ξ hΔ hξ.
    apply E_IndZero' with (i := i); eauto. by asimpl.
    qauto l:on use:Wff_Cons', T_Nat', renaming_up.
    move  /(_ m Δ ξ hΔ) : ihb.
    asimpl. by apply.
    set Ξ := funcomp _ _.
    have hΞ : ⊢ Ξ by  qauto l:on use:Wff_Cons', T_Nat', renaming_up.
    move /(_ _ Ξ  (upRen_PTm_PTm (upRen_PTm_PTm ξ)) hΞ) : ihc.
    move /(_ ltac:(qauto l:on use:renaming_up)).
    suff : ren_PTm (upRen_PTm_PTm (upRen_PTm_PTm ξ))
      (ren_PTm shift
         (subst_PTm
            (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift)) P))= ren_PTm shift
      (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift))
         (ren_PTm (upRen_PTm_PTm ξ) P)) by scongruence.
    by asimpl.
  - move => n Γ P a b c i hP ihP ha iha hb ihb hc ihc m Δ ξ hΔ hξ.
    apply E_IndSuc' with (i := i). by asimpl. by asimpl.
    qauto l:on use:Wff_Cons', T_Nat', renaming_up.
    by eauto with wt.
    move  /(_ m Δ ξ hΔ) : ihb. asimpl. by apply.
    set Ξ := funcomp _ _.
    have hΞ : ⊢ Ξ by  qauto l:on use:Wff_Cons', T_Nat', renaming_up.
    move /(_ _ Ξ  (upRen_PTm_PTm (upRen_PTm_PTm ξ)) hΞ) : ihc.
    move /(_ ltac:(qauto l:on use:renaming_up)).
    by asimpl.
  - move => *.
    apply : E_AppEta'; eauto. by asimpl.
  - qauto l:on use:E_PairEta.
@ -384,6 +272,10 @@ Lemma renaming_wt' : forall n m Δ Γ a A (ξ : fin n -> fin m) u U,
    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 ->
@ -399,6 +291,12 @@ Proof.
  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 ->
@ -444,32 +342,6 @@ Proof.
  - move => *. apply : T_Proj2'; eauto. by asimpl.
  - hauto lq:on ctrs:Wt,LEq.
  - qauto l:on ctrs:Wt.
  - qauto l:on ctrs:Wt.
  - qauto l:on ctrs:Wt.
  - move => s Γ P a b c i hP ihP ha iha hb ihb hc ihc m Δ ξ hΔ hξ.
    have  hξ' : morphing_ok (funcomp (ren_PTm shift) (scons PNat Δ))
    (funcomp (ren_PTm shift) (scons PNat Γ)) (up_PTm_PTm ξ).
    move /morphing_up : hξ.  move /(_ PNat 0).
    apply. by apply T_Nat.
    move => [:hP].
    apply : T_Ind'; eauto. by asimpl.
    abstract :hP. apply ihP. by eauto using Wff_Cons', T_Nat'.
    move /morphing_up : hξ.  move /(_ PNat 0).
    apply. by apply T_Nat.
    move : ihb hξ hΔ; do!move/[apply]. by asimpl.
    set Ξ := funcomp _ _.
    have  hΞ : ⊢ Ξ. subst Ξ.
    apply : Wff_Cons'; eauto. apply hP.
    move /(_ _ Ξ (up_PTm_PTm (up_PTm_PTm ξ)) hΞ) : ihc.
    set Ξ' := (funcomp _ _ : fin (S (S _)) -> _) .
    have : morphing_ok Ξ Ξ' (up_PTm_PTm (up_PTm_PTm ξ)).
    eapply morphing_up; eauto. apply hP.
    move /[swap]/[apply].
    set x := (x in _ ⊢ _ ∈ x).
    set y := (y in _ -> _ ⊢ _ ∈ y).
    suff : x = y by scongruence.
    subst x y. asimpl. substify. by asimpl.
  - qauto l:on ctrs:Wt.
  - hauto lq:on ctrs:Eq.
  - hauto lq:on ctrs:Eq.
  - hauto lq:on ctrs:Eq.
@ -487,27 +359,6 @@ Proof.
    by asimpl.
  - hauto q:on ctrs:Eq.
  - move => *. apply : E_Proj2'; eauto. by asimpl.
  - move => n Γ P0 P1 a0 a1 b0 b1 c0 c1 i hP0 ihP0 hP ihP ha iha hb ihb hc ihc.
    move => m Δ ξ hΔ hξ.
    have  hξ' : morphing_ok (funcomp (ren_PTm shift) (scons PNat Δ))
                  (funcomp (ren_PTm shift) (scons PNat Γ)) (up_PTm_PTm ξ).
    move /morphing_up : hξ.  move /(_ PNat 0).
    apply. by apply T_Nat.
    move => [:hP'].
    apply E_IndCong' with (i := i).
    by asimpl.
    abstract : hP'.
    qauto l:on use:morphing_up, Wff_Cons', T_Nat'.
    qauto l:on use:renaming_up, Wff_Cons', T_Nat'.
    by eauto with wt.
    move : ihb (hΔ) (hξ); do! move/[apply]. by asimpl.
    set Ξ := funcomp _ _.
    have hΞ : ⊢ Ξ.
    subst Ξ. apply :Wff_Cons'; eauto. apply hP'.
    move /(_ _ Ξ  (up_PTm_PTm (up_PTm_PTm ξ)) hΞ) : ihc.
    move /(_ ltac:(qauto l:on use:morphing_up)).
    asimpl. substify. by asimpl.
  - eauto with wt.
  - 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].
@ -525,34 +376,6 @@ Proof.
  - 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 => n Γ P i b c hP ihP hb ihb hc ihc m Δ ξ hΔ hξ.
    have  hξ' : morphing_ok (funcomp (ren_PTm shift) (scons PNat Δ))
                  (funcomp (ren_PTm shift) (scons PNat Γ)) (up_PTm_PTm ξ).
    move /morphing_up : hξ.  move /(_ PNat 0).
    apply. by apply T_Nat.
    apply E_IndZero' with (i := i); eauto. by asimpl.
    qauto l:on use:Wff_Cons', T_Nat', renaming_up.
    move  /(_ m Δ ξ hΔ) : ihb.
    asimpl. by apply.
    set Ξ := funcomp _ _.
    have hΞ : ⊢ Ξ by  qauto l:on use:Wff_Cons', T_Nat', renaming_up.
    move /(_ _ Ξ  (up_PTm_PTm (up_PTm_PTm ξ)) hΞ) : ihc.
    move /(_ ltac:(sauto lq:on use:morphing_up)).
    asimpl. substify. by asimpl.
  - move => n Γ P a b c i hP ihP ha iha hb ihb hc ihc m Δ ξ hΔ hξ.
    have  hξ' : morphing_ok (funcomp (ren_PTm shift) (scons PNat Δ))
                  (funcomp (ren_PTm shift) (scons PNat Γ)) (up_PTm_PTm ξ).
    move /morphing_up : hξ.  move /(_ PNat 0).
    apply. by apply T_Nat'.
    apply E_IndSuc' with (i := i). by asimpl. by asimpl.
    qauto l:on use:Wff_Cons', T_Nat', renaming_up.
    by eauto with wt.
    move  /(_ m Δ ξ hΔ) : ihb. asimpl. by apply.
    set Ξ := funcomp _ _.
    have hΞ : ⊢ Ξ by  qauto l:on use:Wff_Cons', T_Nat', renaming_up.
    move /(_ _ Ξ  (up_PTm_PTm (up_PTm_PTm ξ)) hΞ) : ihc.
    move /(_ ltac:(sauto l:on use:morphing_up)).
    asimpl. substify. by asimpl.
  - move => *.
    apply : E_AppEta'; eauto. by asimpl.
  - qauto l:on use:E_PairEta.
@ -682,8 +505,6 @@ Proof.
    exists j. have : Γ ⊢ PProj PL a ∈ A by qauto use:T_Proj1.
    move : substing_wt h1; repeat move/[apply].
    by asimpl.
  - move => s Γ P a b c i + ? + *. clear. move => h ha. exists i.
    hauto lq:on use:substing_wt.
  - sfirstorder.
  - sfirstorder.
  - sfirstorder.
@ -714,46 +535,9 @@ Proof.
    eauto using bind_inst.
    move /T_Proj1 in iha.
    hauto lq:on ctrs:Wt,Eq,LEq use:Bind_Inv, substing_wt.
  - move => n Γ P0 P1 a0 a1 b0 b1 c0 c1 i _ _ hPE [hP0 [hP1 _]] hae [ha0 [ha1 _]] _ [hb0 [hb1 hb2]] _ [hc0 [hc1 hc2]].
    have wfΓ : ⊢ Γ by hauto use:wff_mutual.
    repeat split. by eauto using T_Ind.
    apply : T_Conv. apply : T_Ind; eauto.
    apply : T_Conv; eauto.
    eapply morphing; by eauto using Su_Eq, morphing_ext, morphing_id with wt.
    apply : T_Conv.  apply : ctx_eq_subst_one; eauto.
    by eauto using Su_Eq, E_Symmetric.
    eapply renaming; eauto.
    eapply morphing; eauto 20 using Su_Eq, morphing_ext, morphing_id with wt.
    apply morphing_ext; eauto.
    replace (funcomp VarPTm shift) with (funcomp (@ren_PTm n _ shift) VarPTm); last by asimpl.
    apply : morphing_ren; eauto using Wff_Cons' with wt.
    apply : renaming_shift; eauto. by apply morphing_id.
    apply T_Suc. apply T_Var'. by asimpl. apply : Wff_Cons'; eauto using T_Nat'.
    apply : Wff_Cons'; eauto. apply : renaming_shift; eauto.
    have /E_Symmetric /Su_Eq : Γ ⊢ PBind PSig PNat P0 ≡ PBind PSig PNat P1 ∈ PUniv i by eauto with wt.
    move /E_Symmetric in hae.
    by eauto using Su_Sig_Proj2.
    sauto lq:on use:substing_wt.
  - hauto lq:on ctrs:Wt.
  - hauto lq:on ctrs:Wt.
  - hauto q:on use:substing_wt db:wt.
  - hauto l:on use:bind_inst db:wt.
  - move => n Γ P i b c hP _ hb _ hc _.
    have ? : ⊢ Γ by hauto use:wff_mutual.
    repeat split=>//.
    by eauto with wt.
    sauto lq:on use:substing_wt.
  - move => s Γ P a b c i hP _ ha _ hb _ hc _.
    have ? : ⊢ Γ by hauto use:wff_mutual.
    repeat split=>//.
    apply : T_Ind; eauto with wt.
    set Ξ : fin (S (S _)) -> _ := (X in X ⊢ _ ∈ _) in hc.
    have : morphing_ok Γ Ξ (scons (PInd P a b c) (scons a VarPTm)).
    apply morphing_ext. apply morphing_ext. by apply morphing_id.
    by eauto. by eauto with wt.
    subst Ξ.
    move : morphing_wt hc; repeat move/[apply]. asimpl. by apply.
    sauto lq:on use:substing_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)
@ -819,7 +603,6 @@ Proof.
    + apply Cumulativity with (i := i1); eauto.
      have : Γ ⊢ a1 ∈ A1 by eauto using T_Conv.
      move : substing_wt ih1';repeat move/[apply]. by asimpl.
      Unshelve. all: exact 0.
 Qed.
 Lemma Var_Inv n Γ (i : fin n) A :
--- a/theories/typing.v
+++ b/theories/typing.v
@ -42,25 +42,6 @@ Inductive Wt : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> Prop :=
  ⊢ Γ ->
  Γ ⊢ PUniv i : PTm n ∈ PUniv (S i)
 | T_Nat n Γ i :
  ⊢ Γ ->
  Γ ⊢ PNat : PTm n ∈ PUniv i
 | T_Zero n Γ :
  ⊢ Γ ->
  Γ ⊢ PZero : PTm n ∈ PNat
 | T_Suc n Γ (a : PTm n) :
  Γ ⊢ a ∈ PNat ->
  Γ ⊢ PSuc a ∈ PNat
 | T_Ind s Γ P (a : PTm s) b c i :
  funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P ∈ PUniv i ->
  Γ ⊢ a ∈ PNat ->
  Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P ->
  funcomp (ren_PTm shift)(scons P (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
  Γ ⊢ PInd P a b c ∈ subst_PTm (scons a VarPTm) P
 | T_Conv n Γ (a : PTm n) A B :
  Γ ⊢ a ∈ A ->
  Γ ⊢ A ≲ B ->
@ -115,18 +96,6 @@ with Eq : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> PTm n -> Prop :=
  Γ ⊢ a ≡ b ∈ PBind PSig A B ->
  Γ ⊢ PProj PR a ≡ PProj PR b ∈ subst_PTm (scons (PProj PL a) VarPTm) B
 | E_IndCong n Γ P0 P1 (a0 a1 : PTm n) b0 b1 c0 c1 i :
  funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P0 ∈ PUniv i ->
  funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P0 ≡ P1 ∈ PUniv i ->
  Γ ⊢ a0 ≡ a1 ∈ PNat ->
  Γ ⊢ b0 ≡ b1 ∈ subst_PTm (scons PZero VarPTm) P0 ->
  funcomp (ren_PTm shift) (scons P0 (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c0 ≡ c1 ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P0) ->
  Γ ⊢ PInd P0 a0 b0 c0 ≡ PInd P1 a1 b1 c1 ∈ subst_PTm (scons a0 VarPTm) P0
 | E_SucCong n Γ (a b : PTm n) :
  Γ ⊢ a ≡ b ∈ PNat ->
  Γ ⊢ PSuc a ≡ PSuc b ∈ PNat
 | E_Conv n Γ (a b : PTm n) A B :
  Γ ⊢ a ≡ b ∈ A ->
  Γ ⊢ A ≲ B ->
@ -151,19 +120,6 @@ with Eq : forall {n}, (fin n -> PTm n) -> PTm n -> PTm n -> PTm n -> Prop :=
  Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B ->
  Γ ⊢ PProj PR (PPair a b) ≡ b ∈ subst_PTm (scons a VarPTm) B
 | E_IndZero n Γ P i (b : PTm n) c :
  funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P ∈ PUniv i ->
  Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P ->
  funcomp (ren_PTm shift)(scons P (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
  Γ ⊢ PInd P PZero b c ≡ b ∈ subst_PTm (scons PZero VarPTm) P
 | E_IndSuc s Γ P (a : PTm s) b c i :
  funcomp (ren_PTm shift) (scons PNat Γ) ⊢ P ∈ PUniv i ->
  Γ ⊢ a ∈ PNat ->
  Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P ->
  funcomp (ren_PTm shift)(scons P (funcomp (ren_PTm shift) (scons PNat Γ))) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) ->
  Γ ⊢ PInd P (PSuc a) b c ≡ (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c) ∈ subst_PTm (scons (PSuc a) VarPTm) P
 (* Eta *)
 | E_AppEta n Γ (b : PTm n) A B i :
  ⊢ Γ ->