diff --git a/theories/Core/Syntactic/CtxEquiv.v b/theories/Core/Syntactic/CtxEquiv.v
index 1d788d3d..6d99fcf6 100644
--- a/theories/Core/Syntactic/CtxEquiv.v
+++ b/theories/Core/Syntactic/CtxEquiv.v
@@ -5,58 +5,91 @@ Require Import Syntactic.Syntax.
 Require Import Syntactic.System.
 Require Import Syntactic.SystemLemmas.
 
-Lemma ctxeq_tm : forall {Γ Δ t T}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢ t : T }} -> {{ Δ ⊢ t : T }}
+#[local]
+Ltac gen_ctxeq_helper_IH ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper H :=
+  match type of H with
+  | {{ ?Γ ⊢ ?M : ?A }} => pose proof ctxeq_exp_helper _ _ _ H
+  | {{ ?Γ ⊢ ?M ≈ ?N : ?A }} => pose proof ctxeq_exp_eq_helper _ _ _ _ H
+  | {{ ?Γ ⊢s ?σ : ?Δ }} => pose proof ctxeq_sub_helper _ _ _ H
+  | {{ ?Γ ⊢s ?σ ≈ ?τ : ?Δ }} => pose proof ctxeq_sub_eq_helper _ _ _ _ H
+  | _ => idtac
+  end.
+
+Lemma ctxeq_exp_helper : forall {Γ M A}, {{ Γ ⊢ M : A }} -> ∀ {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢ M : A }}
 with
