diff --git a/syntax.sig b/syntax.sig
index 6b7e4df..a50911e 100644
--- a/syntax.sig
+++ b/syntax.sig
@@ -16,4 +16,8 @@ PPair : PTm -> PTm -> PTm
 PProj : PTag -> PTm -> PTm
 PBind : BTag -> PTm -> (bind PTm in PTm) -> PTm
 PUniv : nat -> PTm
-PBot : PTm
\ No newline at end of file
+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
diff --git a/theories/Autosubst2/syntax.v b/theories/Autosubst2/syntax.v
index ff9ec18..5d04c05 100644
--- a/theories/Autosubst2/syntax.v
+++ b/theories/Autosubst2/syntax.v
@@ -41,7 +41,13 @@ Inductive PTm (n_PTm : nat) : Type :=
   | PProj : PTag -> PTm n_PTm -> PTm n_PTm
   | PBind : BTag -> PTm n_PTm -> PTm (S n_PTm) -> PTm n_PTm
   | PUniv : nat -> PTm n_PTm
-  | PBot : PTm n_PTm.
+  | PBot : PTm n_PTm
+  | PNat : PTm n_PTm
+  | PZero : PTm n_PTm
+  | PSuc : PTm n_PTm -> PTm n_PTm
+  | PInd :
+      PTm (S n_PTm) ->
+      PTm n_PTm -> PTm n_PTm -> PTm (S (S n_PTm)) -> PTm n_PTm.
 
 Lemma congr_PAbs {m_PTm : nat} {s0 : PTm (S m_PTm)} {t0 : PTm (S m_PTm)}
   (H0 : s0 = t0) : PAbs m_PTm s0 = PAbs m_PTm t0.
@@ -95,6 +101,37 @@ 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.
@@ -119,6 +156,13 @@ 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) :
@@ -150,6 +194,13 @@ 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)
@@ -193,6 +244,15 @@ 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)
@@ -239,6 +299,18 @@ 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)
@@ -286,6 +358,18 @@ 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)
@@ -334,6 +418,20 @@ 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}
@@ -391,6 +489,21 @@ 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}
@@ -468,6 +581,21 @@ 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}
@@ -547,6 +675,21 @@ 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}
@@ -665,6 +808,18 @@ 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}
@@ -871,6 +1026,14 @@ 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}.
@@ -885,9 +1048,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 6fe5fad..096ec94 100644
--- a/theories/algorithmic.v
+++ b/theories/algorithmic.v
@@ -16,13 +16,22 @@ Module HRed.
   | ProjPair p a b :
     R (PProj p (PPair a b)) (if p is PL then a else b)
 
+  | IndZero P b c :
+    R (PInd P PZero b c) b
+
+  | IndSuc P a b c :
+    R (PInd P (PSuc a) b c) (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c)
+
   (*************** Congruence ********************)
   | AppCong a0 a1 b :
     R a0 a1 ->
     R (PApp a0 b) (PApp a1 b)
   | ProjCong p a0 a1 :
     R a0 a1 ->
-    R (PProj p a0) (PProj p a1).
+    R (PProj p a0) (PProj p a1)
+  | IndCong P a0 a1 b c :
+    R a0 a1 ->
+    R (PInd P a0 b c) (PInd P a1 b c).
 
   Lemma ToRRed n (a b : PTm n) : HRed.R a b -> RRed.R a b.
   Proof. induction 1; hauto lq:on ctrs:RRed.R. Qed.
@@ -82,6 +91,17 @@ 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.
@@ -121,6 +141,21 @@ 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 :
@@ -154,6 +189,20 @@ 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 :
@@ -195,6 +244,22 @@ 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 :
@@ -222,11 +287,73 @@ 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 ->
   (* --------------------- *)
@@ -274,6 +401,10 @@ 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
@@ -298,6 +429,16 @@ 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' ->
@@ -328,9 +469,6 @@ 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) /\
@@ -401,6 +539,37 @@ 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'.
@@ -533,6 +702,7 @@ 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.
@@ -553,8 +723,14 @@ 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) :
@@ -574,6 +750,15 @@ 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) :
@@ -609,6 +794,53 @@ 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 ->
@@ -621,6 +853,39 @@ 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.
@@ -682,6 +947,16 @@ 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.
@@ -689,7 +964,7 @@ Proof.
   move : a E.
   elim : u b /hu.
   - hauto l:on.
