diff --git a/syntax.sig b/syntax.sig
index a50911e..6b7e4df 100644
--- 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
-PNat : PTm
-PZero : PTm
-PSuc : PTm -> PTm
-PInd : (bind PTm in PTm) -> PTm -> PTm -> (bind PTm,PTm in PTm) -> PTm
\ No newline at end of file
+PBot : PTm
\ No newline at end of file
diff --git a/theories/Autosubst2/syntax.v b/theories/Autosubst2/syntax.v
index 5d04c05..ff9ec18 100644
--- 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
-  | 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.
+  | PBot : 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.
 
diff --git a/theories/algorithmic.v b/theories/algorithmic.v
index 096ec94..6fe5fad 100644
--- 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)
-  | IndCong P a0 a1 b c :
-    R a0 a1 ->
-    R (PInd P a0 b c) (PInd P a1 b c).
+    R (PProj p a0) (PProj p a1).
 
   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.
-      * move /DJoin.var_inj => ?. subst. qauto l:on use:Var_Inv, T_Var,CE_VarCong.
-      * clear => ? ? _. exfalso.
+    + case : b => //=.
+      move => i j hi _ _.
+      * 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.
-        hauto q:on use:REReds.var_inv, REReds.hne_ind_inv.
-    + case : b => //=;
-                   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.
+    + case : b => //=.
+      * clear. move => i a a0 /algo_metric_join h _ ?. exfalso.
+        hauto l:on 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}.
diff --git a/theories/common.v b/theories/common.v
index 282038d..24e708e 100644
--- 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.
-Qed.
+  move : m ξ b.
+  elim : n / a => //; try solve_anti_ren.
 
-Inductive HF : Set :=
-| H_Pair | H_Abs | H_Univ | H_Bind (p : BTag) | H_Nat | H_Suc | H_Zero | H_Bot.
+  move => n a iha m ξ []//=.
+  move => u hξ [h].
+  apply iha in h. by subst.
+  destruct i, j=>//=.
+  hauto l:on.
+
+  move => n p A ihA B ihB m ξ []//=.
+  move => b A0 B0  hξ [?]. subst.
+  move => ?. have ? : A0 = A by firstorder. subst.
+  move => ?. have : B = B0. apply : ihB; eauto.
+  sauto.
+  congruence.
+Qed.
 
 Definition ishf {n} (a : PTm n) :=
   match a with
@@ -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.
diff --git a/theories/executable.v b/theories/executable.v
deleted file mode 100644
index f773fa6..0000000
--- a/theories/executable.v
+++ /dev/null
@@ -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).
diff --git a/theories/fp_red.v b/theories/fp_red.v
index bffe1a7..e89c191 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -55,22 +55,7 @@ Module EPar.
     R B0 B1 ->
     R (PBind p A0 B0) (PBind p A1 B1)
   | BotCong :
-    R PBot PBot
-  | NatCong :
-    R PNat PNat
-  | IndCong P0 P1 a0 a1 b0 b1 c0 c1 :
-    R P0 P1 ->
-    R a0 a1 ->
-    R b0 b1 ->
-    R c0 c1 ->
-    (* ----------------------- *)
-    R (PInd P0 a0 b0 c0) (PInd P1 a1 b1 c1)
-  | ZeroCong :
-    R PZero PZero
-  | SucCong a0 a1 :
-    R a0 a1 ->
-    (* ------------ *)
-    R (PSuc a0) (PSuc a1).
+    R PBot PBot.
 
   Lemma refl n (a : PTm n) : R a a.
   Proof.
@@ -91,10 +76,9 @@ Module EPar.
     move => h. move : m ξ.
     elim : n a b /h.
 
-    all : try qauto ctrs:R.
-
     move => n a0 a1 ha iha m ξ /=.
     eapply AppEta'; eauto. by asimpl.
+    all : qauto ctrs:R.
   Qed.
 
   Lemma morphing_ren n m p (ρ0 ρ1 : fin n -> PTm m) (ξ : fin m -> fin p) :
@@ -141,12 +125,6 @@ Inductive SNe {n} : PTm n -> Prop :=
   SNe (PProj p a)
 | N_Bot :
   SNe PBot
-| N_Ind P a b c :
-  SN P ->
-  SNe a ->
-  SN b ->
-  SN c ->
-  SNe (PInd P a b c)
 with SN  {n} : PTm n -> Prop :=
 | N_Pair a b :
   SN a ->
@@ -168,13 +146,6 @@ with SN  {n} : PTm n -> Prop :=
   SN (PBind p A B)
 | N_Univ i :
   SN (PUniv i)
-| N_Nat :
-  SN PNat
-| N_Zero :
-  SN PZero
-| N_Suc a :
-  SN a ->
-  SN (PSuc a)
 with TRedSN {n} : PTm n -> PTm n -> Prop :=
 | N_β a b :
   SN b ->
@@ -191,32 +162,10 @@ with TRedSN {n} : PTm n -> PTm n -> Prop :=
   TRedSN (PProj PR (PPair a b)) b
 | N_ProjCong p a b :
   TRedSN a b ->
-  TRedSN (PProj p a) (PProj p b)
-| N_IndZero P b c :
-  SN P ->
-  SN b ->
-  SN c ->
-  TRedSN (PInd P PZero b c) b
-| N_IndSuc P a b c :
-  SN P ->
-  SN a ->
-  SN b ->
-  SN c ->
-  TRedSN (PInd P (PSuc a) b c) (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c)
-| N_IndCong P a0 a1 b c :
-  SN P ->
-  SN b ->
-  SN c ->
-  TRedSN a0 a1 ->
-  TRedSN (PInd P a0 b c) (PInd P a1 b c).
+  TRedSN (PProj p a) (PProj p b).
 
 Derive Dependent Inversion tred_inv with (forall n (a b : PTm n), TRedSN a b) Sort Prop.
 
-Inductive SNat {n} : PTm n -> Prop :=
-| S_Zero : SNat PZero
-| S_Neu a : SNe a -> SNat a
-| S_Suc a : SNat a -> SNat (PSuc a)
-| S_Red a b : TRedSN a b -> SNat b -> SNat a.
 
 Lemma PProj_imp n p a :
   @ishf n a ->
@@ -230,7 +179,7 @@ Proof.
   hauto lq:on inv:TRedSN.
 Qed.
 
-Lemma PApp_imp n a b :
+Lemma PAbs_imp n a b :
   @ishf n a ->
   ~~ isabs a ->
   ~ SN (PApp a b).
@@ -241,35 +190,34 @@ Proof.
   hauto lq:on inv:TRedSN.
 Qed.
 
-Lemma PInd_imp n P (a : PTm n) b c :
-  ishf a ->
-  ~~ iszero a ->
-  ~~ issuc a ->
-  ~ SN (PInd P a b c).
-Proof.
-  move => + + + h. move E : (PInd P a b c) h => u h.
-  move : P a b c E.
-  elim : n u /h => //=.
-  hauto lq:on inv:SNe,PTm.
-  hauto lq:on inv:TRedSN.
-Qed.
-
 Lemma PProjAbs_imp n p (a : PTm (S n)) :
   ~ SN (PProj p (PAbs a)).
 Proof.
-  sfirstorder use:PProj_imp.
+  move E : (PProj p (PAbs a)) => u hu.
+  move : p a E.
+  elim : n u / hu=>//=.
+  hauto lq:on inv:SNe.
+  hauto lq:on inv:TRedSN.
 Qed.
 
 Lemma PAppPair_imp n (a b0 b1 : PTm n ) :
   ~ SN (PApp (PPair b0 b1) a).
 Proof.
-  sfirstorder use:PApp_imp.
+  move E : (PApp (PPair b0 b1) a) => u hu.
+  move : a b0 b1 E.
+  elim : n u / hu=>//=.
+  hauto lq:on inv:SNe.
+  hauto lq:on inv:TRedSN.
 Qed.
 
 Lemma PAppBind_imp n p (A : PTm n) B b :
   ~ SN (PApp (PBind p A B) b).
 Proof.
-  sfirstorder use:PApp_imp.
+  move E :(PApp (PBind p A B) b) => u hu.
+  move : p A B b E.
+  elim : n u /hu=> //=.
+  hauto lq:on inv:SNe.
+  hauto lq:on inv:TRedSN.
 Qed.
 
 Lemma PProjBind_imp n p p' (A : PTm n) B :
@@ -298,10 +246,6 @@ Fixpoint ne {n} (a : PTm n) :=
   | PUniv _ => false
   | PBind _ _ _ => false
   | PBot => true
-  | PInd P a b c => nf P && ne a && nf b && nf c
-  | PNat => false
-  | PSuc a => false
-  | PZero => false
   end
 with nf {n} (a : PTm n) :=
   match a with
@@ -313,10 +257,6 @@ with nf {n} (a : PTm n) :=
   | PUniv _ => true
   | PBind _ A B => nf A && nf B
   | PBot => true
-  | PInd P a b c => nf P && ne a && nf b && nf c
-  | PNat => true
-  | PSuc a => nf a
-  | PZero => true
 end.
 
 Lemma ne_nf n a : @ne n a -> nf a.
@@ -349,15 +289,6 @@ Lemma N_β' n a (b : PTm n) u :
   TRedSN (PApp (PAbs a) b) u.
 Proof. move => ->. apply N_β. Qed.
 
-Lemma N_IndSuc' n P a b c u :
-  u = (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c) ->
-  SN P ->
-  @SN n a ->
-  SN b ->
-  SN c ->
-  TRedSN (PInd P (PSuc a) b c) u.
-Proof. move => ->. apply N_IndSuc. Qed.
-
 Lemma sn_renaming n :
   (forall (a : PTm n) (s : SNe a), forall m (ξ : fin n -> fin m), SNe (ren_PTm ξ a)) /\
   (forall (a : PTm n) (s : SN a), forall m (ξ : fin n -> fin m), SN (ren_PTm ξ a)) /\
