diff --git a/theories/Core/Syntactic/CoreInversions.v b/theories/Core/Syntactic/CoreInversions.v
index e4ae9d3..0c92306 100644
--- a/theories/Core/Syntactic/CoreInversions.v
+++ b/theories/Core/Syntactic/CoreInversions.v
@@ -1,5 +1,5 @@
 From Coq Require Import Setoid.
-From Mcltt Require Import Base LibTactics CtxSub.
+From Mcltt Require Import Base LibTactics.
 From Mcltt.Core Require Export SystemOpt.
 Import Syntax_Notations.
 
diff --git a/theories/Core/Syntactic/Corollaries.v b/theories/Core/Syntactic/Corollaries.v
index fd943a9..e082354 100644
--- a/theories/Core/Syntactic/Corollaries.v
+++ b/theories/Core/Syntactic/Corollaries.v
@@ -1,6 +1,6 @@
 From Coq Require Import Setoid Nat.
-From Mcltt Require Import Base LibTactics CtxSub.
-From Mcltt.Core Require Export SystemOpt CoreInversions.
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core Require Export CoreInversions.
 Import Syntax_Notations.
 
 Corollary sub_id_typ : forall Γ M A,
diff --git a/theories/Core/Syntactic/CtxEq.v b/theories/Core/Syntactic/CtxEq.v
index dbc45f0..83cba1c 100644
--- a/theories/Core/Syntactic/CtxEq.v
+++ b/theories/Core/Syntactic/CtxEq.v
@@ -1,5 +1,5 @@
-From Mcltt Require Import Base LibTactics CtxSub.
-From Mcltt Require Export System.
+From Mcltt Require Import Base LibTactics.
+From Mcltt Require Export CtxSub.
 Import Syntax_Notations.
 
 Lemma ctx_eq_refl : forall {Γ}, {{ ⊢ Γ }} -> {{ ⊢ Γ ≈ Γ }}.
diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index 4fb4f72..3fb5409 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -1,5 +1,5 @@
-From Mcltt Require Import Base CtxEq LibTactics.
-From Mcltt Require Export System.
+From Mcltt Require Import Base LibTactics.
+From Mcltt Require Export CtxEq.
 Import Syntax_Notations.
 
 #[local]
@@ -13,20 +13,11 @@ Ltac gen_presup_ctx H :=
       let HΓ := fresh "HΓ" in
       let HΔ := fresh "HΔ" in
       pose proof presup_ctx_sub H as [HΓ HΔ]
-  | {{ ~?Γ ⊢s ~?σ : ~?Δ }} =>
-      let HΓ := fresh "HΓ" in
-      let HΔ := fresh "HΔ" in
-      pose proof presup_sub_ctx H as [HΓ HΔ]
   end.
 
 #[local]
-Ltac gen_presup_IH presup_exp presup_exp_eq presup_sub_eq presup_subtyp H :=
+Ltac gen_presup_IH presup_exp_eq presup_sub_eq presup_subtyp H :=
   match type of H with