-  - hauto lq:on ctrs:nsteps inv:LoRed.R.
+  - scrush ctrs:nsteps inv:LoRed.R.
 Qed.
 
 Lemma lored_hne_preservation n (a b : PTm n) :
@@ -720,6 +995,37 @@ 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 ->
@@ -785,6 +1091,7 @@ Proof.
   lia.
 Qed.
 
+
 Lemma lored_nsteps_app_cong k n (a0 a1 b : PTm n) :
   nsteps LoRed.R k a0 a1 ->
   ishne a0 ->
@@ -917,6 +1224,24 @@ 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 ->
@@ -946,6 +1271,20 @@ 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) ->
@@ -966,58 +1305,6 @@ 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 ->
@@ -1046,7 +1333,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.
+    + 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.
       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.
@@ -1077,7 +1364,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.
+    + 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.
       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.
@@ -1145,6 +1432,12 @@ 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.
@@ -1152,6 +1445,55 @@ 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.
@@ -1208,6 +1550,27 @@ 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.
@@ -1220,20 +1583,22 @@ Proof.
     by firstorder.
 
     case : a h fb fa => //=.
-    + 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.
+    + case : b => //=; move => > /algo_metric_join.
+      * move /DJoin.var_inj => ?. subst. qauto l:on use:Var_Inv, T_Var,CE_VarCong.
+      * clear => ? ? _. exfalso.
         hauto l:on use:REReds.var_inv, REReds.hne_app_inv.
-      * move => a0 a1 i /algo_metric_join. clear => ? ? _. exfalso.
+      * clear => ? ? _. exfalso.
         hauto l:on use:REReds.var_inv, REReds.hne_proj_inv.
       * sfirstorder use:T_Bot_Imp.
-    + case : b => //=.
-      * clear. move => i a a0 /algo_metric_join h _ ?. exfalso.
-        hauto l:on use:REReds.hne_app_inv, REReds.var_inv.
+      * 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.
       (* real case *)
       * move => b1 a1 b0 a0 halg hne1 hne0 Γ A B wtA wtB.
         move /App_Inv : wtA => [A0][B0][hb0][ha0]hS0.
@@ -1259,7 +1624,7 @@ Proof.
         move => [ih _].
         move : ih (ha0') (ha1'); repeat move/[apply].
         move => iha.
-        split. sauto lq:on.
+        split. qblast.
         exists (subst_PTm (scons a0 VarPTm) B2).
         split.
         apply : Su_Transitive; eauto.
@@ -1279,9 +1644,11 @@ Proof.
         move /E_Symmetric in h01.
         move /regularity_sub0 : hSu20 => [i0].
         sfirstorder use:bind_inst.
-      * move => p p0 p1 p2 /algo_metric_join. clear => ? ? ?. exfalso.
+      * 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.
@@ -1342,7 +1709,66 @@ 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,
@@ -1389,6 +1815,9 @@ 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
@@ -1451,6 +1880,7 @@ 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.
@@ -1475,6 +1905,15 @@ 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)  :
@@ -1511,6 +1950,15 @@ 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) :
@@ -1595,21 +2043,55 @@ 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 24e708e..282038d 100644
--- a/theories/common.v
+++ b/theories/common.v
@@ -1,4 +1,4 @@
-Require Import Autosubst2.fintype Autosubst2.syntax ssreflect.
+Require Import Autosubst2.fintype Autosubst2.syntax Autosubst2.core ssreflect.
 From Ltac2 Require Ltac2.
 Import Ltac2.Notations.
 Import Ltac2.Control.
@@ -7,16 +7,6 @@ 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.
@@ -24,43 +14,58 @@ Proof.
   sblast inv:option.
 Qed.
 
+Local Ltac2 rec solve_anti_ren () :=
+  let x := Fresh.in_goal (Option.get (Ident.of_string "x")) in
+  intro $x;
+  lazy_match! Constr.type (Control.hyp x) with
+  | fin _ -> _ _ => (ltac1:(case;hauto lq:on rew:off use:up_injective))
+  | _ => solve_anti_ren ()
+  end.
+
+Local Ltac solve_anti_ren := ltac2:(Control.enter solve_anti_ren).
+
 Lemma ren_injective n m (a b : PTm n) (ξ : fin n -> fin m) :
   (forall i j, ξ i = ξ j -> i = j) ->
   ren_PTm ξ a = ren_PTm ξ b ->
   a = b.
 Proof.