@@ -366,9 +297,6 @@ Proof.
   move : n. apply sn_mutual => n; try qauto ctrs:SN, SNe, TRedSN depth:1.
   move => a b ha iha m ξ /=.
   apply N_β'. by asimpl. eauto.
-
-  move => * /=.
-  apply N_IndSuc';eauto. by asimpl.
 Qed.
 
 Lemma ne_nf_embed n (a : PTm n) :
@@ -408,15 +336,7 @@ Proof.
   move => a b ha iha m ξ[]//= u u0 [? ]. subst.
   case : u0 => //=. move => p p0 [*]. subst.
   spec_refl. by eauto with sn.
-
-  move => P b c ha iha hb ihb hc ihc m ξ []//= P0 a0 b0 c0 [?]. subst.
-  case : a0 => //= _ *. subst.
-  spec_refl. by eauto with sn.
-
-  move => P a b c hP ihP ha iha hb ihb hc ihc m ξ []//= P0 a0 b0 c0 [?]. subst.
-  case : a0 => //= a0 [*]. subst.
-  spec_refl. eexists; repeat split; eauto with sn.
-  by asimpl. Qed.
+Qed.
 
 Lemma sn_unmorphing n :
   (forall (a : PTm n) (s : SNe a), forall m (ρ : fin m -> PTm n) b, a = subst_PTm ρ b -> SNe b) /\
@@ -455,9 +375,7 @@ Proof.
       * move => p p0 [*]. subst.
         hauto lq:on db:sn.
   - move => a b ha iha m ρ []//=; first by hauto l:on db:sn.
-    case => //=. move => []//=.
-    + hauto lq:on db:sn.
-    + hauto lq:on db:sn.
+    hauto q:on inv:PTm db:sn.
   - move => p a b ha iha m ρ []//=; first by hauto l:on db:sn.
     move => t0 t1 [*]. subst.
     spec_refl.
@@ -466,29 +384,6 @@ Proof.
       left. eexists. split; last by eauto with sn.
       reflexivity.
     + hauto lq:on db:sn.
-  - move => P b c hP ihP hb ihb hc ihc m ρ []//=.
-    + hauto lq:on db:sn.
-    + move => p []//=.
-      * hauto lq:on db:sn.
-      * hauto q:on db:sn.
-  - move => P a b c hP ihP ha iha hb ihb hc ihc m ρ []//=.
-    + hauto lq:on db:sn.
-    + move => P0 a0 b0 c0 [?]. subst.
-      case : a0 => //=.
-      * hauto lq:on db:sn.
-      * move => a0 [*]. subst.
-        spec_refl.
-        left. eexists. split; last by eauto with sn.
-        by asimpl.
-  - move => P a0 a1 b c hP ihP hb ihb hc ihc ha iha m ρ[]//=.
-    + hauto lq:on db:sn.
-    + move => P1 a2 b2 c2 [*]. subst.
-      spec_refl.
-      case : iha.
-      * move => [a3][?]h. subst.
-        left. eexists; split; last by eauto with sn.
-        asimpl. eauto with sn.
-      * hauto lq:on db:sn.
 Qed.
 
 Lemma SN_AppInv : forall n (a b : PTm n), SN (PApp a b) -> SN a /\ SN b.
@@ -512,14 +407,6 @@ Proof.
   hauto lq:on rew:off inv:TRedSN db:sn.
 Qed.
 
-Lemma SN_IndInv : forall n P (a : PTm n) b c, SN (PInd P a b c) -> SN P /\ SN a /\ SN b /\ SN c.
-Proof.
-  move => n P a b c. move E : (PInd P a b c) => u hu. move : P a b c E.
-  elim  : n u / hu => //=.
-  hauto lq:on rew:off inv:SNe db:sn.
-  hauto lq:on rew:off inv:TRedSN db:sn.
-Qed.
-
 Lemma epar_sn_preservation n :
   (forall (a : PTm n) (s : SNe a), forall b, EPar.R a b -> SNe b) /\
   (forall (a : PTm n) (s : SN a), forall b, EPar.R a b -> SN b) /\
@@ -530,7 +417,6 @@ Proof.
   - sauto lq:on.
   - sauto lq:on.
   - sauto lq:on.
-  - sauto lq:on.
   - move => a b ha iha hb ihb b0.
     inversion 1; subst.
     + have /iha : (EPar.R (PProj PL a0) (PProj PL b0)) by sauto lq:on.
@@ -549,9 +435,6 @@ Proof.
   - sauto lq:on.
   - sauto lq:on.
   - sauto lq:on.
-  - sauto lq:on.
-  - sauto lq:on.
-  - sauto lq:on.
   - move => a b ha iha c h0.
     inversion h0; subst.
     inversion H1; subst.
@@ -583,31 +466,17 @@ Proof.
       sauto lq:on.
     + sauto lq:on.
   - sauto.
-  - sauto q:on.
-  - move => P a b c hP ihP ha iha hb ihb hc ihc u.
-    elim /EPar.inv => //=_.
-    move => P0 P1 a0 a1 b0 b1 c0 c1 hP0 ha0 hb0 hc0 [*]. subst.
-    elim /EPar.inv : ha0 => //=_.
-    move => a0 a2 ha0 [*]. subst.
-    eexists. split. apply T_Once. apply N_IndSuc; eauto.
-    hauto q:on ctrs:EPar.R use:EPar.morphing, EPar.refl inv:option.
-  - sauto q:on.
 Qed.
 
 Module RRed.
   Inductive R {n} : PTm n -> PTm n ->  Prop :=
-  (****************** Beta ***********************)
+  (****************** Eta ***********************)
   | AppAbs a b :
     R (PApp (PAbs a) b)  (subst_PTm (scons b VarPTm) a)
 
   | 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 ********************)
   | AbsCong a0 a1 :
     R a0 a1 ->
@@ -632,22 +501,7 @@ Module RRed.
     R (PBind p A0 B) (PBind p A1 B)
   | BindCong1 p A B0 B1 :
     R B0 B1 ->
-    R (PBind p A B0) (PBind p A B1)
-  | IndCong0 P0 P1 a b c :
-    R P0 P1 ->
-    R (PInd P0 a b c) (PInd P1 a b c)
-  | IndCong1 P a0 a1 b c :
-    R a0 a1 ->
-    R (PInd P a0 b c) (PInd P a1 b c)
-  | IndCong2 P a b0 b1 c :
-    R b0 b1 ->
-    R (PInd P a b0 c) (PInd P a b1 c)
-  | IndCong3 P a b c0 c1 :
-    R c0 c1 ->
-    R (PInd P a b c0) (PInd P a b c1)
-  | SucCong a0 a1 :
-    R a0 a1 ->
-    R (PSuc a0) (PSuc a1).
+    R (PBind p A B0) (PBind p A B1).
 
   Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop.
 
@@ -657,21 +511,15 @@ Module RRed.
   Proof.
     move => ->. by apply AppAbs. Qed.
 
-  Lemma IndSuc' n P a b c u :
-    u = (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c) ->
-    R (@PInd n P (PSuc a) b c) u.
-  Proof. move => ->. apply IndSuc. Qed.
-
   Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) :
     R a b -> R (ren_PTm ξ a) (ren_PTm ξ b).
   Proof.
     move => h. move : m ξ.
     elim : n a b /h.
 
-    all : try qauto ctrs:R.
     move => n a b m ξ /=.
     apply AppAbs'. by asimpl.
-    move => */=; apply IndSuc'; eauto. by asimpl.
+    all : qauto ctrs:R.
   Qed.
 
   Ltac2 rec solve_anti_ren () :=
@@ -693,14 +541,6 @@ Module RRed.
       eexists. split. apply AppAbs. by asimpl.
     - move => n p a b m ξ []//=.
       move => p0 []//=. hauto q:on ctrs:R.
-    - move => n p b c m ξ []//= P a0 b0 c0 [*]. subst.
-      destruct a0 => //=.
-      hauto lq:on ctrs:R.
-    - move => n P a b c m ξ []//=.
-      move => p p0 p1 p2 [?].  subst.
-      case : p0 => //=.
-      move => p0 [?] *. subst. eexists. split; eauto using IndSuc.
-      by asimpl.
   Qed.
 
   Lemma nf_imp n (a b : PTm n) :
@@ -717,11 +557,9 @@ Module RRed.
     R a b -> R (subst_PTm ρ a) (subst_PTm ρ b).
   Proof.
     move => h. move : m ρ. elim : n a b / h => n.
-
-    all : try hauto lq:on ctrs:R.
     move => a b m ρ /=.
     eapply AppAbs'; eauto; cycle 1. by asimpl.
-    move => */=; apply : IndSuc'; eauto. by asimpl.
+    all : hauto lq:on ctrs:R.
   Qed.
 
 End RRed.
@@ -739,18 +577,6 @@ Module RPar.
     R b0 b1 ->
     R (PProj p (PPair a0 b0)) (if p is PL then a1 else b1)
 
-  | IndZero P b0 b1  c :
-    R b0 b1 ->
-    R (PInd P PZero b0 c) b1
-
-  | IndSuc P0 P1 a0 a1 b0 b1 c0 c1 :
-    R P0 P1 ->
-    R a0 a1 ->
-    R b0 b1 ->
-    R c0 c1 ->
-    (* ----------------------------- *)
-    R (PInd P0 (PSuc a0) b0 c0) (subst_PTm (scons (PInd P1 a1 b1 c1) (scons a1 VarPTm)) c1)
-
   (*************** Congruence ********************)
   | AbsCong a0 a1 :
     R a0 a1 ->
