diff --git a/theories/SimplyTypedLambdaCalculus/ChurchRosser.v b/theories/SimplyTypedLambdaCalculus/ChurchRosser.v
index 90c06c6..c16a313 100644
--- a/theories/SimplyTypedLambdaCalculus/ChurchRosser.v
+++ b/theories/SimplyTypedLambdaCalculus/ChurchRosser.v
@@ -12,15 +12,38 @@ Inductive par_red: term -> term -> Prop :=
     App (Lam s) t >=> s'.[t'/]
 
   | ParRed_Var (v: var): (Var v) >=> (Var v)
-    
+
+  | ParRed_0 : Const_0 >=> Const_0
+
+  | ParRed_S (n n' : term):
+             n >=> n'
+             -> Const_S n >=> Const_S n'
+
   | ParRed_App (s s' t t': term) :
     s >=> s' ->
     t >=> t' ->
     App s t >=> App s' t'
-    
+
   | ParRed_Lam (t t': term) :
     t >=> t' ->
     Lam t >=> Lam t'
+
+  | ParRed_R (t0 t0' tn tn' n n' : term) : 
+    t0 >=> t0'
+    -> tn >=> tn'
+    -> n >=> n'
+    -> Rec t0 tn n >=> Rec t0' tn' n'
+
+  | ParRed_R0 (t0 t0' tn : term) :
+    t0 >=> t0'
+    -> Rec t0 tn Const_0 >=> t0'
+
+  | ParRed_RN (t0 t0' tn tn' n n' : term) : 
+    t0 >=> t0'
+    -> tn >=> tn'
+    -> n >=> n'
+    -> Rec t0 tn (Const_S n) >=> App (App tn' n') (Rec t0' tn' n')
+
   where "t >=> t'" := (par_red t t').
 
 Notation "R *" := (clos_refl_trans _ R)
@@ -43,6 +66,17 @@ Fixpoint par_red_max_reduction (t: term): term :=
   | App (Lam t) u => (par_red_max_reduction t).[(par_red_max_reduction u)/]
   | App t u => App (par_red_max_reduction t) (par_red_max_reduction u)
   | Lam t => Lam (par_red_max_reduction t)
+  | Const_0 => Const_0
+  | Const_S n => Const_S (par_red_max_reduction n)
+  | Rec t0 tn (Const_S n) => 
+              App (App (par_red_max_reduction tn) (par_red_max_reduction n))
+                  (Rec (par_red_max_reduction t0)
+                       (par_red_max_reduction tn)
+                       (par_red_max_reduction n))
+  | Rec t0 tn Const_0 => par_red_max_reduction t0
+  | Rec t0 tn n =>  (Rec (par_red_max_reduction t0)
+                       (par_red_max_reduction tn)
+                       (par_red_max_reduction n))
   end.
 
 Definition replace_lambda (f: term -> term) (s u: term): term :=
@@ -60,6 +94,9 @@ Proof.
   - apply ParRed_App; assumption.
   - apply ParRed_Lam.
     assumption.
+  - constructor.
+  - constructor. assumption.
+  - apply ParRed_R; assumption.
 Qed.
 
 Lemma beta_star_refl (t: term):
@@ -110,6 +147,12 @@ Proof.
   - apply ParRed_App; [ apply par_red_refl | assumption ].
   - apply ParRed_Lam.
     assumption.
+  - constructor. assumption.
+  - constructor. apply par_red_refl.
+  - constructor; apply par_red_refl.
+  - constructor; [assumption | apply par_red_refl .. ].
+  - constructor; [apply par_red_refl | assumption | apply par_red_refl].
+  - constructor; [apply par_red_refl .. | assumption ].
 Qed.
 
 Lemma par_red_subst (t t': term) (sigma: var -> term):
@@ -120,19 +163,33 @@ Proof.
   revert sigma.
   induction H as [
     s s' t t' par_red_s_s' IHs par_red_t_t' IHt
-    | v
+    | | | t t' H IH
     | s s' t t' par_red_s_s' IHs par_red_t_t' IHt
     | s s' par_red_s_s' IHs
+    | t0 t0' tn tn' n n' H1 IH1 H2 IH2 H3 IH3
+    | t0 t0' ts H IH
+    | t0 t0' tn tn' n n' H1 IH1 H2 IH2 H3 IH3
   ]; intros sigma.
   - asimpl.
     pose proof (ParRed_Subst s.[up sigma] s'.[up sigma] t.[sigma] t'.[sigma]) as H.
     asimpl in H.
     apply H; [ apply IHs | apply IHt ].
   - apply par_red_refl.
+  - apply par_red_refl.
+  - constructor. apply IH.
   - apply ParRed_App; [ apply IHs | apply IHt ].
   - apply ParRed_Lam.
     asimpl.
     apply IHs.
+  - specialize (IH1 sigma).
+    specialize (IH2 sigma).
+    specialize (IH3 sigma).
+    constructor; assumption.
+  - constructor. apply IH.
+  - specialize (IH1 sigma).
+    specialize (IH2 sigma).
+    specialize (IH3 sigma).
+    constructor; assumption.
 Qed.
 
 Lemma par_red_subst_up_equivalence (sigma sigma': var -> term):
@@ -155,9 +212,12 @@ Proof.
   revert sigma sigma' Hv.
   induction H as [
     s s' t t' _ IHs _ IHt
-    | v
+    | | | n n' H IH
     | s s' t t' _ IHs _ IHt
     | s s' _ IHs
+    | t0 t0' tn tn' n n' H1 IH1 H2 IH2 H3 IH3
+    | t0 t0' ts H IH
+    | t0 t0' tn tn' n n' H1 IH1 H2 IH2 H3 IH3
   ]; intros sigma sigma' Hv.
   - asimpl.
     pose proof (ParRed_Subst s.[up sigma] s'.[up sigma'] t.[sigma] t'.[sigma']) as H.
@@ -168,10 +228,10 @@ Proof.
       assumption.
     + apply IHt.
       assumption.
-  - asimpl.
-    apply Hv.
-  - asimpl.
-    apply ParRed_App.
+  - asimpl. apply Hv.
+  - asimpl. constructor. 
+  - asimpl. constructor. apply IH. apply Hv.
+  - apply ParRed_App.
     + apply IHs.
       assumption.
     + apply IHt.
@@ -181,6 +241,15 @@ Proof.
     apply IHs.
     apply par_red_subst_up_equivalence.
     assumption.
+  - specialize (IH1 sigma sigma' Hv).
+    specialize (IH2 sigma sigma' Hv).
+    specialize (IH3 sigma sigma' Hv).
+    asimpl. constructor; assumption.
+  - asimpl. constructor. apply IH. apply Hv.
+  - specialize (IH1 sigma sigma' Hv).
+    specialize (IH2 sigma sigma' Hv).
+    specialize (IH3 sigma sigma' Hv).
+    asimpl. constructor; assumption.
 Qed.
 
 Lemma beta_star_app_r (s s' t: term):
@@ -233,24 +302,83 @@ Proof.
       assumption.
 Qed. 
 
+(* TODO: generalize
+Inductive sub_term: term -> term -> Prop :=
+  | Sub_app1 (t1 t2: term) : sub_term t1 (App t1 t2)
+  | Sub_app2 (t1 t2: term) : sub_term t2 (App t1 t2)
+  | Sub_lam (t: term) : sub_term t (Lam t)
+  | Sub_S (s : term) : sub_term s (Const_S s)
+  | Sub_R0 (t0 ts n: term) : sub_term t0 (Rec t0 ts n)
+  | Sub_RS (t0 ts n: term) : sub_term ts (Rec t0 ts n)
+  | Sub_RN (t0 ts n: term) : sub_term n (Rec t0 ts n).
+*)
+
 Lemma beta_star_lam (s s': term):
   s ~>* s' ->
   Lam s ~>* Lam s'.
 Proof.
   intros beta_star_s_s'.
   induction beta_star_s_s' as [ s s' H | x | x y z IHxy IHAppxy IHyz IHAppyz ].
-  - induction H; apply rt_step, Beta_Lam.
-    + apply Beta_Subst.
-      assumption.
-    + apply Beta_AppL.
-      assumption.
-    + apply Beta_AppR.
-      assumption.
-    + apply Beta_Lam.
-      assumption.
+  - induction H; apply rt_step, Beta_Lam; constructor; assumption.
   - apply rt_refl.
   - apply rt_trans with (y := Lam y); assumption.
-Qed. 
+Qed.
+
+Lemma beta_star_const (s s': term):
+  s ~>* s' ->
+  Const_S s ~>* Const_S s'.
+Proof.
+  intros beta_star_s_s'.
+  induction beta_star_s_s' as [ s s' H | x | x y z IHxy IHAppxy IHyz IHAppyz ].
+  - induction H; apply rt_step; constructor; constructor; assumption.
+  - apply rt_refl.
+  - apply rt_trans with (y := Const_S y); assumption.
+Qed.
+
+Lemma beta_star_R0 (t0 t0' tn n: term):
+  t0 ~>* t0' ->
+  Rec t0 tn n ~>* Rec t0' tn n.
+Proof.
+ intros H.
+ induction H.
+ * apply rt_step. constructor. assumption.
+ * apply rt_refl.
+ * apply rt_trans with (y := Rec y tn n); assumption.
+Qed.
+
+Lemma beta_star_RS (t0 tn tn' n: term):
+  tn ~>* tn' ->
+  Rec t0 tn n ~>* Rec t0 tn' n.
+Proof.
+ intros H.
+ induction H as [ | | ? y ].
+ * apply rt_step. constructor. assumption.
+ * apply rt_refl.
+ * apply rt_trans with (y := Rec t0 y n); assumption.
+Qed.
+
+Lemma beta_star_RN (t0 tn n n': term):
+  n ~>* n' ->
+  Rec t0 tn n ~>* Rec t0 tn n'.
+Proof.
+ intros H.
+ induction H as [ | | ? y ].
+ * apply rt_step. constructor. assumption.
+ * apply rt_refl.
+ * apply rt_trans with (y := Rec t0 tn y); assumption.
+Qed.
+
+Lemma beta_star_R (t0 t0' tn tn' n n': term):
+  t0 ~>* t0' ->
+  tn ~>* tn' ->
+  n ~>* n' ->
+  Rec t0 tn n ~>* Rec t0' tn' n'.
+Proof.
+  intros.
+  apply rt_trans with (y := Rec t0' tn' n); [| apply beta_star_RN; assumption].
+  apply rt_trans with (y := Rec t0' tn n); [| apply beta_star_RS; assumption].
+  apply beta_star_R0; assumption.
+Qed.
 
 Lemma par_red_to_beta_star (s t : term):
   s >=> t -> s ~>* t.
@@ -258,9 +386,12 @@ Proof.
   intros H.
   induction H as [
     s s' t t' _ beta_star_s_s' _ beta_star_t_t'
-    | v
+    | | | n n' H IH
     | s s' t t' _ beta_star_s_s' _ beta_star_t_t'
     | s s' _ beta_star_s_s'
+    | t0 t0' tn tn' n n' H1 IH1 H2 IH2 H3 IH3
+    | t0 t0' ts H IH
+    | t0 t0' tn tn' n n' H1 IH1 H2 IH2 H3 IH3
   ].
   - apply rt_trans with (y := App (Lam s') t).
     + apply beta_star_app.
@@ -273,9 +404,18 @@ Proof.
         apply Beta_Subst.
         reflexivity.
   - apply rt_refl.
+  - apply rt_refl.
+  - apply beta_star_const. assumption. 
   - apply beta_star_app; assumption.
   - apply beta_star_lam.
     assumption.
+  - apply beta_star_R; assumption.
+  - apply rt_trans with (y := Rec t0' ts Const_0).
+      * apply beta_star_R0. assumption.
+      * apply rt_step. constructor.
+  - apply rt_trans with (y := Rec t0' tn' (Const_S n')).
+      * apply beta_star_R; [ | | apply beta_star_const]; assumption.
+      * apply rt_step. constructor.
 Qed.
 
 Lemma beta_star_equiv_par_red_star (s t: term):
@@ -302,23 +442,16 @@ Lemma lam_match : forall (s u : term) (f : term -> term),
   ((replace_lambda f s u) = u /\ ~exists s', s = Lam s').
 Proof.
   intros s u f.
-  destruct s as [ n | s1 s2 | s ].
-  - right.
-    split.
-    + simpl.
-      reflexivity.
-    + intros [ t eq_t ].
-      discriminate.
-  - right.
+  destruct s as [ | | s | | | ].
+  3:{
     simpl.
-    split.
-    + reflexivity.
-    + intros [ t eq_t ].
-      discriminate.
-  - simpl.
     left.
     exists s.
     split; reflexivity.
+  }
+  all: right.
+  all: simpl.
+  all: split; [reflexivity | intros [ ? ? ]; discriminate].
 Qed.
 
 Lemma max_par_red (t t': term):
@@ -327,9 +460,9 @@ Proof.
   intros Ht.
   induction Ht as [
     s s' t t' _ IHs _ IHt
-    | v
+    | | |
     | s s' t t' par_red_s_s' IHs _ IHt
-    | s s' _ IHs
+    | s s' _ IHs | | |
   ]; asimpl.
   - apply par_red_subst_par_red.
     + intros v.
@@ -339,22 +472,38 @@ Proof.
       * asimpl.
         apply par_red_refl.
     + assumption.
-  - apply par_red_refl.
+  - constructor.
+  - constructor.
+  - constructor; assumption.
   - set (f := fun s' => (par_red_max_reduction s').[par_red_max_reduction t/]).
     destruct (lam_match s (App (par_red_max_reduction s) (par_red_max_reduction t)) f) as [ [ u [ H1 H2 ] ] | [ H1 H2 ] ]; subst.
     + inversion par_red_s_s'; subst.
       inversion IHs; subst.
       apply ParRed_Subst; assumption.
-    + destruct s as [ n | s1 s2 | s ]; simpl in IHs.
-      * simpl.
-        apply ParRed_App; assumption.
-      * apply ParRed_App; assumption.
-      * exfalso.
+    + destruct s as [ n | s1 s2 | s | | | ]; simpl in IHs.
+      3:{
+        exfalso.
         apply H2.
         exists s.
         reflexivity.
-  - apply ParRed_Lam.
-    assumption.
+      }
+      all: simpl in *; constructor; assumption.
+  - constructor; assumption.
+  - destruct n.
+    + simpl in *; constructor; assumption.
+    + simpl in *; constructor; assumption.
+    + simpl in *; constructor; assumption.
+    + inversion Ht3; subst.
+      apply ParRed_R0.
+      assumption.
+    + inversion Ht3; subst.
+      apply ParRed_RN; [ assumption .. | ].
+      inversion IHHt3; subst; assumption.
+    + simpl in *; constructor; assumption.
+  - assumption.
+  - constructor.
+    + constructor; assumption.
+    + constructor; assumption.
 Qed.
 
 Lemma local_confluence_par_red: local_confluence par_red.
diff --git a/theories/SimplyTypedLambdaCalculus/Definitions.v b/theories/SimplyTypedLambdaCalculus/Definitions.v
index c810024..8c9a8f0 100644
--- a/theories/SimplyTypedLambdaCalculus/Definitions.v
+++ b/theories/SimplyTypedLambdaCalculus/Definitions.v
@@ -5,7 +5,10 @@ From Autosubst Require Export Autosubst.
 Inductive term : Type :=
   | Var (n: var)
   | App (s t: term)
-  | Lam (s: {bind term}).
+  | Lam (s: {bind term})
+  | Const_0
+  | Const_S (s: term)
+  | Rec   (t0 tn n: term).
 
 Instance Ids_term: Ids term. derive. Defined.
 Instance Rename_term: Rename term. derive. Defined.
@@ -20,6 +23,12 @@ Inductive beta: term -> term -> Prop :=
   | Beta_AppL (s s' t: term): s ~> s' -> App s t ~> App s' t
   | Beta_AppR (s t t': term): t ~> t' -> App s t ~> App s t'
   | Beta_Lam (s s': term): s ~> s' -> Lam s ~> Lam s'
+  | Beta_S (s s': term): s ~> s' -> Const_S s ~> Const_S s'
+  | Beta_R0 (t0 tn : term): Rec t0 tn Const_0 ~> t0
+  | Beta_RS (t0 tn n : term): Rec t0 tn (Const_S n) ~> (App (App tn n) (Rec t0 tn n))
+  | Beta_RI0 (t0 t0' tn n : term): t0 ~> t0' -> Rec t0 tn n ~> Rec t0' tn n
+  | Beta_RIS (t0 tn tn' n : term): tn ~> tn' -> Rec t0 tn n ~> Rec t0 tn' n
+  | Beta_RIN (t0 tn n n': term): n ~> n' -> Rec t0 tn n ~> Rec t0 tn n'
   where "t ~> t'" := (beta t t').
 
 
@@ -28,7 +37,7 @@ Lemma beta_subst (t t': term) (σ: var -> term):
 Proof.
   revert t' σ.
 
-  induction t as [ | ? IHs ? IHt | s IHs ].
+  induction t as [ | ? IHs ? IHt | s IHs | | | ? IH1 ? IH2 ? IH3].
   - inversion 1.
 
   - inversion 1; subst; simpl.
@@ -48,11 +57,29 @@ Proof.
     apply Beta_Lam.
     apply IHs.
     assumption.
+
+  (* zero is a constant and does not reduce *)
+  - inversion 1.
+
+  (* case: S n *)
+  - inversion 1; subst.
+    apply Beta_S. apply IHt. assumption.
+    
+
+  (* case: R operator *)
+  - inversion 1; subst; simpl.
+    + apply Beta_R0.
+    + apply Beta_RS.
+    + apply Beta_RI0. apply IH1. assumption.
+    + apply Beta_RIS. apply IH2. assumption.
+    + apply Beta_RIN. apply IH3. assumption.
+    
 Qed.
 
 
 Inductive type :=
   | Base
+  | Nat
   | Arr (A B: type).
 
 Reserved Notation "Γ ⊢ t : A" (at level 60, t at next level).
@@ -69,6 +96,15 @@ Inductive typing (Γ: var -> type): term -> type -> Prop :=
   | Typing_Lam (s: term) (A B: type):
       A .: Γ ⊢ s : B ->
       Γ ⊢ Lam s : Arr A B
+
+  | Typing_0: Γ ⊢ Const_0 : Nat
+  | Typing_S (n: term): Γ ⊢ n : Nat -> Γ ⊢ (Const_S n) : Nat
+
+  | Typing_R (t0 ts n: term) (A: type):
+      Γ ⊢ t0 : A
+      -> Γ ⊢ ts : (Arr Nat (Arr A A))
+      -> Γ ⊢ n : Nat
+      -> Γ ⊢ Rec t0 ts n : A
   where "Γ ⊢ t : A" := (typing Γ t A).
 
 Lemma type_weakening (Γ: var -> type) (s: term) (A: type):
@@ -76,7 +112,12 @@ Lemma type_weakening (Γ: var -> type) (s: term) (A: type):
     forall (Γ': var -> type) (x': var -> var),
       Γ = x' >>> Γ' -> Γ' ⊢ s.[ren x'] : A.
 Proof.
-  induction 1 as [ ? ? ? H | ? ? ? A ? _ IH1 _ IH2 | ? ? ? ? _ IH ]; intros ? ? H'; simpl.
+  induction 1 as [ ? ? ? H 
+                 | ? ? ? A ? _ IH1 _ IH2
+                 | ? ? ? ? _ IH
+                 |
+                 | ? ? ? IH
+                 | ? ? ? ? ? ? IH1 ? IH2 ? IH3]; intros ? ? H'; simpl.
   - apply Typing_Var.
     rewrite H' in H; simpl in H.
     assumption.
@@ -88,6 +129,13 @@ Proof.
   - apply Typing_Lam; asimpl.
     apply IH.
     now rewrite H'; asimpl.
+
+  - apply Typing_0.
+  - apply Typing_S. apply IH. assumption.
+  - apply Typing_R.
+    + apply IH1. assumption.
+    + apply IH2. assumption.
+    + apply IH3. assumption.
 Qed.
 
 Lemma type_subst (Γ Γ': var -> type) (s: term) (A: type) (σ: var -> term):
@@ -97,8 +145,9 @@ Lemma type_subst (Γ Γ': var -> type) (s: term) (A: type) (σ: var -> term):
 Proof.
   revert Γ Γ' A σ.
 
-  induction s as [ | ? IH1 ? IH2 | ? IH ]; intros Γ Γ' ? ? HΓ HΓ'; simpl.
-  all: inversion HΓ as [ | ? ? A' | ? A' ]; subst.
+  induction s as [ | ? IH1 ? IH2 | ? IH | | | ? IH1 ? IH2 ? IH3];
+    intros Γ Γ' ? ? HΓ HΓ'; simpl.
+  all: inversion HΓ as [ | ? ? A' | ? A' | | | ]; subst.
 
   - apply HΓ'.
   - apply Typing_App with A'.
@@ -109,35 +158,45 @@ Proof.
     intros [| x ]; asimpl.
     + now apply Typing_Var.
     + now apply type_weakening with Γ'.
+  - apply Typing_0.
+  - apply Typing_S. apply IHs with (Γ := Γ). all: assumption.
+  - apply Typing_R.
+    + apply IH1 with (Γ := Γ). all: assumption.
+    + apply IH2 with (Γ := Γ). all: assumption.
+    + apply IH3 with (Γ := Γ). all: assumption.
 Qed.
 
+(* subject reduction *)
 Lemma type_preservation (Γ: var -> type) (s t: term) (A: type):
   Γ ⊢ s : A -> s ~> t -> Γ ⊢ t : A.
 Proof.
   revert Γ t A.
 
-  induction s as [ | ? IH1 ? IH2 | ? IH ]; intros Γ ? ? HΓ HΓ'; asimpl.
+  induction s as [ | ? IH1 ? IH2 | ? IH | | | ]; intros Γ ? ? HΓ HΓ'; asimpl.
   all: inversion HΓ; subst.
-  all: inversion HΓ' as [ s' | | | ]; subst.
-
-  all: match goal with
-       | H: _ ⊢ _ : Arr ?A _ |- _ => rename A into A'
-       end.
-
-  - match goal with
-    | H: Γ ⊢ Lam s' : _ |- _ => inversion H; subst
-    end.
-
-    apply type_subst with (A' .: Γ); [ assumption |].
-    intros [| x ]; asimpl; [ assumption |].
+  all: inversion HΓ'; subst.
+  - inversion H1. subst.
+    apply type_subst with (A0 .: Γ); [assumption |].
+    intros [|x]; asimpl; [assumption |].
     now apply Typing_Var.
-
-  - apply Typing_App with A'; [| assumption ].
-    now apply IH1.
-
-  - apply Typing_App with A'; [ assumption |].
-    now apply IH2.
-
-  - apply Typing_Lam.
-    now apply IH.
+  - apply Typing_App with (A := A0); [| assumption].
+    apply IH1. all: assumption.
+  - apply Typing_App with (A := A0); [assumption |].
+    apply IH2. all: assumption.
+  - inversion HΓ'; subst. apply Typing_Lam. apply IH. all: assumption.
+
+  - apply Typing_S. apply IHs. all: assumption. 
+
+  - clear IHs3. assumption.
+
+  - clear IHs3. inversion H5; subst.
+    apply Typing_App with (A := A).
+    + apply Typing_App with (A := Nat); assumption.
+    + apply Typing_R; assumption.
+  - apply Typing_R; [ | assumption .. ].
+    apply IHs1; assumption.
+  - apply Typing_R; [assumption | | assumption].
+    apply IHs2; assumption.
+  - apply Typing_R; [ assumption | assumption |].
+    apply IHs3; assumption.
 Qed.
diff --git a/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v b/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v
index b4b3a97..bf3197a 100644
--- a/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v
+++ b/theories/SimplyTypedLambdaCalculus/StrongNormalisation.v
@@ -1,5 +1,5 @@
 From FormArith.SimplyTypedLambdaCalculus Require Import Definitions.
-
+From Coq Require Import  Lia .
 
 Inductive SN: term -> Prop :=
   | Strong (t: term) :
@@ -7,21 +7,24 @@ Inductive SN: term -> Prop :=
 
 Fixpoint reducible (A: type) (t: term): Prop :=
   match A with
-  | Base => SN t
+  | Base | Nat => SN t
   | Arr A B => forall (u: term), reducible A u -> reducible B (App t u)
   end.
 
 Definition neutral (t: term): Prop :=
   match t with
-  | Lam _ => False
+  | Lam _ | Const_0 | Const_S _ => False
   | _ => True
   end.
 
 Inductive sub_term: term -> term -> Prop :=
   | Sub_app1 (t1 t2: term) : sub_term t1 (App t1 t2)
   | Sub_app2 (t1 t2: term) : sub_term t2 (App t1 t2)
-  | Sub_lam (t: term) : sub_term t (Lam t).
-
+  | Sub_lam (t: term) : sub_term t (Lam t)
+  | Sub_S (s : term) : sub_term s (Const_S s)
+  | Sub_R0 (t0 ts n: term) : sub_term t0 (Rec t0 ts n)
+  | Sub_RS (t0 ts n: term) : sub_term ts (Rec t0 ts n)
+  | Sub_RN (t0 ts n: term) : sub_term n (Rec t0 ts n).
 
 Lemma SN_lam (t: term):
   SN t -> SN (Lam t).
@@ -34,6 +37,17 @@ Proof.
   now apply H.
 Qed.
 
+Lemma SN_S (t: term):
+  SN t -> SN (Const_S t).
+Proof.
+  revert t.
+
+  apply SN_ind; intros ? _ H.
+  apply Strong; intros ? Hbeta.
+  inversion Hbeta; subst.
+  now apply H.
+Qed.
+
 Lemma SN_sub_term (t: term):
   SN t -> forall (t': term), sub_term t' t -> SN t'.
 Proof.
@@ -46,17 +60,40 @@ Proof.
        | H: _ |- _ => idtac
        end.
 
+  (* case: Sub_app1 *)
   - apply IH with (App u t2).
     + now apply Beta_AppL.
     + apply Sub_app1.
 
+  (* case: Sub_app2 *)
   - apply IH with (App t1 u).
     + now apply Beta_AppR.
     + apply Sub_app2.
 
+  (* case: Sub_lam *)
   - apply IH with (Lam u).
     + now apply Beta_Lam.
     + apply Sub_lam.
+
+  (* case: Sub_S *)
+  - apply IH with (Const_S u).
+    + now apply Beta_S.
+    + apply Sub_S.
+
+  (* case: Sub_R0 *)
+  - apply IH with (Rec u ts n).
+    + now apply Beta_RI0.
+    + apply Sub_R0.
+
+  (* case: Sub_RS *)
+  - apply IH with (Rec t0 u n).
+    + now apply Beta_RIS.
+    + apply Sub_RS.
+
+  (* case: Sub_RN *)
+  - apply IH with (Rec t0 ts u).
+    + now apply Beta_RIN.
+    + apply Sub_RN.
 Qed.
 
 Lemma SN_var_app (t: term) (n: var):
@@ -73,12 +110,25 @@ Proof.
   now inversion 1.
 Qed.
 
+
+
 Lemma reducible_is_SN (A : type):
   (forall (t: term), reducible A t -> SN t) /\
     (forall (t u: term), reducible A t -> t ~> u -> reducible A u) /\
     (forall (t: term), neutral t -> (forall (t': term), t ~> t' -> reducible A t') -> reducible A t).
 Proof.
-  induction A as [ | A [IHA1 [IHA2 IHA3]] B [IHB1 [IHB2 IHB3]] ].
+  induction A as [ | | A [IHA1 [IHA2 IHA3]] B [IHB1 [IHB2 IHB3]] ].
+  - do 3 split.
+    + intros.
+      apply SN_inverted with t'; [| assumption ].
+      now apply SN_inverted with t.
+
+    + intros.
+      apply SN_inverted with u; [| assumption ].
+      now apply SN_inverted with t.
+
+    + assumption.
+
   - do 3 split.
     + intros.
       apply SN_inverted with t'; [| assumption ].
@@ -120,6 +170,22 @@ Proof.
         now apply IHA2 with u.
 Qed.
 
+Lemma reducible_CR1 (A : type) (t: term): reducible A t -> SN t.
+Proof.
+apply reducible_is_SN.
+Qed.
+
+Lemma reducible_CR2 (A : type) (t u: term): reducible A t -> t ~> u -> reducible A u.
+Proof.
+apply reducible_is_SN.
+Qed.
+
+Lemma reducible_CR3 (A: type) (t: term):
+  neutral t -> (forall (t': term), t ~> t' -> reducible A t') -> reducible A t.
+Proof.
+apply reducible_is_SN.
+Qed.
+
 Lemma SN_subst (t: term) (σ: var -> term):
   SN t -> forall (u: term), t = u.[σ] -> SN u.
 Proof.
@@ -134,8 +200,11 @@ Proof.
 Qed.
 
 Lemma SN_ind_pair (P : term -> term -> Prop):
-  (forall t u, (forall t' u', ((t = t' /\ u ~> u') \/ (t ~> t' /\ u = u')) -> P t' u') -> P t u)
-    -> forall t u, SN t -> SN u -> P t u.
+  (forall t u,
+    (forall t' u', ((t = t' /\ u ~> u') \/ (t ~> t' /\ u = u'))
+                   -> P t' u')
+    -> P t u)
+  -> forall t u, SN t -> SN u -> P t u.
 Proof.
   intros IH ? ? Hsnt.
   revert u.
@@ -152,8 +221,83 @@ Proof.
     now apply Strong.
 Qed.
 
+Lemma SN_double_ind (P : term -> term -> Prop):
+    (forall s t,
+      (forall s', s ~> s' -> P s' t)
+      -> (forall t', t ~> t' -> P s t') -> P s t)
+    -> forall s t, SN s -> SN t -> P s t.
+Proof.
+  intros IH s t Hs.
+  revert t. induction Hs as [s Hs1 Hs2].
+  apply Strong in Hs1.
+  intros t Ht. induction Ht as [t Ht1 Ht2].
+  apply Strong in Ht1.
+  apply IH.
+  - intros. apply Hs2. all: assumption.
+  - intros. apply Ht2. all: assumption.
+Qed.
+
+Lemma SN_triple_ind (P : term -> term -> term -> Prop):
+    (forall s t u,
+      (forall s', s ~> s' -> P s' t u)
+      -> (forall t', t ~> t' -> P s t' u)
+      -> (forall u', u ~> u' -> P s t u') -> P s t u)
+    -> forall s t u, SN s -> SN t -> SN u -> P s t u.
+Proof.
+  intros IH s t u Hs.
+  revert t u. induction Hs as [s Hs1 Hs2].
+  apply Strong in Hs1.
+  intros t u Ht.
+  revert u. induction Ht as [t Ht1 Ht2].
+  apply Strong in Ht1.
+  intros u Hu. induction Hu as [u Hu1 Hu2].
+  apply Strong in Hu1.
+  apply IH.
+  - intros. apply Hs2. all: assumption.
+  - intros. apply Ht2. all: assumption.
+  - intros. apply Hu2. all: assumption.
+Qed.
+
+(*
+Inductive SN: term -> Prop :=
+  | Strong (t: term) :
+      (forall (t': term), t ~> t' -> SN t') -> SN t.
+*)
+
+Lemma reducible_Rec (t0 ts n : term) (A: type):
+  reducible A t0 
+  -> reducible (Arr Nat (Arr A A)) ts
+  -> reducible Nat n
+  -> reducible A (Rec t0 ts n).
+Proof.
+intros Hrt0 Hrts Hrn.
+apply reducible_CR1 in Hrt0 as Hsnt0.
+apply reducible_CR1 in Hrts as Hsnts.
+apply reducible_CR1 in Hrn as Hsnn.
+revert Hrn Hrts Hrt0.
+apply SN_triple_ind with (s := t0) (t := ts) (u := n); [ | assumption .. ].
+clear Hsnt0 Hsnts Hsnn.
+clear t0 ts n.
+intros t0 ts n Ht0' Hts' Hn' Hn Hts Ht0.
+
+apply reducible_CR3; [now simpl |].
+fix aaa 1.
+inversion 1; subst.
+  - assumption.
+  - simpl in Hts. apply Hts.
+    ** apply SN_sub_term with (t := Const_S n0); [apply Hn | constructor].
+    ** admit.
+  - apply Ht0'; try assumption.
+    apply reducible_CR2 with (t := t0); assumption.
+  - apply Hts'. all: try assumption.
+    apply reducible_CR2 with (t := ts); assumption.
+  - apply Hn'; try assumption.
+    apply reducible_CR2 with (t := n); assumption.
+Admitted.
+
 Lemma reducible_abs (v: term) (A B: type):
-  (forall (u: term), reducible A u -> reducible B v.[u/]) -> reducible (Arr A B) (Lam v).
+  (forall (u: term), reducible A u -> reducible B v.[u/]) 
+  -> reducible (Arr A B) (Lam v).
 Proof.
   intros Hred u Hredu.
   specialize (reducible_is_SN A) as [HA1 [HA2 HA3]].
@@ -198,13 +342,26 @@ Lemma reducible_var (A: type) (x: var) (Γ: var -> type):
 Proof.
   intros.
   destruct A.
-  - simpl.
-    apply Strong.
-    inversion 1.
+  - simpl. apply Strong. inversion 1.
+  - simpl. apply Strong. inversion 1.
   - apply reducible_is_SN; [ exact I |].
     inversion 1.
 Qed.
 
+(*
+Lemma size_recursion (X : Type) (sigma : X -> nat) (p : X -> Type) :
+  (forall x, (forall y, sigma y < sigma x -> p y) -> p x) ->
+  forall x, p x.
+Proof.
+  intros D x. apply D.
+  cut (forall n y, sigma y < n -> p y); [now eauto |].
+  clear x. intros n.
+  induction n; intros y E.
+  - exfalso. inversion E.
+  - apply D. intros x F. apply IHn. lia.
+Defined.
+*)
+
 Lemma typing_is_reducible (Γ: var -> type) (σ: var -> term):
   (forall (x: var), reducible (Γ x) (σ x)) ->
     forall (A: type) (t: term), Γ ⊢ t : A -> reducible A t.[σ].
@@ -217,17 +374,33 @@ Proof.
   all: inversion 1; subst; simpl.
 
   - apply Hred.
+
   - apply IHt1 with (σ := σ) in H2; [| assumption ].
     apply IHt2 with (σ := σ) in H4; [| assumption ].
     now apply H2.
+
   - apply reducible_abs.
     intros u Hredu. asimpl.
     apply IHt with (A0 .: Γ); [| assumption ].
     intros [| x ]; simpl; [ assumption |].
     apply Hred.
+
+  (* case: Const_0 *)
+  - apply Strong. inversion 1.
+
+  (* case: Const_S *)
+  - specialize (IHt σ Nat Γ Hred H1).
+    simpl in IHt.
+    now apply SN_S.
+
+  (* case: Rec *)
+  - specialize (IHt1 σ A Γ Hred H3).
+    specialize (IHt2 σ (Arr Nat (Arr A A)) Γ Hred H5).
+    specialize (IHt3 σ Nat Γ Hred H6).
+    apply reducible_Rec. all: assumption.
 Qed.
 
-Corollary STLC_is_SN (A: type) (Γ: var -> type) (t: term):
+Corollary ST_is_SN (A: type) (Γ: var -> type) (t: term):
   Γ ⊢ t : A -> SN t.
 Proof.
   intros.