-  move : m ξ b.
-  elim : n / a => //; try solve_anti_ren.
-
-  move => 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.
+  move : m ξ b. elim : n / a => //; try solve_anti_ren.
 Qed.
 
+Inductive HF : Set :=
+| H_Pair | H_Abs | H_Univ | H_Bind (p : BTag) | H_Nat | H_Suc | H_Zero | H_Bot.
+
 Definition ishf {n} (a : PTm n) :=
   match a with
   | PPair _ _ => true
   | 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.
 
@@ -74,6 +79,12 @@ 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
@@ -95,3 +106,7 @@ 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
new file mode 100644
index 0000000..f773fa6
--- /dev/null
+++ b/theories/executable.v
@@ -0,0 +1,145 @@
+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 e89c191..bffe1a7 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -55,7 +55,22 @@ Module EPar.
     R B0 B1 ->
     R (PBind p A0 B0) (PBind p A1 B1)
   | BotCong :
-    R PBot PBot.
+    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).
 
   Lemma refl n (a : PTm n) : R a a.
   Proof.
@@ -76,9 +91,10 @@ 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) :
@@ -125,6 +141,12 @@ 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 ->
@@ -146,6 +168,13 @@ 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 ->
@@ -162,10 +191,32 @@ 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).
+  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).
 
 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 ->
@@ -179,7 +230,7 @@ Proof.
   hauto lq:on inv:TRedSN.
 Qed.
 
-Lemma PAbs_imp n a b :
+Lemma PApp_imp n a b :
   @ishf n a ->
   ~~ isabs a ->
   ~ SN (PApp a b).
@@ -190,34 +241,35 @@ 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.
-  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.
+  sfirstorder use:PProj_imp.
 Qed.
 
 Lemma PAppPair_imp n (a b0 b1 : PTm n ) :
   ~ SN (PApp (PPair b0 b1) a).
 Proof.
-  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.
+  sfirstorder use:PApp_imp.
 Qed.
 
 Lemma PAppBind_imp n p (A : PTm n) B b :
   ~ SN (PApp (PBind p A B) b).
 Proof.
-  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.
+  sfirstorder use:PApp_imp.
 Qed.
 
 Lemma PProjBind_imp n p p' (A : PTm n) B :
@@ -246,6 +298,10 @@ 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
@@ -257,6 +313,10 @@ 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.
@@ -289,6 +349,15 @@ 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)) /\
@@ -297,6 +366,9 @@ 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) :
@@ -336,7 +408,15 @@ Proof.
   move => a b ha iha m ξ[]//= u u0 [? ]. subst.
   case : u0 => //=. move => p p0 [*]. subst.
   spec_refl. by eauto with sn.
-Qed.
+
+  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.
 
 Lemma sn_unmorphing n :
   (forall (a : PTm n) (s : SNe a), forall m (ρ : fin m -> PTm n) b, a = subst_PTm ρ b -> SNe b) /\
@@ -375,7 +455,9 @@ Proof.
       * move => p p0 [*]. subst.
         hauto lq:on db:sn.
   - move => a b ha iha m ρ []//=; first by hauto l:on db:sn.
-    hauto q:on inv:PTm db:sn.
+    case => //=. move => []//=.
+    + hauto lq:on db:sn.
+    + hauto lq:on db:sn.
   - move => p a b ha iha m ρ []//=; first by hauto l:on db:sn.
     move => t0 t1 [*]. subst.
     spec_refl.
@@ -384,6 +466,29 @@ 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.
@@ -407,6 +512,14 @@ 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) /\
@@ -417,6 +530,7 @@ 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.
@@ -435,6 +549,9 @@ 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.
@@ -466,17 +583,31 @@ 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 :=
-  (****************** Eta ***********************)
+  (****************** Beta ***********************)
   | 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 ->
@@ -501,7 +632,22 @@ 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).
+    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).
 
   Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop.
 
@@ -511,15 +657,21 @@ 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.
-    all : qauto ctrs:R.
+    move => */=; apply IndSuc'; eauto. by asimpl.
   Qed.
 
   Ltac2 rec solve_anti_ren () :=