@@ -775,22 +601,7 @@ Module RPar.
     R B0 B1 ->
     R (PBind p A0 B0) (PBind p A1 B1)
   | BotCong :
-    R PBot PBot
-  | NatCong :
-    R PNat PNat
-  | IndCong P0 P1 a0 a1 b0 b1 c0 c1 :
-    R P0 P1 ->
-    R a0 a1 ->
-    R b0 b1 ->
-    R c0 c1 ->
-    (* ----------------------- *)
-    R (PInd P0 a0 b0 c0) (PInd P1 a1 b1 c1)
-  | ZeroCong :
-    R PZero PZero
-  | SucCong a0 a1 :
-    R a0 a1 ->
-    (* ------------ *)
-    R (PSuc a0) (PSuc a1).
+    R PBot PBot.
 
   Lemma refl n (a : PTm n) : R a a.
   Proof.
@@ -813,28 +624,15 @@ Module RPar.
     R (PProj p (PPair a0 b0)) u.
   Proof. move => ->. apply ProjPair. Qed.
 
-  Lemma IndSuc' n P0 P1 (a0 a1 : PTm n) b0 b1 c0 c1 u :
-    u = (subst_PTm (scons (PInd P1 a1 b1 c1) (scons a1 VarPTm)) c1) ->
-    R P0 P1 ->
-    R a0 a1 ->
-    R b0 b1 ->
-    R c0 c1 ->
-    (* ----------------------------- *)
-    R (PInd P0 (PSuc a0) b0 c0) u.
-  Proof. move => ->. apply IndSuc. Qed.
-
   Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) :
     R a b -> R (ren_PTm ξ a) (ren_PTm ξ b).
   Proof.
     move => h. move : m ξ.
     elim : n a b /h.
 
-    all : try qauto ctrs:R use:ProjPair'.
-
     move => n a0 a1 b0 b1 ha iha hb ihb m ξ /=.
     eapply AppAbs'; eauto. by asimpl.
-
-    move => * /=. apply : IndSuc'; eauto. by asimpl.
+    all : qauto ctrs:R use:ProjPair'.
   Qed.
 
   Lemma morphing_ren n m p (ρ0 ρ1 : fin n -> PTm m) (ξ : fin m -> fin p) :
@@ -858,13 +656,10 @@ Module RPar.
     R a b -> R (subst_PTm ρ0 a) (subst_PTm ρ1 b).
   Proof.
     move => + h. move : m ρ0 ρ1. elim : n a b / h => n.
-    all : try hauto lq:on ctrs:R use:morphing_up, ProjPair'.
     move => a0 a1 b0 b1 ha iha hb ihb m ρ0 ρ1 hρ /=.
-    eapply AppAbs'; eauto; cycle 1. sfirstorder use:morphing_up. by asimpl.
-    move => */=; eapply IndSuc'; eauto; cycle 1.
-    sfirstorder use:morphing_up.
-    sfirstorder use:morphing_up.
+    eapply AppAbs'; eauto; cycle 1. sfirstorder use:morphing_up.
     by asimpl.
+    all : hauto lq:on ctrs:R use:morphing_up, ProjPair'.
   Qed.
 
   Lemma substing n m (a : PTm n) b (ρ : fin n -> PTm m) :
@@ -874,6 +669,7 @@ Module RPar.
     hauto l:on use:morphing, refl.
   Qed.
 
+
   Lemma cong n (a0 a1 : PTm (S n)) b0 b1  :
     R a0 a1 ->
     R b0 b1 ->
@@ -901,13 +697,6 @@ Module RPar.
     | PUniv i => PUniv i
     | PBind p A B => PBind p (tstar A) (tstar B)
     | PBot => PBot
-    | PNat => PNat
-    | PZero => PZero
-    | PSuc a => PSuc (tstar a)
-    | PInd P PZero b c => tstar b
-    | PInd P (PSuc a) b c =>
-        (subst_PTm (scons (PInd (tstar P) (tstar a) (tstar b) (tstar c)) (scons (tstar a) VarPTm)) (tstar c))
-    | PInd P a b c => PInd (tstar P) (tstar a) (tstar b) (tstar c)
     end.
 
   Lemma triangle n (a b : PTm n) :
@@ -939,18 +728,6 @@ Module RPar.
     - hauto lq:on ctrs:R inv:R.
     - hauto lq:on ctrs:R inv:R.
     - hauto lq:on ctrs:R inv:R.
-    - hauto lq:on ctrs:R inv:R.
-    - hauto lq:on ctrs:R inv:R.
-    - hauto lq:on ctrs:R inv:R.
-    - move => P b c ?. subst.
-      move => h0. inversion 1; subst. hauto lq:on ctrs:R. qauto l:on inv:R ctrs:R.
-    - move => P a0 b c ? hP ihP ha iha hb ihb u. subst.
-      elim /inv => //= _.
-      + move => P0 P1 a1 a2 b0 b1 c0 c1 hP' ha' hb' hc' [*]. subst.
-        apply morphing. hauto lq:on ctrs:R inv:option.
-        eauto.
-      + sauto q:on ctrs:R.
-    - sauto lq:on.
   Qed.
 
   Lemma diamond n (a b c : PTm n) :
@@ -968,16 +745,12 @@ Proof.
   - qauto l:on inv:RPar.R,SNe,SN ctrs:SNe.
   - hauto lq:on inv:RPar.R, SNe ctrs:SNe.
   - hauto lq:on inv:RPar.R, SNe ctrs:SNe.
-  - qauto l:on inv:RPar.R, SN,SNe ctrs:SNe.
   - qauto l:on ctrs:SN inv:RPar.R.
   - hauto lq:on ctrs:SN inv:RPar.R.
   - hauto lq:on ctrs:SN.
   - hauto q:on ctrs:SN inv:SN, TRedSN'.
   - hauto lq:on ctrs:SN inv:RPar.R.
   - hauto lq:on ctrs:SN inv:RPar.R.
-  - hauto l:on inv:RPar.R.
-  - hauto l:on inv:RPar.R.
-  - hauto lq:on ctrs:SN inv:RPar.R.
   - move => a b ha iha hb ihb.
     elim /RPar.inv : ihb => //=_.
     + move => a0 a1 b0 b1 ha0 hb0 [*]. subst.
@@ -997,19 +770,6 @@ Proof.
   - hauto lq:on inv:RPar.R ctrs:RPar.R, TRedSN', TRedSN.
   - hauto lq:on inv:RPar.R ctrs:RPar.R, TRedSN', TRedSN.
   - sauto.
-  - sauto.
-  - move => P a b c hP ihP ha iha hb ihb hc ihc u.
-    elim /RPar.inv => //=_.
-    + move => P0 P1 a0 a1 b0 b1 c0 c1 hP' ha' hb' hc' [*]. subst.
-      eexists. split; first by apply T_Refl.
-      apply RPar.morphing=>//. hauto lq:on ctrs:RPar.R inv:option.
-    + move => P0 P1 a0 a1 b0 b1 c0 c1 hP' ha' hb' hc' [*]. subst.
-      elim /RPar.inv : ha' => //=_.
-      move => a0 a2 ha' [*]. subst.
-      eexists. split. apply T_Once.
-      apply N_IndSuc; eauto.
-      hauto q:on use:RPar.morphing ctrs:RPar.R inv:option.
-  - sauto q:on.
 Qed.
 
 Module RReds.
@@ -1043,19 +803,6 @@ Module RReds.
     rtc RRed.R (PProj p a0) (PProj p a1).
   Proof. solve_s. Qed.
 
-  Lemma SucCong n (a0 a1 : PTm n) :
-    rtc RRed.R a0 a1 ->
-    rtc RRed.R (PSuc a0) (PSuc a1).
-  Proof. solve_s. Qed.
-
-  Lemma IndCong n P0 P1 (a0 a1 : PTm n) b0 b1 c0 c1 :
-    rtc RRed.R P0 P1 ->
-    rtc RRed.R a0 a1 ->
-    rtc RRed.R b0 b1 ->
-    rtc RRed.R c0 c1 ->
-    rtc RRed.R (PInd P0 a0 b0 c0) (PInd P1 a1 b1 c1).
-  Proof. solve_s. Qed.
-
   Lemma BindCong n p (A0 A1 : PTm n) B0 B1 :
     rtc RRed.R A0 A1 ->
     rtc RRed.R B0 B1 ->
@@ -1071,7 +818,7 @@ Module RReds.
   Lemma FromRPar n (a b : PTm n) (h : RPar.R a b) :
     rtc RRed.R a b.
   Proof.
-    elim : n a b /h; eauto using AbsCong, AppCong, PairCong, ProjCong, rtc_refl, BindCong, IndCong, SucCong.
+    elim : n a b /h; eauto using AbsCong, AppCong, PairCong, ProjCong, rtc_refl, BindCong.
     move => n a0 a1 b0 b1 ha iha hb ihb.
     apply : rtc_r; last by apply RRed.AppAbs.
     by eauto using AppCong, AbsCong.
@@ -1079,12 +826,6 @@ Module RReds.
     move => n p a0 a1 b0 b1 ha iha hb ihb.
     apply : rtc_r; last by apply RRed.ProjPair.
     by eauto using PairCong, ProjCong.
-
-    hauto lq:on ctrs:RRed.R, rtc.
-
-    move => *.
-    apply : rtc_r; last by apply RRed.IndSuc.
-    by eauto using SucCong, IndCong.
   Qed.
 
   Lemma RParIff n (a b : PTm n) :
@@ -1143,21 +884,6 @@ Module NeEPar.
     R_nonelim (PBind p A0 B0) (PBind p A1 B1)
   | BotCong :
     R_nonelim PBot PBot