-  | {{ ~?Γ ⊢ ~?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
@@ -46,69 +37,71 @@ Ltac gen_presup_IH presup_exp presup_exp_eq presup_sub_eq presup_subtyp H :=
       let HM := fresh "HM" in
       let HN := fresh "HN" in
       pose proof presup_subtyp _ _ _ H as [HΓ [i [HM HN]]]
+  | {{ ~?Γ ⊢ ~?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]]
+  | {{ ~?Γ ⊢s ~?σ : ~?Δ }} =>
+      let HΓ := fresh "HΓ" in
+      let HΔ := fresh "HΔ" in
+      pose proof presup_sub H as [HΓ HΔ]
   | _ => gen_presup_ctx H
   end.
 
-Lemma presup_exp : forall {Γ M A}, {{ Γ ⊢ M : A }} -> {{ ⊢ Γ }} /\ exists i, {{ Γ ⊢ A : Type@i }}
-with presup_exp_eq : forall {Γ M M' A}, {{ Γ ⊢ M ≈ M' : A }} -> {{ ⊢ Γ }} /\ {{ Γ ⊢ M : A }} /\ {{ Γ ⊢ M' : A }} /\ exists i, {{ Γ ⊢ A : Type@i }}
+Lemma presup_exp_eq : forall {Γ M M' A}, {{ Γ ⊢ M ≈ M' : A }} -> {{ ⊢ Γ }} /\ {{ Γ ⊢ M : A }} /\ {{ Γ ⊢ M' : A }} /\ exists i, {{ Γ ⊢ A : Type@i }}
 with presup_sub_eq : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Γ }} /\ {{ Γ ⊢s σ : Δ }} /\ {{ Γ ⊢s σ' : Δ }} /\ {{ ⊢ Δ }}
 with presup_subtyp : forall {Γ M M'}, {{ Γ ⊢ M ⊆ M' }} -> {{ ⊢ Γ }} /\ exists i, {{ Γ ⊢ M : Type@i }} /\ {{ Γ ⊢ M' : Type@i }}.
 Proof with mautosolve 4.
-  2: set (WkWksucc := {{{ Wk∘Wk ,, succ #1 }}}).
-  all: inversion_clear 1; (on_all_hyp: gen_presup_IH presup_exp presup_exp_eq presup_sub_eq presup_subtyp);
-    clear presup_exp presup_exp_eq presup_sub_eq presup_subtyp;
+  1: set (WkWksucc := {{{ Wk∘Wk ,, succ #1 }}}).
+  all: inversion_clear 1; (on_all_hyp: gen_presup_IH presup_exp_eq presup_sub_eq presup_subtyp);
+    clear presup_exp_eq presup_sub_eq presup_subtyp;
     repeat split; mauto 4;
     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').
-  (** presup_exp cases *)
-  - 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...
 
   (** presup_exp_eq cases *)
   - assert {{ Γ ⊢s Id ,, N ≈ Id ,, N' : Γ, ℕ }} by mauto 4.
-    assert {{ Γ ⊢ B[Id ,, N] ≈ B[Id ,, N'] : Type@i }} by mauto.
+    assert {{ Γ ⊢ B[Id ,, N] ≈ B[Id ,, N'] : Type@i }} by mauto 3.
     assert {{ Γ ⊢ B[Id ,, N] ≈ B'[Id ,, N'] : Type@i }} by mauto 4.
-    assert {{ Γ ⊢ B[Id ,, zero] ≈ B'[Id ,, zero] : Type@i }} by mauto.
-    assert {{ Γ ⊢ NZ' : B'[Id ,, zero] }} by mauto.
-    assert {{ Γ, ℕ, B ⊢ NS' : B'[WkWksucc] }} by (eapply wf_conv; mauto 4).
+    assert {{ Γ ⊢ NZ' : B'[Id ,, zero] }} by (eapply wf_conv; mauto 3).
+    assert {{ Γ, ℕ, B ⊢ NS' : B'[WkWksucc] }} by (eapply wf_conv; mauto 3).
     assert {{ Γ, ℕ, B' ⊢ NS' : B'[WkWksucc] }} by mauto 4.
-    assert {{ Γ ⊢ rec N' return B' | zero -> NZ' | succ -> NS' end : B'[Id ,, N'] }} by mauto 4.
+    assert {{ Γ ⊢ rec N' return B' | zero -> NZ' | succ -> NS' end : B'[Id ,, N'] }} by mauto 3.
     eapply wf_conv...
 
-  - assert {{ Γ ⊢ B[(Id,,N)][σ] ≈ B[(Id,,N)∘σ] : Type@i }} by mauto 4.
-    assert {{ Γ ⊢s (Id,,N)∘σ ≈ σ,,N[σ] : Δ, ℕ }} by mauto.
+  - assert {{ Γ ⊢ B[(Id,,N)][σ] ≈ B[(Id,,N)∘σ] : Type@i }} by mauto 3.
+    assert {{ Γ ⊢s (Id,,N)∘σ ≈ σ,,N[σ] : Δ, ℕ }} by mauto 3.
     assert {{ Γ ⊢ B[(Id,,N)∘σ] ≈ B[σ,,N[σ]] : Type@i }} by mauto 4.
-    assert {{ Γ ⊢ B[(Id,,N)][σ] ≈ B[σ,,N[σ]] : Type@i }} by mauto 4.
     eapply wf_conv...
 
-  - assert {{ Γ ⊢s Id,,N[σ] : Γ, ℕ }} by mauto.
-    assert {{ Γ, ℕ ⊢s q σ : Δ, ℕ }} by mauto.
-    assert {{ Γ, ℕ ⊢ B[q σ] : Type@i }} by mauto.
-    assert {{ Γ ⊢ B[q σ][(Id,,N[σ])] ≈ B[q σ∘(Id,,N[σ])] : Type@i }} by mauto.
-    assert {{ Γ ⊢s q σ∘(Id,,N[σ]) ≈ σ,,N[σ] : Δ, ℕ }} 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 {{ Γ ⊢ ℕ ≈ ℕ[σ] : Type@0 }} by mauto.
-    assert {{ Γ ⊢ zero : ℕ[σ] }} by mauto.
-    assert {{ Γ ⊢s q σ∘(Id ,, zero) ≈ σ ,, zero : Δ, ℕ }} by mauto.
-    assert {{ Γ ⊢s σ ≈ Id∘σ : Δ }} by mauto.
+  - assert {{ Γ ⊢s Id,,N[σ] : Γ, ℕ }} by mauto 4.
+    assert {{ Γ, ℕ ⊢s q σ : Δ, ℕ }} by mauto 2.
+    assert {{ Γ, ℕ ⊢ B[q σ] : Type@i }} by mauto 2.
+    assert {{ Γ ⊢ B[q σ][(Id,,N[σ])] ≈ B[q σ∘(Id,,N[σ])] : Type@i }} by mauto 2.
+    assert {{ Γ ⊢s q σ∘(Id,,N[σ]) ≈ σ,,N[σ] : Δ, ℕ }} by mauto 3.
+    assert {{ Γ ⊢ B[q σ∘(Id,,N[σ])] ≈ B[σ,,N[σ]] : Type@i }} by mauto 3.
+    assert {{ Γ ⊢ B[q σ][Id,,N[σ]] ≈ B[σ,,N[σ]] : Type@i }} by mauto 3.
+    assert {{ Γ ⊢ NZ[σ] : B[Id ,, zero][σ] }} by mauto 3.
+    assert {{ Γ ⊢ ℕ ≈ ℕ[σ] : Type@0 }} by mauto 3.
+    assert {{ Γ ⊢ zero : ℕ[σ] }} by mauto 3.
+    assert {{ Γ ⊢s q σ∘(Id ,, zero) ≈ σ ,, zero : Δ, ℕ }} by mauto 3.
+    assert {{ Γ ⊢s σ ≈ Id∘σ : Δ }} by mauto 3.
     assert {{ Γ ⊢s σ ,, zero ≈ Id∘σ ,, zero[σ] : Δ, ℕ }} by mauto 4.
     assert {{ Γ ⊢s Id∘σ ,, zero[σ] ≈ (Id ,, zero)∘σ : Δ, ℕ }} by mauto.
-    assert {{ Γ ⊢s 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 {{ Γ ⊢ B[q σ][Id ,, zero] ≈ B[Id ,, zero][σ] : Type@i }} by mauto.
-    assert {{ Γ ⊢ NZ[σ] : B[q σ][Id ,, zero] }} by mauto.
+    assert {{ Γ ⊢s Id ,, zero : Γ, ℕ }} by mauto 2.
+    assert {{ Γ ⊢s q σ∘(Id ,, zero) ≈ (Id ,, zero)∘σ : Δ, ℕ }} by mauto 3.
+    assert {{ Γ ⊢ B[q σ∘(Id ,, zero)] ≈ B[(Id ,, zero)∘σ] : Type@i }} by mauto 3.
+    assert {{ Γ ⊢ B[q σ][Id ,, zero] ≈ B[Id ,, zero][σ] : Type@i }} by mauto 3.
+    assert {{ Γ ⊢ NZ[σ] : B[q σ][Id ,, zero] }} by mauto 4.
     set (Γ' := {{{ Γ, ℕ, B[q σ] }}}).
-    assert {{ Γ' ⊢s q (q σ) : Δ, ℕ, B }} by mauto 4.
-    assert {{ Γ' ⊢s q σ∘WkWksucc ≈ WkWksucc∘q (q σ) : Δ, ℕ }} by mauto.
-    assert {{ Γ' ⊢s WkWksucc : Γ, ℕ }} by mauto.
-    assert {{ Γ' ⊢ B[WkWksucc][q (q σ)] ≈ B[q σ][WkWksucc] : Type@i }} by mauto.
+    assert {{ Γ' ⊢s q (q σ) : Δ, ℕ, B }} by mauto 2.
+    assert {{ Γ' ⊢s q σ∘WkWksucc ≈ WkWksucc∘q (q σ) : Δ, ℕ }} by mauto 2.
+    assert {{ Γ' ⊢s WkWksucc : Γ, ℕ }} by mauto 2.
+    assert {{ Γ' ⊢ B[WkWksucc][q (q σ)] ≈ B[q σ][WkWksucc] : Type@i }} by mauto 4.
     assert {{ Γ' ⊢ NS[q (q σ)] : B[q σ][WkWksucc] }} by mauto 4.
     eapply wf_conv...
 
@@ -116,25 +109,28 @@ Proof with mautosolve 4.
 
   - set (recN := {{{ rec N return B | zero -> NZ | succ -> NS end }}}).
     set (IdNrecN := {{{ Id ,, N ,, recN }}}).
-    assert {{ Γ ⊢ recN : B[Id ,, N] }} by mauto.
+    assert {{ Γ ⊢ ℕ : Type@0 }} by mauto 3.
+    assert {{ Γ ⊢ recN : B[Id ,, N] }} by mauto 4.
+    assert {{ Γ, ℕ ⊢s Wk : Γ }} by mauto 2.
+    assert {{ Γ, ℕ, B ⊢s Wk : Γ, ℕ }} by mauto 2.
+    assert {{ Γ, ℕ, B ⊢s Wk∘Wk : Γ }} by mauto 2.
     assert {{ Γ ⊢s WkWksucc∘IdNrecN ≈ (Wk∘Wk)∘IdNrecN ,, (succ #1)[IdNrecN] : Γ, ℕ }}
-      by (eapply sub_eq_extend_compose_nat; mauto 4).
-    assert {{ Γ ⊢s IdNrecN : Γ, ℕ, B }} by mauto.
-    assert {{ Γ, ℕ, B ⊢s Wk∘Wk : Γ }} by mauto 4.
-    assert {{ Γ ⊢s (Wk∘Wk)∘IdNrecN : Γ }} by mauto 4.
-    assert {{ Γ ⊢s (Wk∘Wk)∘IdNrecN ≈ Wk∘(Wk∘IdNrecN) : Γ }} by mauto 4.
-    assert {{ Γ ⊢s Id,,N : Γ, ℕ }} by mauto 4.
-    assert {{ Γ ⊢s Wk∘(Wk∘IdNrecN) ≈ Wk∘(Id ,, N) : Γ }} by mauto 4.
+      by (eapply sub_eq_extend_compose_nat; mauto 3).
+    assert {{ Γ ⊢s IdNrecN : Γ, ℕ, B }} by mauto 3.
+    assert {{ Γ ⊢s (Wk∘Wk)∘IdNrecN : Γ }} by mauto 2.
+    assert {{ Γ ⊢s (Wk∘Wk)∘IdNrecN ≈ Wk∘(Wk∘IdNrecN) : Γ }} by mauto 2.
+    assert {{ Γ ⊢s Id,,N : Γ, ℕ }} by mauto 2.
+    assert {{ Γ ⊢s Wk∘(Wk∘IdNrecN) ≈ Wk∘(Id,,N) : Γ }} by mauto 4.
     assert {{ Γ ⊢s (Wk∘Wk)∘IdNrecN ≈ Id : Γ }} by mauto 4.
-    assert {{ Γ ⊢ #1[IdNrecN] ≈ #0[Id ,, N] : ℕ }} by mauto.
+    assert {{ Γ ⊢ #1[IdNrecN] ≈ #0[Id ,, N] : ℕ }} by mauto 3.
     assert {{ Γ ⊢ #1[IdNrecN] ≈ N : ℕ }} by mauto 4.
-    assert {{ Γ ⊢ succ #1[IdNrecN] ≈ succ N : ℕ }} by mauto.
+    assert {{ Γ ⊢ succ #1[IdNrecN] ≈ succ N : ℕ }} by mauto 2.
     assert {{ Γ ⊢ (succ #1)[IdNrecN] ≈ succ N : ℕ }} by mauto 4.
-    assert {{ Γ ⊢s (Wk∘Wk)∘IdNrecN ,, (succ #1)[IdNrecN] ≈ Id ,, succ N : Γ , ℕ }} by mauto.
-    assert {{ Γ ⊢s WkWksucc∘IdNrecN : Γ, ℕ }} by mauto.
-    assert {{ Γ ⊢s Id,,succ N : Γ, ℕ }} by mauto.
-    assert {{ Γ ⊢s WkWksucc∘IdNrecN ≈ Id ,, succ N : Γ , ℕ }} by mauto.
-    assert {{ Γ ⊢ B[WkWksucc∘IdNrecN] ≈ B[Id,,succ N] : Type@i }} by mauto 4.
+    assert {{ Γ ⊢s (Wk∘Wk)∘IdNrecN ,, (succ #1)[IdNrecN] ≈ Id ,, succ N : Γ , ℕ }} by mauto 2.
+    assert {{ Γ ⊢s WkWksucc∘IdNrecN : Γ, ℕ }} by mauto 3.
+    assert {{ Γ ⊢s Id,,succ N : Γ, ℕ }} by mauto 3.
+    assert {{ Γ ⊢s WkWksucc∘IdNrecN ≈ Id ,, succ N : Γ , ℕ }} by mauto 2.
+    assert {{ Γ ⊢ B[WkWksucc∘IdNrecN] ≈ B[Id,,succ N] : Type@i }} by mauto 2.
     enough {{ Γ ⊢ B[WkWksucc][IdNrecN] ≈ B[Id,,succ N] : Type@i }}...
 
   - eexists...
@@ -143,111 +139,110 @@ Proof with mautosolve 4.
 
   - mauto.
 
-  - 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.
-    assert {{ Γ ⊢ Π B C ≈ Π B' C : Type@(max i i0) }} by mauto.
+  - assert {{ Γ ⊢ B : Type@(max i i0) }} by mauto 2 using lift_exp_max_left.
+    assert {{ Γ ⊢ B ≈ B' : Type@(max i i0) }} by mauto 2 using lift_exp_eq_max_left.
+    assert {{ Γ, B ⊢ C : Type@(max i i0) }} by mauto 2 using lift_exp_max_right.
+    assert {{ Γ ⊢ Π B C ≈ Π B' C : Type@(max i i0) }} by mauto 3.
     assert {{ Γ, B' ⊢ N' : C }} by mauto 4.
     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[σ] : Type@(max i i0) }} by mauto.
-    assert {{ Γ, B[σ] ⊢ C[q σ] : Type@(max i i0) }} by mauto 4.
-    assert {{ Γ ⊢ Π B[σ] C[q σ] : Type@(max i i0) }} by mauto.
-    assert {{ Γ ⊢ Π B[σ] C[q σ] ≈ Π B[σ] C[q σ] : Type@(max i i0) }} by mauto.
-    assert {{ Γ, B[σ] ⊢ N[q σ] : C[q σ] }} by mauto 4.
-    assert {{ Γ ⊢ λ B[σ] N[q σ] : Π B[σ] C[q σ] }} by mauto 4.
+  - assert {{ Γ ⊢ B : Type@(max i i0) }} by mauto 2 using lift_exp_max_left.
+    assert {{ Γ, B ⊢ C : Type@(max i i0) }} by mauto 2 using lift_exp_max_right...
+
+  - assert {{ Δ ⊢ B : Type@(max i i0) }} by mauto 2 using lift_exp_max_left.
+    assert {{ Δ, B ⊢ C : Type@(max i i0) }} by mauto 2 using lift_exp_max_right.
+    assert {{ Γ ⊢ B[σ] : Type@(max i i0) }} by mauto 2.
+    assert {{ Γ, B[σ] ⊢ C[q σ] : Type@(max i i0) }} by mauto 3.
+    assert {{ Γ ⊢ Π B[σ] C[q σ] : Type@(max i i0) }} by mauto 2.
+    assert {{ Γ ⊢ Π B[σ] C[q σ] ≈ Π B[σ] C[q σ] : Type@(max i i0) }} by mauto 2.
+    assert {{ Γ, B[σ] ⊢ N[q σ] : C[q σ] }} by mauto 3.
+    assert {{ Γ ⊢ λ B[σ] N[q σ] : Π B[σ] C[q σ] }} by mauto 3.
     eapply wf_conv...
 
-  - 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 2 using lift_exp_max_left.
+    assert {{ Δ, B ⊢ C : Type@(max i i0) }} by mauto 2 using lift_exp_max_right.
     enough {{ Δ ⊢ Π B C : Type@(max i i0) }}...
 
-  - assert {{ Γ ⊢s Id ≈ Id : Γ }} by mauto.
-    assert {{ Γ ⊢ B ≈ B[Id] : Type@i }} by mauto.
+  - assert {{ Γ ⊢s Id ≈ Id : Γ }} by mauto 2.
+    assert {{ Γ ⊢ B ≈ B[Id] : Type@i }} by mauto 3.
     assert {{ Γ ⊢ L ≈ L' : B[Id] }} by mauto 4.
-    assert {{ Γ ⊢s Id ,, L ≈ Id ,, L' : Γ, B }} by mauto.
-    assert {{ Γ ⊢ C[Id ,, L] ≈ C[Id ,, L'] : Type@i }} by mauto 4.
+    assert {{ Γ ⊢s Id ,, L ≈ Id ,, L' : Γ, B }} by mauto 2.
+    assert {{ Γ ⊢ C[Id ,, L] ≈ C[Id ,, L'] : Type@i }} by mauto 3.
     eapply wf_conv...
 
   - assert {{ Γ ⊢ N[σ] : Π B[σ] C[q σ] }} by (eapply wf_conv; mauto).
     assert {{ Δ ⊢ L : B[Id] }} by mauto 4.
-    assert {{ Γ ⊢s (Id ,, L)∘σ ≈ Id∘σ ,, L[σ] : Δ, B }} by mauto.
-    assert {{ Γ ⊢s (Id ,, L)∘σ ≈ σ ,, L[σ] : Δ, B }} by mauto.
-    assert {{ Δ ⊢s Id ,, L : Δ, B }} by mauto.
-    assert {{ Γ ⊢s (Id ,, L)∘σ : Δ, B }} by mauto.
-    assert {{ Γ ⊢ C[(Id ,, L)∘σ] ≈ C[σ ,, L[σ]] : Type@i }} by mauto.
-    assert {{ Γ ⊢ C[Id ,, L][σ] ≈ C[σ ,, L[σ]] : Type@i }} by mauto 4.
+    assert {{ Γ ⊢s (Id ,, L)∘σ ≈ Id∘σ ,, L[σ] : Δ, B }} by mauto 3.
+    assert {{ Γ ⊢s (Id ,, L)∘σ ≈ σ ,, L[σ] : Δ, B }} by mauto 3.
+    assert {{ Δ ⊢s Id ,, L : Δ, B }} by mauto 3.
+    assert {{ Γ ⊢s (Id ,, L)∘σ : Δ, B }} by mauto 3.
+    assert {{ Γ ⊢ C[(Id ,, L)∘σ] ≈ C[σ ,, L[σ]] : Type@i }} by mauto 2.
+    assert {{ Γ ⊢ C[Id ,, L][σ] ≈ C[σ ,, L[σ]] : Type@i }} by mauto 3.
     eapply wf_conv...
 
-  - assert {{ Γ ⊢ B[σ] : Type@i }} by mauto.
-    assert {{ Γ, B[σ] ⊢ C[q σ] : Type@i }} by mauto 4.
-    assert {{ Γ ⊢ N[σ] : Π B[σ] C[q σ] }} by (eapply wf_conv; mauto 4).
-    assert {{ Γ ⊢ L[σ] : B[σ] }} by mauto.
-    assert {{ Γ, B[σ] ⊢s q σ : Δ, B }} by mauto.
-    assert {{ Γ ⊢s q σ∘(Id ,, L[σ]) ≈ σ ,, L[σ] : Δ, B }} by mauto.
-    assert {{ Γ ⊢s Id ,, L[σ] : Γ, B[σ] }} by mauto.
-    assert {{ Γ ⊢s q σ∘(Id ,, L[σ]) : Δ, B }} by mauto.
-    assert {{ Γ ⊢ C[q σ∘(Id ,, L[σ])] ≈ C[σ ,, L[σ]] : Type@i }} by mauto 4.
-    assert {{ Γ ⊢ C[q σ][(Id ,, L[σ])] ≈ C[σ ,, L[σ]] : Type@i }} by mauto 4.
+  - assert {{ Γ ⊢ B[σ] : Type@i }} by mauto 2.
+    assert {{ Γ, B[σ] ⊢s q σ : Δ, B }} by mauto 2.
+    assert {{ Γ, B[σ] ⊢ C[q σ] : Type@i }} by mauto 2.
+    assert {{ Γ ⊢ N[σ] : Π B[σ] C[q σ] }} by (eapply wf_conv; mauto 2).
+    assert {{ Γ ⊢ L[σ] : B[σ] }} by mauto 2.
+    assert {{ Γ ⊢s q σ∘(Id ,, L[σ]) ≈ σ ,, L[σ] : Δ, B }} by mauto 2.
+    assert {{ Γ ⊢s Id ,, L[σ] : Γ, B[σ] }} by mauto 2.
+    assert {{ Γ ⊢s q σ∘(Id ,, L[σ]) : Δ, B }} by mauto 2.
+    assert {{ Γ ⊢ C[q σ∘(Id ,, L[σ])] ≈ C[σ ,, L[σ]] : Type@i }} by mauto 2.
+    assert {{ Γ ⊢ C[q σ][(Id ,, L[σ])] ≈ C[σ ,, L[σ]] : Type@i }} by mauto 3.
     eapply wf_conv...
 
   - eexists...
 
   - set (Id0 := {{{ Id ,, #0 }}}).
-    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 Id0 : Γ, B, B[Wk] }} by mauto.
-    assert {{ Γ, B ⊢ M[Wk] #0 : C[q Wk][Id0] }} by mauto.
-    assert {{ Γ, B, B[Wk] ⊢s q Wk : Γ, B }} by mauto 4.
-    assert {{ Γ, B ⊢ M[Wk] #0 : C[q Wk ∘ Id0] }} by (eapply wf_conv; mauto 4).
-    assert {{ Γ, B ⊢ B[Wk][Id] ≈ B[Wk] : Type@i }} by mauto.
-    assert {{ Γ, B ⊢ #0 : B[Wk][Id] }} by mauto 3.
-    assert {{ Γ, B ⊢s Id0 : Γ, B, B[Wk] }} by mauto.
-    assert {{ Γ, B ⊢s Wk : Γ }} by mauto 4.
-    assert {{ Γ, B, B[Wk] ⊢s Wk∘Wk : Γ }} by mauto 4.
-    assert {{ Γ, B ⊢s (Wk∘Wk)∘Id0 : Γ }} by mauto 4.
-    assert {{ Γ, B, B[Wk] ⊢s Wk : Γ, B }} by mauto.
-    assert {{ Γ, B ⊢s Id ≈ Wk∘Id0 : Γ, B }} by mauto.
-    assert {{ Γ, B ⊢s Wk∘Id ≈ Wk∘(Wk∘Id0) : Γ }} by mauto.
+    assert {{ Γ, B ⊢s Wk : Γ }} by mauto 2.
+    assert {{ Γ, B ⊢ B[Wk] : Type@i }} by mauto 2.
+    assert {{ Γ, B, B[Wk] ⊢s Wk : Γ, B }} by mauto 3.
+    assert {{ Γ, B, B[Wk] ⊢s q Wk : Γ, B }} by mauto 2.
+    assert {{ Γ, B, B[Wk] ⊢ C[q Wk] : Type@i }} by mauto 2.
+    assert {{ Γ, B ⊢ M[Wk] : (Π B C)[Wk] }} by mauto 2.
+    assert {{ Γ, B ⊢ M[Wk] : Π B[Wk] C[q Wk] }} by mauto 4.
+    assert {{ Γ, B ⊢ #0 : B[Wk] }} by mauto 2.
+    assert {{ Γ, B ⊢s Id0 : Γ, B, B[Wk] }} by mauto 2.
+    assert {{ Γ, B ⊢ M[Wk] #0 : C[q Wk][Id0] }} by mauto 2.
+    assert {{ Γ, B ⊢ M[Wk] #0 : C[q Wk ∘ Id0] }} by (eapply wf_conv; mauto 3).
+    assert {{ Γ, B ⊢ B[Wk][Id] ≈ B[Wk] : Type@i }} by mauto 2.
+    assert {{ Γ, B ⊢ #0 : B[Wk][Id] }} by mauto 2.
+    assert {{ Γ, B, B[Wk] ⊢s Wk∘Wk : Γ }} by mauto 2.
+    assert {{ Γ, B ⊢s (Wk∘Wk)∘Id0 : Γ }} by mauto 2.
+    assert {{ Γ, B ⊢s Id ≈ Wk∘Id0 : Γ, B }} by mauto 3.
+    assert {{ Γ, B ⊢s Wk∘Id ≈ Wk∘(Wk∘Id0) : Γ }} by mauto 3.
     assert {{ Γ, B ⊢s Wk∘Id ≈ (Wk∘Wk)∘Id0 : Γ }} by mauto 4.
-    assert {{ Γ, B, B[Wk] ⊢ #0 : B[Wk][Wk] }} by mauto 4.
+    assert {{ Γ, B, B[Wk] ⊢ #0 : B[Wk][Wk] }} by mauto 3.
     assert {{ Γ, B, B[Wk] ⊢ #0 : B[Wk∘Wk] }} by (eapply wf_conv; mauto 3).
-    assert {{ Γ, B ⊢s q Wk ∘ Id0 ≈ (Wk∘Wk)∘Id0 ,, #0[Id0] : Γ, B }} by mauto.
-    assert {{ Γ, B ⊢s (Wk∘Wk)∘Id0 ≈ Wk∘(Wk∘Id0) : Γ }} by mauto.
-    assert {{ Γ, B ⊢s (Wk∘Wk)∘Id0 ≈ Wk∘Id : Γ }} by mauto.
-    assert {{ Γ, B ⊢ #0[Id0] ≈ #0 : B[Wk][Id] }} by mauto.
-    assert {{ Γ, B ⊢ #0 ≈ #0[Id] : B[Wk][Id] }} by mauto.
-    assert {{ Γ, B ⊢ #0[Id0] ≈ #0[Id] : B[Wk][Id] }} by mauto.
+    assert {{ Γ, B ⊢s q Wk ∘ Id0 ≈ (Wk∘Wk)∘Id0 ,, #0[Id0] : Γ, B }} by mauto 3.
+    assert {{ Γ, B ⊢s (Wk∘Wk)∘Id0 ≈ Wk∘(Wk∘Id0) : Γ }} by mauto 2.
+    assert {{ Γ, B ⊢s (Wk∘Wk)∘Id0 ≈ Wk∘Id : Γ }} by mauto 2.
+    assert {{ Γ, B ⊢ #0[Id0] ≈ #0 : B[Wk][Id] }} by mauto 3.
+    assert {{ Γ, B ⊢ #0 ≈ #0[Id] : B[Wk][Id] }} by mauto 3.
+    assert {{ Γ, B ⊢ #0[Id0] ≈ #0[Id] : B[Wk][Id] }} by mauto 2.
     assert {{ Γ, B ⊢ #0[Id0] ≈ #0[Id] : B[Wk∘Id] }} by (eapply wf_exp_eq_conv; mauto 4).
-    assert {{ Γ, B ⊢ B[Wk∘Id] ≈ B[(Wk∘Wk)∘Id0] : Type@i }} by mauto.
-    assert {{ Γ, B ⊢ #0[Id0] ≈ #0[Id] : B[(Wk∘Wk)∘Id0] }} by mauto.
-    assert {{ Γ, B ⊢s (Wk∘Wk)∘Id0 ,, #0[Id0] ≈ Wk∘Id ,, #0[Id] : Γ, B }} by mauto.
-    assert {{ Γ, B ⊢s Wk∘Id ,, #0[Id] ≈ Id : Γ, B }} by mauto.
-    assert {{ Γ, B ⊢s q Wk ∘ Id0 ≈ Id : Γ, B }} by mauto.
-    assert {{ Γ, B ⊢ C[q Wk ∘ Id0] ≈ C[Id] : Type@i }} by mauto 4.
+    assert {{ Γ, B ⊢ B[Wk∘Id] ≈ B[(Wk∘Wk)∘Id0] : Type@i }} by mauto 3.
+    assert {{ Γ, B ⊢ #0[Id0] ≈ #0[Id] : B[(Wk∘Wk)∘Id0] }} by mauto 3.
+    assert {{ Γ, B ⊢s (Wk∘Wk)∘Id0 ,, #0[Id0] ≈ Wk∘Id ,, #0[Id] : Γ, B }} by mauto 2.
+    assert {{ Γ, B ⊢s Wk∘Id ,, #0[Id] ≈ Id : Γ, B }} by mauto 4.
+    assert {{ Γ, B ⊢s q Wk ∘ Id0 ≈ Id : Γ, B }} by mauto 3.
+    assert {{ Γ, B ⊢ C[q Wk ∘ Id0] ≈ C[Id] : Type@i }} by mauto 3.
     enough {{ Γ, B ⊢ M[Wk] #0 : C }}...
 
-  - assert {{ Γ ⊢s Wk∘(σ ,, N') ≈ σ : Δ }} by mauto.
-    assert {{ Γ ⊢ B[Wk∘(σ ,, N')] ≈ B[σ] : Type@i }} by mauto.
-    assert {{ ⊢ Δ, B }} by mauto.
-    assert {{ Δ, B ⊢s Wk : Δ }} by mauto.
-    assert {{ Γ ⊢s σ ,, N' : Δ, B }} by mauto.
+  - assert {{ Γ ⊢s Wk∘(σ ,, N') ≈ σ : Δ }} by mauto 3.
+    assert {{ Γ ⊢ B[Wk∘(σ ,, N')] ≈ B[σ] : Type@i }} by mauto 4.
+    assert {{ ⊢ Δ, B }} by mauto 2.
+    assert {{ Δ, B ⊢s Wk : Δ }} by mauto 2.
+    assert {{ Γ ⊢s σ ,, N' : Δ, B }} by mauto 2.
     assert {{ Γ ⊢ B[Wk][σ ,, N'] ≈ B[σ] : Type@i }} by mauto 3.
     enough {{ Γ ⊢ #0[σ ,, N'] : B[Wk][σ ,, N'] }}...
 
-  - assert (exists i, {{ Δ ⊢ C : Type@i }}) as [i'] by mauto 3.
-    assert {{ Γ ⊢s Wk∘(σ ,, N) ≈ σ : Δ }} by mauto.
-    assert {{ Γ ⊢ C[Wk∘(σ ,, N)] ≈ C[σ] : Type@i' }} by mauto.
-    assert {{ Δ, B ⊢s Wk : Δ }} by mauto.
-    assert {{ Γ ⊢s σ ,, N : Δ, B }} by mauto.
+  - assert (exists i, {{ Δ ⊢ C : Type@i }}) as [i'] by mauto 2.
+    assert {{ Γ ⊢s Wk∘(σ ,, N) ≈ σ : Δ }} by mauto 2.
+    assert {{ Γ ⊢ C[Wk∘(σ ,, N)] ≈ C[σ] : Type@i' }} by mauto 4.
+    assert {{ Δ, B ⊢s Wk : Δ }} by mauto 3.
+    assert {{ Γ ⊢s σ ,, N : Δ, B }} by mauto 2.
     assert {{ Γ ⊢ C[Wk][σ ,, N] ≈ C[σ] : Type@i' }} by mauto 3.
     assert {{ Δ, B ⊢ #(S x) : C[Wk] }} by mauto 4.
     enough {{ Γ ⊢ #(S x)[σ ,, N] : C[Wk][σ ,, N] }}...
@@ -257,23 +252,23 @@ Proof with mautosolve 4.
   (** presup_sub_eq cases *)
   - econstructor...
 
-  - assert {{ Γ ⊢ B[σ] ≈ B[σ'] : Type@i }} by mauto 4.
+  - assert {{ Γ ⊢ B[σ] ≈ B[σ'] : Type@i }} by mauto 2.
     eapply wf_conv...
 
   - assert {{ Γ ⊢ N'[Id] : A[Id] }}...
 
-  - assert {{ Γ ⊢ N[σ][τ] : B[σ][τ] }} by mauto 4.
+  - assert {{ Γ ⊢ N[σ][τ] : B[σ][τ] }} by mauto 3.
     eapply wf_conv...
 
   - econstructor...
 
-  - econstructor; mauto 4.
+  - econstructor; mauto 3.
     eapply wf_conv...
 
   - mauto.
 
-  - assert (exists i, {{ Γ0 ⊢ A : Type@i }}) as [] by mauto.
-    assert {{ Γ ⊢ #0[σ] : A[Wk][σ] }} by mauto 4.
+  - assert (exists i, {{ Γ0 ⊢ A : Type@i }}) as [] by mauto 2.
+    assert {{ Γ ⊢ #0[σ] : A[Wk][σ] }} by mauto 3.
     enough {{ Γ ⊢ #0[σ] : A[Wk∘σ] }} by mauto 4.
     eapply wf_conv...
 
@@ -283,6 +278,6 @@ Proof with mautosolve 4.
   - mauto.
 Qed.
 
-Ltac gen_presup H := gen_presup_IH @presup_exp @presup_exp_eq @presup_sub_eq @presup_subtyp H.
+Ltac gen_presup H := gen_presup_IH @presup_exp_eq @presup_sub_eq @presup_subtyp H.
 
 Ltac gen_presups := (on_all_hyp: fun H => gen_presup H); invert_wf_ctx; clear_dups.
diff --git a/theories/Core/Syntactic/System/Lemmas.v b/theories/Core/Syntactic/System/Lemmas.v
index 2148760..0b742a6 100644
--- a/theories/Core/Syntactic/System/Lemmas.v
+++ b/theories/Core/Syntactic/System/Lemmas.v
@@ -1,7 +1,9 @@
 From Mcltt Require Import Base LibTactics System.Definitions.
 Import Syntax_Notations.
 
-(** *** Core Presuppositions *)
+(** ** Core Presuppositions *)
+
+(** *** Basic inversion *)
 Lemma ctx_decomp : forall {Γ A}, {{ ⊢ Γ , A }} -> {{ ⊢ Γ }} /\ exists i, {{ Γ ⊢ A : Type@i }}.
 Proof with now eauto.
   inversion 1...
@@ -23,6 +25,8 @@ Qed.
 #[export]
 Hint Resolve ctx_decomp_left ctx_decomp_right : mcltt.
 
+(** *** Context Presuppositions *)
+
 Lemma presup_ctx_eq : forall {Γ Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ ⊢ Γ }} /\ {{ ⊢ Δ }}.
 Proof with mautosolve.
   induction 1; destruct_pairs...
@@ -41,23 +45,25 @@ Qed.
 #[export]
 Hint Resolve presup_ctx_eq presup_ctx_eq_left presup_ctx_eq_right : mcltt.
 
-Lemma presup_sub_ctx : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ ⊢ Γ }} /\ {{ ⊢ Δ }}.
+Lemma presup_sub : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ ⊢ Γ }} /\ {{ ⊢ Δ }}.
 Proof with mautosolve.
   induction 1; destruct_pairs...
 Qed.
 
-Corollary presup_sub_ctx_left : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ ⊢ Γ }}.
+Corollary presup_sub_left : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ ⊢ Γ }}.
 Proof with easy.
-  intros * ?%presup_sub_ctx...
+  intros * ?%presup_sub...
 Qed.
 
-Corollary presup_sub_ctx_right : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ ⊢ Δ }}.
+Corollary presup_sub_right : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ ⊢ Δ }}.
 Proof with easy.
-  intros * ?%presup_sub_ctx...
+  intros * ?%presup_sub...
 Qed.
 
 #[export]
-Hint Resolve presup_sub_ctx presup_sub_ctx_left presup_sub_ctx_right : mcltt.
+Hint Resolve presup_sub presup_sub_left presup_sub_right : mcltt.
+
+(** With [presup_sub], we can prove similar for [exp]. *)
 
 Lemma presup_exp_ctx : forall {Γ M A}, {{ Γ ⊢ M : A }} -> {{ ⊢ Γ }}.
 Proof with mautosolve.
@@ -67,6 +73,8 @@ Qed.
 #[export]
 Hint Resolve presup_exp_ctx : mcltt.
 
+(** and other presuppositions about context well-formedness. *)
+
 Lemma presup_sub_eq_ctx : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Γ }} /\ {{ ⊢ Δ }}.
 Proof with mautosolve.
   induction 1; destruct_pairs...
@@ -93,24 +101,37 @@ Qed.
 #[export]
 Hint Resolve presup_exp_eq_ctx : mcltt.
 
-(** Recover some rules we had before adding subtyping.
-    Rest are recovered after presupposition lemmas (in SystemOpt). *)
+(** *** Immediate Results of Context Presuppositions *)
 
-Lemma wf_ctx_sub_refl : forall Γ Δ,
-    {{ ⊢ Γ ≈ Δ }} ->
-    {{ ⊢ Γ ⊆ Δ }}.
-Proof. induction 1; mauto. Qed.
+(** From above, we can get following helper lemmas about [{{{ Type@i }}}] and [{{{ ℕ }}}]. *)
+
+Lemma exp_sub_typ : forall {Δ Γ A σ i},
+    {{ Δ ⊢ A : Type@i }} ->
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Γ ⊢ A[σ] : Type@i }}.
+Proof with mautosolve 3.
+  intros.
+  econstructor; mauto 3.
+  econstructor...
+Qed.
 
 #[export]
-Hint Resolve wf_ctx_sub_refl : mcltt.
+Hint Resolve exp_sub_typ : mcltt.
 
-Lemma wf_conv : forall Γ M A i A',
-    {{ Γ ⊢ M : A }} ->
-    (** The next argument will be removed in SystemOpt *)
-    {{ Γ ⊢ A' : Type@i }} ->
-    {{ Γ ⊢ A ≈ A' : Type@i }} ->
-    {{ Γ ⊢ M : A' }}.
-Proof. mauto. Qed.
+Lemma exp_sub_nat : forall {Δ Γ M σ},
+    {{ Δ ⊢ M : ℕ }} ->
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Γ ⊢ M[σ] : ℕ }}.
+Proof with mautosolve 3.
+  intros.
+  econstructor; mauto 3.
+  econstructor...
+Qed.
+
+#[export]
+Hint Resolve exp_sub_nat : mcltt.
+
+(** Also we can recover cumulativity rules we had before adding subtyping. *)
 
 Lemma wf_cumu : forall Γ A i,
     {{ Γ ⊢ A : Type@i }} ->
@@ -120,26 +141,6 @@ Proof with mautosolve.
   enough {{ ⊢ Γ }}...
 Qed.
 
-#[export]
-Hint Resolve wf_conv wf_cumu : mcltt.
-
-Lemma wf_sub_conv : forall Γ σ Δ Δ',
-  {{ Γ ⊢s σ : Δ }} ->
-  {{ ⊢ Δ ≈ Δ' }} ->
-  {{ Γ ⊢s σ : Δ' }}.
-Proof. mauto. Qed.
-
-#[export]
-Hint Resolve wf_sub_conv : mcltt.
-
-Lemma wf_exp_eq_conv : forall Γ M M' A A' i,
-   {{ Γ ⊢ M ≈ M' : A }} ->
-   (** The next argument will be removed in SystemOpt *)
-   {{ Γ ⊢ A' : Type@i }} ->
-   {{ Γ ⊢ A ≈ A' : Type@i }} ->
-   {{ Γ ⊢ M ≈ M' : A' }}.
-Proof. mauto. Qed.
-
 Lemma wf_exp_eq_cumu : forall Γ A A' i,
     {{ Γ ⊢ A ≈ A' : Type@i }} ->
     {{ Γ ⊢ A ≈ A' : Type@(S i) }}.
@@ -149,29 +150,16 @@ Proof with mautosolve.
 Qed.
 
 #[export]
-Hint Resolve wf_exp_eq_conv wf_exp_eq_cumu : mcltt.
+Hint Resolve wf_cumu wf_exp_eq_cumu : mcltt.
 
-Lemma wf_sub_eq_conv : forall Γ σ σ' Δ Δ',
-    {{ Γ ⊢s σ ≈ σ' : Δ }} ->
-    {{ ⊢ Δ ≈ Δ' }} ->
-    {{ Γ ⊢s σ ≈ σ' : Δ' }}.
-Proof. mauto. Qed.
-
-#[export]
-Hint Resolve wf_sub_eq_conv : mcltt.
-
-Add Parametric Morphism Γ : (wf_sub_eq Γ)
-    with signature wf_ctx_eq ==> eq ==> eq ==> iff as wf_sub_eq_morphism_iff3.
-Proof.
-  intros Δ Δ' H **; split; [| symmetry in H]; mauto.
-Qed.
+(** We can prove some additional lemmas for type presuppositions as well. *)
 
 Lemma lift_exp_ge : forall {Γ A n m},
     n <= m ->
     {{ Γ ⊢ A : Type@n }} ->
     {{ Γ ⊢ A : Type@m }}.
 Proof with mautosolve.
-  induction 1...
+  induction 1; intros; mauto.
 Qed.
 
 #[export]
@@ -198,7 +186,7 @@ Lemma lift_exp_eq_ge : forall {Γ A A' n m},
     {{ Γ ⊢ A ≈ A': Type@n }} ->
     {{ Γ ⊢ A ≈ A' : Type@m }}.
 Proof with mautosolve.
-  induction 1; subst...
+  induction 1; subst; mauto.
 Qed.
 
 #[export]
@@ -220,6 +208,98 @@ Proof with mautosolve.
   assert (m <= max n m) by lia...
 Qed.
 
+(** *** Types Presuppositions *)
+
+Lemma presup_ctx_lookup_typ : forall {Γ A x},
+    {{ ⊢ Γ }} ->
+    {{ #x : A ∈ Γ }} ->
+    exists i, {{ Γ ⊢ A : Type@i }}.
+Proof with mautosolve 4.
+  intros * HΓ.
+  induction 1; inversion_clear HΓ;
+    [assert {{ Γ, A ⊢ Type@i[Wk] ≈ Type@i : Type@(S i) }} by mauto 4
+    | assert (exists i, {{ Γ ⊢ A : Type@i }}) as [] by eauto]; econstructor...
+Qed.
+
+#[export]
+Hint Resolve presup_ctx_lookup_typ : mcltt.
+
+Lemma presup_exp_typ : forall {Γ M A},
+    {{ Γ ⊢ M : A }} ->
+    exists i, {{ Γ ⊢ A : Type@i }}.
+Proof.
+  induction 1; assert {{ ⊢ Γ }} by mauto 3; destruct_conjs; mauto 3.
+  - enough {{ Γ ⊢s Id,,M : Γ, ℕ }} by mauto 3.
+    do 3 (econstructor; mauto 3).
+  - eexists; mauto 4 using lift_exp_max_left, lift_exp_max_right.
+  - enough {{ Γ ⊢s Id,,N : Γ, A }} by mauto 3.
+    do 3 (econstructor; mauto 3).
+Qed.
+
+Lemma presup_exp : forall {Γ M A},
+    {{ Γ ⊢ M : A }} ->
+    {{ ⊢ Γ }} /\ exists i, {{ Γ ⊢ A : Type@i }}.
+Proof.
+  mauto 4 using presup_exp_typ.
+Qed.
+
+(** Recover some rules we had before adding subtyping.
+    Rest are recovered after presupposition lemmas (in SystemOpt). *)
+
+Lemma wf_ctx_sub_refl : forall Γ Δ,
+    {{ ⊢ Γ ≈ Δ }} ->
+    {{ ⊢ Γ ⊆ Δ }}.
+Proof. induction 1; mauto. Qed.
+
+#[export]
+Hint Resolve wf_ctx_sub_refl : mcltt.
+
+Lemma wf_conv : forall Γ M A i A',
+    {{ Γ ⊢ M : A }} ->
+    (** The next argument will be removed in SystemOpt *)
+    {{ Γ ⊢ A' : Type@i }} ->
+    {{ Γ ⊢ A ≈ A' : Type@i }} ->
+    {{ Γ ⊢ M : A' }}.
+Proof. mauto. Qed.
+
+#[export]
+Hint Resolve wf_conv : mcltt.
+
+Lemma wf_sub_conv : forall Γ σ Δ Δ',
+  {{ Γ ⊢s σ : Δ }} ->
+  {{ ⊢ Δ ≈ Δ' }} ->
+  {{ Γ ⊢s σ : Δ' }}.
+Proof. mauto. Qed.
+
+#[export]
+Hint Resolve wf_sub_conv : mcltt.
+
+Lemma wf_exp_eq_conv : forall Γ M M' A A' i,
+   {{ Γ ⊢ M ≈ M' : A }} ->
+   (** The next argument will be removed in SystemOpt *)
+   {{ Γ ⊢ A' : Type@i }} ->
+   {{ Γ ⊢ A ≈ A' : Type@i }} ->
+   {{ Γ ⊢ M ≈ M' : A' }}.
+Proof. mauto. Qed.
+
+#[export]
+Hint Resolve wf_exp_eq_conv : mcltt.
+
+Lemma wf_sub_eq_conv : forall Γ σ σ' Δ Δ',
+    {{ Γ ⊢s σ ≈ σ' : Δ }} ->
+    {{ ⊢ Δ ≈ Δ' }} ->
+    {{ Γ ⊢s σ ≈ σ' : Δ' }}.
+Proof. mauto. Qed.
+
+#[export]
+Hint Resolve wf_sub_eq_conv : mcltt.
+
+Add Parametric Morphism Γ : (wf_sub_eq Γ)
+    with signature wf_ctx_eq ==> eq ==> eq ==> iff as wf_sub_eq_morphism_iff3.
+Proof.
+  intros Δ Δ' H **; split; [| symmetry in H]; mauto.
+Qed.
+
 (** *** Additional Lemmas for Syntactic PERs *)
 
 Lemma exp_eq_refl : forall {Γ M A},
@@ -253,15 +333,6 @@ Hint Resolve sub_eq_refl : mcltt.
 
 (** *** Lemmas for [exp] of [{{{ Type@i }}}] *)
 
-Lemma exp_sub_typ : forall {Δ Γ A σ i},
-    {{ Δ ⊢ A : Type@i }} ->
-    {{ Γ ⊢s σ : Δ }} ->
-    {{ Γ ⊢ A[σ] : Type@i }}.
-Proof with mautosolve 3.
-  intros.
-  eapply wf_conv...
-Qed.
-
 Lemma exp_eq_sub_cong_typ1 : forall {Δ Γ A A' σ i},
     {{ Δ ⊢ A ≈ A' : Type@i }} ->
     {{ Γ ⊢s σ : Δ }} ->
@@ -292,7 +363,7 @@ Proof with mautosolve 3.
 Qed.
 
 #[export]
-Hint Resolve exp_sub_typ exp_eq_sub_cong_typ1 exp_eq_sub_cong_typ2' exp_eq_sub_compose_typ : mcltt.
+Hint Resolve exp_eq_sub_cong_typ1 exp_eq_sub_cong_typ2' exp_eq_sub_compose_typ : mcltt.
 
 Lemma exp_eq_typ_sub_sub : forall {Γ Δ Ψ σ τ i},
     {{ Δ ⊢s σ : Ψ }} ->
@@ -477,15 +548,6 @@ Hint Resolve exp_eq_sub_sub_compose_cong_typ : mcltt.
 
 (** *** Lemmas for [exp] of [{{{ ℕ }}}] *)
 
-Lemma exp_sub_nat : forall {Δ Γ M σ},
-    {{ Δ ⊢ M : ℕ }} ->
-    {{ Γ ⊢s σ : Δ }} ->
-    {{ Γ ⊢ M[σ] : ℕ }}.
-Proof with mautosolve 3.
-  intros.
-  eapply wf_conv...
-Qed.
-
 Lemma exp_eq_sub_cong_nat1 : forall {Δ Γ M M' σ},
     {{ Δ ⊢ M ≈ M' : ℕ }} ->
     {{ Γ ⊢s σ : Δ }} ->
@@ -698,20 +760,6 @@ Qed.
 #[export]
 Hint Resolve exp_eq_sub_sub_compose_cong : mcltt.
 
-Lemma ctx_lookup_wf : forall {Γ A x},
-    {{ ⊢ Γ }} ->
-    {{ #x : A ∈ Γ }} ->
-    exists i, {{ Γ ⊢ A : Type@i }}.
-Proof with mautosolve 4.
-  intros * HΓ.
-  induction 1; inversion_clear HΓ;
-    [assert {{ Γ, A ⊢ Type@i[Wk] ≈ Type@i : Type@(S i) }} by mauto 4
-    | assert (exists i, {{ Γ ⊢ A : Type@i }}) as [] by eauto]; econstructor...
-Qed.
-
-#[export]
-Hint Resolve ctx_lookup_wf : mcltt.
-
 Lemma ctxeq_ctx_lookup : forall {Γ Δ A x},
     {{ ⊢ Γ ≈ Δ }} ->
     {{ #x : A ∈ Γ }} ->
diff --git a/theories/Core/Syntactic/SystemOpt.v b/theories/Core/Syntactic/SystemOpt.v
index c1daad9..f72fa87 100644
--- a/theories/Core/Syntactic/SystemOpt.v
+++ b/theories/Core/Syntactic/SystemOpt.v
@@ -1,6 +1,6 @@
 From Coq Require Import Setoid.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Export CtxEq Presup System CoreTypeInversions.
+From Mcltt.Core Require Export Presup CoreTypeInversions.
 Import Syntax_Notations.
 
 Add Parametric Morphism i Γ : (wf_exp Γ)