-ctxeq_eq : forall {Γ Δ t t' T}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢ t ≈ t' : T }} -> {{ Δ ⊢ t ≈ t' : T }}
+ctxeq_exp_eq_helper : forall {Γ M M' A}, {{ Γ ⊢ M ≈ M' : A }} -> ∀ {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢ M ≈ M' : A }}
 with
-ctxeq_s : forall {Γ Γ' Δ σ}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢s σ : Γ' }} -> {{ Δ ⊢s σ : Γ' }}
+ctxeq_sub_helper : forall {Γ Γ' σ}, {{ Γ ⊢s σ : Γ' }} -> ∀ {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢s σ : Γ' }}
 with
-ctxeq_s_eq : forall {Γ Γ' Δ σ σ'}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢s σ ≈ σ' : Γ' }} -> {{ Δ ⊢s σ ≈ σ' : Γ' }}.
-Proof with mauto.
-  (*ctxeq_tm*)
-  - clear ctxeq_tm.
-    intros * HΓΔ Ht.
-    gen Δ.
-    induction Ht; intros; destruct (presup_ctx_eq HΓΔ)...
-    -- pose proof (IHHt1 _ HΓΔ).
-       assert ({{ ⊢ Γ , A ≈ Δ , A }})...
-    -- destruct (var_in_eq HΓΔ H0) as [T' [i [xT'G [GTT' DTT']]]].
-       eapply wf_conv...
-    -- assert ({{ ⊢ Γ , A ≈ Δ , A }}); mauto 6.
-    -- pose proof (IHHt1 _ HΓΔ).
-       assert ({{ ⊢ Γ , A ≈ Δ , A }})...
-  (*ctxeq_eq*)
-  - clear ctxeq_eq.
-    intros * HΓΔ Htt'.
-    gen Δ.
-    induction Htt'; intros; destruct (presup_ctx_eq HΓΔ).
-    1-4,6-19: mauto.
-    -- pose proof (IHHtt'1 _ HΓΔ).
-       pose proof (ctxeq_tm _ _ _ _ HΓΔ H).
-       assert ({{ ⊢ Γ , M ≈ Δ , M }})...
-    -- inversion_clear HΓΔ.
-       pose proof (var_in_eq H3 H0) as [T'' [n [xT'' [GTT'' DTT'']]]].
-       destruct (presup_ctx_eq H3).
-       eapply wf_eq_conv...
-    -- pose proof (var_in_eq HΓΔ H0) as [T'' [n [xT'' [GTT'' DTT'']]]].
-       eapply wf_eq_conv...
-  (*ctxeq_s*)
-  - clear ctxeq_s.
-    intros * HΓΔ Hσ.
-    gen Δ.
-    induction Hσ; intros; destruct (presup_ctx_eq HΓΔ)...
+ctxeq_sub_eq_helper : forall {Γ Γ' σ σ'}, {{ Γ ⊢s σ ≈ σ' : Γ' }} -> ∀ {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢s σ ≈ σ' : Γ' }}.
+Proof with solve [mauto].
+  (* ctxeq_exp_helper *)
+  - intros * HM * HΓΔ. gen Δ.
+    inversion_clear HM; (on_all_hyp: gen_ctxeq_helper_IH ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper); clear ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper; intros; destruct (presup_ctx_eq HΓΔ); mauto.
+    all: try (rename B into C); try (rename A0 into B).
+    2-4: assert {{ Δ ⊢ B : Type@i }} as HB by eauto.
+    2-4: assert {{ ⊢ Γ, B ≈ Δ, B }} by mauto; clear HB.
+    2-3: solve [mauto].
+
+    + assert {{ ⊢ Γ, ℕ ≈ Δ, ℕ }} by (econstructor; mauto).
+      assert {{ Δ, ℕ ⊢ B : Type@i }} by mauto.
+      econstructor...
+
+    + econstructor...
+
+    + assert (∃ B i, {{ #x : B ∈ Δ }} ∧ {{ Γ ⊢ A ≈ B : Type@i }} ∧ {{ Δ ⊢ A ≈ B : Type@i }}) as [? [? [? [? ?]]]]...
+
+  (* ctxeq_exp_eq_helper *)
+  - intros * HMM' * HΓΔ. gen Δ.
+    inversion_clear HMM'; (on_all_hyp: gen_ctxeq_helper_IH ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper); clear ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper; intros; destruct (presup_ctx_eq HΓΔ); mauto.
+    all: try (rename B into C); try (rename B' into C'); try (rename A0 into B); try (rename A' into B').
+    1-3: assert {{ ⊢ Γ, ℕ ≈ Δ, ℕ }} by (econstructor; mauto).
+    1-3: assert {{ Δ, ℕ ⊢ B : Type@i }} by eauto.
+    1-3: econstructor...
+    1-5: assert {{ Δ ⊢ B : Type@i }} by eauto.
+    1-5: assert {{ ⊢ Γ, B ≈ Δ, B }}...
+
+    + assert (∃ B i, {{ #x : B ∈ Δ }} ∧ {{ Γ ⊢ A ≈ B : Type@i }} ∧ {{ Δ ⊢ A ≈ B : Type@i }}) as [? [? [? [? ?]]]]...
+
+    + inversion_clear HΓΔ as [|? Δ0 ? ? C'].
+      assert (∃ D i', {{ #x : D ∈ Δ0 }} ∧ {{ Γ0 ⊢ B ≈ D : Type@i' }} ∧ {{ Δ0 ⊢ B ≈ D : Type@i' }}) as [D [i0 [? [? ?]]]] by mauto.
+      assert {{ Δ0, C' ⊢ B[Wk] ≈ D[Wk] : Type @ i0 }}...
+
+  (* ctxeq_sub_helper *)
+  - intros * Hσ * HΓΔ. gen Δ.
+    inversion_clear Hσ; (on_all_hyp: gen_ctxeq_helper_IH ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper); clear ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper; intros; destruct (presup_ctx_eq HΓΔ); mauto.
     inversion_clear HΓΔ.
     econstructor...
-  (*ctxeq_s_eq*)
-  - clear ctxeq_s_eq.
-    intros * HΓΔ Hσσ'.
-    gen Δ.
-    induction Hσσ'; intros; destruct (presup_ctx_eq HΓΔ).
-    3-9,11-13: mauto.
-    -- inversion_clear HΓΔ; eapply wf_sub_eq_conv...
-    -- inversion_clear HΓΔ; eapply wf_sub_eq_conv...
-    -- econstructor. eapply ctxeq_s...
+
+  (* ctxeq_sub_eq_helper *)
+  - intros * Hσσ' * HΓΔ. gen Δ.
+    inversion_clear Hσσ'; (on_all_hyp: gen_ctxeq_helper_IH ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper); clear ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper; intros; destruct (presup_ctx_eq HΓΔ); mauto.
+    inversion_clear HΓΔ.
+    eapply wf_sub_eq_conv...
+
+  Unshelve.
+  all: constructor.
+Qed.
+
+Lemma ctxeq_exp : forall {Γ Δ M A}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢ M : A }} -> {{ Δ ⊢ M : A }}.
+Proof.
+  eauto using ctxeq_exp_helper.
+Qed.
+
+Lemma ctxeq_exp_eq : forall {Γ Δ M M' A}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢ M ≈ M' : A }} -> {{ Δ ⊢ M ≈ M' : A }}.
+Proof.
+  eauto using ctxeq_exp_eq_helper.
+Qed.
+
+Lemma ctxeq_sub : forall {Γ Δ σ Γ'}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢s σ : Γ' }} -> {{ Δ ⊢s σ : Γ' }}.
+Proof.
+  eauto using ctxeq_sub_helper.
+Qed.
+
+Lemma ctxeq_sub_eq : forall {Γ Δ σ σ' Γ'}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢s σ ≈ σ' : Γ' }} -> {{ Δ ⊢s σ ≈ σ' : Γ' }}.
+Proof.
+  eauto using ctxeq_sub_eq_helper.
 Qed.
 
 #[export]
-Hint Resolve ctxeq_tm ctxeq_eq ctxeq_s ctxeq_s_eq : mcltt.
+Hint Resolve ctxeq_exp ctxeq_exp_eq ctxeq_sub ctxeq_sub_eq : mcltt.
diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index 252ed165..a16b8433 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -8,15 +8,6 @@ Require Import Syntactic.SystemLemmas.
 Require Import Syntactic.CtxEquiv.
 Require Import Syntactic.Relations.
 
-Ltac breakdown_goal :=
-  let rec splitting :=
-    match goal with
-    | [|- ?X ∧ ?Y] => split; splitting
-    | [|- _] => mauto
-    end
-  in splitting
-.
-
 Ltac gen_presup_ctx H :=
   match type of H with
   | {{ ⊢ ?Γ ≈ ?Δ }} =>
@@ -26,101 +17,191 @@ Ltac gen_presup_ctx H :=
   | {{ ?Γ ⊢s ?σ : ?Δ }} =>
       let HΓ := fresh "HΓ" in
       let HΔ := fresh "HΔ" in
-      pose proof presup_sb_ctx H as [HΓ HΔ]
+      pose proof presup_sub_ctx H as [HΓ HΔ]
   | _ => idtac
   end.
 
-Ltac gen_presup_IH presup_tm presup_eq presup_sb_eq H :=
+Ltac gen_presup_IH presup_exp presup_exp_eq presup_sub_eq H :=
   match type of H with
-  | {{ ?Γ ⊢ ?t : ?T }} =>
+  | {{ ?Γ ⊢ ?M : ?A }} =>
+      let HΓ := fresh "HΓ" in
+      let i := fresh "i" in
+      let HAi := fresh "HAi" in
+      pose proof presup_exp _ _ _ H as [HΓ [i HAi]]
+  | {{ ?Γ ⊢ ?M ≈ ?N : ?A }} =>
       let HΓ := fresh "HΓ" in
       let i := fresh "i" in
-      let HTi := fresh "HTi" in
-      pose proof presup_tm _ _ _ H as [HΓ [i HTi]]
+      let HM := fresh "HM" in
+      let HN := fresh "HN" in
+      let HAi := fresh "HAi" in
+      pose proof presup_exp_eq _ _ _ _ H as [HΓ [HM [HN [i HAi]]]]
   | {{ ?Γ ⊢s ?σ ≈ ?τ : ?Δ }} =>
       let HΓ := fresh "HΓ" in
       let Hσ := fresh "Hσ" in
       let Hτ := fresh "Hτ" in
       let HΔ := fresh "HΔ" in
-      pose proof presup_sb_eq _ _ _ _ H as [HΓ [Hσ [Hτ HΔ]]]
-  | {{ ?Γ ⊢ ?s ≈ ?t : ?T }} =>
-      let HΓ := fresh "HΓ" in
-      let i := fresh "i" in
-      let Hs := fresh "Hs" in
-      let Ht := fresh "Ht" in
-      let HTi := fresh "HTi" in
-      pose proof presup_eq _ _ _ _ H as [HΓ [Hs [Ht [i HTi]]]]
+      pose proof presup_sub_eq _ _ _ _ H as [HΓ [Hσ [Hτ HΔ]]]
   | _ => gen_presup_ctx H
   end.
 
-Lemma presup_tm : forall {Γ t T}, {{ Γ ⊢ t : T }} -> {{ ⊢ Γ }} ∧ ∃ i, {{ Γ ⊢ T : Type@i }}
-with presup_eq : forall {Γ s t T}, {{ Γ ⊢ s ≈ t : T }} -> {{ ⊢ Γ }} ∧ {{ Γ ⊢ s : T }} ∧ {{ Γ ⊢ t : T }} ∧ ∃ i, {{ Γ ⊢ T : Type@i }}
-with presup_sb_eq : forall {Γ Δ σ τ}, {{ Γ ⊢s σ ≈ τ : Δ }} -> {{ ⊢ Γ }} ∧ {{ Γ ⊢s σ : Δ }} ∧ {{ Γ ⊢s τ : Δ }} ∧ {{ ⊢ Δ }}.
-Proof with mauto.
-  - intros * Ht.
-    inversion_clear Ht; (on_all_hyp: gen_presup_IH presup_tm presup_eq presup_sb_eq); clear presup_tm presup_eq presup_sb_eq; breakdown_goal.
-    -- eexists.
-       eapply exp_sub_typ...
-       econstructor...
-    -- eexists.
-       pose proof (lift_tm_max_left i0 H).
-       pose proof (lift_tm_max_right i HTi).
-       econstructor...
-
-  - intros * Hst.
-    inversion_clear Hst; (on_all_hyp: gen_presup_IH presup_tm presup_eq presup_sb_eq); clear presup_tm presup_eq presup_sb_eq; breakdown_goal.
-    -- econstructor...
-       eapply exp_sub_typ...
-       econstructor...
-       eapply wf_conv...
-       eapply wf_eq_conv; mauto 6.
-
-    -- econstructor...
-       eapply wf_eq_conv...
-
-    -- eapply wf_exp_sub...
-       econstructor...
-       inversion H...
-
-    -- eapply wf_conv; [|eapply wf_eq_conv]...
-
-    -- eapply wf_conv; [econstructor; mauto|].
-       eapply wf_eq_trans.
-       + eapply wf_eq_sym.
-         eapply wf_eq_conv.
-         ++ eapply wf_eq_exp_sub_compose...
-         ++ econstructor...
-       + do 2 econstructor...
-
-    -- eapply wf_conv; [econstructor; mauto|].
-       eapply wf_eq_trans.
-       + eapply wf_eq_sym.
-         eapply wf_eq_conv.
-         ++ eapply wf_eq_exp_sub_compose...
-         ++ econstructor...
-       + do 2 econstructor...
-
-  - intros * Hστ.
-    inversion_clear Hστ; (on_all_hyp: gen_presup_IH presup_tm presup_eq presup_sb_eq); clear presup_tm presup_eq presup_sb_eq; breakdown_goal.
-    -- inversion_clear H...
-
-    -- econstructor...
-       eapply wf_conv...
-
-    -- econstructor...
-       eapply wf_conv...
-       eapply wf_eq_conv...
-
-    -- inversion_clear HΔ...
-       econstructor...
-       eapply wf_conv...
-       eapply wf_eq_conv...
-
-    Unshelve.
-    all: constructor.
+Lemma presup_exp : forall {Γ M A}, {{ Γ ⊢ M : A }} -> {{ ⊢ Γ }} ∧ ∃ i, {{ Γ ⊢ A : Type@i }}
+with presup_exp_eq : forall {Γ M M' A}, {{ Γ ⊢ M ≈ M' : A }} -> {{ ⊢ Γ }} ∧ {{ Γ ⊢ M : A }} ∧ {{ Γ ⊢ M' : A }} ∧ ∃ i, {{ Γ ⊢ A : Type@i }}
+with presup_sub_eq : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Γ }} ∧ {{ Γ ⊢s σ : Δ }} ∧ {{ Γ ⊢s σ' : Δ }} ∧ {{ ⊢ Δ }}.
+Proof with solve [mauto].
+  (* presup_exp *)
+  - intros * HM.
+    inversion_clear HM; (on_all_hyp: gen_presup_IH presup_exp presup_exp_eq presup_sub_eq); clear presup_exp presup_exp_eq presup_sub_eq; repeat split; mauto.
+    all: try (rename B into C); try (rename B' into C'); try (rename A0 into B); try (rename A' into B').
+    + eexists.
+      assert {{ Γ ⊢ B : Type@(max i i0) }} by mauto using lift_exp_max_left.
+      assert {{ Γ, B ⊢ C : Type@(max i i0) }} by mauto using lift_exp_max_right...
+
+  - intros * HMM'.
+    set (WkWksucc := {{{ Wk∘Wk ,, succ #1 }}}).
+    inversion_clear HMM'; (on_all_hyp: gen_presup_IH presup_exp presup_exp_eq presup_sub_eq); clear presup_exp presup_exp_eq presup_sub_eq; repeat split; mauto.
+    all: try (rename B into C); try (rename B' into C'); try (rename A0 into B); try (rename A' into B');
+      try (rename N into L); try (rename N' into L'); try (rename M0 into N); try (rename MZ into NZ); try (rename MS into NS); try (rename M'0 into N'); try (rename MZ' into NZ'); try (rename MS' into NS'); try (rename M' into N').
+    + assert {{ Γ ⊢s Id ,, N ≈ Id ,, N' : Γ, ℕ }} by mauto.
+      assert {{ Γ ⊢ B[Id ,, N] ≈ B[Id ,, N'] : Type@i }} by mauto.
+      assert {{ Γ ⊢ B[Id ,, N] ≈ B'[Id ,, N'] : Type@i }} by mauto.
+      assert {{ Γ ⊢ B[Id ,, zero] ≈ B'[Id ,, zero] : Type@i }} by mauto.
+      assert {{ Γ ⊢ NZ' : B'[Id ,, zero] }} by mauto.
+      assert {{ Γ, ℕ, B ⊢ NS' : B'[WkWksucc] }} by mauto.
+      assert {{ Γ, ℕ, B' ⊢ NS' : B'[WkWksucc] }} by mauto.
+      enough {{ Γ ⊢ rec N' return B' | zero -> NZ' | succ -> NS' end : B'[Id ,, N'] }}...
+
+    + assert {{ Γ ⊢ B[(Id,,N)][σ] ≈ B[(Id,,N)∘σ] : Type@i }} by mauto.
+      assert {{ Γ ⊢ B[(Id,,N)∘σ] ≈ B[σ,,N[σ]] : Type@i }} by mauto.
+      enough {{ Γ ⊢ B[(Id,,N)][σ] ≈ B[σ,,N[σ]] : Type@i }}...
+
+    + assert {{ Γ ⊢s Id,,N[σ] : Γ, ℕ }} by mauto.
+      assert {{ Γ, ℕ ⊢s q σ : Δ, ℕ }} by mauto.
+      assert {{ Γ ⊢ B[q σ][(Id,,N[σ])] ≈ B[q σ∘(Id,,N[σ])] : Type@i }} by mauto.
+      assert {{ Γ ⊢ B[q σ∘(Id,,N[σ])] ≈ B[σ,,N[σ]] : Type@i }} by mauto.
+      assert {{ Γ ⊢ B[q σ][Id,,N[σ]] ≈ B[σ,,N[σ]] : Type@i }} by mauto.
+      assert {{ Γ ⊢ NZ[σ] : B[Id ,, zero][σ] }} by mauto.
+      assert {{ Γ ⊢ zero : ℕ[σ] }} by mauto.
+      assert {{ Γ ⊢s q σ∘(Id ,, zero) ≈ σ ,, zero : Δ, ℕ }} by mauto.
+      assert {{ Γ ⊢s σ ≈ Id∘σ : Δ }} by mauto.
+      assert {{ Γ ⊢s σ ,, zero ≈ Id∘σ ,, zero[σ] : Δ, ℕ }} by mauto.
+      assert {{ Γ ⊢s Id∘σ ,, zero[σ] ≈ (Id ,, zero)∘σ : Δ, ℕ }} by mauto.
+      assert {{ Γ ⊢s q σ∘(Id ,, zero) ≈ (Id ,, zero)∘σ : Δ, ℕ }} by mauto.
+      assert {{ Γ ⊢ B[q σ][Id ,, zero] ≈ B[Id ,, zero][σ] : Type@i }} by mauto.
+      assert {{ Γ ⊢ NZ[σ] : B[q σ][Id ,, zero] }} by mauto.
+      set (Γ' := {{{ Γ, ℕ, B[q σ] }}}).
+      assert {{ Γ' ⊢s q (q σ) : Δ, ℕ, B }} by mauto.
+      assert {{ Γ' ⊢s q σ∘WkWksucc ≈ WkWksucc∘q (q σ) : Δ, ℕ }} by mauto.
+      assert {{ Γ' ⊢ B[q σ][WkWksucc] ≈ B[WkWksucc][q (q σ)] : Type@i }} by mauto.
+      enough {{ Γ' ⊢ NS[q (q σ)] : B[q σ][WkWksucc] }}...
+
+    + set (recN := {{{ rec N return B | zero -> NZ | succ -> NS end }}}).
+      assert {{ Γ ⊢ recN : B[Id ,, N] }} by mauto.
+      assert {{ Γ ⊢s WkWksucc∘(Id ,, N ,, recN) ≈ (Wk∘Wk)∘(Id ,, N ,, recN) ,, (succ #1)[(Id ,, N ,, recN)] : Γ, ℕ }}
+        by (eapply sub_eq_extend_compose_nat; mauto).
+      assert {{ Γ ⊢s Id ,, N ,, recN : Γ, ℕ, B }} by mauto.
+      assert {{ Γ ⊢s (Wk∘Wk)∘(Id ,, N ,, recN) : Γ }} by mauto.
+      assert {{ Γ ⊢s (Wk∘Wk)∘(Id ,, N ,, recN) ≈ Wk∘(Wk∘(Id ,, N ,, recN)) : Γ }} by mauto.
+      assert {{ Γ ⊢s Wk∘(Wk∘(Id ,, N ,, recN)) ≈ Wk∘(Id ,, N) : Γ }} by mauto.
+      assert {{ Γ ⊢s (Wk∘Wk)∘(Id ,, N ,, recN) ≈ Id : Γ }} by mauto.
+      assert {{ Γ ⊢ #1[Id ,, N ,, recN] ≈ #0[Id ,, N] : ℕ }} by mauto.
+      assert {{ Γ ⊢ succ #1[Id ,, N ,, recN] ≈ succ N : ℕ }} by mauto.
+      assert {{ Γ ⊢ (succ #1)[Id ,, N ,, recN] ≈ succ N : ℕ }} by mauto.
+      assert {{ Γ ⊢s (Wk∘Wk)∘(Id ,, N ,, recN) ,, (succ #1)[Id ,, N ,, recN] ≈ Id ,, succ N : Γ , ℕ }} by mauto.
+      assert {{ Γ ⊢s WkWksucc∘(Id ,, N ,, recN) ≈ Id ,, succ N : Γ , ℕ }} by mauto.
+      assert {{ Γ ⊢ B[WkWksucc∘(Id ,, N ,, recN)] ≈ B[Id ,, succ N] : Type@i }} by mauto.
+      enough {{ Γ ⊢ B[WkWksucc][Id ,, N ,, recN] ≈ B[Id ,, succ N] : Type@i }}...
+
+    + assert {{ Γ ⊢ B : Type@(max i i0) }} by mauto using lift_exp_max_left.
+      assert {{ Γ ⊢ B ≈ B' : Type@(max i i0) }} by mauto using lift_exp_eq_max_left.
+      assert {{ Γ, B ⊢ C : Type@(max i i0) }} by mauto using lift_exp_max_right.
+      enough {{ Γ ⊢ λ B' N' : Π B' C }}...
+
+    + assert {{ Γ ⊢ B : Type@(max i i0) }} by mauto using lift_exp_max_left.
+      assert {{ Γ, B ⊢ C : Type@(max i i0) }} by mauto using lift_exp_max_right...
+
+    + assert {{ Δ ⊢ B : Type@(max i i0) }} by mauto using lift_exp_max_left.
+      assert {{ Δ, B ⊢ C : Type@(max i i0) }} by mauto using lift_exp_max_right.
+      assert {{ Γ ⊢ Π B[σ] C[q σ] ≈ Π B[σ] C[q σ] : Type@(max i i0) }} by mauto.
+      enough {{ Γ ⊢ λ B[σ] N[q σ] : Π B[σ] C[q σ] }}...
+
+    + assert {{ Δ ⊢ B : Type@(max i i0) }} by mauto using lift_exp_max_left.
+      assert {{ Δ, B ⊢ C : Type@(max i i0) }} by mauto using lift_exp_max_right...
+
+    + assert {{ Γ ⊢s Id ,, L ≈ Id ,, L' : Γ, B }} by (econstructor; mauto).
+      enough {{ Γ ⊢ C[Id ,, L] ≈ C[Id ,, L'] : Type@i }}...
+
+    + assert {{ Γ ⊢ N[σ] : Π B[σ] C[q σ] }} by mauto.
+      assert {{ Γ ⊢ L[σ] : B[σ] }} by mauto.
+      assert {{ Γ ⊢s (Id ,, L)∘σ ≈ Id∘σ ,, L[σ] : Δ, B }} by (econstructor; mauto).
+      assert {{ Γ ⊢s (Id ,, L)∘σ ≈ σ ,, L[σ] : Δ, B }} by mauto.
+      assert {{ Γ ⊢ C[(Id ,, L)∘σ] ≈ C[σ ,, L[σ]] : Type@i }} by mauto.
+      enough {{ Γ ⊢ C[Id ,, L][σ] ≈ C[σ ,, L[σ]] : Type@i }}...
+
+    + assert {{ Γ ⊢ N[σ] : Π B[σ] C[q σ] }} by mauto.
+      assert {{ Γ ⊢ L[σ] : B[σ] }} by mauto.
+      assert {{ Γ, B[σ] ⊢s q σ : Δ, B }} by mauto.
+      assert {{ Γ ⊢s q σ∘(Id ,, L[σ]) ≈ σ ,, L[σ] : Δ, B }} by mauto.
+      assert {{ Γ ⊢ C[q σ∘(Id ,, L[σ])] ≈ C[σ ,, L[σ]] : Type@i }} by mauto.
+      enough {{ Γ ⊢ C[q σ][(Id ,, L[σ])] ≈ C[σ ,, L[σ]] : Type@i }}...
+
+    + assert {{ Γ, B ⊢ B[Wk] : Type@i }} by mauto.
+      assert {{ Γ, B, B[Wk] ⊢ C[q Wk] : Type@i }} by mauto.
+      assert {{ Γ, B ⊢ M[Wk] : (Π B C)[Wk] }} by mauto.
+      assert {{ Γ, B ⊢ M[Wk] : Π B[Wk] C[q Wk] }} by mauto.
+      assert {{ Γ, B ⊢ #0 : B[Wk] }} by mauto.
+      assert {{ Γ, B ⊢s Id ,, #0 : Γ, B, B[Wk] }} by mauto.
+      assert {{ Γ, B ⊢ M[Wk] #0 : C[q Wk][Id,,#0] }} by mauto.
+      assert {{ Γ, B ⊢ M[Wk] #0 : C[q Wk∘(Id,,#0)] }} by mauto.
+      assert {{ Γ, B ⊢ #0 : B[Wk][Id] }} by mauto.
+      assert {{ Γ, B ⊢s Id ,, #0 : Γ, B, B[Wk] }} by mauto.
+      assert {{ Γ, B ⊢s Wk : Γ }} by mauto.
+      assert {{ Γ, B ⊢s Wk∘(Id ,, # 0) ≈ Id : Γ, B }} by mauto.
+      assert {{ Γ, B ⊢s Wk∘Id ≈ (Wk∘Wk)∘(Id ,, # 0) : Γ }} by mauto.
+      assert {{ Γ, B, B[Wk] ⊢ #0 : B[Wk][Wk] }} by mauto.
+      assert {{ Γ, B, B[Wk] ⊢ #0 : B[Wk∘Wk] }} by mauto.
+      assert {{ Γ, B ⊢s q Wk ∘ (Id ,, #0) ≈ (Wk∘Wk)∘(Id ,, #0) ,, #0[Id ,, #0] : Γ, B }} by mauto.
+      assert {{ Γ, B ⊢s (Wk∘Wk)∘(Id ,, #0) ≈ Wk∘(Wk∘(Id ,, #0)) : Γ }} by mauto.
+      assert {{ Γ, B ⊢s (Wk∘Wk)∘(Id ,, #0) ≈ Wk∘Id : Γ }} by mauto.
+      assert {{ Γ, B ⊢ #0[Id ,, #0] ≈ #0 : B[Wk][Id] }} by mauto.
+      assert {{ Γ, B ⊢ #0 ≈ #0[Id] : B[Wk][Id] }} by mauto.
+      assert {{ Γ, B ⊢ #0[Id ,, #0] ≈ #0[Id] : B[Wk][Id] }} by mauto.
+      assert {{ Γ, B ⊢ #0[Id ,, #0] ≈ #0[Id] : B[Wk∘Id] }} by mauto.
+      assert {{ Γ, B ⊢ #0[Id ,, #0] ≈ #0[Id] : B[(Wk∘Wk)∘(Id ,, #0)] }} by mauto.
+      assert {{ Γ, B ⊢s (Wk∘Wk)∘(Id ,, #0) ,, #0[Id ,, #0] ≈ Wk∘Id ,, #0[Id] : Γ, B }} by mauto.
+      assert {{ Γ, B ⊢s Wk∘Id ,, #0[Id] ≈ Id : Γ, B }} by mauto.
+      assert {{ Γ, B ⊢s q Wk ∘ (Id ,, #0) ≈ Id : Γ, B }} by mauto.
+      assert {{ Γ, B ⊢ M[Wk] #0 : C[Id] }} by mauto.
+      enough {{ Γ, B ⊢ M[Wk] #0 : C }}...
+
+    + assert {{ Γ ⊢s Wk∘(σ ,, N') ≈ σ : Δ }} by mauto.
+      assert {{ Γ ⊢ B[Wk∘(σ ,, N')] ≈ B[σ] : Type@i }} by mauto.
+      assert {{ Δ, B ⊢s Wk : Δ }} by mauto.
+      assert {{ Γ ⊢ B[Wk][σ ,, N'] ≈ B[σ] : Type@i }} by mauto.
+      enough {{ Γ ⊢ #0[σ ,, N'] : B[Wk][σ ,, N'] }}...
+
+    + assert (∃ i, {{ Δ ⊢ C : Type@i }}) as [i'] by mauto.
+      assert {{ Γ ⊢s Wk∘(σ ,, N) ≈ σ : Δ }} by mauto.
+      assert {{ Γ ⊢ C[Wk∘(σ ,, N)] ≈ C[σ] : Type@i' }} by mauto.
+      assert {{ Δ, B ⊢s Wk : Δ }} by mauto.
+      assert {{ Γ ⊢ C[Wk][σ ,, N] ≈ C[σ] : Type@i' }} by mauto.
+      assert {{ Δ, B ⊢ #(S x) : C[Wk] }} by mauto.
+      enough {{ Γ ⊢ #(S x)[σ ,, N] : C[Wk][σ ,, N] }}...
+
+    + assert (∃ i, {{ Δ ⊢ C : Type@i }}) as []...
+
+  - intros * Hσσ'.
+    inversion_clear Hσσ'; (on_all_hyp: gen_presup_IH presup_exp presup_exp_eq presup_sub_eq); clear presup_exp presup_exp_eq presup_sub_eq; repeat split; mauto.
+    + econstructor...
+
+    + assert (exists i, {{ Γ0 ⊢ A : Type@i }}) as [] by mauto.
+      assert {{ Γ ⊢ #0[σ] : A[Wk][σ] }} by mauto.
+      enough {{ Γ ⊢ #0[σ] : A[Wk∘σ] }}...
+
+  Unshelve.
+  all: constructor.
 Qed.
 
 #[export]
-Hint Resolve presup_tm presup_eq presup_sb_eq : mcltt.
+Hint Resolve presup_exp presup_exp_eq presup_sub_eq : mcltt.
 
-Ltac gen_presup H := gen_presup_IH presup_tm presup_eq presup_sb_eq H; gen_presup_ctx H.
+Ltac gen_presup H := gen_presup_IH presup_exp presup_exp_eq presup_sub_eq H; gen_presup_ctx H.
diff --git a/theories/Core/Syntactic/Relations.v b/theories/Core/Syntactic/Relations.v
index 9497b30f..f17875ab 100644
--- a/theories/Core/Syntactic/Relations.v
+++ b/theories/Core/Syntactic/Relations.v
@@ -24,10 +24,10 @@ Proof with mauto.
   induction HΓ01 as [|? ? ? i01 * HΓ01 IHΓ01 HΓ0T0 _ HΓ0T01 _]; intros...
   rename HΓ12 into HT1Γ12.
   inversion_clear HT1Γ12 as [|? ? ? i12 * HΓ12' _ HΓ2'T2 _ HΓ2'T12].
-  pose proof (lift_tm_max_left i12 HΓ0T0).
-  pose proof (lift_tm_max_right i01 HΓ2'T2).
-  pose proof (lift_eq_max_left i12 HΓ0T01).
-  pose proof (lift_eq_max_right i01 HΓ2'T12).
+  pose proof (lift_exp_max_left i12 HΓ0T0).
+  pose proof (lift_exp_max_right i01 HΓ2'T2).
+  pose proof (lift_exp_eq_max_left i12 HΓ0T01).
+  pose proof (lift_exp_eq_max_right i01 HΓ2'T12).
   econstructor...
 Qed.
 
@@ -37,11 +37,11 @@ Add Relation (ctx) (wf_ctx_eq)
     as ctx_eq.
 
 Add Parametric Relation (Γ : ctx) (T : typ) : (exp) (λ t t', {{ Γ ⊢ t ≈ t' : T }})
-    symmetry proved by (λ t t', wf_eq_sym Γ t t' T)
-    transitivity proved by (λ t t' t'', wf_eq_trans Γ t t' T t'')
-    as tm_eq.                                                
+    symmetry proved by (λ t t', wf_exp_eq_sym Γ t t' T)
+    transitivity proved by (λ t t' t'', wf_exp_eq_trans Γ t t' T t'')
+    as exp_eq.                                                
 
 Add Parametric Relation (Γ Δ : ctx) : (sub) (λ σ τ, {{ Γ ⊢s σ ≈ τ : Δ }})
     symmetry proved by (λ σ τ, wf_sub_eq_sym Γ σ τ Δ)
     transitivity proved by (λ σ τ ρ, wf_sub_eq_trans Γ σ τ Δ ρ)
-    as sb_eq.
+    as sub_eq.
diff --git a/theories/Core/Syntactic/Syntax.v b/theories/Core/Syntactic/Syntax.v
index c814a0ae..bfcb0cfe 100644
--- a/theories/Core/Syntactic/Syntax.v
+++ b/theories/Core/Syntactic/Syntax.v
@@ -4,36 +4,38 @@ Require Import List.
 (* CST term *)
 Module Cst.
 Inductive obj : Set :=
-  | typ : nat -> obj
-  | nat : obj
-  | zero : obj
-  | succ : obj -> obj
-  | app : obj -> obj -> obj
-  | fn : string -> obj -> obj -> obj
-  | pi : string -> obj -> obj -> obj
-  | var : string -> obj.
+| typ : nat -> obj
+| nat : obj
+| zero : obj
+| succ : obj -> obj
+| natrec : obj -> string -> obj -> obj -> string -> string -> obj -> obj
+| app : obj -> obj -> obj
+| fn : string -> obj -> obj -> obj
+| pi : string -> obj -> obj -> obj
+| var : string -> obj.
 End Cst.
 
 (* AST term *)
 Inductive exp : Set :=
-  (* Natural numbers *)
-  | a_zero : exp
-  | a_succ : exp -> exp
-  (* Type constructors *)
-  | a_nat : exp
-  | a_typ : nat -> exp
-  | a_var : nat -> exp
-  (* Functions *)
-  | a_fn : exp -> exp -> exp
-  | a_app : exp -> exp -> exp
-  | a_pi : exp -> exp -> exp
-  (* Substitutions *)
-  | a_sub : exp -> sub -> exp
+(* Natural numbers *)
+| a_zero : exp
+| a_succ : exp -> exp
+| a_natrec : exp -> exp -> exp -> exp -> exp
+(* Type constructors *)
+| a_nat : exp
+| a_typ : nat -> exp
+| a_var : nat -> exp
+(* Functions *)
+| a_fn : exp -> exp -> exp
+| a_app : exp -> exp -> exp
+| a_pi : exp -> exp -> exp
+(* Substitutions *)
+| a_sub : exp -> sub -> exp
 with sub : Set :=
-  | a_id : sub
-  | a_weaken : sub
-  | a_compose : sub -> sub -> sub
-  | a_extend : sub -> exp -> sub.
+| a_id : sub
+| a_weaken : sub
+| a_compose : sub -> sub -> sub
+| a_extend : sub -> exp -> sub.
 
 Fixpoint nat_to_exp n : exp :=
   match n with
@@ -72,14 +74,15 @@ Notation "( x )" := x (in custom exp at level 0, x custom exp at level 60) : exp
 Notation "~ x" := x (in custom exp at level 0, x constr at level 0) : exp_scope.
 Notation "x" := x (in custom exp at level 0, x constr at level 0) : exp_scope.
 Notation "e [ s ]" := (a_sub e s) (in custom exp at level 0, s custom exp at level 60) : exp_scope.
-Notation "'λ' T e" := (a_fn T e) (in custom exp at level 0, T custom exp at level 30, e custom exp at level 30) : exp_scope.
+Notation "'λ' T e" := (a_fn T e) (in custom exp at level 0, T custom exp at level 0, e custom exp at level 60) : exp_scope.
 Notation "f x .. y" := (a_app .. (a_app f x) .. y) (in custom exp at level 40, f custom exp, x custom exp at next level, y custom exp at next level) : exp_scope.
 Notation "'ℕ'" := a_nat (in custom exp) : exp_scope.
 Notation "'Type' @ n" := (a_typ n) (in custom exp at level 0, n constr at level 0) : exp_scope.
-Notation "'Π' T S" := (a_pi T S) (in custom exp at level 0, T custom exp at level 30, S custom exp at level 30) : exp_scope.
+Notation "'Π' T S" := (a_pi T S) (in custom exp at level 0, T custom exp at level 0, S custom exp at level 60) : exp_scope.
 Number Notation exp num_to_exp exp_to_num : exp_scope.
 Notation "'zero'" := a_zero (in custom exp at level 0) : exp_scope.
-Notation "'succ' e" := (a_succ e) (in custom exp at level 30, e custom exp at level 30) : exp_scope.
+Notation "'succ' e" := (a_succ e) (in custom exp at level 0, e custom exp at level 0) : exp_scope.
+Notation "'rec' e 'return' m | 'zero' -> ez | 'succ' -> es 'end'" := (a_natrec m ez es e) (in custom exp at level 0, m custom exp at level 60, ez custom exp at level 60, es custom exp at level 60, e custom exp at level 60) : exp_scope.
 Notation "'#' n" := (a_var n) (in custom exp at level 0, n constr at level 0) : exp_scope.
 Notation "'Id'" := a_id (in custom exp at level 0) : exp_scope.
 Notation "'Wk'" := a_weaken (in custom exp at level 0) : exp_scope.
@@ -89,6 +92,7 @@ Notation "x , y" := (cons y x) (in custom exp at level 50) : exp_scope.
 
 Infix "∘" := a_compose (in custom exp at level 40) : exp_scope.
 Infix ",," := a_extend (in custom exp at level 50) : exp_scope.
+Notation "'q' σ" := ({{{ σ ∘ Wk ,, # 0 }}}) (in custom exp at level 30) : exp_scope.
 
 Notation ctx := (list exp).
 Notation typ := exp.
diff --git a/theories/Core/Syntactic/System.v b/theories/Core/Syntactic/System.v
index cfeb4480..be179c97 100644
--- a/theories/Core/Syntactic/System.v
+++ b/theories/Core/Syntactic/System.v
@@ -1,6 +1,5 @@
 Require Import List.
 Require Import Unicode.Utf8_core.
-Import ListNotations.
 
 Require Import LibTactics.
 Require Import Syntactic.Syntax.
@@ -8,80 +7,86 @@ Require Import Syntactic.Syntax.
 #[global] Declare Custom Entry judg.
 Notation "{{ x }}" := x (at level 0, x custom judg at level 99, format "'{{'  x  '}}'").
 Reserved Notation "⊢ Γ" (in custom judg at level 80, Γ custom exp).
-Reserved Notation "⊢ Γ ≈ Δ" (in custom judg at level 80, Γ custom exp, Δ custom exp).
-Reserved Notation "Γ ⊢ A ≈ B : T" (in custom judg at level 80, Γ custom exp, A custom exp, B custom exp, T custom exp).
-Reserved Notation "Γ ⊢ t : T" (in custom judg at level 80, Γ custom exp, t custom exp, T custom exp).
+Reserved Notation "⊢ Γ ≈ Γ'" (in custom judg at level 80, Γ custom exp, Γ' custom exp).
+Reserved Notation "Γ ⊢ M ≈ M' : A" (in custom judg at level 80, Γ custom exp, M custom exp, M' custom exp, A custom exp).
+Reserved Notation "Γ ⊢ M : A" (in custom judg at level 80, Γ custom exp, M custom exp, A custom exp).
 Reserved Notation "Γ ⊢s σ : Δ" (in custom judg at level 80, Γ custom exp, σ custom exp, Δ custom exp).
-Reserved Notation "Γ ⊢s S1 ≈ S2 : Δ" (in custom judg at level 80, Γ custom exp, S1 custom exp, S2 custom exp, Δ custom exp).
-Reserved Notation "'#' x : T ∈ Γ" (in custom judg at level 80, x constr at level 0, T custom exp, Γ custom exp at level 50).
+Reserved Notation "Γ ⊢s σ ≈ σ' : Δ" (in custom judg at level 80, Γ custom exp, σ custom exp, σ' custom exp, Δ custom exp).
+Reserved Notation "'#' x : A ∈ Γ" (in custom judg at level 80, x constr at level 0, A custom exp, Γ custom exp at level 50).
 
 Generalizable All Variables.
 
 Inductive ctx_lookup : nat -> typ -> ctx -> Prop :=
-  | here : `({{ #0 : T[Wk] ∈ Γ , T }})
-  | there : `({{ #n : T ∈ Γ }} -> {{ #(S n) : T[Wk] ∈ Γ , T' }})
-where "'#' x : T ∈ Γ" := (ctx_lookup x T Γ) (in custom judg) : type_scope.
+  | here : `({{ #0 : A[Wk] ∈ Γ , A }})
+  | there : `({{ #n : A ∈ Γ }} -> {{ #(S n) : A[Wk] ∈ Γ , B }})
+where "'#' x : A ∈ Γ" := (ctx_lookup x A Γ) (in custom judg) : type_scope.
 
 Inductive wf_ctx : ctx -> Prop :=
 | wf_ctx_empty : {{ ⊢ ⋅ }}
 | wf_ctx_extend :
   `( {{ ⊢ Γ }} ->
-     {{ Γ ⊢ T : Type@i }} ->
-     {{ ⊢ Γ , T }} )
+     {{ Γ ⊢ A : Type@i }} ->
+     {{ ⊢ Γ , A }} )
 where "⊢ Γ" := (wf_ctx Γ) (in custom judg) : type_scope
 with wf_ctx_eq : ctx -> ctx -> Prop :=
 | wf_ctx_eq_empty : {{ ⊢ ⋅ ≈ ⋅ }}
 | wf_ctx_eq_extend :
   `( {{ ⊢ Γ ≈ Δ }} ->
-     {{ Γ ⊢ T : Type@i }} ->
-     {{ Δ ⊢ T' : Type@i }} ->
-     {{ Γ ⊢ T ≈ T' : Type@i }} ->
-     {{ Δ ⊢ T ≈ T' : Type@i }} ->
-     {{ ⊢ Γ , T ≈ Δ , T' }} )
-where "⊢ Γ ≈ Δ" := (wf_ctx_eq Γ Δ) (in custom judg) : type_scope
+     {{ Γ ⊢ A : Type@i }} ->
+     {{ Δ ⊢ A' : Type@i }} ->
+     {{ Γ ⊢ A ≈ A' : Type@i }} ->
+     {{ Δ ⊢ A ≈ A' : Type@i }} ->
+     {{ ⊢ Γ , A ≈ Δ , A' }} )
+where "⊢ Γ ≈ Γ'" := (wf_ctx_eq Γ Γ') (in custom judg) : type_scope
 with wf_exp : ctx -> exp -> typ -> Prop :=
+| wf_univ :
+  `( {{ ⊢ Γ }} ->
+     {{ Γ ⊢ Type@i : Type@(S i) }} )
 | wf_nat :
   `( {{ ⊢ Γ }} ->
      {{ Γ ⊢ ℕ : Type@i }} )
-| wf_univ :
+| wf_zero :
   `( {{ ⊢ Γ }} ->
-     {{ Γ ⊢ Type@i : Type@(S i) }} )
+     {{ Γ ⊢ zero : ℕ }} )
+| wf_succ :
+  `( {{ Γ ⊢ M : ℕ }} ->
+     {{ Γ ⊢ succ M : ℕ }} )
+| wf_natrec :
+  `( {{ Γ , ℕ ⊢ A : Type@i }} ->
+     {{ Γ ⊢ MZ : A[Id,,zero] }} ->
+     {{ Γ , ℕ , A ⊢ MS : A[Wk∘Wk,,succ(#1)] }} ->
+     {{ Γ ⊢ M : ℕ }} ->
+     {{ Γ ⊢ rec M return A | zero -> MZ | succ -> MS end : A[Id,,M] }} )
 | wf_pi :
   `( {{ Γ ⊢ A : Type@i }} ->
      {{ Γ , A ⊢ B : Type@i }} ->
      {{ Γ ⊢ Π A B : Type@i }} )
-| wf_vlookup :
-  `( {{ ⊢ Γ }} ->
-     {{ #x : T ∈ Γ }} ->
-     {{ Γ ⊢ #x : T }} )
+| wf_fn :
+  `( {{ Γ ⊢ A : Type@i }} ->
+     {{ Γ , A ⊢ M : B }} ->
+     {{ Γ ⊢ λ A M : Π A B }} )
 | wf_app :
   `( {{ Γ ⊢ A : Type@i }} ->
      {{ Γ , A ⊢ B : Type@i }} ->
      {{ Γ ⊢ M : Π A B }} ->
      {{ Γ ⊢ N : A }} ->
      {{ Γ ⊢ M N : B[Id,,N] }} )
-| wf_fn :
-  `( {{ Γ ⊢ A : Type@i }} ->
-     {{ Γ , A ⊢ M : B }} ->
-     {{ Γ ⊢ λ A M : Π A B }} )
-| wf_zero :
+| wf_vlookup :
   `( {{ ⊢ Γ }} ->
-     {{ Γ ⊢ zero : ℕ }} )
-| wf_succ :
-  `( {{ Γ ⊢ n : ℕ }} ->
-     {{ Γ ⊢ succ n : ℕ }} )
+     {{ #x : A ∈ Γ }} ->
+     {{ Γ ⊢ #x : A }} )
 | wf_exp_sub :
   `( {{ Γ ⊢s σ : Δ }} ->
      {{ Δ ⊢ M : A }} ->
      {{ Γ ⊢ M[σ] : A[σ] }} )
 | wf_conv :
-  `( {{ Γ ⊢ t : T }} ->
-     {{ Γ ⊢ T ≈ T' : Type@i }} ->
-     {{ Γ ⊢ t : T' }} )
+  `( {{ Γ ⊢ M : A }} ->
+     {{ Γ ⊢ A ≈ A' : Type@i }} ->
+     {{ Γ ⊢ M : A' }} )
 | wf_cumu :
-  `( {{ Γ ⊢ T : Type@i }} ->
-     {{ Γ ⊢ T : Type@(S i) }} )
-where "Γ ⊢ t : T" := (wf_exp Γ t T) (in custom judg) : type_scope
+  `( {{ Γ ⊢ A : Type@i }} ->
+     {{ Γ ⊢ A : Type@(S i) }} )
+where "Γ ⊢ M : A" := (wf_exp Γ M A) (in custom judg) : type_scope
 with wf_sub : ctx -> sub -> ctx -> Prop :=
 | wf_sub_id :
   `( {{ ⊢ Γ }} ->
@@ -103,98 +108,154 @@ with wf_sub : ctx -> sub -> ctx -> Prop :=
      {{ ⊢ Δ ≈ Δ' }} ->
      {{ Γ ⊢s σ : Δ' }} )
 where "Γ ⊢s σ : Δ" := (wf_sub Γ σ Δ) (in custom judg) : type_scope
-with wf_eq : ctx -> exp -> exp -> typ -> Prop :=
-| wf_eq_nat_sub :
+with wf_exp_eq : ctx -> exp -> exp -> typ -> Prop :=
+| wf_exp_eq_typ_sub :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ Γ ⊢ Type@i[σ] ≈ Type@i : Type@(S i) }} )
+| wf_exp_eq_nat_sub :
   `( {{ Γ ⊢s σ : Δ }} ->
      {{ Γ ⊢ ℕ[σ] ≈ ℕ : Type@i }} )
-| wf_eq_typ_sub :
+| wf_exp_eq_zero_sub :
   `( {{ Γ ⊢s σ : Δ }} ->
-     {{ Γ ⊢ Type@i[σ] ≈ Type@i : Type@(S i) }} )
-| wf_eq_pi_sub :
+     {{ Γ ⊢ zero[σ] ≈ zero : ℕ }} )
+| wf_exp_eq_succ_sub :
   `( {{ Γ ⊢s σ : Δ }} ->
-     {{ Δ ⊢ T' : Type@i }} ->
-     {{ Δ , T' ⊢ T : Type@i }} ->
-     {{ Γ ⊢ (Π T' T)[σ] ≈ Π (T'[σ]) (T[σ ∘ Wk ,, #0]) : Type@i }} )
-| wf_eq_pi_cong :
-  `( {{ Γ ⊢ M : Type@i }} ->
-     {{ Γ ⊢ M ≈ M' : Type@i }} ->
-     {{ Γ , M ⊢ T ≈ T' : Type@i }} ->
-     {{ Γ ⊢ Π M T ≈ Π M' T' : Type@i }} )
-| wf_eq_var :
-  `( {{ ⊢ Γ }} ->
-     {{ #x : T ∈ Γ }} ->
-     {{ Γ ⊢ #x ≈ #x : T }} )
-| wf_eq_zero :
+     {{ Δ ⊢ M : ℕ }} ->
+     {{ Γ ⊢ (succ M)[σ] ≈ succ (M[σ]) : ℕ }} )
+| wf_exp_eq_succ_cong :
+  `( {{ Γ ⊢ M ≈ M' : ℕ }} ->
+     {{ Γ ⊢ succ M ≈ succ M' : ℕ }} )
+| wf_exp_eq_natrec_cong :
+  `( {{ Γ , ℕ ⊢ A : Type@i }} ->
+     {{ Γ , ℕ ⊢ A ≈ A' : Type@i }} ->
+     {{ Γ ⊢ MZ ≈ MZ' : A[Id,,zero] }} ->
+     {{ Γ , ℕ , A ⊢ MS ≈ MS' : A[Wk∘Wk,,succ(#1)] }} ->
+     {{ Γ ⊢ M ≈ M' : ℕ }} ->
+     {{ Γ ⊢ rec M return A | zero -> MZ | succ -> MS end ≈ rec M' return A' | zero -> MZ' | succ -> MS' end : A[Id,,M] }} )
+| wf_exp_eq_natrec_sub :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ Δ , ℕ ⊢ A : Type@i }} ->
+     {{ Δ ⊢ MZ : A[Id,,zero] }} ->
+     {{ Δ , ℕ , A ⊢ MS : A[Wk∘Wk,,succ(#1)] }} ->
+     {{ Δ ⊢ M : ℕ }} ->
+     {{ Γ ⊢ rec M return A | zero -> MZ | succ -> MS end[σ] ≈ rec M[σ] return A[q σ] | zero -> MZ[σ] | succ -> MS[q (q σ)] end : A[σ,,M[σ]] }} )
+| wf_exp_eq_nat_beta_zero :
+  `( {{ Γ , ℕ ⊢ A : Type@i }} ->
+     {{ Γ ⊢ MZ : A[Id,,zero] }} ->
+     {{ Γ , ℕ , A ⊢ MS : A[Wk∘Wk,,succ(#1)] }} ->
+     {{ Γ ⊢ rec zero return A | zero -> MZ | succ -> MS end ≈ MZ : A[Id,,zero] }} )
+| wf_exp_eq_nat_beta_succ :
+  `( {{ Γ , ℕ ⊢ A : Type@i }} ->
+     {{ Γ ⊢ MZ : A[Id,,zero] }} ->
+     {{ Γ , ℕ , A ⊢ MS : A[Wk∘Wk,,succ(#1)] }} ->
+     {{ Γ ⊢ M : ℕ }} ->
+     {{ Γ ⊢ rec (succ M) return A | zero -> MZ | succ -> MS end ≈ MS[Id,,M,,rec M return A | zero -> MZ | succ -> MS end] : A[Id,,succ M] }} )
+| wf_exp_eq_pi_sub :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ Δ ⊢ A : Type@i }} ->
+     {{ Δ , A ⊢ B : Type@i }} ->
+     {{ Γ ⊢ (Π A B)[σ] ≈ Π (A[σ]) (B[q σ]) : Type@i }} )
+| wf_exp_eq_pi_cong :
+  `( {{ Γ ⊢ A : Type@i }} ->
+     {{ Γ ⊢ A ≈ A' : Type@i }} ->
+     {{ Γ , A ⊢ B ≈ B' : Type@i }} ->
+     {{ Γ ⊢ Π A B ≈ Π A' B' : Type@i }} )
+| wf_exp_eq_fn_cong :
+  `( {{ Γ ⊢ A : Type@i }} ->
+     {{ Γ ⊢ A ≈ A' : Type@i }} ->
+     {{ Γ , A ⊢ M ≈ M' : B }} ->
+     {{ Γ ⊢ λ A M ≈ λ A' M' : Π A B }} )
+| wf_exp_eq_fn_sub :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ Δ ⊢ A : Type@i }} ->
+     {{ Δ , A ⊢ M : B }} ->
+     {{ Γ ⊢ (λ A M)[σ] ≈ λ A[σ] M[q σ] : (Π A B)[σ] }} )
+| wf_exp_eq_app_cong :
+  `( {{ Γ ⊢ A : Type@i }} ->
+     {{ Γ , A ⊢ B : Type@i }} ->
+     {{ Γ ⊢ M ≈ M' : Π A B }} ->
+     {{ Γ ⊢ N ≈ N' : A }} ->
+     {{ Γ ⊢ M N ≈ M' N' : B[Id,,N] }} )
+| wf_exp_eq_app_sub :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ Δ ⊢ A : Type@i }} ->
+     {{ Δ , A ⊢ B : Type@i }} ->
+     {{ Δ ⊢ M : Π A B }} ->
+     {{ Δ ⊢ N : A }} ->
+     {{ Γ ⊢ (M N)[σ] ≈ M[σ] N[σ] : B[σ,,N[σ]] }} )
+| wf_exp_eq_pi_beta :
+  `( {{ Γ ⊢ A : Type@i }} ->
+     {{ Γ , A ⊢ B : Type@i }} ->
+     {{ Γ , A ⊢ M : B }} ->
+     {{ Γ ⊢ N : A }} ->
+     {{ Γ ⊢ (λ A M) N ≈ M[Id,,N] : B[Id,,N] }} )
+| wf_exp_eq_pi_eta :
+  `( {{ Γ ⊢ A : Type@i }} ->
+     {{ Γ , A ⊢ B : Type@i }} ->
+     {{ Γ ⊢ M : Π A B }} ->
+     {{ Γ ⊢ M ≈ λ A (M[Wk] #0) : Π A B }} )
+| wf_exp_eq_var :
   `( {{ ⊢ Γ }} ->
-     {{ Γ ⊢ zero ≈ zero : ℕ }} )
-| wf_eq_zero_sub :
+     {{ #x : A ∈ Γ }} ->
+     {{ Γ ⊢ #x ≈ #x : A }} )
+| wf_exp_eq_var_0_sub :
   `( {{ Γ ⊢s σ : Δ }} ->
-     {{ Γ ⊢ zero[σ] ≈ zero : ℕ }} )
-| wf_eq_succ_cong :
-  `( {{ Γ ⊢ t ≈ t' : ℕ }} ->
-     {{ Γ ⊢ succ t ≈ succ t' : ℕ }} )
-| wf_eq_succ_sub :
+     {{ Δ ⊢ A : Type@i }} ->
+     {{ Γ ⊢ M : A[σ] }} ->
+     {{ Γ ⊢ #0[σ ,, M] ≈ M : A[σ] }} )
+| wf_exp_eq_var_S_sub :
   `( {{ Γ ⊢s σ : Δ }} ->
-     {{ Δ ⊢ t : ℕ }} ->
-     {{ Γ ⊢ (succ t)[σ] ≈ succ (t[σ]) : ℕ }} )
-| wf_eq_exp_sub_cong :
-  `( {{ Δ ⊢ t ≈ t' : T }} ->
+     {{ Δ ⊢ A : Type@i }} ->
+     {{ Γ ⊢ M : A[σ] }} ->
+     {{ #x : B ∈ Δ }} ->
+     {{ Γ ⊢ #(S x)[σ ,, M] ≈ #x[σ] : B[σ] }} )
+| wf_exp_eq_var_weaken :
+  `( {{ ⊢ Γ , B }} ->
+     {{ #x : A ∈ Γ }} ->
+     {{ Γ , B ⊢ #x[Wk] ≈ #(S x) : A[Wk] }} )
+| wf_exp_eq_sub_cong :
+  `( {{ Δ ⊢ M ≈ M' : A }} ->
      {{ Γ ⊢s σ ≈ σ' : Δ }} ->
-     {{ Γ ⊢ t[σ] ≈ t'[σ'] : T[σ] }} )
-| wf_eq_exp_sub_id :
-  `( {{ Γ ⊢ t : T }} ->
-     {{ Γ ⊢ t[Id] ≈ t : T }} )
-| wf_eq_exp_sub_weaken :
-  `( {{ ⊢ Γ , M }} ->
-     {{ #x : T ∈ Γ }} ->
-     {{ Γ , M ⊢ (#x)[Wk] ≈ #(S x) : T[Wk] }} )
-| wf_eq_exp_sub_compose :
+     {{ Γ ⊢ M[σ] ≈ M'[σ'] : A[σ] }} )
+| wf_exp_eq_sub_id :
+  `( {{ Γ ⊢ M : A }} ->
+     {{ Γ ⊢ M[Id] ≈ M : A }} )
+| wf_exp_eq_sub_compose :
   `( {{ Γ ⊢s τ : Γ' }} ->
      {{ Γ' ⊢s σ : Γ'' }} ->
-     {{ Γ'' ⊢ t : T }} ->
-     {{ Γ ⊢ t[σ ∘ τ] ≈ t[σ][τ] : T[σ ∘ τ] }} )
-| wf_eq_var_0_sub :
-  `( {{ Γ ⊢s σ : Δ }} ->
-     {{ Δ ⊢ T : Type@i }} ->
-     {{ Γ ⊢ t : T[σ] }} ->
-     {{ Γ ⊢ (#0)[σ ,, t] ≈ t : T[σ] }} )
-| wf_eq_var_S_sub :
-  `( {{ Γ ⊢s σ : Δ }} ->
-     {{ Δ ⊢ T : Type@i }} ->
-     {{ Γ ⊢ t : T[σ] }} ->
-     {{ #x : T ∈ Δ }} ->
-     {{ Γ ⊢ (#(S x))[σ ,, t] ≈ (#x)[σ] : T[σ] }} )
-| wf_eq_cumu :
-  `( {{ Γ ⊢ T ≈ T' : Type@i }} ->
-     {{ Γ ⊢ T ≈ T' : Type@(S i) }} )
-| wf_eq_conv :
-  `( {{ Γ ⊢ t ≈ t' : T }} ->
-     {{ Γ ⊢ T ≈ T' : Type@i }} ->
-     {{ Γ ⊢ t ≈ t' : T' }} )
-| wf_eq_sym :
-  `( {{ Γ ⊢ t ≈ t' : T }} ->
-     {{ Γ ⊢ t' ≈ t : T }} )
-| wf_eq_trans :
-  `( {{ Γ ⊢ t ≈ t' : T }} ->
-     {{ Γ ⊢ t' ≈ t'' : T }} ->
-     {{ Γ ⊢ t ≈ t'' : T }} )
-where "Γ ⊢ A ≈ B : T" := (wf_eq Γ A B T) (in custom judg) : type_scope
+     {{ Γ'' ⊢ M : A }} ->
+     {{ Γ ⊢ M[σ ∘ τ] ≈ M[σ][τ] : A[σ ∘ τ] }} )
+| wf_exp_eq_cumu :
+  `( {{ Γ ⊢ A ≈ A' : Type@i }} ->
+     {{ Γ ⊢ A ≈ A' : Type@(S i) }} )
+| wf_exp_eq_conv :
+  `( {{ Γ ⊢ M ≈ M' : A }} ->
+     {{ Γ ⊢ A ≈ A' : Type@i }} ->
+     {{ Γ ⊢ M ≈ M' : A' }} )
+| wf_exp_eq_sym :
+  `( {{ Γ ⊢ M ≈ M' : A }} ->
+     {{ Γ ⊢ M' ≈ M : A }} )
+| wf_exp_eq_trans :
+  `( {{ Γ ⊢ M ≈ M' : A }} ->
+     {{ Γ ⊢ M' ≈ M'' : A }} ->
+     {{ Γ ⊢ M ≈ M'' : A }} )
+where "Γ ⊢ M ≈ M' : A" := (wf_exp_eq Γ M M' A) (in custom judg) : type_scope
 with wf_sub_eq : ctx -> sub -> sub -> ctx -> Prop :=
 | wf_sub_eq_id :
   `( {{ ⊢ Γ }} ->
      {{ Γ ⊢s Id ≈ Id : Γ }} )
 | wf_sub_eq_weaken :
-  `( {{ ⊢ Γ , T }} ->
-     {{ Γ , T ⊢s Wk ≈ Wk : Γ }} )
+  `( {{ ⊢ Γ , A }} ->
+     {{ Γ , A ⊢s Wk ≈ Wk : Γ }} )
 | wf_sub_eq_compose_cong :
   `( {{ Γ ⊢s τ ≈ τ' : Γ' }} ->
      {{ Γ' ⊢s σ ≈ σ' : Γ'' }} ->
      {{ Γ ⊢s σ ∘ τ ≈ σ' ∘ τ' : Γ'' }} )
 | wf_sub_eq_extend_cong :
   `( {{ Γ ⊢s σ ≈ σ' : Δ }} ->
-     {{ Δ ⊢ T : Type@i }} ->
-     {{ Γ ⊢ t ≈ t' : T[σ] }} ->
-     {{ Γ ⊢s (σ ,, t) ≈ (σ' ,, t') : Δ , T }} )
+     {{ Δ ⊢ A : Type@i }} ->
+     {{ Γ ⊢ M ≈ M' : A[σ] }} ->
+     {{ Γ ⊢s (σ ,, M) ≈ (σ' ,, M') : Δ , A }} )
 | wf_sub_eq_id_compose_right :
   `( {{ Γ ⊢s σ : Δ }} ->
      {{ Γ ⊢s Id ∘ σ ≈ σ : Δ }} )
@@ -208,18 +269,18 @@ with wf_sub_eq : ctx -> sub -> sub -> ctx -> Prop :=
      {{ Γ''' ⊢s (σ ∘ σ') ∘ σ'' ≈ σ ∘ (σ' ∘ σ'') : Γ }} )
 | wf_sub_eq_extend_compose :
   `( {{ Γ' ⊢s σ : Γ'' }} ->
-     {{ Γ'' ⊢ T : Type@i }} ->
-     {{ Γ' ⊢ t : T[σ] }} ->
+     {{ Γ'' ⊢ A : Type@i }} ->
+     {{ Γ' ⊢ M : A[σ] }} ->
      {{ Γ ⊢s τ : Γ' }} ->
-     {{ Γ ⊢s (σ ,, t) ∘ τ ≈ ((σ ∘ τ) ,, t[τ]) : Γ'' , T }} )
+     {{ Γ ⊢s (σ ,, M) ∘ τ ≈ ((σ ∘ τ) ,, M[τ]) : Γ'' , A }} )
 | wf_sub_eq_p_extend :
   `( {{ Γ' ⊢s σ : Γ }} ->
-     {{ Γ ⊢ T : Type@i }} ->
-     {{ Γ' ⊢ t : T[σ] }} ->
-     {{ Γ' ⊢s Wk ∘ (σ ,, t) ≈ σ : Γ }} )
+     {{ Γ ⊢ A : Type@i }} ->
+     {{ Γ' ⊢ M : A[σ] }} ->
+     {{ Γ' ⊢s Wk ∘ (σ ,, M) ≈ σ : Γ }} )
 | wf_sub_eq_extend :
-  `( {{ Γ' ⊢s σ : Γ , T }} ->
-     {{ Γ' ⊢s σ ≈ ((Wk ∘ σ) ,, (#0)[σ]) : Γ , T }} )
+  `( {{ Γ' ⊢s σ : Γ , A }} ->
+     {{ Γ' ⊢s σ ≈ ((Wk ∘ σ) ,, #0[σ]) : Γ , A }} )
 | wf_sub_eq_sym :
   `( {{ Γ ⊢s σ ≈ σ' : Δ }} ->
      {{ Γ ⊢s σ' ≈ σ : Δ }} )
@@ -234,4 +295,4 @@ with wf_sub_eq : ctx -> sub -> sub -> ctx -> Prop :=
 where "Γ ⊢s S1 ≈ S2 : Δ" := (wf_sub_eq Γ S1 S2 Δ) (in custom judg) : type_scope.
 
 #[export]
-Hint Constructors wf_ctx wf_ctx_eq wf_exp wf_sub wf_eq wf_sub_eq ctx_lookup: mcltt.
+Hint Constructors wf_ctx wf_ctx_eq wf_exp wf_sub wf_exp_eq wf_sub_eq ctx_lookup: mcltt.
diff --git a/theories/Core/Syntactic/SystemLemmas.v b/theories/Core/Syntactic/SystemLemmas.v
index 4092e3e4..2b2c1fe0 100644
--- a/theories/Core/Syntactic/SystemLemmas.v
+++ b/theories/Core/Syntactic/SystemLemmas.v
@@ -4,161 +4,705 @@ Require Import LibTactics.
 Require Import Syntactic.Syntax.
 Require Import Syntactic.System.
 
-Lemma ctx_decomp : forall {Γ T}, {{ ⊢ Γ , T }} -> {{ ⊢ Γ }} ∧ ∃ i, {{ Γ ⊢ T : Type@i }}.
-Proof with mauto.
-  intros * HTΓ.
-  inversion HTΓ; subst...
+Lemma ctx_decomp : forall {Γ A}, {{ ⊢ Γ , A }} -> {{ ⊢ Γ }} ∧ ∃ i, {{ Γ ⊢ A : Type@i }}.
+Proof with solve [mauto].
+  intros * HAΓ.
+  inversion HAΓ; subst...
 Qed.
 
-Lemma lift_tm_ge : forall {Γ T n m}, n <= m -> {{ Γ ⊢ T : Type@n }} -> {{ Γ ⊢ T : Type@m }}.
-Proof with mauto.
-  intros * Hnm HT.
-  induction m; inversion Hnm; subst...
+#[export]
+Hint Resolve ctx_decomp : mcltt.
+
+Lemma ctx_decomp_left : forall {Γ A}, {{ ⊢ Γ , A }} -> {{ ⊢ Γ }}.
+Proof with solve [eauto].
+  intros * HAΓ.
+  eapply proj1, ctx_decomp...
+Qed.
+
+Lemma ctx_decomp_right : forall {Γ A}, {{ ⊢ Γ , A }} -> ∃ i, {{ Γ ⊢ A : Type@i }}.
+Proof with solve [eauto].
+  intros * HAΓ.
+  eapply proj2, ctx_decomp...
 Qed.
 
 #[export]
-Hint Resolve lift_tm_ge : mcltt.
+Hint Resolve ctx_decomp_left ctx_decomp_right : mcltt.
 
-Lemma lift_tm_max_left : forall {Γ T n} m, {{ Γ ⊢ T : Type@n }} -> {{ Γ ⊢ T : Type@(max n m) }}.
-Proof with mauto.
+Lemma lift_exp_ge : forall {Γ A n m}, n <= m -> {{ Γ ⊢ A : Type@n }} -> {{ Γ ⊢ A : Type@m }}.
+Proof with solve [mauto].
+  intros * Hnm HA.
+  induction Hnm...
+Qed.
+
+#[export]
+Hint Resolve lift_exp_ge : mcltt.
+
+Lemma lift_exp_max_left : forall {Γ A n} m, {{ Γ ⊢ A : Type@n }} -> {{ Γ ⊢ A : Type@(max n m) }}.
+Proof with solve [mauto].
   intros.
   assert (n <= max n m) by lia...
 Qed.
 
-Lemma lift_tm_max_right : forall {Γ T} n {m}, {{ Γ ⊢ T : Type@m }} -> {{ Γ ⊢ T : Type@(max n m) }}.
-Proof with mauto.
+Lemma lift_exp_max_right : forall {Γ A} n {m}, {{ Γ ⊢ A : Type@m }} -> {{ Γ ⊢ A : Type@(max n m) }}.
+Proof with solve [mauto].
   intros.
   assert (m <= max n m) by lia...
 Qed.
 
-Lemma lift_eq_ge : forall {Γ T T' n m}, n <= m -> {{ Γ ⊢ T ≈ T': Type@n }} -> {{ Γ ⊢ T ≈ T' : Type@m }}.
-Proof with mauto.
-  intros * Hnm HTT'.
-  induction m; inversion Hnm; subst...
+Lemma lift_exp_eq_ge : forall {Γ A A' n m}, n <= m -> {{ Γ ⊢ A ≈ A': Type@n }} -> {{ Γ ⊢ A ≈ A' : Type@m }}.
+Proof with solve [mauto].
+  intros * Hnm HAA'.
+  induction Hnm; subst...
 Qed.
 
 #[export]
-Hint Resolve lift_eq_ge : mcltt.
+Hint Resolve lift_exp_eq_ge : mcltt.
 
-Lemma lift_eq_max_left : forall {Γ T T' n} m, {{ Γ ⊢ T ≈ T' : Type@n }} -> {{ Γ ⊢ T ≈ T' : Type@(max n m) }}.
-Proof with mauto.
+Lemma lift_exp_eq_max_left : forall {Γ A A' n} m, {{ Γ ⊢ A ≈ A' : Type@n }} -> {{ Γ ⊢ A ≈ A' : Type@(max n m) }}.
+Proof with solve [mauto].
   intros.
   assert (n <= max n m) by lia...
 Qed.
 
-Lemma lift_eq_max_right : forall {Γ T T'} n {m}, {{ Γ ⊢ T ≈ T' : Type@m }} -> {{ Γ ⊢ T ≈ T' : Type@(max n m) }}.
-Proof with mauto.
+Lemma lift_exp_eq_max_right : forall {Γ A A'} n {m}, {{ Γ ⊢ A ≈ A' : Type@m }} -> {{ Γ ⊢ A ≈ A' : Type@(max n m) }}.
+Proof with solve [mauto].
   intros.
   assert (m <= max n m) by lia...
 Qed.
 
-(* Corresponds to presup-⊢≈ in the Agda proof *)
 Lemma presup_ctx_eq : forall {Γ Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ ⊢ Γ }} ∧ {{ ⊢ Δ }}.
-Proof with mauto.
+Proof with solve [mauto].
   intros * HΓΔ.
-  induction HΓΔ as [|* ? [? ?]]...
+  induction HΓΔ as [|* ? []]...
+Qed.
+
+Lemma presup_ctx_eq_left : forall {Γ Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ ⊢ Γ }}.
+Proof with solve [eauto].
+  intros * HΓΔ.
+  eapply proj1, presup_ctx_eq...
+Qed.
+
+Lemma presup_ctx_eq_right : forall {Γ Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ ⊢ Δ }}.
+Proof with solve [eauto].
+  intros * HΓΔ.
+  eapply proj2, presup_ctx_eq...
+Qed.
+
+#[export]
+Hint Resolve presup_ctx_eq presup_ctx_eq_left presup_ctx_eq_right : mcltt.
+
+Lemma presup_sub_ctx : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ ⊢ Γ }} ∧ {{ ⊢ Δ }}.
+Proof with solve [mauto].
+  intros * Hσ.
+  induction Hσ; repeat destruct_one_pair...
+Qed.
+
+Lemma presup_sub_ctx_left : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ ⊢ Γ }}.
+Proof with solve [eauto].
+  intros * Hσ.
+  eapply proj1, presup_sub_ctx...
+Qed.
+
+Lemma presup_sub_ctx_right : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ ⊢ Δ }}.
+Proof with solve [eauto].
+  intros * Hσ.
+  eapply proj2, presup_sub_ctx...
+Qed.
+
+#[export]
+Hint Resolve presup_sub_ctx presup_sub_ctx_left presup_sub_ctx_right : mcltt.
+
+Lemma presup_exp_ctx : forall {Γ M A}, {{ Γ ⊢ M : A }} -> {{ ⊢ Γ }}.
+Proof with solve [mauto].
+  intros * HM.
+  induction HM...
+Qed.
+
+#[export]
+Hint Resolve presup_exp_ctx : mcltt.
+
+Lemma presup_sub_eq_ctx : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Γ }} /\ {{ ⊢ Δ }}.
+Proof with solve [mauto].
+  intros * Hσσ'.
+  induction Hσσ'; repeat destruct_one_pair...
 Qed.
 
-(* Corresponds to ≈-refl in the Agda code *)
-Lemma tm_eq_refl : forall {Γ t T}, {{ Γ ⊢ t : T }} -> {{ Γ ⊢ t ≈ t : T }}.
+Lemma presup_sub_eq_ctx_left : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Γ }}.
+Proof with solve [eauto].
+  intros * Hσσ'.
+  eapply proj1, presup_sub_eq_ctx...
+Qed.
+
+Lemma presup_sub_eq_ctx_right : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Δ }}.
+Proof with solve [eauto].
+  intros * Hσσ'.
+  eapply proj2, presup_sub_eq_ctx...
+Qed.
+
+#[export]
+Hint Resolve presup_sub_eq_ctx presup_sub_eq_ctx_left presup_sub_eq_ctx_right : mcltt.
+
+Lemma presup_exp_eq_ctx : forall {Γ M M' A}, {{ Γ ⊢ M ≈ M' : A }} -> {{ ⊢ Γ }}.
+Proof with solve [mauto].
+  intros * HMM'.
+  induction HMM'...
+  Unshelve.
+  all: constructor.
+Qed.
+
+#[export]
+Hint Resolve presup_exp_eq_ctx : mcltt.
+
+Lemma exp_eq_refl : forall {Γ M A}, {{ Γ ⊢ M : A }} -> {{ Γ ⊢ M ≈ M : A }}.
 Proof.
   mauto.
 Qed.
 
-Lemma sb_eq_refl : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢s σ ≈ σ : Δ }}.
+#[export]
+Hint Resolve exp_eq_refl : mcltt.
+
+Lemma sub_eq_refl : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢s σ ≈ σ : Δ }}.
 Proof.
   mauto.
 Qed.
 
 #[export]
-Hint Resolve ctx_decomp presup_ctx_eq tm_eq_refl sb_eq_refl : mcltt.
+Hint Resolve sub_eq_refl : mcltt.
+
+Lemma ctx_eq_sym : forall {Γ Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ ⊢ Δ ≈ Γ }}.
+Proof with solve [mauto].
+  intros * HΓΔ.
+  induction HΓΔ...
+Qed.
+
+#[export]
+Hint Resolve ctx_eq_sym : mcltt.
 
-(* Corresponds to t[σ]-Se in the Agda proof *)
-Lemma exp_sub_typ : forall {Δ Γ T σ i}, {{ Δ ⊢ T : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ T[σ] : Type@i }}.
+Lemma exp_sub_typ : forall {Δ Γ A σ i}, {{ Δ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ A[σ] : Type@i }}.
 Proof.
   mauto.
 Qed.
 
-(* Corresponds to []-cong-Se′ in the Agda proof*)
-Lemma eq_exp_sub_typ : forall {Δ Γ T T' σ i}, {{ Δ ⊢ T ≈ T' : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ T[σ] ≈ T'[σ] : Type@i }}.
+Lemma exp_eq_sub_cong_typ1 : forall {Δ Γ A A' σ i}, {{ Δ ⊢ A ≈ A' : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ A[σ] ≈ A'[σ] : Type@i }}.
 Proof.
   mauto.
 Qed.
 
+Lemma exp_eq_sub_cong_typ2' : forall {Δ Γ A σ τ i}, {{ Δ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢s σ ≈ τ : Δ }} -> {{ Γ ⊢ A[σ] ≈ A[τ] : Type@i }}.
+Proof with solve [mauto].
+  intros.
+  eapply wf_exp_eq_conv...
+Qed.
+
+Lemma exp_eq_sub_compose_typ : forall {Ψ Δ Γ A σ τ i}, {{ Ψ ⊢ A : Type@i }} -> {{ Δ ⊢s σ : Ψ }} -> {{ Γ ⊢s τ : Δ }} -> {{ Γ ⊢ A[σ][τ] ≈ A[σ∘τ] : Type@i }}.
+Proof with solve [mauto].
+  intros.
+  eapply wf_exp_eq_conv...
+Qed.
+
 #[export]
-Hint Resolve exp_sub_typ eq_exp_sub_typ : mcltt.
+Hint Resolve exp_sub_typ exp_eq_sub_cong_typ1 exp_eq_sub_cong_typ2' exp_eq_sub_compose_typ : mcltt.
 
-(* Corresponds to ∈!⇒ty-wf in Agda proof *)
-Lemma var_in_wf : forall {Γ T x}, {{ ⊢ Γ }} -> {{ #x : T ∈ Γ }} -> ∃ i, {{ Γ ⊢ T : Type@i }}.
-Proof with mauto.
-  intros * HΓ Hx. gen x T.
-  induction HΓ; intros; inversion_clear Hx as [|? ? ? ? Hx']...
-  destruct (IHHΓ _ _ Hx')...
+Lemma exp_eq_typ_sub_sub : forall {Γ Δ Ψ σ τ i}, {{ Δ ⊢s σ : Ψ }} -> {{ Γ ⊢s τ : Δ }} -> {{ Γ ⊢ Type@i[σ][τ] ≈ Type@i : Type@(S i) }}.
+Proof.
+  mauto.
 Qed.
 
 #[export]
-Hint Resolve var_in_wf : mcltt.
+Hint Resolve exp_eq_typ_sub_sub : mcltt.
 
-Lemma presup_sb_ctx : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ ⊢ Γ }} ∧ {{ ⊢ Δ }}.
-Proof with mauto.
-  intros * Hσ.
-  induction Hσ...
-  - split; [|eapply ctx_decomp]...
-  - destruct IHHσ1, IHHσ2...
-  - destruct IHHσ...
-  - destruct IHHσ; split...
-    eapply proj2...
+Lemma vlookup_0_typ : forall {Γ i}, {{ ⊢ Γ }} -> {{ Γ, Type@i ⊢ # 0 : Type@i }}.
+Proof with solve [mauto].
+  intros.
+  eapply wf_conv...
+  Unshelve.
+  all: constructor.
+Qed.
+
+Lemma vlookup_1_typ : forall {Γ i A j}, {{ ⊢ Γ }} -> {{ Γ, Type@i ⊢ A : Type@j }} -> {{ Γ, Type@i, A ⊢ # 1 : Type@i }}.
+Proof with solve [mauto].
+  intros.
+  assert {{ ⊢ Γ, Type@i }} by mauto.
+  assert {{ ⊢ Γ, Type@i, A }} by mauto.
+  eapply wf_conv...
+  Unshelve.
+  all: constructor.
 Qed.
 
 #[export]
-Hint Resolve presup_sb_ctx : mcltt.
+Hint Resolve vlookup_0_typ vlookup_1_typ : mcltt.
 
-Lemma presup_tm_ctx : forall {Γ t T}, {{ Γ ⊢ t : T }} -> {{ ⊢ Γ }}.
-Proof with mauto.
-  intros * Ht.
-  induction Ht...
-  eapply proj1...
+Lemma exp_eq_var_0_sub_typ : forall {Γ σ Δ M i}, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ M : Type@i }} -> {{ Γ ⊢ #0[σ ,, M] ≈ M : Type@i }}.
+Proof with solve [mauto].
+  intros.
+  assert {{ ⊢ Δ }} by mauto.
+  assert {{ Γ ⊢ M : Type@i[σ] }} by mauto.
+  eapply wf_exp_eq_conv...
+  Unshelve.
+  constructor.
+Qed.
+
+Lemma exp_eq_var_1_sub_typ : forall {Γ σ Δ A i M j}, {{ Γ ⊢s σ : Δ }} -> {{ Δ ⊢ A : Type@i }} -> {{ Γ ⊢ M : A[σ] }} -> {{ #0 : Type@j[Wk] ∈ Δ }} -> {{ Γ ⊢ #1[σ ,, M] ≈ #0[σ] : Type@j }}.
+Proof with solve [mauto].
+  intros * ? ? ? Hvar0.
+  inversion Hvar0 as [? Δ'|]; subst.
+  assert {{ ⊢ Δ' }} by mauto.
+  eapply wf_exp_eq_conv...
 Qed.
 
 #[export]
-Hint Resolve presup_tm_ctx : mcltt.
+Hint Resolve exp_eq_var_0_sub_typ exp_eq_var_1_sub_typ : mcltt.
 
-(* Corresponds to ∈!⇒ty≈ in Agda proof *)
-Lemma var_in_eq : forall {Γ Δ T x}, {{ ⊢ Γ ≈ Δ }} -> {{ #x : T ∈ Γ }} -> ∃ S i, {{ #x : S ∈ Δ }} ∧ {{ Γ ⊢ T ≈ S : Type@i }} ∧ {{ Δ ⊢ T ≈ S : Type@i }}.
-Proof with mauto.
-  intros * HΓΔ Hx.
-  gen Δ; induction Hx; intros; inversion_clear HΓΔ as [|? ? ? ? ? HΓΔ'].
-  - do 2 eexists; repeat split...
-  - destruct (IHHx _ HΓΔ') as [? [? [? [? ?]]]].
-    do 2 eexists; repeat split...
+Lemma exp_eq_var_0_weaken_typ : forall {Γ A i}, {{ ⊢ Γ , A }} -> {{ #0 : Type@i[Wk] ∈ Γ }} -> {{ Γ , A ⊢ #0[Wk] ≈ #1 : Type@i }}.
+Proof with solve [mauto].
+  intros * ? Hvar0.
+  assert {{ ⊢ Γ }} by mauto.
+  inversion Hvar0 as [? Γ'|]; subst.
+  assert {{ ⊢ Γ' }} by mauto.
+  eapply wf_exp_eq_conv; only 1: solve [mauto].
+  eapply exp_eq_typ_sub_sub; [|solve [mauto]]...
 Qed.
 
-(* Corresponds to ⊢≈-sym in Agda proof *)
-Lemma ctx_eq_sym : forall {Γ Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ ⊢ Δ ≈ Γ }}.
-Proof with mauto.
+#[export]
+Hint Resolve exp_eq_var_0_weaken_typ : mcltt.
+
+Lemma sub_extend_typ : forall {Γ σ Δ M i}, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ M : Type@i }} -> {{ Γ ⊢s (σ ,, M) : Δ , Type@i }}.
+Proof with solve [mauto].
   intros.
-  induction H...
+  assert {{ ⊢ Δ }} by mauto.
+  econstructor...
+  Unshelve.
+  constructor.
 Qed.
 
 #[export]
-Hint Resolve var_in_eq ctx_eq_sym : mcltt.
+Hint Resolve sub_extend_typ : mcltt.
+
+Lemma sub_eq_extend_cong_typ' : forall {Γ σ σ' Δ M M' i}, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ Γ ⊢ M ≈ M' : Type@i }} -> {{ Γ ⊢s (σ ,, M) ≈ (σ' ,, M') : Δ , Type@i }}.
+Proof with solve [mauto].
+  intros.
+  assert {{ ⊢ Δ }} by mauto.
+  econstructor...
+  Unshelve.
+  constructor.
+Qed.
 
-Lemma presup_sb_eq_ctx : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Γ }}.
-Proof with mauto.
+Lemma sub_eq_extend_compose_typ : forall {Γ τ Γ' σ Γ'' A i M j}, {{ Γ' ⊢s σ : Γ'' }} -> {{ Γ'' ⊢ A : Type@i }} -> {{ Γ' ⊢ M : Type@j }} -> {{ Γ ⊢s τ : Γ' }} -> {{ Γ ⊢s (σ ,, M) ∘ τ ≈ ((σ ∘ τ) ,, M[τ]) : Γ'' , Type@j }}.
+Proof with solve [mauto].
   intros.
-  induction H; mauto; now (eapply proj1; mauto).
+  econstructor...
+Qed.
+
+Lemma sub_eq_p_extend_typ : forall {Γ σ Γ' M i}, {{ Γ' ⊢s σ : Γ }} -> {{ Γ' ⊢ M : Type@i }} -> {{ Γ' ⊢s Wk ∘ (σ ,, M) ≈ σ : Γ }}.
+Proof with solve [mauto].
+  intros.
+  assert {{ ⊢ Γ }} by mauto.
+  econstructor; only 1,3: solve [mauto]...
+  Unshelve.
+  constructor.
 Qed.
 
 #[export]
-Hint Resolve presup_sb_eq_ctx : mcltt.
+Hint Resolve sub_eq_extend_cong_typ' sub_eq_extend_compose_typ sub_eq_p_extend_typ : mcltt.
 
-Lemma presup_tm_eq_ctx : forall {Γ t t' T}, {{ Γ ⊢ t ≈ t' : T }} -> {{ ⊢ Γ }}.
-Proof with mauto.
+Lemma exp_eq_sub_sub_compose_cong_typ : forall {Γ Δ Δ' Ψ σ τ σ' τ' A i}, {{ Ψ ⊢ A : Type@i }} -> {{ Δ ⊢s σ : Ψ }} -> {{ Δ' ⊢s σ' : Ψ }} -> {{ Γ ⊢s τ : Δ }} -> {{ Γ ⊢s τ' : Δ' }} -> {{ Γ ⊢s σ∘τ ≈ σ'∘τ' : Ψ }} -> {{ Γ ⊢ A[σ][τ] ≈ A[σ'][τ'] : Type@i }}.
+Proof with solve [mauto].
   intros.
-  induction H...
+  assert {{ Γ ⊢ A[σ][τ] ≈ A[σ∘τ] : Type@i }} by mauto.
+  assert {{ Γ ⊢ A[σ∘τ] ≈ A[σ'∘τ'] : Type@i }} by mauto.
+  assert {{ Γ ⊢ A[σ'∘τ'] ≈ A[σ'][τ'] : Type@i }}...
+Qed.
+
+#[export]
+Hint Resolve exp_eq_sub_sub_compose_cong_typ : mcltt.
+
+Lemma exp_sub_nat : forall {Δ Γ M σ}, {{ Δ ⊢ M : ℕ }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ M[σ] : ℕ }}.
+Proof.
+  mauto.
   Unshelve.
   constructor.
 Qed.
 
+Lemma exp_eq_sub_cong_nat1 : forall {Δ Γ M M' σ}, {{ Δ ⊢ M ≈ M' : ℕ }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ M[σ] ≈ M'[σ] : ℕ }}.
+Proof.
+  mauto.
+  Unshelve.
+  constructor.
+Qed.
+
+Lemma exp_eq_sub_cong_nat2' : forall {Δ Γ M σ τ}, {{ Δ ⊢ M : ℕ }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢s σ ≈ τ : Δ }} -> {{ Γ ⊢ M[σ] ≈ M[τ] : ℕ }}.
+Proof with solve [mauto].
+  intros.
+  eapply wf_exp_eq_conv...
+  Unshelve.
+  constructor.
+Qed.
+
+Lemma exp_eq_sub_compose_nat : forall {Ψ Δ Γ M σ τ}, {{ Ψ ⊢ M : ℕ }} -> {{ Δ ⊢s σ : Ψ }} -> {{ Γ ⊢s τ : Δ }} -> {{ Γ ⊢ M[σ][τ] ≈ M[σ∘τ] : ℕ }}.
+Proof with solve [mauto].
+  intros.
+  eapply wf_exp_eq_conv...
+  Unshelve.
+  constructor.
+Qed.
+
+#[export]
+Hint Resolve exp_sub_nat exp_eq_sub_cong_nat1 exp_eq_sub_cong_nat2' exp_eq_sub_compose_nat : mcltt.
+
+Lemma exp_eq_nat_sub_sub : forall {Γ Δ Ψ σ τ i}, {{ Δ ⊢s σ : Ψ }} -> {{ Γ ⊢s τ : Δ }} -> {{ Γ ⊢ ℕ[σ][τ] ≈ ℕ : Type@i }}.
+Proof.
+  mauto.
+Qed.
+
+#[export]
+Hint Resolve exp_eq_nat_sub_sub : mcltt.
+
+Lemma exp_eq_nat_sub_sub_to_nat_sub : forall {Γ Δ Ψ Ψ' σ τ σ' i}, {{ Δ ⊢s σ : Ψ }} -> {{ Γ ⊢s τ : Δ }} -> {{ Γ ⊢s σ' : Ψ' }} -> {{ Γ ⊢ ℕ[σ][τ] ≈ ℕ[σ'] : Type@i }}.
+Proof.
+  mauto.
+Qed.
+
+#[export]
+Hint Resolve exp_eq_nat_sub_sub_to_nat_sub : mcltt.
+
+Lemma vlookup_0_nat : forall {Γ}, {{ ⊢ Γ }} -> {{ Γ, ℕ ⊢ # 0 : ℕ }}.
+Proof with solve [mauto].
+  intros.
+  assert {{ Γ, ℕ ⊢ # 0 : ℕ[Wk] }}...
+  Unshelve.
+  all: constructor.
+Qed.
+
+Lemma vlookup_1_nat : forall {Γ A i}, {{ ⊢ Γ }} -> {{ Γ, ℕ ⊢ A : Type@i }} -> {{ Γ, ℕ, A ⊢ # 1 : ℕ }}.
+Proof with solve [mauto].
+  intros.
+  assert {{ ⊢ Γ, ℕ }} by mauto.
+  assert {{ ⊢ Γ, ℕ, A }} by mauto.
+  assert {{ Γ, ℕ, A ⊢ #1 : ℕ[Wk][Wk] }}...
+  Unshelve.
+  all: constructor.
+Qed.
+
+#[export]
+Hint Resolve vlookup_0_nat vlookup_1_nat : mcltt.
+
+Lemma exp_eq_var_0_sub_nat : forall {Γ σ Δ M}, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ M : ℕ }} -> {{ Γ ⊢ #0[σ ,, M] ≈ M : ℕ }}.
+Proof with solve [mauto].
+  intros.
+  assert {{ ⊢ Δ }} by mauto.
+  assert {{ Γ ⊢ M : ℕ[σ] }} by mauto.
+  assert {{ Γ ⊢ #0[σ,, M] ≈ M : ℕ[σ] }}...
+  Unshelve.
+  all: constructor.
+Qed.
+
+Lemma exp_eq_var_1_sub_nat : forall {Γ σ Δ A i M}, {{ Γ ⊢s σ : Δ }} -> {{ Δ ⊢ A : Type@i }} -> {{ Γ ⊢ M : A[σ] }} -> {{ #0 : ℕ[Wk] ∈ Δ }} -> {{ Γ ⊢ #1[σ ,, M] ≈ #0[σ] : ℕ }}.
+Proof with solve [mauto].
+  intros * ? ? ? Hvar0.
+  inversion Hvar0 as [? Δ'|]; subst.
+  assert {{ ⊢ Δ' }} by mauto.
+  assert {{ Γ ⊢ #1[σ,, M] ≈ #0[σ] : ℕ[Wk][σ] }}...
+  Unshelve.
+  constructor.
+Qed.
+
+#[export]
+Hint Resolve exp_eq_var_0_sub_nat exp_eq_var_1_sub_nat : mcltt.
+
+Lemma exp_eq_var_0_weaken_nat : forall {Γ A}, {{ ⊢ Γ , A }} -> {{ #0 : ℕ[Wk] ∈ Γ }} -> {{ Γ , A ⊢ #0[Wk] ≈ #1 : ℕ }}.
+Proof with solve [mauto].
+  intros * ? Hvar0.
+  assert {{ ⊢ Γ }} by mauto.
+  inversion Hvar0 as [? Γ'|]; subst.
+  assert {{ ⊢ Γ' }} by mauto.
+  assert {{ Γ', ℕ, A ⊢ #0[Wk] ≈ # 1 : ℕ[Wk][Wk] }}...
+  Unshelve.
+  constructor.
+Qed.
+
+#[export]
+Hint Resolve exp_eq_var_0_weaken_nat : mcltt.
+
+Lemma sub_extend_nat : forall {Γ σ Δ M}, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ M : ℕ }} -> {{ Γ ⊢s (σ ,, M) : Δ , ℕ }}.
+Proof with solve [mauto].
+  intros.
+  assert {{ ⊢ Δ }} by mauto.
+  econstructor...
+  Unshelve.
+  all: constructor.
+Qed.
+
+#[export]
+Hint Resolve sub_extend_nat : mcltt.
+
+Lemma sub_eq_extend_cong_nat' : forall {Γ σ σ' Δ M M'}, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ Γ ⊢ M ≈ M' : ℕ }} -> {{ Γ ⊢s (σ ,, M) ≈ (σ' ,, M') : Δ , ℕ }}.
+Proof with solve [mauto].
+  intros.
+  assert {{ ⊢ Δ }} by mauto.
+  econstructor...
+  Unshelve.
+  all: constructor.
+Qed.
+
+Lemma sub_eq_extend_compose_nat : forall {Γ τ Γ' σ Γ'' A i M}, {{ Γ' ⊢s σ : Γ'' }} -> {{ Γ'' ⊢ A : Type@i }} -> {{ Γ' ⊢ M : ℕ }} -> {{ Γ ⊢s τ : Γ' }} -> {{ Γ ⊢s (σ ,, M) ∘ τ ≈ ((σ ∘ τ) ,, M[τ]) : Γ'' , ℕ }}.
+Proof with solve [mauto].
+  intros.
+  econstructor...
+  Unshelve.
+  all: constructor.
+Qed.
+
+Lemma sub_eq_p_extend_nat : forall {Γ σ Γ' M}, {{ Γ' ⊢s σ : Γ }} -> {{ Γ' ⊢ M : ℕ }} -> {{ Γ' ⊢s Wk ∘ (σ ,, M) ≈ σ : Γ }}.
+Proof with solve [mauto].
+  intros.
+  assert {{ ⊢ Γ }} by mauto.
+  econstructor; only 1,3: solve [mauto]...
+  Unshelve.
+  all: constructor.
+Qed.
+
+#[export]
+Hint Resolve sub_eq_extend_cong_nat' sub_eq_extend_compose_nat sub_eq_p_extend_nat : mcltt.
+
+Lemma exp_eq_sub_sub_compose_cong_nat : forall {Γ Δ Δ' Ψ σ τ σ' τ' M}, {{ Ψ ⊢ M : ℕ }} -> {{ Δ ⊢s σ : Ψ }} -> {{ Δ' ⊢s σ' : Ψ }} -> {{ Γ ⊢s τ : Δ }} -> {{ Γ ⊢s τ' : Δ' }} -> {{ Γ ⊢s σ∘τ ≈ σ'∘τ' : Ψ }} -> {{ Γ ⊢ M[σ][τ] ≈ M[σ'][τ'] : ℕ }}.
+Proof with solve [mauto].
+  intros.
+  assert {{ Γ ⊢ M[σ][τ] ≈ M[σ∘τ] : ℕ }} by mauto.
+  assert {{ Γ ⊢ M[σ∘τ] ≈ M[σ'∘τ'] : ℕ }} by mauto.
+  assert {{ Γ ⊢ M[σ'∘τ'] ≈ M[σ'][τ'] : ℕ }}...
+Qed.
+
+#[export]
+Hint Resolve exp_eq_sub_sub_compose_cong_nat : mcltt.
+
+Lemma exp_eq_sub_sub_compose_cong : forall {Γ Δ Δ' Ψ σ τ σ' τ' M A i}, {{ Ψ ⊢ A : Type@i }} -> {{ Ψ ⊢ M : A }} -> {{ Δ ⊢s σ : Ψ }} -> {{ Δ' ⊢s σ' : Ψ }} -> {{ Γ ⊢s τ : Δ }} -> {{ Γ ⊢s τ' : Δ' }} -> {{ Γ ⊢s σ∘τ ≈ σ'∘τ' : Ψ }} -> {{ Γ ⊢ M[σ][τ] ≈ M[σ'][τ'] : A[σ∘τ] }}.
+Proof with solve [mauto].
+  intros.
+  assert {{ Γ ⊢ M[σ][τ] ≈ M[σ∘τ] : A[σ∘τ] }} by mauto.
+  assert {{ Γ ⊢ M[σ∘τ] ≈ M[σ'∘τ'] : A[σ∘τ] }} by mauto.
+  assert {{ Γ ⊢ M[σ'∘τ'] ≈ M[σ'][τ'] : A[σ'∘τ'] }} by mauto.
+  assert {{ Γ ⊢ M[σ'∘τ'] ≈ M[σ'][τ'] : A[σ∘τ] }}...
+Qed.
+
+#[export]
+Hint Resolve exp_eq_sub_sub_compose_cong : mcltt.
+
+Lemma ctx_lookup_wf : forall {Γ A x}, {{ ⊢ Γ }} -> {{ #x : A ∈ Γ }} -> ∃ i, {{ Γ ⊢ A : Type@i }}.
+Proof with solve [mauto].
+  intros * HΓ Hx.
+  induction Hx; inversion_clear HΓ; [|assert (exists i, {{ Γ ⊢ A : Type@i }}) as [] by eauto]...
+Qed.
+
+#[export]
+Hint Resolve ctx_lookup_wf : mcltt.
+
+Lemma ctxeq_ctx_lookup : forall {Γ Δ A x}, {{ ⊢ Γ ≈ Δ }} -> {{ #x : A ∈ Γ }} -> ∃ B i, {{ #x : B ∈ Δ }} ∧ {{ Γ ⊢ A ≈ B : Type@i }} ∧ {{ Δ ⊢ A ≈ B : Type@i }}.
+Proof with solve [mauto].
+  intros * HΓΔ Hx; gen Δ.
+  induction Hx as [|* ? IHHx]; intros; inversion_clear HΓΔ as [|? ? ? ? ? HΓΔ'];
+    [|destruct (IHHx _ HΓΔ') as [? [? [? [? ?]]]]]; repeat eexists; repeat split...
+Qed.
+
+#[export]
+Hint Resolve ctxeq_ctx_lookup : mcltt.
+
+Lemma sub_id_extend : ∀ {Γ M A i}, {{ Γ ⊢ A : Type@i }} -> {{ Γ ⊢ M : A }} -> {{ Γ ⊢s Id,,M : Γ, A }}.
+Proof with solve [mauto].
+  intros.
+  econstructor...
+Qed.
+
+#[export]
+Hint Resolve sub_id_extend : mcltt.
+
+Lemma sub_eq_p_id_extend : ∀ {Γ M A i}, {{ Γ ⊢ A : Type@i }} -> {{ Γ ⊢ M : A }} -> {{ Γ ⊢s Wk∘(Id ,, M) ≈ Id : Γ }}.
+Proof with solve [mauto].
+  intros.
+  econstructor...
+Qed.
+
+#[export]
+Hint Resolve sub_eq_p_id_extend : mcltt.
+
+Lemma sub_q : forall {Γ A i σ Δ}, {{ Δ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ , A[σ] ⊢s q σ : Δ , A }}.
+Proof with solve [mauto].
+  intros.
+  assert {{ Γ, A[σ] ⊢ # 0 : A[σ][Wk] }} by mauto.
+  econstructor; [econstructor| |]...
+Qed.
+
+Lemma sub_q_typ : forall {Γ σ Δ i}, {{ Γ ⊢s σ : Δ }} -> {{ Γ , Type@i ⊢s q σ : Δ , Type@i }}.
+Proof with solve [mauto].
+  intros.
+  assert {{ ⊢ Δ }} by mauto.
+  assert {{ Γ, Type@i ⊢s σ ∘ Wk : Δ }} by (econstructor; mauto).
+  assert {{ Γ, Type@i ⊢ # 0 : Type@i[Wk] }} by mauto.
+  assert {{ Γ, Type@i ⊢ # 0 : Type@i }}...
+Qed.
+
+Lemma sub_q_nat : forall {Γ σ Δ}, {{ Γ ⊢s σ : Δ }} -> {{ Γ , ℕ ⊢s q σ : Δ , ℕ }}.
+Proof with solve [mauto].
+  intros.
+  assert {{ ⊢ Δ }} by mauto.
+  assert {{ Γ, ℕ ⊢s σ ∘ Wk : Δ }} by (econstructor; mauto).
+  assert {{ Γ, ℕ ⊢ # 0 : ℕ[Wk] }} by mauto.
+  assert {{ Γ, ℕ ⊢ # 0 : ℕ }}...
+Qed.
+
+#[export]
+Hint Resolve sub_q sub_q_typ sub_q_nat : mcltt.
+
+Lemma exp_eq_var_1_sub_q_sigma_nat : forall {Γ A i σ Δ}, {{ Δ, ℕ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ, ℕ, A[q σ] ⊢ #1[q (q σ)] ≈ #1 : ℕ }}.
+Proof with solve [mauto].
+  intros.
+  assert {{ ⊢ Δ }} by mauto.
+  assert {{ ⊢ Δ, ℕ }} by mauto.
+  assert {{ ⊢ Γ }} by mauto.
+  assert {{ ⊢ Γ, ℕ }} by mauto.
+  assert {{ Γ, ℕ ⊢s q σ : Δ, ℕ }} by mauto.
+  assert {{ ⊢ Γ, ℕ, A[q σ] }} by mauto.
+  assert {{ Γ, ℕ, A[q σ] ⊢ #1[q (q σ)] ≈ #0[q σ∘Wk] : ℕ }} by (eapply exp_eq_var_1_sub_nat; mauto).
+  assert {{ Γ, ℕ, A[q σ] ⊢ #0[q σ∘Wk] ≈ #0[q σ][Wk] : ℕ }} by mauto.
+  assert {{ Γ, ℕ ⊢ #0[q σ] ≈ #0 : ℕ }} by mauto.
+  assert {{ Γ, ℕ, A[q σ] ⊢ #0[q σ][Wk] ≈ #0[Wk] : ℕ }} by mauto.
+  assert {{ Γ, ℕ, A[q σ] ⊢ #0[Wk] ≈ #1 : ℕ }} by mauto.
+  assert {{ Γ, ℕ, A[q σ] ⊢ #1[q (q σ)] ≈ #1 : ℕ }}...
+Qed.
+
+#[export]
+Hint Resolve exp_eq_var_1_sub_q_sigma_nat : mcltt.
+
+Lemma sub_id_extend_zero : ∀ {Γ}, {{ ⊢ Γ }} -> {{ Γ ⊢s Id,,zero : Γ, ℕ }}.
+Proof.
+  mauto.
+Qed.
+
+Lemma sub_weak_compose_weak_extend_succ_var_1 : ∀ {Γ A i}, {{ Γ, ℕ ⊢ A : Type@i }} -> {{ Γ, ℕ, A ⊢s Wk∘Wk,,succ #1 : Γ, ℕ }}.
+Proof with solve [mauto].
+  intros.
+  assert {{ ⊢ Γ, ℕ }} by mauto.
+  assert {{ ⊢ Γ }} by mauto.
+  eapply sub_extend_nat...
+Qed.
+
+Lemma sub_eq_id_extend_nat_compose_sigma : ∀ {Γ M σ Δ}, {{ Γ ⊢s σ : Δ }} -> {{ Δ ⊢ M : ℕ }} -> {{ Γ ⊢s (Id,,M)∘σ ≈ σ,,M[σ] : Δ, ℕ }}.
+Proof with solve [mauto].
+  intros.
+  assert {{ Γ ⊢s (Id ,, M)∘σ ≈ Id∘σ ,, M[σ] : Δ, ℕ }} by (eapply sub_eq_extend_compose_nat; mauto).
+  assert {{ Γ ⊢s Id∘σ ,, M[σ] ≈ σ ,, M[σ] : Δ, ℕ }} by (eapply sub_eq_extend_cong_nat'; mauto)...
+  Unshelve.
+  constructor.
+Qed.
+
+Lemma sub_eq_id_extend_compose_sigma : ∀ {Γ M A σ Δ i}, {{ Γ ⊢s σ : Δ }} -> {{ Δ ⊢ A : Type@i }} -> {{ Δ ⊢ M : A }} -> {{ Γ ⊢s (Id,,M)∘σ ≈ σ,,M[σ] : Δ, A }}.
+Proof with solve [mauto].
+  intros.
+  assert {{ Γ ⊢s (Id ,, M)∘σ ≈ Id∘σ ,, M[σ] : Δ, A }} by (eapply wf_sub_eq_extend_compose; mauto).
+  assert {{ Γ ⊢ M[σ] ≈ M[σ] : A[σ] }} by mauto.
+  assert {{ Γ ⊢ M[σ] ≈ M[σ] : A[Id∘σ] }}...
+Qed.
+
+#[export]
+Hint Resolve sub_id_extend_zero sub_weak_compose_weak_extend_succ_var_1 sub_eq_id_extend_nat_compose_sigma sub_eq_id_extend_compose_sigma : mcltt.
+
+Lemma sub_eq_sigma_compose_weak_id_extend : ∀ {Γ M A i σ Δ}, {{ Γ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ M : A }} -> {{ Γ ⊢s (σ∘Wk)∘(Id,,M) ≈ σ : Δ }}.
+Proof with solve [mauto].
+  intros.
+  assert {{ Γ ⊢s Id,,M : Γ, A }} by mauto.
+  assert {{ Γ ⊢s (σ∘Wk)∘(Id,,M) ≈ σ∘(Wk∘(Id ,, M)) : Δ }} by mauto.
+  assert {{ Γ ⊢s Wk ∘ (Id,, M) ≈ Id : Γ }} by mauto.
+  assert {{ Γ ⊢s σ∘(Wk∘(Id ,, M)) ≈ σ∘Id : Δ }}...
+Qed.
+
+#[export]
+Hint Resolve sub_eq_sigma_compose_weak_id_extend : mcltt.
+
+Lemma sub_eq_q_sigma_id_extend : ∀ {Γ M A i σ Δ}, {{ Δ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ M : A[σ] }} -> {{ Γ ⊢s q σ∘(Id,,M) ≈ σ,,M : Δ, A }}.
+Proof with solve [mauto].
+  intros.
+  assert {{ Γ ⊢s Id ,, M : Γ, A[σ] }} by mauto.
+  assert {{ Γ, A[σ] ⊢ #0 : A[σ][Wk] }} by mauto.
+  assert {{ Γ, A[σ] ⊢ #0 : A[σ∘Wk] }} by mauto.
+  assert {{ Γ ⊢s q σ∘(Id ,, M) ≈ (σ∘Wk)∘(Id ,, M) ,, #0[Id ,, M] : Δ, A }} by mauto.
+  assert {{ Γ ⊢s (σ∘Wk)∘(Id ,, M) ≈ σ : Δ }} by mauto.
+  assert {{ Γ ⊢ M : A[σ][Id] }} by mauto.
+  assert {{ Γ ⊢ #0[Id ,, M] ≈ M : A[σ][Id] }} by mauto.
+  assert {{ Γ ⊢ #0[Id ,, M] ≈ M : A[σ] }} by mauto.
+  assert {{ Γ ⊢ #0[Id ,, M] ≈ M : A[(σ∘Wk)∘(Id ,, M)] }}...
+Qed.
+
+#[export]
+Hint Resolve sub_eq_q_sigma_id_extend : mcltt.
+
+Lemma sub_eq_p_q_sigma : ∀ {Γ A i σ Δ}, {{ Δ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ, A[σ] ⊢s Wk∘q σ ≈ σ∘Wk : Δ }}.
+Proof with solve [mauto].
+  intros.
+  assert {{ ⊢ Γ }} by mauto.
+  assert {{ Γ, A[σ] ⊢ #0 : A[σ][Wk] }} by mauto.
+  assert {{ Γ, A[σ] ⊢ #0 : A[σ∘Wk] }}...
+Qed.
+
+#[export]
+Hint Resolve sub_eq_p_q_sigma : mcltt.
+
+Lemma sub_eq_p_q_sigma_nat : ∀ {Γ σ Δ}, {{ Γ ⊢s σ : Δ }} -> {{ Γ, ℕ ⊢s Wk∘q σ ≈ σ∘Wk : Δ }}.
+Proof with solve [mauto].
+  intros.
+  assert {{ ⊢ Γ }} by mauto.
+  assert {{ Γ, ℕ ⊢ #0 : ℕ }}...
+Qed.
+
+#[export]
+Hint Resolve sub_eq_p_q_sigma_nat : mcltt.
+
+Lemma sub_eq_p_p_q_q_sigma_nat : ∀ {Γ A i σ Δ}, {{ Δ, ℕ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ, ℕ, A[q σ] ⊢s Wk∘(Wk∘q (q σ)) ≈ (σ∘Wk)∘Wk : Δ }}.
+Proof with solve [mauto].
+  intros.
+  assert {{ ⊢ Γ }} by mauto.
+  assert {{ Γ, ℕ, A[q σ] ⊢s Wk∘q (q σ) ≈ q σ ∘ Wk : Δ, ℕ }} by mauto.
+  assert {{ Γ, ℕ, A[q σ] ⊢s Wk∘(Wk∘q (q σ)) ≈ Wk ∘ (q σ ∘ Wk) : Δ }} by mauto.
+  assert {{ Δ, ℕ ⊢s Wk : Δ }} by mauto.
+  assert {{ Γ, ℕ ⊢s q σ : Δ, ℕ }} by mauto.
+  assert {{ Γ, ℕ, A[q σ] ⊢s Wk ∘ (q σ ∘ Wk) ≈ (Wk ∘ q σ) ∘ Wk : Δ }} by mauto.
+  assert {{ Γ, ℕ, A[q σ] ⊢s (Wk ∘ q σ) ∘ Wk ≈ (σ ∘ Wk) ∘ Wk : Δ }}...
+Qed.
+
+#[export]
+Hint Resolve sub_eq_p_p_q_q_sigma_nat : mcltt.
+
+Lemma sub_eq_q_sigma_compose_weak_weak_extend_succ_var_1 : ∀ {Γ A i σ Δ}, {{ Δ, ℕ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ, ℕ, A[q σ] ⊢s q σ∘(Wk∘Wk,,succ #1) ≈ (Wk∘Wk,,succ #1)∘q (q σ) : Δ, ℕ }}.
+Proof with solve [mauto].
+  intros.
+  assert {{ ⊢ Δ }} by mauto.
+  assert {{ Γ, ℕ ⊢s Wk : Γ }} by mauto.
+  assert {{ Γ, ℕ ⊢s σ∘Wk : Δ }} by mauto.
+  set (Γ' := {{{ Γ, ℕ, A[q σ] }}}).
+  set (WkWksucc := {{{ Wk∘Wk ,, succ #1 }}}).
+  assert {{ Γ' ⊢s Wk ∘ Wk : Γ }} by mauto.
+  assert {{ Γ' ⊢s WkWksucc : Γ, ℕ }} by mauto.
+  assert {{ Γ' ⊢s q σ∘WkWksucc ≈ (σ∘Wk)∘WkWksucc ,, #0[WkWksucc] : Δ, ℕ }} by mauto.
+  assert {{ Γ' ⊢ #1 : ℕ }} by mauto.
+  assert {{ Γ' ⊢ succ #1 : ℕ }} by mauto.
+  assert {{ Γ' ⊢s Wk∘WkWksucc ≈ Wk∘Wk : Γ }} by mauto.
+  assert {{ Γ' ⊢s (σ∘Wk)∘WkWksucc ≈ σ∘(Wk∘Wk) : Δ }} by mauto.
+  assert {{ Γ' ⊢s σ∘(Wk∘Wk) ≈ (σ∘Wk)∘Wk : Δ }} by mauto.
+  assert {{ Γ' ⊢s (σ∘Wk)∘Wk ≈ Wk∘(Wk∘q (q σ)) : Δ }} by mauto.
+  assert {{ Δ, ℕ, A ⊢s Wk : Δ, ℕ }} by mauto.
+  assert {{ Γ' ⊢s q (q σ) : Δ, ℕ, A }} by mauto.
+  assert {{ Γ' ⊢s (Wk∘Wk)∘q (q σ) ≈ Wk∘(Wk∘q (q σ)) : Δ }} by mauto.
+  assert {{ Γ' ⊢s σ∘(Wk∘Wk) ≈ (Wk∘Wk)∘q (q σ) : Δ }} by mauto.
+  assert {{ Γ' ⊢ #0[WkWksucc] ≈ succ #1 : ℕ }} by mauto.
+  assert {{ Γ' ⊢ succ #1 ≈ succ #1[q (q σ)] : ℕ }} by mauto.
+  assert {{ Γ' ⊢ succ #1 ≈ (succ #1)[q (q σ)] : ℕ }} by mauto.
+  assert {{ Γ' ⊢ #0[WkWksucc] ≈ (succ #1)[q (q σ)] : ℕ }} by mauto.
+  assert {{ Γ' ⊢s (σ∘Wk)∘WkWksucc ,, #0[WkWksucc] ≈ (Wk∘Wk)∘q (q σ) ,, (succ #1)[q (q σ)] : Δ, ℕ }} by mauto.
+  assert {{ Δ, ℕ, A ⊢s Wk∘Wk : Δ }} by mauto.
+  assert {{ Δ, ℕ, A ⊢ #1 : ℕ }} by mauto.
+  assert {{ Δ, ℕ, A ⊢ succ #1 : ℕ }} by mauto.
+  assert {{ Γ' ⊢s (Wk∘Wk)∘q (q σ) ,, (succ #1)[q (q σ)] ≈ WkWksucc∘q (q σ) : Δ, ℕ }}...
+  Unshelve.
+  all: constructor.
+Qed.
+
 #[export]
-Hint Resolve presup_tm_eq_ctx : mcltt.
+Hint Resolve sub_eq_q_sigma_compose_weak_weak_extend_succ_var_1 : mcltt.
diff --git a/theories/Frontend/Elaborator.v b/theories/Frontend/Elaborator.v
index 00adacb3..122f0901 100644
--- a/theories/Frontend/Elaborator.v
+++ b/theories/Frontend/Elaborator.v
@@ -42,6 +42,11 @@ Fixpoint elaborate (cst : Cst.obj) (ctx : list string) : option exp :=
       | Some a => Some (a_succ a)
       | None => None
       end
+  | Cst.natrec n mx m z sx sr s =>
+      match elaborate m (mx :: ctx), elaborate z ctx, elaborate s (sx :: sr :: ctx), elaborate n ctx with
+      | Some m, Some z, Some s, Some n => Some (a_natrec m z s n)
+      | _, _, _, _ => None
+      end
   | Cst.var s =>
       match lookup s ctx with
       | Some n => Some (a_var n)
@@ -72,6 +77,7 @@ Fixpoint cst_variables (cst : Cst.obj) : StrSet.t :=
   | Cst.nat => StrSet.empty
   | Cst.zero => StrSet.empty
   | Cst.succ c => cst_variables c
+  | Cst.natrec n mx m z sx sy s => StrSet.union (StrSet.union (cst_variables n) (StrSet.remove mx (cst_variables m))) (StrSet.union (cst_variables z) (StrSet.remove sx (StrSet.remove sy (cst_variables s))))
   | Cst.var s => StrSet.singleton s
   | Cst.fn s t c => StrSet.union (cst_variables t) (StrSet.remove s (cst_variables c))
   | Cst.pi s t c => StrSet.union (cst_variables t) (StrSet.remove s (cst_variables c))
@@ -89,6 +95,7 @@ Inductive closed_at : exp -> nat -> Prop :=
  | ca_zero : forall n, closed_at (a_zero) n
  | ca_type : forall n m, closed_at (a_typ m) n
  | ca_succ : forall a n, closed_at a n -> closed_at (a_succ a) n
+ | ca_natrec : forall n m z s l, closed_at n l -> closed_at m (1+l) -> closed_at z l -> closed_at s (2+l) -> closed_at (a_natrec m z s n) l
 .
 (* TODO: JH: create our own hint database. *)
 #[local]
@@ -160,6 +167,14 @@ exists a : exp, (elaborate cst ctx = Some a) /\ (closed_at a (length ctx)).
 Proof.
   induction cst; intros; simpl in *; eauto.
   - destruct (IHcst _ H) as [ast [-> ?]]; eauto.
+  - assert (cst_variables cst1 [<=] StrSProp.of_list ctx) by fsetdec.
+    assert (cst_variables cst2 [<=] StrSProp.of_list (s :: ctx)) by (simpl; fsetdec).
+    assert (cst_variables cst3 [<=] StrSProp.of_list ctx) by fsetdec.
+    assert (cst_variables cst4 [<=] StrSProp.of_list (s0 :: s1 :: ctx)) by (simpl; fsetdec).
+    destruct (IHcst1 _ H0) as [ast [-> ?]];
+      destruct (IHcst2 _ H1) as [ast' [-> ?]];
+      destruct (IHcst3 _ H2) as [ast'' [-> ?]];
+      destruct (IHcst4 _ H3) as [ast''' [-> ?]]; eauto.
   - assert (cst_variables cst1 [<=] StrSProp.of_list ctx) by fsetdec.
     assert (cst_variables cst2 [<=] StrSProp.of_list ctx) by fsetdec.
     destruct (IHcst1 _ H0) as [ast [-> ?]];