-  | NatCong :
-    R_nonelim PNat PNat
-  | IndCong P0 P1 a0 a1 b0 b1 c0 c1 :
-    R_nonelim P0 P1 ->
-    R_elim a0 a1 ->
-    R_nonelim b0 b1 ->
-    R_nonelim c0 c1 ->
-    (* ----------------------- *)
-    R_nonelim (PInd P0 a0 b0 c0) (PInd P1 a1 b1 c1)
-  | ZeroCong :
-    R_nonelim PZero PZero
-  | SucCong a0 a1 :
-    R_nonelim a0 a1 ->
-    (* ------------ *)
-    R_nonelim (PSuc a0) (PSuc a1)
   with R_elim {n} : PTm n -> PTm n -> Prop :=
   | NAbsCong a0 a1 :
     R_nonelim a0 a1 ->
@@ -1182,22 +908,7 @@ Module NeEPar.
     R_nonelim B0 B1 ->
     R_elim (PBind p A0 B0) (PBind p A1 B1)
   | NBotCong :
-    R_elim PBot PBot
-  | NNatCong :
-    R_elim PNat PNat
-  | NIndCong P0 P1 a0 a1 b0 b1 c0 c1 :
-    R_nonelim P0 P1 ->
-    R_elim a0 a1 ->
-    R_nonelim b0 b1 ->
-    R_nonelim c0 c1 ->
-    (* ----------------------- *)
-    R_elim (PInd P0 a0 b0 c0) (PInd P1 a1 b1 c1)
-  | NZeroCong :
-    R_elim PZero PZero
-  | NSucCong a0 a1 :
-    R_nonelim a0 a1 ->
-    (* ------------ *)
-    R_elim (PSuc a0) (PSuc a1).
+    R_elim PBot PBot.
 
   Scheme epar_elim_ind := Induction for R_elim Sort Prop
       with epar_nonelim_ind := Induction for R_nonelim Sort Prop.
@@ -1216,7 +927,6 @@ Module NeEPar.
     - hauto lb:on.
     - hauto lq:on inv:R_elim.
     - hauto b:on.
-    - hauto lqb:on inv:R_elim.
     - move => a0 a1 /negP ha' ha ih ha1.
       have {ih} := ih ha1.
       move => ha0.
@@ -1234,7 +944,6 @@ Module NeEPar.
     - hauto lb: on drew: off.
     - hauto lq:on rew:off inv:R_elim.
     - sfirstorder b:on.
-    - hauto lqb:on inv:R_elim.
   Qed.
 
   Lemma R_nonelim_nothf n (a b : PTm n) :
@@ -1269,18 +978,12 @@ Module Type NoForbid.
   (* Axiom P_ProjAbs : forall n p (a : PTm (S n)), ~ P (PProj p (PAbs a)). *)
   (* Axiom P_ProjBind : forall n p p' (A : PTm n) B, ~ P (PProj p (PBind p' A B)). *)
   (* Axiom P_AppBind : forall n p (A : PTm n) B b, ~ P (PApp (PBind p A B) b). *)
-  Axiom PApp_imp : forall n a b, @ishf n a -> ~~ isabs a -> ~ P (PApp a b).
+  Axiom PAbs_imp : forall n a b, @ishf n a -> ~~ isabs a -> ~ P (PApp a b).
   Axiom PProj_imp : forall  n p a, @ishf n a -> ~~ ispair a -> ~ P (PProj p a).
-  Axiom PInd_imp : forall n Q (a : PTm n) b c,
-  ishf a ->
-  ~~ iszero a ->
-  ~~ issuc a  -> ~ P (PInd Q a b c).
 
   Axiom P_AppInv : forall n (a b : PTm n), P (PApp a b) -> P a /\ P b.
   Axiom P_AbsInv : forall n (a : PTm (S n)), P (PAbs a) -> P a.
-  Axiom P_SucInv : forall n (a : PTm n), P (PSuc a) -> P a.
   Axiom P_BindInv : forall n p (A : PTm n) B, P (PBind p A B) -> P A /\ P B.
-  Axiom P_IndInv : forall n Q (a : PTm n) b c, P (PInd Q a b c) -> P Q /\ P a /\ P b /\ P c.
 
   Axiom P_PairInv : forall n (a b : PTm n), P (PPair a b) -> P a /\ P b.
   Axiom P_ProjInv : forall n p (a : PTm n), P (PProj p a) -> P a.
@@ -1320,17 +1023,11 @@ Module SN_NoForbid <: NoForbid.
   Lemma P_RRed : forall n (a b : PTm n), RRed.R a b -> P a -> P b.
   Proof. hauto q:on use:red_sn_preservation, RPar.FromRRed. Qed.
 
-  Lemma PApp_imp : forall n a b, @ishf n a -> ~~ isabs a -> ~ P (PApp a b).
-    sfirstorder use:fp_red.PApp_imp. Qed.
+  Lemma PAbs_imp : forall n a b, @ishf n a -> ~~ isabs a -> ~ P (PApp a b).
+    sfirstorder use:fp_red.PAbs_imp. Qed.
   Lemma PProj_imp : forall  n p a, @ishf n a -> ~~ ispair a -> ~ P (PProj p a).
     sfirstorder use:fp_red.PProj_imp. Qed.
 
-  Lemma PInd_imp : forall n Q (a : PTm n) b c,
-      ishf a ->
-      ~~ iszero a ->
-      ~~ issuc a  -> ~ P (PInd Q a b c).
-  Proof. sfirstorder use: fp_red.PInd_imp. Qed.
-
   Lemma P_AppInv : forall n (a b : PTm n), P (PApp a b) -> P a /\ P b.
   Proof. sfirstorder use:SN_AppInv. Qed.
 
@@ -1348,9 +1045,6 @@ Module SN_NoForbid <: NoForbid.
     move : p A B E. elim : n u /hu=>//=;sauto lq:on rew:off.
   Qed.
 
-  Lemma P_SucInv : forall n (a : PTm n), P (PSuc a) -> P a.
-  Proof. sauto lq:on. Qed.
-
   Lemma P_AbsInv : forall n (a : PTm (S n)), P (PAbs a) -> P a.
   Proof.
     move => n a. move E : (PAbs a) => u h.
@@ -1367,16 +1061,13 @@ Module SN_NoForbid <: NoForbid.
   Lemma P_AppBind : forall n p (A : PTm n) B b, ~ P (PApp (PBind p A B) b).
   Proof. sfirstorder use:PAppBind_imp. Qed.
 
-  Lemma P_IndInv : forall n Q (a : PTm n) b c, P (PInd Q a b c) -> P Q /\ P a /\ P b /\ P c.
-  Proof. sfirstorder use:SN_IndInv. Qed.
-
 End SN_NoForbid.
 
 Module NoForbid_FactSN := NoForbid_Fact SN_NoForbid.
 
 Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
   Import M MFacts.
-  #[local]Hint Resolve P_EPar P_RRed PApp_imp PProj_imp : forbid.
+  #[local]Hint Resolve P_EPar P_RRed PAbs_imp PProj_imp : forbid.
 
   Lemma η_split n (a0 a1 : PTm n) :
     EPar.R a0 a1 ->
@@ -1413,7 +1104,7 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
         have ? : ~~ isabs (ren_PTm shift b) by scongruence use:isabs_ren.
         have ? : ishf (ren_PTm shift b) by scongruence use:ishf_ren.
         exfalso.
-        sfirstorder use:PApp_imp.
+        sfirstorder use:PAbs_imp.
     - move => n a0 a1 h ih /[dup] hP.
       move /P_PairInv => [/P_ProjInv + _].
       move : ih => /[apply].
@@ -1460,7 +1151,7 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
         (* Impossible *)
         * move =>*. exfalso.
           have : P (PApp a2 b0) by sfirstorder use:RReds.AppCong, @rtc_refl, P_RReds.
-          sfirstorder use:PApp_imp.
+          sfirstorder use:PAbs_imp.
     - hauto lq:on ctrs:NeEPar.R_nonelim use:RReds.PairCong, P_PairInv.
     - move => n p a0 a1 ha ih /[dup] hP /P_ProjInv.
       move : ih => /[apply]. move => [a2 [iha0 iha1]].
@@ -1487,33 +1178,9 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
     - hauto l:on.
     - hauto lq:on ctrs:NeEPar.R_nonelim, rtc use:RReds.BindCong, P_BindInv.
     - hauto lq:on ctrs:NeEPar.R_nonelim, rtc use:RReds.BindCong, P_BindInv.
-    - hauto l:on ctrs:NeEPar.R_nonelim.
-    - move => n P0 P1 a0 a1 b0 b1 c0 c1 hP ihP ha iha hb ihb hc ihc /[dup] hInd /P_IndInv.
-      move => []. move : ihP => /[apply].
-      move => [P01][ihP0]ihP1.
-      move => []. move : iha => /[apply].
-      move => [a01][iha0]iha1.
-      move => []. move : ihb => /[apply].
-      move => [b01][ihb0]ihb1.
-      move : ihc => /[apply].
-      move => [c01][ihc0]ihc1.
-      case /orP : (orNb (ishf a01)) => [h|].
-      + eexists. split. by eauto using RReds.IndCong.
-        hauto q:on ctrs:NeEPar.R_nonelim use:NeEPar.R_nonelim_nothf.
-      + move => h.
-        case /orP : (orNb (issuc a01 || iszero a01)).
-        * move /norP.
-          have : P (PInd P01 a01 b01 c01) by eauto using P_RReds, RReds.IndCong.
-          hauto lq:on use:PInd_imp.
-        * move => ha01.
-          eexists. split. eauto using RReds.IndCong.
-          apply NeEPar.IndCong; eauto.
-          move : iha1 ha01. clear.
-          inversion 1; subst => //=; hauto lq:on ctrs:NeEPar.R_elim.
-    - hauto l:on.
-    - hauto lq:on ctrs:NeEPar.R_nonelim use:RReds.SucCong, P_SucInv.
   Qed.
 