@@ -541,6 +693,14 @@ 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) :
@@ -557,9 +717,11 @@ 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.
-    all : hauto lq:on ctrs:R.
+    move => */=; apply : IndSuc'; eauto. by asimpl.
   Qed.
 
 End RRed.
@@ -577,6 +739,18 @@ 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 ->
@@ -601,7 +775,22 @@ Module RPar.
     R B0 B1 ->
     R (PBind p A0 B0) (PBind p A1 B1)
   | BotCong :
-    R PBot PBot.
+    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).
 
   Lemma refl n (a : PTm n) : R a a.
   Proof.
@@ -624,15 +813,28 @@ 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.
-    all : qauto ctrs:R use:ProjPair'.
+
+    move => * /=. apply : IndSuc'; eauto. by asimpl.
   Qed.
 
   Lemma morphing_ren n m p (ρ0 ρ1 : fin n -> PTm m) (ξ : fin m -> fin p) :
@@ -656,10 +858,13 @@ 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.
+    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.
     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) :
@@ -669,7 +874,6 @@ 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 ->
@@ -697,6 +901,13 @@ 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) :
@@ -728,6 +939,18 @@ 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) :
@@ -745,12 +968,16 @@ 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.
@@ -770,6 +997,19 @@ 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.
@@ -803,6 +1043,19 @@ 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 ->
@@ -818,7 +1071,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.
+    elim : n a b /h; eauto using AbsCong, AppCong, PairCong, ProjCong, rtc_refl, BindCong, IndCong, SucCong.
     move => n a0 a1 b0 b1 ha iha hb ihb.
     apply : rtc_r; last by apply RRed.AppAbs.
     by eauto using AppCong, AbsCong.
@@ -826,6 +1079,12 @@ 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) :
@@ -884,6 +1143,21 @@ 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 ->
@@ -908,7 +1182,22 @@ Module NeEPar.
     R_nonelim B0 B1 ->
     R_elim (PBind p A0 B0) (PBind p A1 B1)
   | NBotCong :
-    R_elim PBot PBot.
+    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).
 
   Scheme epar_elim_ind := Induction for R_elim Sort Prop
       with epar_nonelim_ind := Induction for R_nonelim Sort Prop.
@@ -927,6 +1216,7 @@ 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.
@@ -944,6 +1234,7 @@ 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) :
@@ -978,12 +1269,18 @@ 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 PAbs_imp : forall n a b, @ishf n a -> ~~ isabs a -> ~ P (PApp a b).
+  Axiom PApp_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.
@@ -1023,11 +1320,17 @@ 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 PAbs_imp : forall n a b, @ishf n a -> ~~ isabs a -> ~ P (PApp a b).
-    sfirstorder use:fp_red.PAbs_imp. 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 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.
 
@@ -1045,6 +1348,9 @@ 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.
@@ -1061,13 +1367,16 @@ 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 PAbs_imp PProj_imp : forbid.
+  #[local]Hint Resolve P_EPar P_RRed PApp_imp PProj_imp : forbid.
 
   Lemma η_split n (a0 a1 : PTm n) :
     EPar.R a0 a1 ->
@@ -1104,7 +1413,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:PAbs_imp.
+        sfirstorder use:PApp_imp.
     - move => n a0 a1 h ih /[dup] hP.
       move /P_PairInv => [/P_ProjInv + _].
       move : ih => /[apply].
@@ -1151,7 +1460,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:PAbs_imp.
+          sfirstorder use:PApp_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]].
@@ -1178,9 +1487,33 @@ 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 ->
@@ -1231,7 +1564,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:PAbs_imp.
+          sfirstorder use:PApp_imp.
         * exists (subst_PTm (scons b0 VarPTm) a1).
           split.
           apply : rtc_r; last by apply RRed.AppAbs.
@@ -1286,6 +1619,66 @@ 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 :
@@ -1355,7 +1748,22 @@ 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).
+    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).
 
   Derive Dependent Inversion inv with (forall n (a b : PTm n), R a b) Sort Prop.
 
@@ -1395,7 +1803,54 @@ Module ERed.
     all : qauto ctrs:R.
   Qed.
 