+
   Lemma eta_postponement n a b c :
     @P n a ->
     EPar.R a b ->
@@ -1564,7 +1231,7 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
           have : rtc RRed.R (PApp a0 b0) (PApp (PPair (PProj PL a1) (PProj PR a1)) b0)
             by qauto l:on ctrs:rtc use:RReds.AppCong.
           move : P_RReds hP. repeat move/[apply].
-          sfirstorder use:PApp_imp.
+          sfirstorder use:PAbs_imp.
         * exists (subst_PTm (scons b0 VarPTm) a1).
           split.
           apply : rtc_r; last by apply RRed.AppAbs.
@@ -1619,66 +1286,6 @@ Module UniqueNF (M : NoForbid) (MFacts : NoForbid_FactSig M).
     - hauto lq:on inv:RRed.R ctrs:rtc.
     - sauto lq:on ctrs:EPar.R, rtc use:RReds.BindCong, P_BindInv, @relations.rtc_transitive.
     - hauto lq:on inv:RRed.R ctrs:rtc.
-    - hauto q:on ctrs:rtc inv:RRed.R.
-    - move => n P0 P1 a0 a1 b0 b1 c0 c1 hP ihP ha iha hb ihb hc ihc u.
-      move => /[dup] hInd.
-      move /P_IndInv.
-      move => [pP0][pa0][pb0]pc0.
-      elim /RRed.inv => //= _.
-      + move => P2 b2 c2 [*]. subst.
-        move /η_split : pa0 ha; repeat move/[apply].
-        move => [a1][h0]h1 {iha}.
-        inversion h1; subst.
-        * exfalso.
-          have :P (PInd P0 (PAbs (PApp (ren_PTm shift a2) (VarPTm var_zero))) b0 c0) by eauto using RReds.IndCong, rtc_refl, P_RReds.
-          clear. hauto lq:on use:PInd_imp.
-        * have :P (PInd P0 (PPair (PProj PL a2) (PProj PR a2)) b0 c0) by eauto using RReds.IndCong, rtc_refl, P_RReds.
-          clear. hauto lq:on use:PInd_imp.
-        * eexists. split; eauto.
-          apply : rtc_r.
-          apply : RReds.IndCong; eauto; eauto using rtc_refl.
-          apply RRed.IndZero.
-      + move => P2 a2 b2 c [*]. subst.
-        move /η_split /(_ pa0) : ha.
-        move => [a1][h0]h1.
-        inversion h1; subst.
-        * have :P (PInd P0 (PAbs (PApp (ren_PTm shift a3) (VarPTm var_zero))) b0 c0) by eauto using RReds.IndCong, rtc_refl, P_RReds.
-          clear. hauto q:on use:PInd_imp.
-        * have :P (PInd P0 (PPair (PProj PL a3) (PProj PR a3)) b0 c0) by eauto using RReds.IndCong, rtc_refl, P_RReds.
-          clear. hauto q:on use:PInd_imp.
-        * eexists. split.
-          apply : rtc_r.
-          apply RReds.IndCong; eauto; eauto using rtc_refl.
-          apply RRed.IndSuc.
-          apply EPar.morphing;eauto. hauto lq:on ctrs:EPar.R inv:option use:NeEPar.ToEPar.
-      + move => P2 P3 a2 b2 c hP0 [*]. subst.
-        move : ihP hP0 pP0. repeat move/[apply].
-        move => [P2][h0]h1.
-        exists (PInd P2 a0 b0 c0).
-        sfirstorder use:RReds.IndCong, @rtc_refl, EPar.IndCong.
-      + move => P2 a2 a3 b2 c + [*]. subst.
-        move : iha pa0; repeat move/[apply].
-        move => [a2][*].
-        exists (PInd P0 a2 b0 c0).
-        sfirstorder use:RReds.IndCong, @rtc_refl, EPar.IndCong.
-      + move => P2 a2 b2 b3 c + [*]. subst.
-        move : ihb pb0; repeat move/[apply].
-        move => [b2][*].
-        exists (PInd P0 a0 b2 c0).
-        sfirstorder use:RReds.IndCong, @rtc_refl, EPar.IndCong.
-      + move => P2 a2 b2 b3 c + [*]. subst.
-        move : ihc pc0; repeat move/[apply].
-        move => [c2][*].
-        exists (PInd P0 a0 b0 c2).
-        sfirstorder use:RReds.IndCong, @rtc_refl, EPar.IndCong.
-    - hauto lq:on inv:RRed.R ctrs:rtc, EPar.R.
-    - move => n a0 a1 ha iha u /P_SucInv ha0.
-      elim /RRed.inv => //= _ a2 a3 h [*]. subst.
-      move : iha (ha0) (h); repeat move/[apply].
-      move => [a2 [ih0 ih1]].
-      exists (PSuc a2).
-      split. by apply RReds.SucCong.
-      by apply EPar.SucCong.
   Qed.
 
   Lemma η_postponement_star n a b c :
@@ -1748,22 +1355,7 @@ Module ERed.
     R (PBind p A0 B) (PBind p A1 B)
   | BindCong1 p A B0 B1 :
     R B0 B1 ->
-    R (PBind p A B0) (PBind p A B1)
-  | IndCong0 P0 P1 a b c :
-    R P0 P1 ->
-    R (PInd P0 a b c) (PInd P1 a b c)
-  | IndCong1 P a0 a1 b c :
-    R a0 a1 ->
-    R (PInd P a0 b c) (PInd P a1 b c)
-  | IndCong2 P a b0 b1 c :
-    R b0 b1 ->
-    R (PInd P a b0 c) (PInd P a b1 c)
-  | IndCong3 P a b c0 c1 :
-    R c0 c1 ->
-    R (PInd P a b c0) (PInd P a b c1)
-  | SucCong a0 a1 :
-    R a0 a1 ->
-    R (PSuc a0) (PSuc a1).
+    R (PBind p A B0) (PBind p A B1).
 
   Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop.
 
@@ -1803,54 +1395,7 @@ Module ERed.
     all : qauto ctrs:R.
   Qed.
 
-  (* Characterization of variable freeness conditions *)
-  Definition tm_i_free {n} a (i : fin n) := exists m (ξ ξ0 : fin n -> fin m), ξ i <> ξ0 i /\ ren_PTm ξ a = ren_PTm ξ0 a.
-
-  Lemma subst_differ_one_ren_up n m i (ξ0 ξ1 : fin n -> fin m) :
-    (forall j, i <> j -> ξ0 j = ξ1 j) ->
-    (forall j, shift i <> j -> upRen_PTm_PTm ξ0 j =  upRen_PTm_PTm ξ1 j).
-  Proof.
-    move => hξ.
-    destruct j. asimpl.
-    move => h. have :  i<> f by hauto lq:on rew:off inv:option.
-    move /hξ. by rewrite /funcomp => ->.
-    done.
-  Qed.
-
-  Lemma tm_free_ren_any n a i :
-    tm_i_free a i ->
-    forall m (ξ0 ξ1 : fin n -> fin m), (forall j, i <> j -> ξ0 j = ξ1 j) ->
-             ren_PTm ξ0 a = ren_PTm ξ1 a.
-  Proof.
-    rewrite /tm_i_free.
-    move => [+ [+ [+ +]]].
-    move : i.
-    elim : n / a => n.
-    - hauto q:on.
-    - move => a iha i m ρ0 ρ1 [] => h [] h' m' ξ0 ξ1 hξ /=.
-      f_equal. move /subst_differ_one_ren_up in hξ.
-      move /(_ (shift i)) in iha.
-      move : iha hξ; move/[apply].
-      apply=>//. split; eauto.
-      asimpl. rewrite /funcomp. hauto l:on.
-    - hauto lq:on rew:off.
-    - hauto lq:on rew:off.
-    - hauto lq:on rew:off.
-    - move => p A ihA a iha i m ρ0 ρ1 [] ? h m' ξ0 ξ1 hξ /=.
-      f_equal. hauto lq:on rew:off.
-      move /subst_differ_one_ren_up in hξ.
-      move /(_ (shift i)) in iha.
-      move : iha hξ. repeat move/[apply].
-      move /(_ _ (upRen_PTm_PTm ρ0) (upRen_PTm_PTm ρ1)).
-      apply. hauto l:on.
-    - hauto lq:on rew:off.
-    - hauto lq:on rew:off.
-    - hauto lq:on rew:off.
-    - hauto lq:on rew:off.
-    - hauto lq:on rew:off.
-    - admit.
-  Admitted.
-
+  (* Need to generalize to injective renaming *)
   Lemma antirenaming n m (a : PTm n) (b : PTm m) (ξ : fin n -> fin m) :
     (forall i j, ξ i = ξ j -> i = j) ->
     R (ren_PTm ξ a) b -> exists b0, R a b0 /\ ren_PTm ξ b0 = b.
@@ -1949,19 +1494,6 @@ Module EReds.
   Proof. solve_s. Qed.
 
 
-  Lemma SucCong n (a0 a1 : PTm n) :
-    rtc ERed.R a0 a1 ->
-    rtc ERed.R (PSuc a0) (PSuc a1).
-  Proof. solve_s. Qed.
-
-  Lemma IndCong n P0 P1 (a0 a1 : PTm n) b0 b1 c0 c1 :
-    rtc ERed.R P0 P1 ->
-    rtc ERed.R a0 a1 ->
-    rtc ERed.R b0 b1 ->
-    rtc ERed.R c0 c1 ->
-    rtc ERed.R (PInd P0 a0 b0 c0) (PInd P1 a1 b1 c1).
-  Proof. solve_s. Qed.
-
   Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) :
     rtc ERed.R a b -> rtc ERed.R (ren_PTm ξ a) (ren_PTm ξ b).
   Proof. induction 1; hauto l:on use:ERed.renaming ctrs:rtc. Qed.
@@ -1970,7 +1502,7 @@ Module EReds.
     EPar.R a b ->
     rtc ERed.R a b.
   Proof.
-    move => h. elim : n a b /h; eauto using AbsCong, AppCong, PairCong, ProjCong, rtc_refl, BindCong, IndCong, SucCong.
+    move => h. elim : n a b /h; eauto using AbsCong, AppCong, PairCong, ProjCong, rtc_refl, BindCong.
     - move => n a0 a1 _ h.
       have {}h : rtc ERed.R (ren_PTm shift a0) (ren_PTm shift a1) by apply renaming.
       apply : rtc_r. apply AbsCong. apply AppCong; eauto. apply rtc_refl.
@@ -2013,7 +1545,7 @@ Module EReds.
     move E : (PProj p a) => u hu.
     move : p a E.
     elim : u C /hu;
-      scrush ctrs:rtc,ERed.R inv:ERed.R.
+      hauto q:on ctrs:rtc,ERed.R inv:ERed.R.
   Qed.
 
   Lemma bind_inv n p (A : PTm n) B C :
@@ -2027,37 +1559,6 @@ Module EReds.
     hauto lq:on rew:off ctrs:rtc, ERed.R inv:ERed.R, rtc.
   Qed.
 
-  Lemma suc_inv n (a : PTm n) C :
-    rtc ERed.R (PSuc a) C ->
-    exists b, rtc ERed.R a b /\ C = PSuc b.
-  Proof.
-    move E : (PSuc a) => u hu.
-    move : a E.
-    elim : u C / hu=>//=.
-    - hauto l:on.
-    - hauto lq:on rew:off ctrs:rtc, ERed.R inv:ERed.R, rtc.
-  Qed.
-
-  Lemma zero_inv n (C : PTm n) :
-    rtc ERed.R PZero C -> C = PZero.
-    move E : PZero => u hu.
-    move : E. elim : u C /hu=>//=.
-    - hauto lq:on rew:off ctrs:rtc, ERed.R inv:ERed.R, rtc.
-  Qed.
-
-  Lemma ind_inv n P (a : PTm n) b c C :
-    rtc ERed.R (PInd P a b c) C ->
-    exists P0 a0 b0 c0,  rtc ERed.R P P0 /\ rtc ERed.R a a0 /\
-                      rtc ERed.R b b0 /\ rtc ERed.R c c0 /\
-                      C = PInd P0 a0 b0 c0.
-  Proof.
-    move E : (PInd P a b c) => u hu.
-    move : P a b c E.
-    elim : u C / hu.
-    - hauto lq:on ctrs:rtc.
-    - hauto lq:on rew:off ctrs:rtc, ERed.R inv:ERed.R, rtc.
-  Qed.
-
 End EReds.
 
 #[export]Hint Constructors ERed.R RRed.R EPar.R : red.
@@ -2086,18 +1587,6 @@ Module EJoin.
     hauto lq:on rew:off use:EReds.bind_inv.
   Qed.
 
-  Lemma suc_inj n  (A0 A1 : PTm n)  :
-    R (PSuc A0) (PSuc A1) ->
-    R A0 A1.
-  Proof.
-    hauto lq:on rew:off use:EReds.suc_inv.
-  Qed.
-
-  Lemma ind_inj n P0 P1 (a0 a1 : PTm n) b0 b1 c0 c1 :
-    R (PInd P0 a0 b0 c0) (PInd P1 a1 b1 c1) ->
-    R P0 P1 /\ R a0 a1 /\ R b0 b1 /\ R c0 c1.
-  Proof. hauto q:on use:EReds.ind_inv. Qed.
-
 End EJoin.
 
 Module RERed.
@@ -2109,12 +1598,6 @@ Module RERed.
   | 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)
-
   (****************** Eta ***********************)
   | AppEta a :
     R (PAbs (PApp (ren_PTm shift a) (VarPTm var_zero))) a
@@ -2145,22 +1628,7 @@ Module RERed.
     R (PBind p A0 B) (PBind p A1 B)
   | BindCong1 p A B0 B1 :
     R B0 B1 ->
-    R (PBind p A B0) (PBind p A B1)
-  | IndCong0 P0 P1 a b c :
-    R P0 P1 ->
-    R (PInd P0 a b c) (PInd P1 a b c)
-  | IndCong1 P a0 a1 b c :
-    R a0 a1 ->
-    R (PInd P a0 b c) (PInd P a1 b c)
-  | IndCong2 P a b0 b1 c :
-    R b0 b1 ->
-    R (PInd P a b0 c) (PInd P a b1 c)
-  | IndCong3 P a b c0 c1 :
-    R c0 c1 ->
-    R (PInd P a b c0) (PInd P a b c1)
-  | SucCong a0 a1 :
-    R a0 a1 ->
-    R (PSuc a0) (PSuc a1).
+    R (PBind p A B0) (PBind p A B1).
 
   Lemma ToBetaEta n (a b : PTm n) :
     R a b ->
@@ -2196,10 +1664,6 @@ Module RERed.
     R a b -> isuniv a -> isuniv b.
   Proof. hauto q:on inv:R. Qed.
 
-  Lemma nat_preservation n (a b : PTm n) :
-    R a b -> isnat a -> isnat b.
-  Proof. hauto q:on inv:R. Qed.
-
   Lemma sne_preservation n (a b : PTm n) :
     R a b -> SNe a -> SNe b.
   Proof.
@@ -2268,19 +1732,6 @@ Module REReds.
     rtc RERed.R (PProj p a0) (PProj p a1).
   Proof. solve_s. Qed.
 
-  Lemma SucCong n (a0 a1 : PTm n) :
-    rtc RERed.R a0 a1 ->
-    rtc RERed.R (PSuc a0) (PSuc a1).
-  Proof. solve_s. Qed.
-
-  Lemma IndCong n P0 P1 (a0 a1 : PTm n) b0 b1 c0 c1 :
-    rtc RERed.R P0 P1 ->
-    rtc RERed.R a0 a1 ->
-    rtc RERed.R b0 b1 ->
-    rtc RERed.R c0 c1 ->
-    rtc RERed.R (PInd P0 a0 b0 c0) (PInd P1 a1 b1 c1).
-  Proof. solve_s. Qed.
-
   Lemma BindCong n p (A0 A1 : PTm n) B0 B1 :
     rtc RERed.R A0 A1 ->
     rtc RERed.R B0 B1 ->
@@ -2295,10 +1746,6 @@ Module REReds.
     rtc RERed.R a b -> isuniv a -> isuniv b.
   Proof. induction 1; qauto l:on ctrs:rtc use:RERed.univ_preservation. Qed.
 
-  Lemma nat_preservation n (a b : PTm n) :
-    rtc RERed.R a b -> isnat a -> isnat b.
-  Proof. induction 1; qauto l:on ctrs:rtc use:RERed.nat_preservation. Qed.
-
   Lemma sne_preservation n (a b : PTm n) :
     rtc RERed.R a b -> SNe a -> SNe b.
   Proof. induction 1; qauto l:on ctrs:rtc use:RERed.sne_preservation. Qed.
@@ -2351,22 +1798,8 @@ Module REReds.
   Proof.
     move E : (PProj p a) => u hu.
     move : p a E.
-    elim : u C /hu => //=;
-      scrush ctrs:rtc,RERed.R use:RERed.hne_preservation inv:RERed.R.
-  Qed.
-
-  Lemma hne_ind_inv n P a b c (C : PTm n) :
-    rtc RERed.R (PInd P a b c) C -> ishne a ->
-    exists P0 a0 b0 c0, C = PInd P0 a0 b0 c0 /\
-                     rtc RERed.R P P0 /\
-                     rtc RERed.R a a0 /\
-                     rtc RERed.R b b0 /\
-                     rtc RERed.R c c0.
-  Proof.
-    move E : (PInd P a b c) => u hu.
-    move : P a b c E.
-    elim  : u C / hu => //=;
-      scrush ctrs:rtc,RERed.R use:RERed.hne_preservation inv:RERed.R.
+    elim : u C /hu;
+      hauto q:on ctrs:rtc,RERed.R use:RERed.hne_preservation inv:RERed.R.
   Qed.
 
   Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) :
@@ -2385,17 +1818,12 @@ Module REReds.
          apply rtc_refl.
   Qed.
 
-  Lemma cong_up2 n m (ρ0 ρ1 : fin n -> PTm m) :
-    (forall i, rtc RERed.R (ρ0 i) (ρ1 i)) ->
-    (forall i, rtc RERed.R (up_PTm_PTm (up_PTm_PTm ρ0) i) (up_PTm_PTm (up_PTm_PTm ρ1) i)).
-  Proof. hauto l:on use:cong_up. Qed.
-
   Lemma cong n m (a : PTm n) (ρ0 ρ1 : fin n -> PTm m) :
     (forall i, rtc RERed.R (ρ0 i) (ρ1 i)) ->
     rtc RERed.R (subst_PTm ρ0 a) (subst_PTm ρ1 a).
   Proof.
-    move : m ρ0 ρ1. elim : n / a => /=;
-      eauto 20 using AppCong, AbsCong, BindCong, ProjCong, PairCong, cong_up, rtc_refl, IndCong, SucCong, cong_up2.
+    move : m ρ0 ρ1. elim : n / a;
+      eauto using AppCong, AbsCong, BindCong, ProjCong, PairCong, cong_up, rtc_refl.
   Qed.
 
   Lemma cong' n m (a b : PTm n) (ρ0 ρ1 : fin n -> PTm m) :