-  (* Need to generalize to injective renaming *)
+  (* 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.
+
   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.
@@ -1494,6 +1949,19 @@ 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.
@@ -1502,7 +1970,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.
+    move => h. elim : n a b /h; eauto using AbsCong, AppCong, PairCong, ProjCong, rtc_refl, BindCong, IndCong, SucCong.
     - 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.
@@ -1545,7 +2013,7 @@ Module EReds.
     move E : (PProj p a) => u hu.
     move : p a E.
     elim : u C /hu;
-      hauto q:on ctrs:rtc,ERed.R inv:ERed.R.
+      scrush ctrs:rtc,ERed.R inv:ERed.R.
   Qed.
 
   Lemma bind_inv n p (A : PTm n) B C :
@@ -1559,6 +2027,37 @@ 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.
@@ -1587,6 +2086,18 @@ 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.
@@ -1598,6 +2109,12 @@ 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
@@ -1628,7 +2145,22 @@ 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).
+    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).
 
   Lemma ToBetaEta n (a b : PTm n) :
     R a b ->
@@ -1664,6 +2196,10 @@ 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.
@@ -1732,6 +2268,19 @@ 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 ->
@@ -1746,6 +2295,10 @@ 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.
@@ -1798,8 +2351,22 @@ Module REReds.
   Proof.
     move E : (PProj p a) => u hu.
     move : p a E.
-    elim : u C /hu;
-      hauto q:on ctrs:rtc,RERed.R use:RERed.hne_preservation inv:RERed.R.
+    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.
   Qed.
 
   Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) :
@@ -1818,12 +2385,17 @@ 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 using AppCong, AbsCong, BindCong, ProjCong, PairCong, cong_up, rtc_refl.
+    move : m ρ0 ρ1. elim : n / a => /=;
+      eauto 20 using AppCong, AbsCong, BindCong, ProjCong, PairCong, cong_up, rtc_refl, IndCong, SucCong, cong_up2.
   Qed.
 
   Lemma cong' n m (a b : PTm n) (ρ0 ρ1 : fin n -> PTm m) :
@@ -1845,6 +2417,33 @@ 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.
@@ -1856,6 +2455,13 @@ 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 ->
@@ -1885,7 +2491,29 @@ Module LoRed.
   | BindCong1 p A B0 B1 :
     nf A ->
     R B0 B1 ->
-    R (PBind p A B0) (PBind p A 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).
 
   Lemma hf_preservation n (a b : PTm n) :
     LoRed.R a b ->
@@ -1905,6 +2533,11 @@ 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.
@@ -1914,6 +2547,7 @@ 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.
@@ -1975,6 +2609,22 @@ 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,
@@ -1987,12 +2637,16 @@ 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.
@@ -2002,6 +2656,11 @@ 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.
@@ -2022,6 +2681,10 @@ 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.
 
@@ -2112,7 +2775,43 @@ 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.
+                     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.
 Qed.
 
 Lemma ered_confluence n (a b c : PTm n) :
@@ -2229,16 +2928,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.
@@ -2293,6 +2992,19 @@ 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.
@@ -2301,6 +3013,14 @@ 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.
@@ -2348,6 +3068,14 @@ 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.
@@ -2366,6 +3094,13 @@ 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 ->
@@ -2430,6 +3165,15 @@ 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) ->
@@ -2660,6 +3404,13 @@ 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.
@@ -2722,6 +3473,22 @@ 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.
@@ -2770,6 +3537,48 @@ 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.
@@ -2809,6 +3618,14 @@ 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 52a4438..a245362 100644
--- a/theories/logrel.v
+++ b/theories/logrel.v
@@ -31,6 +31,9 @@ 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)
@@ -68,6 +71,7 @@ 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.
 
@@ -88,14 +92,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)) ->
@@ -107,11 +111,12 @@ 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 hUniv hRed.
+  move => n P  hSN hBind hNat 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.
@@ -144,6 +149,9 @@ 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.
 
@@ -176,6 +184,14 @@ 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.
@@ -202,6 +218,7 @@ 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.
@@ -227,6 +244,7 @@ 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.
 
@@ -238,14 +256,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).
+  exists H, rtc TRedSN A H /\  ⟦ H ⟧ i ↘ PA /\ (SNe H \/ isbind H \/ isuniv H \/ isnat 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.
@@ -262,7 +280,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: 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.
 
 Lemma InterpUniv_SNe_inv n i (A : PTm n) PA :
   SNe A ->
@@ -285,6 +303,14 @@ 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.
@@ -331,7 +357,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 by itauto.
+      suff : ~ isbind H /\ ~ isuniv H /\ ~ isnat H by itauto.
       move : hA hAB. clear. hauto lq:on db:noconf.
       move : InterpUniv_SNe_inv h1 h0. repeat move/[apply]. move => ?. subst.
       tauto.
@@ -341,7 +367,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 by itauto.
+      suff : ~ isbind H /\ ~ isuniv H /\ ~ isnat 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.
@@ -351,7 +377,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 by itauto.
+      suff : ~ SNe H /\ ~ isuniv H /\ ~ isnat H by itauto.
       have : isbind (PBind p A B) by scongruence.
       move : h. clear. hauto l:on db:noconf.
       case : H h1 h => //=.
@@ -370,7 +396,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 by itauto.
+      suff : ~ SNe H /\ ~ isuniv H /\ ~ isnat 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 => //=.
@@ -382,13 +408,36 @@ 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 by tauto. move : h. clear. hauto lq:on db:noconf.
+      suff : ~ SNe H /\ ~ isbind H /\ ~ isnat 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.
@@ -400,7 +449,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 by tauto. move : h. clear. hauto lq:on db:noconf.
+      suff : ~ SNe H /\ ~ isbind H /\ ~ isnat 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.
@@ -634,6 +683,70 @@ 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) :
@@ -683,15 +796,20 @@ 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.
-  move /(_ i) => [j /SemWt_Univ h].
-  rewrite /SemWt => ρ /[dup] hρ {}/h [S hS].
-  exists j, S.
-  asimpl. firstorder.
-Qed.
+Proof. hauto l:on use:ST_Var' unfold:SemWff. Qed.
 
 Lemma InterpUniv_Bind_nopf n p i (A : PTm n) B PA :
   ⟦ A ⟧ i ↘ PA ->
@@ -925,6 +1043,59 @@ 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 Δ ρ.
@@ -942,6 +1113,25 @@ 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 Δ ρ.
@@ -1153,6 +1343,206 @@ 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 ->
@@ -1188,6 +1578,15 @@ 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 ->
@@ -1332,4 +1731,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 : 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 ST_Nat ST_Ind ST_Suc ST_Zero SE_IndCong SE_SucCong SE_IndZero SE_IndSuc SE_SucCong : sem.
diff --git a/theories/preservation.v b/theories/preservation.v
index 6fe081d..b78f87e 100644
--- a/theories/preservation.v
+++ b/theories/preservation.v
@@ -76,6 +76,23 @@ 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.
@@ -108,6 +125,19 @@ 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 ->
@@ -130,6 +160,13 @@ 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.
@@ -170,6 +207,11 @@ 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 2773c3c..c25986c 100644
--- a/theories/structural.v
+++ b/theories/structural.v
@@ -12,6 +12,11 @@ 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 ξ) .
@@ -45,7 +50,10 @@ Proof.
   move E :(PBind p A B) => T h.
   move : p A B E.
   elim : n Γ T U / h => //=.
-  - hauto lq:on ctrs:Wt,LEq,Eq use:Wt_Univ.
+  - 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 rew:off ctrs:LEq.
 Qed.
 
@@ -92,6 +100,25 @@ 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 ->
@@ -103,9 +130,7 @@ 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 ->
@@ -162,6 +187,30 @@ 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 Δ Γ ξ ->
@@ -184,6 +233,22 @@ 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.
@@ -199,6 +264,27 @@ 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].
@@ -216,6 +302,32 @@ 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.
@@ -272,10 +384,6 @@ 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 ->
@@ -291,12 +399,6 @@ 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 ->
@@ -342,6 +444,32 @@ 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.
@@ -359,6 +487,27 @@ 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].
@@ -376,6 +525,34 @@ 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.
@@ -505,6 +682,8 @@ 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.
@@ -535,9 +714,46 @@ 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)
@@ -603,6 +819,7 @@ 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 052eab8..818d6b5 100644
--- a/theories/typing.v
+++ b/theories/typing.v
@@ -42,6 +42,25 @@ 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 ->
@@ -96,6 +115,18 @@ 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 ->
@@ -120,6 +151,19 @@ 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 :
   ⊢ Γ ->