@@ -2417,33 +1845,6 @@ Module REReds.
     induction h; hauto lq:on rew:off ctrs:rtc use:RERed.ToBetaEta, RReds.nf_refl, @rtc_once, ERed.nf_preservation.
   Qed.
 
-  Lemma zero_inv n (C : PTm n) :
-    rtc RERed.R PZero C -> C = PZero.
-    move E : PZero => u hu.
-    move : E. elim : u C /hu=>//=.
-    - hauto lq:on rew:off ctrs:rtc, RERed.R inv:RERed.R, rtc.
-  Qed.
-
-  Lemma suc_inv n (a : PTm n) C :
-    rtc RERed.R (PSuc a) C ->
-    exists b, rtc RERed.R a b /\ C = PSuc b.
-  Proof.
-    move E : (PSuc a) => u hu.
-    move : a E.
-    elim : u C / hu=>//=.
-    - hauto l:on.
-    - hauto lq:on rew:off ctrs:rtc, RERed.R inv:RERed.R, rtc.
-  Qed.
-
-  Lemma nat_inv n C :
-    rtc RERed.R (@PNat n) C ->
-    C = PNat.
-  Proof.
-    move E : PNat => u hu. move : E.
-    elim : u C / hu=>//=.
-    hauto lq:on rew:off ctrs:rtc, RERed.R inv:RERed.R.
-  Qed.
-
 End REReds.
 
 Module LoRed.
@@ -2455,13 +1856,6 @@ Module LoRed.
   | 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 ********************)
   | AbsCong a0 a1 :
     R a0 a1 ->
@@ -2491,29 +1885,7 @@ Module LoRed.
   | BindCong1 p A B0 B1 :
     nf A ->
     R B0 B1 ->
-    R (PBind p A B0) (PBind p A B1)
-  | IndCong0 P0 P1 a b c :
-    ne a ->
-    R P0 P1 ->
-    R (PInd P0 a b c) (PInd P1 a b c)
-  | IndCong1 P a0 a1 b c :
-    ~~ ishf a0 ->
-    R a0 a1 ->
-    R (PInd P a0 b c) (PInd P a1 b c)
-  | IndCong2 P a b0 b1 c :
-    nf P ->
-    ne a ->
-    R b0 b1 ->
-    R (PInd P a b0 c) (PInd P a b1 c)
-  | IndCong3 P a b c0 c1 :
-    nf P ->
-    ne a ->
-    nf b ->
-    R c0 c1 ->
-    R (PInd P a b c0) (PInd P a b c1)
-  | SucCong a0 a1 :
-    R a0 a1 ->
-    R (PSuc a0) (PSuc a1).
+    R (PBind p A B0) (PBind p A B1).
 
   Lemma hf_preservation n (a b : PTm n) :
     LoRed.R a b ->
@@ -2533,11 +1905,6 @@ Module LoRed.
     R (PApp (PAbs a) b)  u.
   Proof. move => ->. apply AppAbs. Qed.
 
-  Lemma IndSuc' n P a b c u :
-    u = (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c) ->
-    R (@PInd n P (PSuc a) b c) u.
-  Proof. move => ->. apply IndSuc. Qed.
-
   Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) :
     R a b -> R (ren_PTm ξ a) (ren_PTm ξ b).
   Proof.
@@ -2547,7 +1914,6 @@ Module LoRed.
     move => n a b m ξ /=.
     apply AppAbs'. by asimpl.
     all : try qauto ctrs:R use:ne_nf_ren, ishf_ren.
-    move => * /=; apply IndSuc'. by asimpl.
   Qed.
 
 End LoRed.
@@ -2609,22 +1975,6 @@ Module LoReds.
     rtc LoRed.R (PBind p A0 B0) (PBind p A1 B1).
   Proof. solve_s. Qed.
 
-  Lemma IndCong n P0 P1 (a0 a1 : PTm n) b0 b1 c0 c1 :
-    rtc LoRed.R a0 a1 ->
-    rtc LoRed.R P0 P1 ->
-    rtc LoRed.R b0 b1 ->
-    rtc LoRed.R c0 c1 ->
-    ne a1 ->
-    nf P1 ->
-    nf b1 ->
-    rtc LoRed.R (PInd P0 a0 b0 c0) (PInd P1 a1 b1 c1).
-  Proof. solve_s. Qed.
-
-  Lemma SucCong n (a0 a1 : PTm n) :
-    rtc LoRed.R a0 a1 ->
-    rtc LoRed.R (PSuc a0) (PSuc a1).
-  Proof. solve_s. Qed.
-
   Local Ltac triv := simpl in *; itauto.
 
   Lemma FromSN_mutual : forall n,
@@ -2637,16 +1987,12 @@ Module LoReds.
     - hauto lq:on rew:off use:LoReds.AppCong solve+:triv.
     - hauto l:on use:LoReds.ProjCong solve+:triv.
     - hauto lq:on ctrs:rtc.
-    - hauto lq:on use:LoReds.IndCong solve+:triv.
     - hauto q:on use:LoReds.PairCong solve+:triv.
     - hauto q:on use:LoReds.AbsCong solve+:triv.
     - sfirstorder use:ne_nf.
     - hauto lq:on ctrs:rtc.
     - hauto lq:on use:LoReds.BindCong solve+:triv.
     - hauto lq:on ctrs:rtc.
-    - hauto lq:on ctrs:rtc.
-    - hauto lq:on ctrs:rtc.
-    - hauto l:on use:SucCong.
     - qauto ctrs:LoRed.R.
     - move => n a0 a1 b hb ihb h.
       have : ~~ ishf a0 by inversion h.
@@ -2656,11 +2002,6 @@ Module LoReds.
     - move => n p a b h.
       have : ~~ ishf a by inversion h.
       hauto lq:on ctrs:LoRed.R.
-    - sfirstorder.
-    - sfirstorder.
-    - move => n P a0 a1 b c hP ihP hb ihb hc ihc hr.
-      have : ~~ ishf a0 by inversion hr.
-      hauto q:on ctrs:LoRed.R.
   Qed.
 
   Lemma FromSN : forall n a, @SN n a -> exists v, rtc LoRed.R a v /\ nf v.
@@ -2681,10 +2022,6 @@ Fixpoint size_PTm {n} (a : PTm n) :=
   | PPair a b => 3 + Nat.add (size_PTm a) (size_PTm b)
   | PUniv _ => 3
   | PBind p A B => 3 + Nat.add (size_PTm A) (size_PTm B)
-  | PInd P a b c => 3 + size_PTm P + size_PTm a + size_PTm b + size_PTm c
-  | PNat => 3
-  | PSuc a => 3 + size_PTm a
-  | PZero => 3
   | PBot => 1
   end.
 
@@ -2775,43 +2112,7 @@ Proof.
       hauto lq:on ctrs:rtc use:EReds.BindCong.
   - move => p A B0 B1 hB ihB u.
     elim /ERed.inv => //=_;
-                     hauto lq:on ctrs:rtc use:EReds.BindCong.
-  - move => P0 P1 a b c hP ihP u.
-    elim /ERed.inv => //=_.
-    + move => P2 P3 a0 b0 c0 hP' [*]. subst.
-      move : ihP hP' => /[apply]. move => [P4][hP0]hP1.
-      eauto using EReds.IndCong, rtc_refl.
-    + move => P2 a0 a1 b0 c0  + [*]. subst.
-      eauto 20 using rtc_refl, EReds.IndCong, rtc_l.
-    + move => P2 a0 b0 b1 c0 hb [*] {ihP}. subst.
-      eauto 20 using rtc_refl, EReds.IndCong, rtc_l.
-    + move => P2 a0 b0 c0 c1 h [*] {ihP}. subst.
-      eauto 20 using rtc_refl, EReds.IndCong, rtc_l.
-  - move => P a0 a1 b c ha iha u.
-    elim /ERed.inv => //=_;
-                     try solve [move => P0 P1 a2 b0 c0 hP[*]; subst;
-      eauto 20 using rtc_refl, EReds.IndCong, rtc_l].
-    move => P0 P1 a2 b0 c0 hP[*]. subst.
-    move : iha hP => /[apply].
-    move => [? [*]].
-    eauto 20 using rtc_refl, EReds.IndCong, rtc_l.
-  - move => P a b0 b1 c hb ihb u.
-    elim /ERed.inv => //=_;
-      try solve [
-          move => P0 P1 a0 b2 c0 hP [*]; subst;
-          eauto 20 using rtc_refl, EReds.IndCong, rtc_l].
-    move => P0 a0 b2 b3 c0 h [*]. subst.
-    move : ihb h => /[apply]. move => [b2 [*]].
-    eauto 20 using rtc_refl, EReds.IndCong, rtc_l.
-  - move => P a b c0 c1 hc ihc u.
-    elim /ERed.inv => //=_;
-      try solve [
-          move => P0 P1 a0 b0 c hP [*]; subst;
-          eauto 20 using rtc_refl, EReds.IndCong, rtc_l].
-    move => P0 a0 b0 c2 c3 h [*]. subst.
-    move : ihc h => /[apply]. move => [c2][*].
-    eauto 20 using rtc_refl, EReds.IndCong, rtc_l.
-  - qauto l:on inv:ERed.R ctrs:rtc use:EReds.SucCong.
+      hauto lq:on ctrs:rtc use:EReds.BindCong.
 Qed.
 
 Lemma ered_confluence n (a b c : PTm n) :
@@ -2928,16 +2229,16 @@ Module BJoin.
     exists v. sfirstorder use:@relations.rtc_transitive.
   Qed.
 
-  (* Lemma AbsCong n (a b : PTm (S n)) : *)
-  (*   R a b -> *)
-  (*   R (PAbs a) (PAbs b). *)
-  (* Proof. hauto lq:on use:RReds.AbsCong unfold:R. Qed. *)
+  Lemma AbsCong n (a b : PTm (S n)) :
+    R a b ->
+    R (PAbs a) (PAbs b).
+  Proof. hauto lq:on use:RReds.AbsCong unfold:R. Qed.
 
-  (* Lemma AppCong n (a0 a1 b0 b1 : PTm n) : *)
-  (*   R a0 a1 -> *)
-  (*   R b0 b1 -> *)
-  (*   R (PApp a0 b0) (PApp a1 b1). *)
-  (* Proof. hauto lq:on use:RReds.AppCong unfold:R. Qed. *)
+  Lemma AppCong n (a0 a1 b0 b1 : PTm n) :
+    R a0 a1 ->
+    R b0 b1 ->
+    R (PApp a0 b0) (PApp a1 b1).
+  Proof. hauto lq:on use:RReds.AppCong unfold:R. Qed.
 End BJoin.
 
 Module DJoin.
@@ -2992,19 +2293,6 @@ Module DJoin.
     R (PBind p A0 B0) (PBind p A1 B1).
   Proof. hauto q:on use:REReds.BindCong. Qed.
 
-  Lemma IndCong n P0 P1 (a0 a1 : PTm n) b0 b1 c0 c1 :
-    R P0 P1 ->
-    R a0 a1 ->
-    R b0 b1 ->
-    R c0 c1 ->
-    R (PInd P0 a0 b0 c0) (PInd P1 a1 b1 c1).
-  Proof. hauto q:on use:REReds.IndCong. Qed.
-
-  Lemma SucCong n (a0 a1 : PTm n) :
-    R a0 a1 ->
-    R (PSuc a0) (PSuc a1).
-  Proof. qauto l:on use:REReds.SucCong. Qed.
-
   Lemma FromRedSNs n (a b : PTm n) :
     rtc TRedSN a b ->
     R a b.
@@ -3013,14 +2301,6 @@ Module DJoin.
     sfirstorder use:@rtc_refl unfold:R.
   Qed.
 
-  Lemma sne_nat_noconf n (a b : PTm n) :
-    R a b -> SNe a -> isnat b -> False.
-  Proof.
-    move => [c [? ?]] *.
-    have : SNe c /\ isnat c by sfirstorder use:REReds.sne_preservation, REReds.nat_preservation.
-    qauto l:on inv:SNe.
-  Qed.
-
   Lemma sne_bind_noconf n (a b : PTm n) :
     R a b -> SNe a -> isbind b -> False.
   Proof.
@@ -3068,14 +2348,6 @@ Module DJoin.
     case : c => //=.
   Qed.
 
-  Lemma hne_nat_noconf n (a b : PTm n) :
-    R a b -> ishne a -> isnat b -> False.
-  Proof.
-    move => [c [h0 h1]] h2 h3.
-    have : ishne c /\ isnat c by sfirstorder use:REReds.hne_preservation, REReds.nat_preservation.
-    clear. case : c => //=; itauto.
-  Qed.
-
   Lemma bind_inj n p0 p1 (A0 A1 : PTm n) B0 B1 :
     DJoin.R (PBind p0 A0 B0) (PBind p1 A1 B1) ->
     p0 = p1 /\ DJoin.R A0 A1 /\ DJoin.R B0 B1.
@@ -3094,13 +2366,6 @@ Module DJoin.
     sauto lq:on rew:off use:REReds.univ_inv.
   Qed.
 
-  Lemma suc_inj n  (A0 A1 : PTm n)  :
-    R (PSuc A0) (PSuc A1) ->
-    R A0 A1.
-  Proof.
-    hauto lq:on rew:off use:REReds.suc_inv.
-  Qed.
-
   Lemma hne_app_inj n (a0 b0 a1 b1 : PTm n) :
     R (PApp a0 b0) (PApp a1 b1) ->
     ishne a0 ->
@@ -3165,15 +2430,6 @@ Module DJoin.
     hauto q:on ctrs:rtc inv:option use:REReds.cong.
   Qed.
 
-  Lemma cong' n m (a b : PTm (S n)) c d (ρ : fin n -> PTm m) :
-    R a b ->
-    R c d -> R (subst_PTm (scons c ρ) a) (subst_PTm (scons d ρ) b).
-  Proof.
-    rewrite /R. move => [ab [h2 h3]] [cd [h0 h1]].
-    exists (subst_PTm (scons cd ρ) ab).
-    hauto q:on ctrs:rtc inv:option use:REReds.cong'.
-  Qed.
-
   Lemma pair_inj n (a0 a1 b0 b1 : PTm n) :
     SN (PPair a0 b0) ->
     SN (PPair a1 b1) ->
@@ -3404,13 +2660,6 @@ Module ESub.
     sauto lq:on rew:off inv:Sub1.R.
   Qed.
 
-  Lemma suc_inj n (a b : PTm n) :
-    R (PSuc a) (PSuc b) ->
-    R a b.
-  Proof.
-    sauto lq:on use:EReds.suc_inv inv:Sub1.R.
-  Qed.
-
 End ESub.
 
 Module Sub.
@@ -3473,22 +2722,6 @@ Module Sub.
     @R n (PUniv i) (PUniv j).
   Proof. hauto lq:on ctrs:Sub1.R, rtc. Qed.
 
-  Lemma sne_nat_noconf n (a b : PTm n) :
-    R a b -> SNe a -> isnat b -> False.
-  Proof.
-    move => [c [d [h0 [h1 h2]]]] *.
-    have : SNe c /\ isnat d by sfirstorder use:REReds.sne_preservation, REReds.nat_preservation, Sub1.sne_preservation.
-    move : h2. clear. hauto q:on inv:Sub1.R, SNe.
-  Qed.
-
-  Lemma nat_sne_noconf n (a b : PTm n) :
-    R a b -> isnat a -> SNe b -> False.
-  Proof.
-    move => [c [d [h0 [h1 h2]]]] *.
-    have : SNe d /\ isnat c by sfirstorder use:REReds.sne_preservation, REReds.nat_preservation.
-    move : h2. clear. hauto q:on inv:Sub1.R, SNe.
-  Qed.
-
   Lemma sne_bind_noconf n (a b : PTm n) :
     R a b -> SNe a -> isbind b -> False.
   Proof.
@@ -3537,48 +2770,6 @@ Module Sub.
     clear. case : c => //=. inversion 2.
   Qed.
 
-  Lemma univ_nat_noconf n (a b : PTm n)  :
-    R a b -> isuniv b -> isnat a -> False.
-  Proof.
-    move => [c[d] [? []]] h0 h1 h2 h3.
-    have : isuniv d by eauto using REReds.univ_preservation.
-    have : isnat c by sfirstorder use:REReds.nat_preservation.
-    inversion h1; subst => //=.
-    clear. case : d => //=.
-  Qed.
-
-  Lemma nat_univ_noconf n (a b : PTm n)  :
-    R a b -> isnat b -> isuniv a -> False.
-  Proof.
-    move => [c[d] [? []]] h0 h1 h2 h3.
-    have : isuniv c by eauto using REReds.univ_preservation.
-    have : isnat d by sfirstorder use:REReds.nat_preservation.
-    inversion h1; subst => //=.
-    clear. case : d => //=.
-  Qed.
-
-  Lemma bind_nat_noconf n (a b : PTm n)  :
-    R a b -> isbind b -> isnat a -> False.
-  Proof.
-    move => [c[d] [? []]] h0 h1 h2 h3.
-    have : isbind d by eauto using REReds.bind_preservation.
-    have : isnat c by sfirstorder use:REReds.nat_preservation.
-    move : h1. clear.
-    inversion 1; subst => //=.
-    case : d h1 => //=.
-  Qed.
-
-  Lemma nat_bind_noconf n (a b : PTm n)  :
-    R a b -> isnat b -> isbind a -> False.
-  Proof.
-    move => [c[d] [? []]] h0 h1 h2 h3.
-    have : isbind c by eauto using REReds.bind_preservation.
-    have : isnat d by sfirstorder use:REReds.nat_preservation.
-    move : h1. clear.
-    inversion 1; subst => //=.
-    case : d h1 => //=.
-  Qed.
-
   Lemma bind_univ_noconf n (a b : PTm n) :
     R a b -> isbind a -> isuniv b -> False.
   Proof.
@@ -3618,14 +2809,6 @@ Module Sub.
     sauto lq:on rew:off use:REReds.univ_inv.
   Qed.
 
-  Lemma suc_inj n  (A0 A1 : PTm n)  :
-    R (PSuc A0) (PSuc A1) ->
-    R A0 A1.
-  Proof.
-    sauto q:on use:REReds.suc_inv.
-  Qed.
-
-
   Lemma cong n m (a b : PTm (S n)) c d (ρ : fin n -> PTm m) :
     R a b -> DJoin.R c d -> R (subst_PTm (scons c ρ) a) (subst_PTm (scons d ρ) b).
   Proof.
diff --git a/theories/logrel.v b/theories/logrel.v
index a245362..52a4438 100644
--- 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.
diff --git a/theories/preservation.v b/theories/preservation.v
index b78f87e..6fe081d 100644
--- 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) :
diff --git a/theories/structural.v b/theories/structural.v
index c25986c..2773c3c 100644
--- 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.
-    exists i. repeat split => //=.
-    eapply wff_mutual in hA.
-    apply Su_Univ; eauto.
+  - hauto lq:on ctrs:Wt,LEq,Eq use:Wt_Univ.
   - 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 :
diff --git a/theories/typing.v b/theories/typing.v
index 818d6b5..052eab8 100644
--- 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 :
   ⊢ Γ ->