diff --git a/theories/Algorithmic/Subtyping/Lemmas.v b/theories/Algorithmic/Subtyping/Lemmas.v
index 2d13a93c..5df8a3b0 100644
--- a/theories/Algorithmic/Subtyping/Lemmas.v
+++ b/theories/Algorithmic/Subtyping/Lemmas.v
@@ -21,7 +21,7 @@ Lemma alg_subtyping_nf_sound : forall M N,
       {{ Γ ⊢ M ⊆ N }}.
 Proof.
   induction 1; intros; subst; simpl in *.
-  - econstructor. mauto.
+  - eapply wf_subtyp_refl'; mauto.
   - assert (i < j \/ i = j) as H2 by lia.
     destruct H2; mauto 3.
   - on_all_hyp: fun H => (apply wf_pi_inversion in H; destruct H as [? ?]).
@@ -33,6 +33,8 @@ Proof.
                fail_if_dup
            end.
     apply_subtyping.
+    assert {{ Γ, ~(nf_to_exp A') ⊢ B : Type@(max x x0) }} by mauto using lift_exp_max_right.
+    assert {{ Γ, ~(nf_to_exp A') ⊢ B' : Type@(max x x0) }} by mauto using lift_exp_max_left.
     deepexec IHalg_subtyping_nf ltac:(fun H => pose proof H).
     mauto 3.
 Qed.
@@ -80,8 +82,8 @@ Lemma alg_subtyping_complete : forall Γ M N,
     {{ Γ ⊢a M ⊆ N }}.
 Proof.
   induction 1; mauto.
-  - apply completeness in H.
-    destruct H as [W [? ?]].
+  - apply completeness in H0.
+    destruct H0 as [W [? ?]].
     econstructor; mauto.
   - assert {{ Γ ⊢ Type@i : Type@(S i) }} by mauto.
     assert {{ Γ ⊢ Type@j : Type@(S j) }} by mauto.
diff --git a/theories/Core/Completeness/FundamentalTheorem.v b/theories/Core/Completeness/FundamentalTheorem.v
index 75b5135c..87c70ed9 100644
--- a/theories/Core/Completeness/FundamentalTheorem.v
+++ b/theories/Core/Completeness/FundamentalTheorem.v
@@ -13,7 +13,6 @@ From Mcltt.Core.Syntactic Require Export SystemOpt.
 Import Domain_Notations.
 
 Section completeness_fundamental.
-
   Theorem completeness_fundamental :
     (forall Γ, {{ ⊢ Γ }} -> {{ ⊨ Γ }}) /\
       (forall Γ Γ', {{ ⊢ Γ ⊆ Γ' }} -> {{ SubE Γ <: Γ' }}) /\
@@ -37,7 +36,7 @@ Section completeness_fundamental.
   Theorem completeness_fundamental_ctx : forall Γ, {{ ⊢ Γ }} -> {{ ⊨ Γ }}.
   Proof. solve_it. Qed.
 
-  Theorem completeness_fundamental_ctx_sub : forall Γ Γ', {{ ⊢ Γ ⊆ Γ' }} -> {{ SubE Γ <: Γ' }}.
+  Theorem completeness_fundamental_ctx_subtyp : forall Γ Γ', {{ ⊢ Γ ⊆ Γ' }} -> {{ SubE Γ <: Γ' }}.
   Proof. solve_it. Qed.
 
   Theorem completeness_fundamental_exp : forall Γ M A, {{ Γ ⊢ M : A }} -> {{ Γ ⊨ M : A }}.
@@ -59,8 +58,7 @@ Section completeness_fundamental.
   Proof.
     induction 1.
     - apply valid_ctx_empty.
-    - apply completeness_fundamental_exp_eq in H2.
+    - assert {{ Γ ⊨ A ≈ A' : Type@i }} by mauto using completeness_fundamental_exp_eq.
       mauto.
   Qed.
-
 End completeness_fundamental.
diff --git a/theories/Core/Completeness/LogicalRelation/Definitions.v b/theories/Core/Completeness/LogicalRelation/Definitions.v
index 105bb6ef..cf09a2cb 100644
--- a/theories/Core/Completeness/LogicalRelation/Definitions.v
+++ b/theories/Core/Completeness/LogicalRelation/Definitions.v
@@ -45,7 +45,7 @@ Hint Transparent valid_sub_under_ctx : mcltt.
 #[export]
 Hint Unfold valid_sub_under_ctx : mcltt.
 
-Definition sub_typ_under_ctx Γ M M' :=
+Definition subtyp_under_ctx Γ M M' :=
   exists env_rel (_ : {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ env_rel }}) i,
   forall p p' (equiv_p_p' : {{ Dom p ≈ p' ∈ env_rel }}),
     exists R R', rel_typ i M p M p' R /\ rel_typ i M' p M' p' R' /\ rel_exp M p M' p' (per_subtyp i).
@@ -53,7 +53,7 @@ Definition sub_typ_under_ctx Γ M M' :=
 Notation "⊨ Γ ≈ Γ'" := (per_ctx Γ Γ')  (in custom judg at level 80, Γ custom exp, Γ' custom exp).
 Notation "⊨ Γ" := (valid_ctx Γ) (in custom judg at level 80, Γ custom exp).
 Notation "Γ ⊨ M ≈ M' : A" := (rel_exp_under_ctx Γ A M M') (in custom judg at level 80, Γ custom exp, M custom exp, M' custom exp, A custom exp).
-Notation "Γ ⊨ M ⊆ M'" := (sub_typ_under_ctx Γ M M') (in custom judg at level 80, Γ custom exp, M custom exp, M' custom exp).
+Notation "Γ ⊨ M ⊆ M'" := (subtyp_under_ctx Γ M M') (in custom judg at level 80, Γ custom exp, M custom exp, M' custom exp).
 Notation "Γ ⊨ M : A" := (valid_exp_under_ctx Γ A M) (in custom judg at level 80, Γ custom exp, M custom exp, A custom exp).
 Notation "Γ ⊨s σ ≈ σ' : Δ" := (rel_sub_under_ctx Γ Δ σ σ') (in custom judg at level 80, Γ custom exp, σ custom exp, σ' custom exp, Δ custom exp).
 Notation "Γ ⊨s σ : Δ" := (valid_sub_under_ctx Γ Δ σ) (in custom judg at level 80, Γ custom exp, σ custom exp, Δ custom exp).
diff --git a/theories/Core/Completeness/LogicalRelation/Tactics.v b/theories/Core/Completeness/LogicalRelation/Tactics.v
index 2b5fe357..9e64f58f 100644
--- a/theories/Core/Completeness/LogicalRelation/Tactics.v
+++ b/theories/Core/Completeness/LogicalRelation/Tactics.v
@@ -18,12 +18,12 @@ Ltac eexists_rel_sub :=
   eexists;
   eexists; [eassumption |].
 
-Ltac eexists_sub_typ :=
+Ltac eexists_subtyp :=
   eexists;
   eexists; [eassumption |];
   eexists.
 
-Ltac eexists_sub_typ_with i :=
+Ltac eexists_subtyp_with i :=
   eexists;
   eexists; [eassumption |];
   exists i.
diff --git a/theories/Core/Completeness/SubtypingCases.v b/theories/Core/Completeness/SubtypingCases.v
index 7d1de36c..2868c261 100644
--- a/theories/Core/Completeness/SubtypingCases.v
+++ b/theories/Core/Completeness/SubtypingCases.v
@@ -3,13 +3,13 @@ From Mcltt Require Import Base LibTactics.
 From Mcltt.Core Require Import Completeness.LogicalRelation Completeness.FunctionCases Evaluation.
 Import Domain_Notations.
 
-Lemma sub_typ_subtyp_refl : forall Γ M M' i,
+Lemma subtyp_refl : forall Γ M M' i,
     {{ Γ ⊨ M ≈ M' : Type@i }} ->
     {{ Γ ⊨ M ⊆ M' }}.
 Proof.
   intros * [env_relΓ].
   destruct_conjs.
-  eexists_sub_typ.
+  eexists_subtyp.
   intros.
   saturate_refl.
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).
@@ -23,7 +23,7 @@ Proof.
     etransitivity; try eassumption; symmetry; eassumption.
 Qed.
 
-Lemma sub_typ_subtyp_trans : forall Γ M M' M'',
+Lemma subtyp_trans : forall Γ M M' M'',
     {{ Γ ⊨ M ⊆ M' }} ->
     {{ Γ ⊨ M' ⊆ M'' }} ->
     {{ Γ ⊨ M ⊆ M'' }}.
@@ -32,7 +32,7 @@ Proof.
   destruct_conjs.
   pose env_relΓ.
   handle_per_ctx_env_irrel.
-  eexists_sub_typ_with (max i j).
+  eexists_subtyp_with (max i j).
   intros.
   saturate_refl.
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).
@@ -48,16 +48,16 @@ Proof.
 Qed.
 
 #[export]
-Instance sub_typ_trans Γ : Transitive (sub_typ_under_ctx Γ).
-Proof. eauto using sub_typ_subtyp_trans. Qed.
+Instance subtyp_Transitive Γ : Transitive (subtyp_under_ctx Γ).
+Proof. eauto using subtyp_trans. Qed.
 
-Lemma sub_typ_subtyp_univ : forall Γ i j,
+Lemma subtyp_univ : forall Γ i j,
     {{ ⊨ Γ }} ->
     i < j ->
     {{ Γ ⊨ Type@i ⊆ Type@j }}.
 Proof.
   intros * [env_relΓ] ?.
-  eexists_sub_typ.
+  eexists_subtyp.
   intros.
   assert (i < S (max i j)) by lia.
   assert (j < S (max i j)) by lia.
@@ -68,7 +68,7 @@ Proof.
   econstructor; lia.
 Qed.
 
-Lemma sub_typ_subtyp_pi : forall Γ A A' B B' i,
+Lemma subtyp_pi : forall Γ A A' B B' i,
   {{ Γ ⊨ A ≈ A' : Type@i }} ->
   {{ Γ , A' ⊨ B ⊆ B' }} ->
   {{ Γ ⊨ Π A B ⊆ Π A' B' }}.
@@ -79,7 +79,7 @@ Proof.
   pose env_relΓA'.
   match_by_head (per_ctx_env env_relΓA') invert_per_ctx_env.
   handle_per_ctx_env_irrel.
-  eexists_sub_typ.
+  eexists_subtyp.
   intros.
   saturate_refl.
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).
@@ -140,4 +140,4 @@ Proof.
 Qed.
 
 #[export]
-Hint Resolve sub_typ_subtyp_refl sub_typ_subtyp_trans sub_typ_subtyp_univ sub_typ_subtyp_pi : mcltt.
+Hint Resolve subtyp_refl subtyp_trans subtyp_univ subtyp_pi : mcltt.
diff --git a/theories/Core/Soundness/FundamentalTheorem.v b/theories/Core/Soundness/FundamentalTheorem.v
index d32223f5..f96fe1bf 100644
--- a/theories/Core/Soundness/FundamentalTheorem.v
+++ b/theories/Core/Soundness/FundamentalTheorem.v
@@ -14,21 +14,13 @@ From Mcltt.Core.Syntactic Require Export SystemOpt.
 Import Domain_Notations.
 
 Section soundness_fundamental.
-
   Theorem soundness_fundamental :
     (forall Γ, {{ ⊢ Γ }} -> {{ ⊩ Γ }}) /\
       (forall Γ A M, {{ Γ ⊢ M : A }} -> {{ Γ ⊩ M : A }}) /\
       (forall Γ Δ σ, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊩s σ : Δ }}).
   Proof.
     apply syntactic_wf_mut_ind'; mauto 3.
-
-    - intros.
-      assert (exists i, {{ Γ ⊩ A' : Type@i }}) as [] by admit. (* this should be added to the syntactic judgement *)
-      mauto.
-    - intros.
-      assert {{ ⊩ Δ' }} by admit. (* this should be added to the syntactic judgement *)
-      mauto.
-  Admitted.
+  Qed.
 
   #[local]
   Ltac solve_it := pose proof soundness_fundamental; firstorder.
@@ -41,5 +33,4 @@ Section soundness_fundamental.
 
   Theorem soundness_fundamental_sub : forall Γ σ Δ, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊩s σ : Δ }}.
   Proof. solve_it. Qed.
-
 End soundness_fundamental.
diff --git a/theories/Core/Soundness/LogicalRelation/CoreLemmas.v b/theories/Core/Soundness/LogicalRelation/CoreLemmas.v
index d57d9b1a..0bfe4186 100644
--- a/theories/Core/Soundness/LogicalRelation/CoreLemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/CoreLemmas.v
@@ -821,19 +821,20 @@ Proof.
         bulky_rewrite.
       }
       assert {{Δ0 ⊢ (m [σ][σ0]) m' ≈ (m [σ ∘ σ0]) m' : OT [σ ∘ σ0,, m']}}. {
-        rewrite <- sub_eq_q_sigma_id_extend; mauto 4.
-        rewrite <- exp_eq_sub_compose_typ; mauto 3;
+        rewrite <- @sub_eq_q_sigma_id_extend; mauto 4.
+        rewrite <- @exp_eq_sub_compose_typ; mauto 3;
           [eapply wf_exp_eq_app_cong' |];
           mauto 4.
         symmetry.
         bulky_rewrite_in H4.
-        eapply wf_exp_eq_conv; mauto 3.
+        assert {{ Δ0 ⊢ Π IT[σ ∘ σ0] (OT[q (σ ∘ σ0)]) ≈ (Π IT OT)[σ ∘ σ0] : Type@(S (max i4 i)) }} by mauto.
+        eapply wf_exp_eq_conv'; mauto 4.
       }
 
       bulky_rewrite.
       edestruct H10 with (b := b) as [? []];
         simplify_evals; [| | eassumption];
-      mauto.
+        mauto.
 
   - simpl_glu_rel.
     econstructor; repeat split; mauto 3;
diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
index 74410c3a..f2664c41 100644
--- a/theories/Core/Soundness/LogicalRelation/Lemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -402,7 +402,7 @@ Proof.
     assert {{ Γ ⊢ A[Id] ≈ A : Type@i }} as <- by mauto 4.
     assert {{ Γ ⊢ A'[Id] ≈ A' : Type@i }} as <- by mauto 4.
     assert {{ Γ ⊢ A'[Id] ≈ V : Type@i }} as -> by mauto 4.
-    econstructor.
+    eapply wf_subtyp_refl'.
     mauto 4.
   - bulky_rewrite.
     mauto 3.
diff --git a/theories/Core/Soundness/Realizability.v b/theories/Core/Soundness/Realizability.v
index c368da0d..7decbf95 100644
--- a/theories/Core/Soundness/Realizability.v
+++ b/theories/Core/Soundness/Realizability.v
@@ -61,7 +61,7 @@ Proof.
     etransitivity; [eapply wf_exp_eq_sub_compose; mauto 3 |].
     pose proof (wf_ctx_sub_length _ _ H0).
 
-    rewrite <- exp_eq_sub_compose_typ; mauto 2.
+    rewrite <- @exp_eq_sub_compose_typ; mauto 2.
     deepexec wf_ctx_sub_ctx_lookup ltac:(fun H => destruct H as [? [? [? [? [-> [? [-> []]]]]]]]).
     repeat rewrite List.app_length in *.
     rewrite H6 in *.
@@ -70,14 +70,14 @@ Proof.
 
     etransitivity.
     + eapply wf_exp_eq_sub_cong; [ |mauto 3].
-      eapply wf_exp_eq_subtyp.
+      eapply wf_exp_eq_subtyp'.
       * eapply wf_exp_eq_var_weaken; [mauto 3|]; eauto.
       * mauto 4.
-    + eapply wf_exp_eq_subtyp.
+    + eapply wf_exp_eq_subtyp'.
       * eapply IHweakening with (Γ1 := T :: _).
         reflexivity.
-      * eapply wf_subtyping_subst; [ |mauto 3].
-        simpl. eapply wf_subtyping_subst; mauto 3.
+      * eapply wf_subtyp_subst; [ |mauto 3].
+        simpl. eapply wf_subtyp_subst; mauto 3.
 Qed.
 
 Lemma var_glu_elem_bot : forall A i P El Γ T,
@@ -226,16 +226,16 @@ Proof.
       etransitivity.
       * rewrite sub_decompose_q_typ; mauto 4.
       * simpl.
-        rewrite <- sub_eq_q_sigma_id_extend; mauto 4.
-        rewrite <- exp_eq_sub_compose_typ; mauto 3;
+        rewrite <- @sub_eq_q_sigma_id_extend; mauto 4.
+        rewrite <- @exp_eq_sub_compose_typ; mauto 3;
           [eapply wf_exp_eq_app_cong' |].
         -- specialize (H12 _ {{{σ ∘ σ0}}} _ ltac:(mauto 3) ltac:(eassumption)).
            rewrite wf_exp_eq_sub_compose with (M := t) in H12; mauto 3.
            bulky_rewrite_in H12.
-        -- rewrite <- exp_eq_sub_compose_typ; mauto 3.
+        -- rewrite <- @exp_eq_sub_compose_typ; mauto 3.
         -- econstructor; mauto 3.
            autorewrite with mcltt.
-           rewrite <- exp_eq_sub_compose_typ; mauto 3.
+           rewrite <- @exp_eq_sub_compose_typ; mauto 3.
 
   - handle_functional_glu_univ_elem.
     handle_per_univ_elem_irrel.
@@ -280,9 +280,9 @@ Proof.
       do 2 (rewrite wf_exp_eq_sub_id in H40; mauto 4).
       etransitivity; [|eassumption].
       simpl.
-      assert {{ Δ, IT[σ] ⊢ # 0 : IT[σ ∘ Wk] }} by (rewrite <- exp_eq_sub_compose_typ; mauto 3).
-      rewrite <- sub_eq_q_sigma_id_extend; mauto 4.
-      rewrite <- exp_eq_sub_compose_typ; mauto 2.
+      assert {{ Δ, IT[σ] ⊢ # 0 : IT[σ ∘ Wk] }} by (rewrite <- @exp_eq_sub_compose_typ; mauto 3).
+      rewrite <- @sub_eq_q_sigma_id_extend; mauto 4.
+      rewrite <- @exp_eq_sub_compose_typ; mauto 2.
       2:eapply sub_q; mauto 4.
       2:gen_presup H41; econstructor; mauto 3.
       eapply wf_exp_eq_app_cong'; [| mauto 3].
diff --git a/theories/Core/Soundness/SubtypingCases.v b/theories/Core/Soundness/SubtypingCases.v
index a1a91ea7..9c1a16ef 100644
--- a/theories/Core/Soundness/SubtypingCases.v
+++ b/theories/Core/Soundness/SubtypingCases.v
@@ -8,12 +8,12 @@ From Mcltt.Core.Syntactic Require Import Corollaries.
 Import Domain_Notations.
 
 Lemma glu_rel_exp_subtyp : forall {Γ M A A' i},
-    {{ Γ ⊩ A' : Type@i }} ->
     {{ Γ ⊩ M : A }} ->
+    {{ Γ ⊩ A' : Type@i }} ->
     {{ Γ ⊢ A ⊆ A' }} ->
     {{ Γ ⊩ M : A' }}.
 Proof.
-  intros * HA' [Sb [? [i]]] [env_relΓ [? [j]]]%completeness_fundamental_subtyp.
+  intros * [Sb [? [i]]] HA' [env_relΓ [? [j]]]%completeness_fundamental_subtyp.
   destruct_conjs.
   eapply destruct_glu_rel_exp in HA'; try eassumption.
   destruct_conjs.
@@ -53,21 +53,20 @@ Proof.
   eapply glu_univ_elem_per_subtyp_trm_if; mauto.
   - assert (k <= max i (max j k)) by lia.
     eapply glu_univ_elem_typ_cumu_ge; revgoals; mauto.
-  - assert (i <= max i (max j k)) by lia.
-    eapply glu_univ_elem_exp_cumu_ge; mauto.
+  - eapply glu_univ_elem_exp_cumu_max_left; revgoals; mauto.
 Qed.
 
 #[export]
 Hint Resolve glu_rel_exp_subtyp : mcltt.
 
 Lemma glu_rel_sub_subtyp : forall {Γ σ Δ Δ'},
-    {{ ⊩ Δ' }} ->
     {{ Γ ⊩s σ : Δ }} ->
+    {{ ⊩ Δ' }} ->
     {{ ⊢ Δ ⊆ Δ' }} ->
     {{ Γ ⊩s σ : Δ' }}.
 Proof.
-  intros * [SbΔ'] [SbΓ [SbΔ]] Hsubtyp.
-  pose proof (completeness_fundamental_ctx_sub _ _ Hsubtyp).
+  intros * [SbΓ [SbΔ]] [SbΔ'] Hsubtyp.
+  pose proof (completeness_fundamental_ctx_subtyp _ _ Hsubtyp).
   destruct_conjs.
   econstructor; eexists; repeat split; [eassumption | eassumption |].
   intros.
diff --git a/theories/Core/Syntactic/CoreInversions.v b/theories/Core/Syntactic/CoreInversions.v
index ab9ceb86..2a8e7b57 100644
--- a/theories/Core/Syntactic/CoreInversions.v
+++ b/theories/Core/Syntactic/CoreInversions.v
@@ -21,7 +21,7 @@ Corollary wf_succ_inversion : forall Γ A M,
 Proof with mautosolve.
   intros * H.
   dependent induction H;
-    try specialize (IHwf_exp _ eq_refl);
+    try specialize (IHwf_exp1 _ eq_refl);
     destruct_conjs...
 Qed.
 
@@ -31,11 +31,11 @@ Hint Resolve wf_succ_inversion : mcltt.
 Lemma wf_natrec_inversion : forall Γ A M A' MZ MS,
     {{ Γ ⊢ rec M return A' | zero -> MZ | succ -> MS end : A }} ->
     {{ Γ ⊢ MZ : A'[Id,,zero] }} /\ {{ Γ, ℕ, A' ⊢ MS : A'[Wk∘Wk,,succ(#1)] }} /\ {{ Γ ⊢ M : ℕ }} /\ {{ Γ ⊢ A'[Id,,M] ⊆ A }}.
-Proof with mautosolve 4.
+Proof with mautosolve.
   intros * H.
   pose (A0 := A).
   dependent induction H;
-    try (specialize (IHwf_exp _ _ _ _ eq_refl));
+    try (specialize (IHwf_exp1 _ _ _ _ eq_refl));
     destruct_conjs;
     assert {{ Γ ⊢s Id : Γ }} by mauto 3;
     repeat split...
@@ -50,7 +50,7 @@ Corollary wf_fn_inversion : forall {Γ A M C},
 Proof with mautosolve 4.
   intros * H.
   dependent induction H;
-    try specialize (IHwf_exp _ _ eq_refl);
+    try specialize (IHwf_exp1 _ _ eq_refl);
     destruct_conjs;
     gen_presups;
     eexists; split...
@@ -62,10 +62,10 @@ Hint Resolve wf_fn_inversion : mcltt.
 Lemma wf_app_inversion : forall {Γ M N C},
     {{ Γ ⊢ M N : C }} ->
     exists A B, {{ Γ ⊢ M : Π A B }} /\ {{ Γ ⊢ N : A }} /\ {{ Γ ⊢ B[Id,,N] ⊆ C }}.
-Proof with mautosolve 4.
+Proof with mautosolve.
   intros * H.
   dependent induction H;
-    try specialize (IHwf_exp _ _ eq_refl);
+    try specialize (IHwf_exp1 _ _ eq_refl);
     destruct_conjs;
     do 2 eexists; repeat split...
 Qed.
@@ -80,7 +80,7 @@ Proof with mautosolve 4.
   intros * H.
   dependent induction H;
     [assert (exists i, {{ Γ ⊢ A : Type@i }}) as [] by mauto 4 |];
-    try (specialize (IHwf_exp _ eq_refl));
+    try (specialize (IHwf_exp1 _ eq_refl));
     destruct_conjs;
     eexists; split...
 Qed.
@@ -91,10 +91,10 @@ Hint Resolve wf_vlookup_inversion : mcltt.
 Lemma wf_exp_sub_inversion : forall {Γ M σ A},
     {{ Γ ⊢ M[σ] : A }} ->
     exists Δ A', {{ Γ ⊢s σ : Δ }} /\ {{ Δ ⊢ M : A' }} /\ {{ Γ ⊢ A'[σ] ⊆ A }}.
-Proof with mautosolve 4.
+Proof with mautosolve.
   intros * H.
   dependent induction H;
-    try (specialize (IHwf_exp _ _ eq_refl));
+    try (specialize (IHwf_exp1 _ _ eq_refl));
     destruct_conjs;
     gen_presups;
     do 2 eexists; split...
diff --git a/theories/Core/Syntactic/CoreTypeInversions.v b/theories/Core/Syntactic/CoreTypeInversions.v
index c7bc40d3..aa7d97e0 100644
--- a/theories/Core/Syntactic/CoreTypeInversions.v
+++ b/theories/Core/Syntactic/CoreTypeInversions.v
@@ -32,7 +32,7 @@ Lemma wf_pi_inversion : forall {Γ A B C},
 Proof with mautosolve 4.
   intros * H.
   dependent induction H;
-    try specialize (IHwf_exp _ _ eq_refl);
+    try specialize (IHwf_exp1 _ _ eq_refl);
     destruct_conjs;
     assert {{ ⊢ Γ }} by mauto 3;
     eexists; split...
@@ -47,9 +47,9 @@ Corollary wf_pi_inversion' : forall {Γ A B i},
 Proof with mautosolve 4.
   intros * [j [? []]]%wf_pi_inversion.
   assert {{ Γ, A ⊢s Wk : Γ }} by mauto 4.
-  assert {{ Γ, A ⊢ Type@j ⊆ Type@j[Wk] }} by mauto 4.
+  assert {{ Γ, A ⊢ Type@j ⊆ Type@j[Wk] }} by (econstructor; mauto 4).
   assert {{ Γ, A ⊢ Type@j[Wk] ⊆ Type@i[Wk] }} by mauto 4.
-  assert {{ Γ, A ⊢ Type@i[Wk] ⊆ Type@i }} by mauto 4.
+  assert {{ Γ, A ⊢ Type@i[Wk] ⊆ Type@i }} by (econstructor; mauto 4).
   enough {{ Γ, A ⊢ Type@j ⊆ Type@i }}...
 Qed.
 
diff --git a/theories/Core/Syntactic/Corollaries.v b/theories/Core/Syntactic/Corollaries.v
index c8f77f5c..513dcf37 100644
--- a/theories/Core/Syntactic/Corollaries.v
+++ b/theories/Core/Syntactic/Corollaries.v
@@ -78,19 +78,20 @@ Proof.
   intros. gen_presup H0.
   econstructor; mauto 3.
   - econstructor; mauto 4.
-  - rewrite <- exp_eq_sub_compose_typ; mauto 4.
+  - rewrite <- @exp_eq_sub_compose_typ; mauto 4.
 Qed.
 #[export]
  Hint Resolve sub_q_eq : mcltt.
 
-Lemma wf_subtyping_subst_eq : forall Δ A B,
+Lemma wf_subtyp_subst_eq : forall Δ A B,
     {{ Δ ⊢ A ⊆ B }} ->
     forall Γ σ σ',
       {{ Γ ⊢s σ ≈ σ' : Δ }} ->
       {{ Γ ⊢ A [σ] ⊆ B[σ'] }}.
 Proof.
   induction 1; intros * Hσσ'; gen_presup Hσσ'.
-  - econstructor. mauto 4.
+  - eapply wf_subtyp_refl'.
+    eapply wf_exp_eq_conv; mauto 4.
   - etransitivity; mauto 4.
   - autorewrite with mcltt.
     mauto 2.
@@ -98,17 +99,16 @@ Proof.
     eapply wf_subtyp_pi'; mauto.
 Qed.
 
-
-Lemma wf_subtyping_subst : forall Δ A B,
+Lemma wf_subtyp_subst : forall Δ A B,
     {{ Δ ⊢ A ⊆ B }} ->
     forall Γ σ,
       {{ Γ ⊢s σ : Δ }} ->
       {{ Γ ⊢ A [σ] ⊆ B[σ] }}.
 Proof.
-  intros; mauto 2 using wf_subtyping_subst_eq.
+  intros; mauto 2 using wf_subtyp_subst_eq.
 Qed.
 #[export]
- Hint Resolve wf_subtyping_subst_eq wf_subtyping_subst : mcltt.
+ Hint Resolve wf_subtyp_subst_eq wf_subtyp_subst : mcltt.
 
 Lemma sub_decompose_q : forall Γ S i σ Δ Δ' τ t,
   {{Γ ⊢ S : Type@i}} ->
@@ -122,14 +122,13 @@ Proof.
   symmetry.
   rewrite wf_sub_eq_extend_compose; mauto 3;
     [| mauto
-    | rewrite <- exp_eq_sub_compose_typ; mauto 4].
+    | rewrite <- @exp_eq_sub_compose_typ; mauto 4].
   eapply wf_sub_eq_extend_cong; eauto.
   - rewrite wf_sub_eq_compose_assoc; mauto 3; mauto 4.
     rewrite wf_sub_eq_p_extend; eauto; mauto 4.
-  - rewrite <- exp_eq_sub_compose_typ; mauto 4.
+  - rewrite <- @exp_eq_sub_compose_typ; mauto 4.
 Qed.
 
-
 Lemma sub_decompose_q_typ : forall Γ S T i σ Δ Δ' τ t,
   {{Γ, S ⊢ T : Type@i}} ->
   {{Δ ⊢s σ : Γ}} ->
@@ -139,6 +138,6 @@ Lemma sub_decompose_q_typ : forall Γ S T i σ Δ Δ' τ t,
 Proof.
   intros. gen_presups.
   autorewrite with mcltt.
-  eapply exp_eq_sub_cong_typ2'; [mauto 2 | mauto |].
+  eapply exp_eq_sub_cong_typ2'; [mauto 2 | econstructor; mauto 4 |].
   symmetry. mauto using sub_decompose_q.
 Qed.
diff --git a/theories/Core/Syntactic/CtxEq.v b/theories/Core/Syntactic/CtxEq.v
index 271c9026..dbc45f04 100644
--- a/theories/Core/Syntactic/CtxEq.v
+++ b/theories/Core/Syntactic/CtxEq.v
@@ -11,8 +11,10 @@ Qed.
 Hint Resolve ctx_eq_refl : mcltt.
 
 Lemma ctx_eq_sym : forall {Γ Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ ⊢ Δ ≈ Γ }}.
-Proof with mautosolve.
-  induction 1...
+Proof.
+  intros.
+  symmetry.
+  eassumption.
 Qed.
 
 #[export]
@@ -30,11 +32,11 @@ Proof. mauto. Qed.
 Lemma ctxeq_sub_eq : forall {Γ Δ σ σ' Γ'}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢s σ ≈ σ' : Γ' }} -> {{ Δ ⊢s σ ≈ σ' : Γ' }}.
 Proof. mauto. Qed.
 
-Lemma ctxeq_subtyping : forall {Γ Δ A B}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢ A ⊆ B }} -> {{ Δ ⊢ A ⊆ B }}.
+Lemma ctxeq_subtyp : forall {Γ Δ A B}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢ A ⊆ B }} -> {{ Δ ⊢ A ⊆ B }}.
 Proof. mauto. Qed.
 
 #[export]
-  Hint Resolve ctxeq_exp ctxeq_exp_eq ctxeq_sub ctxeq_sub_eq ctxeq_subtyping : mcltt.
+Hint Resolve ctxeq_exp ctxeq_exp_eq ctxeq_sub ctxeq_sub_eq ctxeq_subtyp : mcltt.
 
 
 Lemma ctx_eq_trans : forall {Γ0 Γ1 Γ2}, {{ ⊢ Γ0 ≈ Γ1 }} -> {{ ⊢ Γ1 ≈ Γ2 }} -> {{ ⊢ Γ0 ≈ Γ2 }}.
@@ -95,8 +97,8 @@ Proof.
 Qed.
 
 
-Add Parametric Morphism : wf_subtyping
-  with signature wf_ctx_eq ==> eq ==> eq ==> iff as ctxeq_subtyping_morphism.
+Add Parametric Morphism : wf_subtyp
+  with signature wf_ctx_eq ==> eq ==> eq ==> iff as ctxeq_subtyp_morphism.
 Proof.
   intros. split; mauto 3.
 Qed.
diff --git a/theories/Core/Syntactic/CtxSub.v b/theories/Core/Syntactic/CtxSub.v
index 18684f24..a2ab536a 100644
--- a/theories/Core/Syntactic/CtxSub.v
+++ b/theories/Core/Syntactic/CtxSub.v
@@ -2,7 +2,9 @@ From Mcltt Require Import Base LibTactics.
 From Mcltt Require Export System.
 Import Syntax_Notations.
 
-Lemma ctx_sub_refl : forall {Γ}, {{ ⊢ Γ }} -> {{ ⊢ Γ ⊆ Γ }}.
+Lemma ctx_sub_refl : forall {Γ},
+    {{ ⊢ Γ }} ->
+    {{ ⊢ Γ ⊆ Γ }}.
 Proof with mautosolve.
   induction 1...
 Qed.
@@ -12,13 +14,13 @@ Hint Resolve ctx_sub_refl : mcltt.
 
 Module ctxsub_judg.
   #[local]
-  Ltac gen_ctxsub_helper_IH ctxsub_exp_helper ctxsub_exp_eq_helper ctxsub_sub_helper ctxsub_sub_eq_helper ctxsub_subtyping_helper H :=
+  Ltac gen_ctxsub_helper_IH ctxsub_exp_helper ctxsub_exp_eq_helper ctxsub_sub_helper ctxsub_sub_eq_helper ctxsub_subtyp_helper H :=
   match type of H with
   | {{ ~?Γ ⊢ ~?M : ~?A }} => pose proof ctxsub_exp_helper _ _ _ H
   | {{ ~?Γ ⊢ ~?M ≈ ~?N : ~?A }} => pose proof ctxsub_exp_eq_helper _ _ _ _ H
   | {{ ~?Γ ⊢s ~?σ : ~?Δ }} => pose proof ctxsub_sub_helper _ _ _ H
   | {{ ~?Γ ⊢s ~?σ ≈ ~?τ : ~?Δ }} => pose proof ctxsub_sub_eq_helper _ _ _ _ H
-  | {{ ~?Γ ⊢ ~?M ⊆ ~?M' }} => pose proof ctxsub_subtyping_helper _ _ _ H
+  | {{ ~?Γ ⊢ ~?M ⊆ ~?M' }} => pose proof ctxsub_subtyp_helper _ _ _ H
   end.
 
   #[local]
@@ -30,11 +32,11 @@ Module ctxsub_judg.
   with
   ctxsub_sub_eq_helper : forall {Γ Γ' σ σ'}, {{ Γ ⊢s σ ≈ σ' : Γ' }} -> forall {Δ}, {{ ⊢ Δ ⊆ Γ }} -> {{ Δ ⊢s σ ≈ σ' : Γ' }}
   with
-  ctxsub_subtyping_helper : forall {Γ M M'}, {{ Γ ⊢ M ⊆ M' }} -> forall {Δ}, {{ ⊢ Δ ⊆ Γ }} -> {{ Δ ⊢ M ⊆ M' }}.
+  ctxsub_subtyp_helper : forall {Γ M M'}, {{ Γ ⊢ M ⊆ M' }} -> forall {Δ}, {{ ⊢ Δ ⊆ Γ }} -> {{ Δ ⊢ M ⊆ M' }}.
   Proof with mautosolve.
     all: inversion_clear 1;
-      (on_all_hyp: gen_ctxsub_helper_IH ctxsub_exp_helper ctxsub_exp_eq_helper ctxsub_sub_helper ctxsub_sub_eq_helper ctxsub_subtyping_helper);
-      clear ctxsub_exp_helper ctxsub_exp_eq_helper ctxsub_sub_helper ctxsub_sub_eq_helper ctxsub_subtyping_helper;
+      (on_all_hyp: gen_ctxsub_helper_IH ctxsub_exp_helper ctxsub_exp_eq_helper ctxsub_sub_helper ctxsub_sub_eq_helper ctxsub_subtyp_helper);
+      clear ctxsub_exp_helper ctxsub_exp_eq_helper ctxsub_sub_helper ctxsub_sub_eq_helper ctxsub_subtyp_helper;
       intros * HΓΔ; destruct (presup_ctx_sub HΓΔ); mauto 4;
       try (rename B into C); try (rename B' into C'); try (rename A0 into B); try (rename A' into B').
     (* ctxsub_exp_helper & ctxsub_exp_eq_helper recursion cases *)
@@ -42,9 +44,9 @@ Module ctxsub_judg.
     assert {{ Δ, ℕ ⊢ B : Type@i }} by eauto; econstructor...
     (* ctxsub_exp_helper & ctxsub_exp_eq_helper function cases *)
     1-3,5-9: assert {{ Δ ⊢ B : Type@i }} by eauto; assert {{ ⊢ Δ, B ⊆ Γ, B }} by mauto;
-      try econstructor...
+    try econstructor...
     (* ctxsub_exp_helper & ctxsub_exp_eq_helper variable cases *)
-    1-2: assert (exists B, {{ #x : B ∈ Δ }} /\ {{ Δ ⊢  B ⊆ A }}); destruct_conjs; mautosolve 4.
+    1-2: assert (exists B, {{ #x : B ∈ Δ }} /\ {{ Δ ⊢ B ⊆ A }}); destruct_conjs; mautosolve 4.
     (* ctxsub_sub_helper & ctxsub_sub_eq_helper weakening cases *)
     2-3: inversion_clear HΓΔ; econstructor; mautosolve 4.
 
@@ -77,13 +79,13 @@ Module ctxsub_judg.
     eauto using ctxsub_sub_eq_helper.
   Qed.
 
-  Corollary ctxsub_subtyping : forall {Γ Δ A B}, {{ ⊢ Δ ⊆ Γ }} -> {{ Γ ⊢ A ⊆ B }} -> {{ Δ ⊢ A ⊆ B }}.
+  Corollary ctxsub_subtyp : forall {Γ Δ A B}, {{ ⊢ Δ ⊆ Γ }} -> {{ Γ ⊢ A ⊆ B }} -> {{ Δ ⊢ A ⊆ B }}.
   Proof.
-    eauto using ctxsub_subtyping_helper.
+    eauto using ctxsub_subtyp_helper.
   Qed.
 
   #[export]
-  Hint Resolve ctxsub_exp ctxsub_exp_eq ctxsub_sub ctxsub_sub_eq ctxsub_subtyping : mcltt.
+  Hint Resolve ctxsub_exp ctxsub_exp_eq ctxsub_sub ctxsub_sub_eq ctxsub_subtyp : mcltt.
 End ctxsub_judg.
 
 Export ctxsub_judg.
@@ -103,40 +105,35 @@ Qed.
  Hint Resolve wf_ctx_sub_trans : mcltt.
 
 #[export]
-  Instance wf_ctx_sub_trans_ins : Transitive wf_ctx_sub.
+Instance wf_ctx_sub_trans_ins : Transitive wf_ctx_sub.
 Proof. eauto using wf_ctx_sub_trans. Qed.
 
-
 Add Parametric Morphism : wf_exp
   with signature wf_ctx_sub --> eq ==> eq ==> Basics.impl as ctxsub_exp_morphism.
 Proof.
   cbv. intros. mauto 3.
 Qed.
 
-
 Add Parametric Morphism : wf_exp_eq
   with signature wf_ctx_sub --> eq ==> eq ==> eq ==> Basics.impl as ctxsub_exp_eq_morphism.
 Proof.
   cbv. intros. mauto 3.
 Qed.
 
-
 Add Parametric Morphism : wf_sub
   with signature wf_ctx_sub --> eq ==> eq ==> Basics.impl as ctxsub_sub_morphism.
 Proof.
   cbv. intros. mauto 3.
 Qed.
 
-
 Add Parametric Morphism : wf_sub_eq
   with signature wf_ctx_sub --> eq ==> eq ==> eq ==> Basics.impl as ctxsub_sub_eq_morphism.
 Proof.
   cbv. intros. mauto 3.
 Qed.
 
-
-Add Parametric Morphism : wf_subtyping
-  with signature wf_ctx_sub --> eq ==> eq ==> Basics.impl as ctxsub_subtyping_morphism.
+Add Parametric Morphism : wf_subtyp
+  with signature wf_ctx_sub --> eq ==> eq ==> Basics.impl as ctxsub_subtyp_morphism.
 Proof.
   cbv. intros. mauto 3.
 Qed.
diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index a2199ca1..6f70f993 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -20,7 +20,7 @@ Ltac gen_presup_ctx H :=
   end.
 
 #[local]
-Ltac gen_presup_IH presup_exp presup_exp_eq presup_sub_eq presup_subtyping H :=
+Ltac gen_presup_IH presup_exp presup_exp_eq presup_sub_eq presup_subtyp H :=
   match type of H with
   | {{ ~?Γ ⊢ ~?M : ~?A }} =>
       let HΓ := fresh "HΓ" in
@@ -45,18 +45,18 @@ Ltac gen_presup_IH presup_exp presup_exp_eq presup_sub_eq presup_subtyping H :=
       let i := fresh "i" in
       let HM := fresh "HM" in
       let HN := fresh "HN" in
-      pose proof presup_subtyping _ _ _ H as [HΓ [i [HM HN]]]
+      pose proof presup_subtyp _ _ _ H as [HΓ [i [HM HN]]]
   | _ => 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 }}
 with presup_sub_eq : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Γ }} /\ {{ Γ ⊢s σ : Δ }} /\ {{ Γ ⊢s σ' : Δ }} /\ {{ ⊢ Δ }}
-with presup_subtyping : forall {Γ M M'}, {{ Γ ⊢ M ⊆ M' }} -> {{ ⊢ Γ }} /\ exists i, {{ Γ ⊢ M : Type@i }} /\ {{ Γ ⊢ M' : Type@i }}.
+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_subtyping);
-    clear presup_exp presup_exp_eq presup_sub_eq presup_subtyping;
+  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;
     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');
@@ -74,14 +74,16 @@ Proof with mautosolve 4.
     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 mauto 4.
+    assert {{ Γ, ℕ, B ⊢ NS' : B'[WkWksucc] }} by (eapply wf_conv; mauto 4).
     assert {{ Γ, ℕ, B' ⊢ NS' : B'[WkWksucc] }} by mauto 4.
-    enough {{ Γ ⊢ rec N' return B' | zero -> NZ' | succ -> NS' end : B'[Id ,, N'] }}...
+    assert {{ Γ ⊢ rec N' return B' | zero -> NZ' | succ -> NS' end : B'[Id ,, N'] }} by mauto 4.
+    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[σ,,N[σ]] : Type@i }} by mauto 4.
-    enough {{ Γ ⊢ B[(Id,,N)][σ] ≈ B[σ,,N[σ]] : Type@i }}...
+    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.
@@ -106,8 +108,9 @@ Proof with mautosolve 4.
     assert {{ Γ' ⊢s q (q σ) : Δ, ℕ, B }} by mauto 4.
     assert {{ Γ' ⊢s q σ∘WkWksucc ≈ WkWksucc∘q (q σ) : Δ, ℕ }} by mauto.
     assert {{ Γ' ⊢s WkWksucc : Γ, ℕ }} by mauto.
-    assert {{ Γ' ⊢ B[q σ][WkWksucc] ≈ B[WkWksucc][q (q σ)] : Type@i }} by mauto.
-    assert {{ Γ' ⊢ NS[q (q σ)] : B[q σ][WkWksucc] }}...
+    assert {{ Γ' ⊢ B[WkWksucc][q (q σ)] ≈ B[q σ][WkWksucc] : Type@i }} by mauto.
+    assert {{ Γ' ⊢ NS[q (q σ)] : B[q σ][WkWksucc] }} by mauto 4.
+    eapply wf_conv...
 
   - eexists...
 
@@ -157,37 +160,41 @@ Proof with mautosolve 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.
-    enough {{ Γ ⊢ λ B[σ] N[q σ] : Π B[σ] C[q σ] }}...
+    assert {{ Γ ⊢ λ B[σ] N[q σ] : Π B[σ] C[q σ] }} by mauto 4.
+    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.
     enough {{ Δ ⊢ Π B C : Type@(max i i0) }}...
 
   - assert {{ Γ ⊢s Id ≈ Id : Γ }} by mauto.
-    assert {{ Γ ⊢ B[Id] ≈ B : Type@i }} by mauto.
-    assert {{ Γ ⊢ L ≈ L' : B[Id] }} by mauto.
+    assert {{ Γ ⊢ B ≈ B[Id] : Type@i }} by mauto.
+    assert {{ Γ ⊢ L ≈ L' : B[Id] }} by mauto 4.
     assert {{ Γ ⊢s Id ,, L ≈ Id ,, L' : Γ, B }} by mauto.
-    enough {{ Γ ⊢ C[Id ,, L] ≈ C[Id ,, L'] : Type@i }}...
+    assert {{ Γ ⊢ C[Id ,, L] ≈ C[Id ,, L'] : Type@i }} by mauto 4.
+    eapply wf_conv...
 
-  - assert {{ Γ ⊢ N[σ] : Π B[σ] C[q σ] }} by mauto 4.
+  - 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.
-    enough {{ Γ ⊢ C[Id ,, L][σ] ≈ C[σ ,, L[σ]] : Type@i }}...
+    assert {{ Γ ⊢ C[Id ,, L][σ] ≈ C[σ ,, L[σ]] : Type@i }} by mauto 4.
+    eapply wf_conv...
 
   - assert {{ Γ ⊢ B[σ] : Type@i }} by mauto.
     assert {{ Γ, B[σ] ⊢ C[q σ] : Type@i }} by mauto 4.
-    assert {{ Γ ⊢ N[σ] : Π B[σ] C[q σ] }} 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.
-    enough {{ Γ ⊢ C[q σ][(Id ,, L[σ])] ≈ C[σ ,, L[σ]] : Type@i }}...
+    assert {{ Γ ⊢ C[q σ][(Id ,, L[σ])] ≈ C[σ ,, L[σ]] : Type@i }} by mauto 4.
+    eapply wf_conv...
 
   - eexists...
 
@@ -200,7 +207,7 @@ Proof with mautosolve 4.
     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 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.
@@ -212,14 +219,14 @@ Proof with mautosolve 4.
     assert {{ Γ, B ⊢s Wk∘Id ≈ Wk∘(Wk∘Id0) : Γ }} by mauto.
     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 ⊢ #0[Id0] ≈ #0[Id] : B[Wk∘Id] }} by mauto 4.
+    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.
@@ -250,26 +257,32 @@ Proof with mautosolve 4.
   (* presup_sub_eq cases *)
   - econstructor...
 
-  - assert {{ Γ ⊢ B[σ] ≈ B[σ'] : Type@i }}...
+  - assert {{ Γ ⊢ B[σ] ≈ B[σ'] : Type@i }} by mauto 4.
+    eapply wf_conv...
 
   - assert {{ Γ ⊢ N'[Id] : A[Id] }}...
 
-  - assert {{ Γ ⊢ N[σ][τ] : B[σ][τ] }}...
+  - assert {{ Γ ⊢ N[σ][τ] : B[σ][τ] }} by mauto 4.
+    eapply wf_conv...
 
   - econstructor...
 
-  - assert {{ ⊢ Δ, A }}...
+  - econstructor; mauto 4.
+    eapply wf_conv...
+
+  - mauto.
 
   - assert (exists i, {{ Γ0 ⊢ A : Type@i }}) as [] by mauto.
-    assert {{ Γ ⊢ #0[σ] : A[Wk][σ] }} by mauto.
-    enough {{ Γ ⊢ #0[σ] : A[Wk∘σ] }}...
+    assert {{ Γ ⊢ #0[σ] : A[Wk][σ] }} by mauto 4.
+    enough {{ Γ ⊢ #0[σ] : A[Wk∘σ] }} by mauto 4.
+    eapply wf_conv...
 
-    (* presup_subtyping cases *)
+    (* presup_subtyp cases *)
   - exists (max i i0); split; mauto 3 using lift_exp_max_left, lift_exp_max_right.
   - exists (max (S i) (S j)); split; mauto 3 using lift_exp_max_left, lift_exp_max_right.
   - mauto.
 Qed.
 
-Ltac gen_presup H := gen_presup_IH @presup_exp @presup_exp_eq @presup_sub_eq @presup_subtyping H.
+Ltac gen_presup H := gen_presup_IH @presup_exp @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/Definitions.v b/theories/Core/Syntactic/System/Definitions.v
index c4cf5e06..f86eeef1 100644
--- a/theories/Core/Syntactic/System/Definitions.v
+++ b/theories/Core/Syntactic/System/Definitions.v
@@ -80,8 +80,18 @@ with wf_exp : ctx -> typ -> exp -> Prop :=
   `( {{ Γ ⊢s σ : Δ }} ->
      {{ Δ ⊢ M : A }} ->
      {{ Γ ⊢ M[σ] : A[σ] }} )
-| wf_subtyp :
+| wf_exp_subtyp :
   `( {{ Γ ⊢ M : A }} ->
+     (** We have this extra argument for soundness.
+         Note that we need to keep it asymmetric:
+         only [A'] is checked. If we check A as well,
+         we cannot even construct something like
+         [{{ Γ ⊢ Type@0[Wk] : Type@1 }}] with the current
+         rules. Under the symmetric rule, the example requires
+         [{{ Γ ⊢ Type@1[Wk] : Type@2 }}] to apply [wf_exp_sub],
+         which requires [{{ Γ ⊢ Type@2[Wk] : Type@3 }}], and so on.
+      *)
+     {{ Γ ⊢ A' : Type@i }} ->
      {{ Γ ⊢ A ⊆ A' }} ->
      {{ Γ ⊢ M : A' }} )
 where "Γ ⊢ M : A" := (wf_exp Γ A M) (in custom judg) : type_scope
@@ -104,6 +114,11 @@ with wf_sub : ctx -> ctx -> sub -> Prop :=
      {{ Γ ⊢s (σ ,, M) : Δ , A }} )
 | wf_sub_subtyp :
   `( {{ Γ ⊢s σ : Δ }} ->
+     (** As in [wf_exp_subtyp], this extra argument is
+         for soundness. We don't need to keep it asymmetric,
+         but do so to match with [wf_exp_subtyp].
+      *)
+     {{ ⊢ Δ' }} ->
      {{ ⊢ Δ ⊆ Δ' }} ->
      {{ Γ ⊢s σ : Δ' }} )
 where "Γ ⊢s σ : Δ" := (wf_sub Γ Δ σ) (in custom judg) : type_scope
@@ -225,11 +240,12 @@ with wf_exp_eq : ctx -> typ -> exp -> exp -> Prop :=
      {{ Γ' ⊢s σ : Γ'' }} ->
      {{ Γ'' ⊢ M : A }} ->
      {{ Γ ⊢ M[σ ∘ τ] ≈ M[σ][τ] : A[σ ∘ τ] }} )
-| wf_exp_eq_cumu :
-  `( {{ Γ ⊢ A ≈ A' : Type@i }} ->
-     {{ Γ ⊢ A ≈ A' : Type@(S i) }} )
 | wf_exp_eq_subtyp :
   `( {{ Γ ⊢ M ≈ M' : A }} ->
+     {{ Γ ⊢ A' : Type@i }} ->
+     (** This extra argument is here to be consistent with
+         [wf_exp_subtyp].
+      *)
      {{ Γ ⊢ A ⊆ A' }} ->
      {{ Γ ⊢ M ≈ M' : A' }} )
 | wf_exp_eq_sym :
@@ -291,13 +307,27 @@ with wf_sub_eq : ctx -> ctx -> sub -> sub -> Prop :=
      {{ Γ ⊢s σ ≈ σ'' : Δ }} )
 | wf_sub_eq_subtyp :
   `( {{ Γ ⊢s σ ≈ σ' : Δ }} ->
+     (** This extra argument is here to be consistent with
+         [wf_sub_subtyp].
+      *)
+     {{ ⊢ Δ' }} ->
      {{ ⊢ Δ ⊆ Δ' }} ->
      {{ Γ ⊢s σ ≈ σ' : Δ' }} )
 where "Γ ⊢s S1 ≈ S2 : Δ" := (wf_sub_eq Γ Δ S1 S2) (in custom judg) : type_scope
 
-with wf_subtyping : ctx -> typ -> typ -> Prop :=
+with wf_subtyp : ctx -> typ -> typ -> Prop :=
 | wf_subtyp_refl :
-  `( {{ Γ ⊢ M ≈ M' : Type@i }} ->
+  (** We need this extra argument in order to prove the lemmas
+      in CtxSub.v independently. We can prove those and
+      presupposition lemmas mutually dependently, but that would
+      be more messy.
+
+      The main point of this assumption gives presupposition for
+      RHS directly so that we can remove the extra arguments in
+      type checking rules immediately.
+   *)
+  `( {{ Γ ⊢ M' : Type@i }} ->
+     {{ Γ ⊢ M ≈ M' : Type@i }} ->
      {{ Γ ⊢ M ⊆ M' }} )
 | wf_subtyp_trans :
   `( {{ Γ ⊢ M ⊆ M' }} ->
@@ -315,7 +345,7 @@ with wf_subtyping : ctx -> typ -> typ -> Prop :=
      {{ Γ , A' ⊢ B' : Type@i }} ->
      {{ Γ , A' ⊢ B ⊆ B' }} ->
      {{ Γ ⊢ Π A B ⊆ Π A' B' }} )
-where "Γ ⊢ A ⊆ A'" := (wf_subtyping Γ A A') (in custom judg) : type_scope.
+where "Γ ⊢ A ⊆ A'" := (wf_subtyp Γ A A') (in custom judg) : type_scope.
 
 Scheme wf_ctx_mut_ind := Induction for wf_ctx Sort Prop
 with wf_ctx_sub_mut_ind := Induction for wf_ctx_sub Sort Prop
@@ -323,7 +353,7 @@ with wf_exp_mut_ind := Induction for wf_exp Sort Prop
 with wf_exp_eq_mut_ind := Induction for wf_exp_eq Sort Prop
 with wf_sub_mut_ind := Induction for wf_sub Sort Prop
 with wf_sub_eq_mut_ind := Induction for wf_sub_eq Sort Prop
-with wf_subtyping_mut_ind := Induction for wf_subtyping Sort Prop.
+with wf_subtyp_mut_ind := Induction for wf_subtyp Sort Prop.
 Combined Scheme syntactic_wf_mut_ind from
   wf_ctx_mut_ind,
   wf_ctx_sub_mut_ind,
@@ -331,7 +361,7 @@ Combined Scheme syntactic_wf_mut_ind from
   wf_exp_eq_mut_ind,
   wf_sub_mut_ind,
   wf_sub_eq_mut_ind,
-  wf_subtyping_mut_ind.
+  wf_subtyp_mut_ind.
 
 Scheme wf_ctx_mut_ind' := Induction for wf_ctx Sort Prop
 with wf_exp_mut_ind' := Induction for wf_exp Sort Prop
@@ -346,6 +376,8 @@ Inductive wf_ctx_eq : ctx -> ctx -> Prop :=
 | wf_ctx_eq_extend :
   `( {{ ⊢ Γ ≈ Δ }} ->
      {{ Γ ⊢ A : Type@i }} ->
+     {{ Γ ⊢ A' : Type@i }} ->
+     {{ Δ ⊢ A : Type@i }} ->
      {{ Δ ⊢ A' : Type@i }} ->
      {{ Γ ⊢ A ≈ A' : Type@i }} ->
      {{ Δ ⊢ A ≈ A' : Type@i }} ->
@@ -353,10 +385,10 @@ Inductive wf_ctx_eq : ctx -> ctx -> Prop :=
 where "⊢ Γ ≈ Γ'" := (wf_ctx_eq Γ Γ') (in custom judg) : type_scope.
 
 #[export]
-Hint Constructors wf_ctx wf_ctx_eq wf_ctx_sub wf_exp wf_sub wf_exp_eq wf_sub_eq wf_subtyping ctx_lookup : mcltt.
+Hint Constructors wf_ctx wf_ctx_eq wf_ctx_sub wf_exp wf_sub wf_exp_eq wf_sub_eq wf_subtyp ctx_lookup : mcltt.
 
 #[export]
-Instance wf_exp_PER Γ A : PER (wf_exp_eq Γ A).
+Instance wf_exp_eq_PER Γ A : PER (wf_exp_eq Γ A).
 Proof.
   split.
   - eauto using wf_exp_eq_sym.
@@ -364,7 +396,7 @@ Proof.
 Qed.
 
 #[export]
-Instance wf_sub_PER Γ Δ : PER (wf_sub_eq Γ Δ).
+Instance wf_sub_eq_PER Γ Δ : PER (wf_sub_eq Γ Δ).
 Proof.
   split.
   - eauto using wf_sub_eq_sym.
@@ -372,34 +404,133 @@ Proof.
 Qed.
 
 #[export]
-  Instance wf_subtyping_trans Γ : Transitive (wf_subtyping Γ).
+Instance wf_ctx_eq_Symmetric : Symmetric wf_ctx_eq.
+Proof.
+  induction 1; mauto.
+Qed.
+
+#[export]
+Instance wf_subtyp_Transitive Γ : Transitive (wf_subtyp Γ).
 Proof.
   hnf; mauto.
 Qed.
 
+(** Immediate & Independent Presuppositions *)
+
+Lemma presup_ctx_sub : forall {Γ Δ}, {{ ⊢ Γ ⊆ Δ }} -> {{ ⊢ Γ }} /\ {{ ⊢ Δ }}.
+Proof with mautosolve.
+  induction 1; destruct_pairs...
+Qed.
+
+#[export]
+Hint Resolve presup_ctx_sub : mcltt.
+
+Lemma presup_ctx_sub_left : forall {Γ Δ}, {{ ⊢ Γ ⊆ Δ }} -> {{ ⊢ Γ }}.
+Proof with easy.
+  intros * ?%presup_ctx_sub...
+Qed.
+
+#[export]
+Hint Resolve presup_ctx_sub_left : mcltt.
+
+Lemma presup_ctx_sub_right : forall {Γ Δ}, {{ ⊢ Γ ⊆ Δ }} -> {{ ⊢ Δ }}.
+Proof with easy.
+  intros * ?%presup_ctx_sub...
+Qed.
+
+#[export]
+Hint Resolve presup_ctx_sub_right : mcltt.
+
+Lemma presup_subtyp_right : forall {Γ A B}, {{ Γ ⊢ A ⊆ B }} -> exists i, {{ Γ ⊢ B : Type@i }}.
+Proof with mautosolve.
+  induction 1...
+Qed.
+
+#[export]
+Hint Resolve presup_subtyp_right : mcltt.
+
+(** Subtyping Rules without Extra Arguments *)
+
+Lemma wf_exp_subtyp' : forall Γ A A' M,
+    {{ Γ ⊢ M : A }} ->
+    {{ Γ ⊢ A ⊆ A' }} ->
+    {{ Γ ⊢ M : A' }}.
+Proof.
+  intros.
+  assert (exists i, {{ Γ ⊢ A' : Type@i }}) as [] by mauto.
+  econstructor; mauto.
+Qed.
+
+#[export]
+Hint Resolve wf_exp_subtyp' : mcltt.
+#[export]
+Remove Hints wf_exp_subtyp : mcltt.
 
-Add Parametric Morphism i Γ : (wf_exp Γ)
-    with signature wf_exp_eq Γ {{{ Type@i }}} ==> eq ==> iff as wf_exp_morph.
+Lemma wf_sub_subtyp' : forall Γ Δ Δ' σ,
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ ⊢ Δ ⊆ Δ' }} ->
+    {{ Γ ⊢s σ : Δ' }}.
 Proof.
-  intros; split; mauto.
+  intros.
+  econstructor; mauto.
 Qed.
 
-Add Parametric Morphism i Γ : (wf_exp_eq Γ)
-    with signature wf_exp_eq Γ {{{ Type@i }}} ==> eq ==> eq ==> iff as wf_exp_eq_morph.
+#[export]
+Hint Resolve wf_sub_subtyp' : mcltt.
+#[export]
+Remove Hints wf_sub_subtyp : mcltt.
+
+Lemma wf_exp_eq_subtyp' : forall Γ A A' M M',
+    {{ Γ ⊢ M ≈ M' : A }} ->
+    {{ Γ ⊢ A ⊆ A' }} ->
+    {{ Γ ⊢ M ≈ M' : A' }}.
 Proof.
-  intros; split; mauto.
+  intros.
+  assert (exists i, {{ Γ ⊢ A' : Type@i }}) as [] by mauto.
+  econstructor; mauto.
 Qed.
 
+#[export]
+Hint Resolve wf_exp_eq_subtyp' : mcltt.
+#[export]
+Remove Hints wf_exp_eq_subtyp : mcltt.
+
+Lemma wf_sub_eq_subtyp' : forall Γ Δ Δ' σ σ',
+    {{ Γ ⊢s σ ≈ σ' : Δ }} ->
+    {{ ⊢ Δ ⊆ Δ' }} ->
+    {{ Γ ⊢s σ ≈ σ' : Δ' }}.
+Proof.
+  intros.
+  econstructor; mauto.
+Qed.
+
+#[export]
+Hint Resolve wf_sub_eq_subtyp' : mcltt.
+#[export]
+Remove Hints wf_sub_eq_subtyp : mcltt.
+
 Add Parametric Morphism Γ T : (wf_exp_eq Γ T)
-    with signature (wf_exp_eq Γ T) ==> eq ==> iff as wf_exp_eq_morph1.
+    with signature wf_exp_eq Γ T ==> eq ==> iff as wf_exp_eq_morphism_iff1.
 Proof.
-  intros; split; mauto.
+  split; mauto.
 Qed.
 
 Add Parametric Morphism Γ T : (wf_exp_eq Γ T)
-    with signature eq ==> (wf_exp_eq Γ T) ==> iff as wf_exp_eq_morph2.
+    with signature eq ==> wf_exp_eq Γ T ==> iff as wf_exp_eq_morphism_iff2.
 Proof.
-  intros; split; mauto.
+  split; mauto.
+Qed.
+
+Add Parametric Morphism Γ Δ : (wf_sub_eq Γ Δ)
+    with signature wf_sub_eq Γ Δ ==> eq ==> iff as wf_sub_eq_morphism_iff1.
+Proof.
+  split; mauto.
+Qed.
+
+Add Parametric Morphism Γ Δ : (wf_sub_eq Γ Δ)
+    with signature eq ==> wf_sub_eq Γ Δ ==> iff as wf_sub_eq_morphism_iff2.
+Proof.
+  split; mauto.
 Qed.
 
 #[export]
@@ -410,35 +541,18 @@ Hint Rewrite -> wf_sub_eq_id_compose_right wf_sub_eq_id_compose_left
                   wf_sub_eq_compose_assoc (* prefer right association *)
                   wf_sub_eq_p_extend using mauto 4 : mcltt.
 
-
 #[export]
- Hint Rewrite -> wf_exp_eq_sub_id wf_exp_eq_pi_sub using mauto 4 : mcltt.
+Hint Rewrite -> wf_exp_eq_sub_id wf_exp_eq_pi_sub using mauto 4 : mcltt.
 
 #[export]
-  Instance wf_exp_eq_per_elem Γ T : PERElem _ (wf_exp Γ T) (wf_exp_eq Γ T).
+Instance wf_exp_eq_per_elem Γ T : PERElem _ (wf_exp Γ T) (wf_exp_eq Γ T).
 Proof.
   intros a Ha. mauto.
 Qed.
 
 
 #[export]
-  Instance wf_sub_eq_per_elem Γ Δ : PERElem _ (wf_sub Γ Δ) (wf_sub_eq Γ Δ).
+Instance wf_sub_eq_per_elem Γ Δ : PERElem _ (wf_sub Γ Δ) (wf_sub_eq Γ Δ).
 Proof.
   intros a Ha. mauto.
 Qed.
-
-
-Add Parametric Morphism Γ j : (wf_subtyping Γ)
-    with signature eq ==> (wf_exp_eq Γ {{{Type@j}}}) ==> iff as wf_subtyping_resp_exp_eq_morphism1.
-Proof.
-  split; intros;
-    etransitivity; mauto 3.
-Qed.
-
-
-Add Parametric Morphism Γ i : (wf_subtyping Γ)
-    with signature (wf_exp_eq Γ {{{Type@i}}}) ==> eq ==> iff as wf_subtyping_resp_exp_eq_morphism2.
-Proof.
-  split; intros;
-    etransitivity; mauto 3.
-Qed.
diff --git a/theories/Core/Syntactic/System/Lemmas.v b/theories/Core/Syntactic/System/Lemmas.v
index c17a06fa..cf85bb04 100644
--- a/theories/Core/Syntactic/System/Lemmas.v
+++ b/theories/Core/Syntactic/System/Lemmas.v
@@ -1,51 +1,7 @@
 From Mcltt Require Import Base LibTactics System.Definitions.
 Import Syntax_Notations.
 
-(* Recover previous rules without subtyping *)
-
-Lemma wf_conv : forall Γ M A i A',
-    {{ Γ ⊢ M : A }} ->
-    {{ Γ ⊢ A ≈ A' : Type@i }} ->
-    {{ Γ ⊢ M : A' }}.
-Proof. mauto. Qed.
-
-Lemma wf_cumu : forall Γ A i,
-    {{ ⊢ Γ }} ->
-    {{ Γ ⊢ A : Type@i }} ->
-    {{ Γ ⊢ A : Type@(S i) }}.
-Proof. mauto. Qed.
-
-Lemma wf_ctx_sub_refl : forall Γ Δ,
-    {{ ⊢ Γ ≈ Δ }} ->
-    {{ ⊢ Γ ⊆ Δ }}.
-Proof.
-  induction 1; mauto.
-Qed.
-
-#[export]
-  Hint Resolve wf_conv wf_cumu wf_ctx_sub_refl : mcltt.
-
-Lemma wf_sub_conv : forall Γ σ Δ Δ',
-  {{ Γ ⊢s σ : Δ }} ->
-  {{ ⊢ Δ ≈ Δ' }} ->
-  {{ Γ ⊢s σ : Δ' }}.
-Proof. mauto. Qed.
-
-Lemma wf_exp_eq_conv : forall Γ M M' A A' i,
-   {{ Γ ⊢ M ≈ M' : A }} ->
-   {{ Γ ⊢ A ≈ A' : Type@i }} ->
-   {{ Γ ⊢ M ≈ M' : A' }}.
-Proof. mauto. Qed.
-
-Lemma wf_sub_eq_conv : forall Γ σ σ' Δ Δ',
-    {{ Γ ⊢s σ ≈ σ' : Δ }} ->
-    {{ ⊢ Δ ≈ Δ' }} ->
-    {{ Γ ⊢s σ ≈ σ' : Δ' }}.
-Proof. mauto. Qed.
-
-#[export]
-  Hint Resolve wf_sub_conv wf_exp_eq_conv wf_sub_eq_conv : mcltt.
-
+(* Core Presuppositions *)
 Lemma ctx_decomp : forall {Γ A}, {{ ⊢ Γ , A }} -> {{ ⊢ Γ }} /\ exists i, {{ Γ ⊢ A : Type@i }}.
 Proof with now eauto.
   inversion 1...
@@ -67,46 +23,6 @@ Qed.
 #[export]
 Hint Resolve ctx_decomp_left ctx_decomp_right : mcltt.
 
-Lemma lift_exp_ge : forall {Γ A n m}, {{ ⊢ Γ }} -> n <= m -> {{ Γ ⊢ A : Type@n }} -> {{ Γ ⊢ A : Type@m }}.
-Proof with mautosolve.
-  induction 2...
-Qed.
-
-#[export]
-Hint Resolve lift_exp_ge : mcltt.
-
-Corollary lift_exp_max_left : forall {Γ A n} m, {{ ⊢ Γ }} -> {{ Γ ⊢ A : Type@n }} -> {{ Γ ⊢ A : Type@(max n m) }}.
-Proof with mautosolve.
-  intros.
-  assert (n <= max n m) by lia...
-Qed.
-
-Corollary lift_exp_max_right : forall {Γ A} n {m}, {{ ⊢ Γ }} -> {{ Γ ⊢ A : Type@m }} -> {{ Γ ⊢ A : Type@(max n m) }}.
-Proof with mautosolve.
-  intros.
-  assert (m <= max n m) by lia...
-Qed.
-
-Lemma lift_exp_eq_ge : forall {Γ A A' n m}, n <= m -> {{ Γ ⊢ A ≈ A': Type@n }} -> {{ Γ ⊢ A ≈ A' : Type@m }}.
-Proof with mautosolve.
-  induction 1; subst...
-Qed.
-
-#[export]
-Hint Resolve lift_exp_eq_ge : mcltt.
-
-Corollary lift_exp_eq_max_left : forall {Γ A A' n} m, {{ Γ ⊢ A ≈ A' : Type@n }} -> {{ Γ ⊢ A ≈ A' : Type@(max n m) }}.
-Proof with mautosolve.
-  intros.
-  assert (n <= max n m) by lia...
-Qed.
-
-Corollary lift_exp_eq_max_right : forall {Γ A A'} n {m}, {{ Γ ⊢ A ≈ A' : Type@m }} -> {{ Γ ⊢ A ≈ A' : Type@(max n m) }}.
-Proof with mautosolve.
-  intros.
-  assert (m <= max n m) by lia...
-Qed.
-
 Lemma presup_ctx_eq : forall {Γ Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ ⊢ Γ }} /\ {{ ⊢ Δ }}.
 Proof with mautosolve.
   induction 1; destruct_pairs...
@@ -125,25 +41,6 @@ Qed.
 #[export]
 Hint Resolve presup_ctx_eq presup_ctx_eq_left presup_ctx_eq_right : mcltt.
 
-Lemma presup_ctx_sub : forall {Γ Δ}, {{ ⊢ Γ ⊆ Δ }} -> {{ ⊢ Γ }} /\ {{ ⊢ Δ }}.
-Proof with mautosolve.
-  induction 1; destruct_pairs...
-Qed.
-
-Corollary presup_ctx_sub_left : forall {Γ Δ}, {{ ⊢ Γ ⊆ Δ }} -> {{ ⊢ Γ }}.
-Proof with easy.
-  intros * ?%presup_ctx_sub...
-Qed.
-
-Corollary presup_ctx_sub_right : forall {Γ Δ}, {{ ⊢ Γ ⊆ Δ }} -> {{ ⊢ Δ }}.
-Proof with easy.
-  intros * ?%presup_ctx_sub...
-Qed.
-
-#[export]
-  Hint Resolve presup_ctx_sub presup_ctx_sub_left presup_ctx_sub_right : mcltt.
-
-
 Lemma presup_sub_ctx : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ ⊢ Γ }} /\ {{ ⊢ Δ }}.
 Proof with mautosolve.
   induction 1; destruct_pairs...
@@ -189,28 +86,149 @@ Qed.
 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 (mautosolve 2).
+Proof with mautosolve 2.
   induction 1...
 Qed.
 
 #[export]
 Hint Resolve presup_exp_eq_ctx : mcltt.
 
-Lemma exp_eq_refl : forall {Γ M A}, {{ Γ ⊢ M : A }} -> {{ Γ ⊢ M ≈ M : A }}.
-Proof.
-  mauto.
+(* Recover some previous rules without 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 }} ->
+    (* this will be removed in SystemOpt *)
+    {{ Γ ⊢ A' : Type@i }} ->
+    {{ Γ ⊢ A ≈ A' : Type@i }} ->
+    {{ Γ ⊢ M : A' }}.
+Proof. mauto. Qed.
+
+Lemma wf_cumu : forall Γ A i,
+    {{ Γ ⊢ A : Type@i }} ->
+    {{ Γ ⊢ A : Type@(S i) }}.
+Proof with mautosolve.
+  intros.
+  enough {{ ⊢ Γ }}...
 Qed.
 
 #[export]
-Hint Resolve exp_eq_refl : mcltt.
+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 sub_eq_refl : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢s σ ≈ σ : Δ }}.
+Lemma wf_exp_eq_conv : forall Γ M M' A A' i,
+   {{ Γ ⊢ M ≈ M' : A }} ->
+    (* this 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) }}.
+Proof with mautosolve.
+  intros.
+  enough {{ ⊢ Γ }}...
+Qed.
+
+#[export]
+Hint Resolve wf_exp_eq_conv 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.
-  mauto.
+  intros Δ Δ' H **; split; [| symmetry in H]; mauto.
+Qed.
+
+Lemma lift_exp_ge : forall {Γ A n m},
+    n <= m ->
+    {{ Γ ⊢ A : Type@n }} ->
+    {{ Γ ⊢ A : Type@m }}.
+Proof with mautosolve.
+  induction 1...
 Qed.
 
 #[export]
-Hint Resolve sub_eq_refl : mcltt.
+Hint Resolve lift_exp_ge : mcltt.
+
+Corollary lift_exp_max_left : forall {Γ A n} m,
+    {{ Γ ⊢ A : Type@n }} ->
+    {{ Γ ⊢ A : Type@(max n m) }}.
+Proof with mautosolve.
+  intros.
+  assert (n <= max n m) by lia...
+Qed.
+
+Corollary lift_exp_max_right : forall {Γ A} n {m},
+    {{ Γ ⊢ A : Type@m }} ->
+    {{ Γ ⊢ A : Type@(max n m) }}.
+Proof with mautosolve.
+  intros.
+  assert (m <= max n m) by lia...
+Qed.
+
+Lemma lift_exp_eq_ge : forall {Γ A A' n m},
+    n <= m ->
+    {{ Γ ⊢ A ≈ A': Type@n }} ->
+    {{ Γ ⊢ A ≈ A' : Type@m }}.
+Proof with mautosolve.
+  induction 1; subst...
+Qed.
+
+#[export]
+Hint Resolve lift_exp_eq_ge : mcltt.
+
+Corollary lift_exp_eq_max_left : forall {Γ A A' n} m,
+    {{ Γ ⊢ A ≈ A' : Type@n }} ->
+    {{ Γ ⊢ A ≈ A' : Type@(max n m) }}.
+Proof with mautosolve.
+  intros.
+  assert (n <= max n m) by lia...
+Qed.
+
+Corollary lift_exp_eq_max_right : forall {Γ A A'} n {m},
+    {{ Γ ⊢ A ≈ A' : Type@m }} ->
+    {{ Γ ⊢ A ≈ A' : Type@(max n m) }}.
+Proof with mautosolve.
+  intros.
+  assert (m <= max n m) by lia...
+Qed.
+
+(* PER extension *)
+
+Lemma exp_eq_refl : forall {Γ M A},
+    {{ Γ ⊢ M : A }} ->
+    {{ Γ ⊢ M ≈ M : A }}.
+Proof. mauto. Qed.
+
+#[export]
+Hint Resolve exp_eq_refl : mcltt.
 
 Lemma exp_eq_trans_typ_max : forall {Γ i i' A A' A''},
     {{ Γ ⊢ A ≈ A' : Type@i }} ->
@@ -225,302 +243,455 @@ Qed.
 #[export]
 Hint Resolve exp_eq_trans_typ_max : mcltt.
 
-Lemma exp_sub_typ : forall {Δ Γ A σ i}, {{ Δ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ A[σ] : Type@i }}.
-Proof.
-  mauto.
+Lemma sub_eq_refl : forall {Γ σ Δ},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Γ ⊢s σ ≈ σ : Δ }}.
+Proof. mauto. Qed.
+
+#[export]
+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 σ : Δ }} -> {{ Γ ⊢ A[σ] ≈ A'[σ] : Type@i }}.
-Proof.
-  intros; econstructor; mauto 3.
+Lemma exp_eq_sub_cong_typ1 : forall {Δ Γ A A' σ i},
+    {{ Δ ⊢ A ≈ A' : Type@i }} ->
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Γ ⊢ A[σ] ≈ A'[σ] : Type@i }}.
+Proof with mautosolve 3.
+  intros.
+  eapply wf_exp_eq_conv...
 Qed.
 
-Lemma exp_eq_sub_cong_typ2' : forall Δ Γ A σ τ i, {{ Δ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢s σ ≈ τ : Δ }} -> {{ Γ ⊢ A[σ] ≈ A[τ] : Type@i }}.
-Proof with mautosolve.
+Lemma exp_eq_sub_cong_typ2' : forall {Δ Γ A σ τ i},
+    {{ Δ ⊢ A : Type@i }} ->
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Γ ⊢s σ ≈ τ : Δ }} ->
+    {{ Γ ⊢ A[σ] ≈ A[τ] : Type@i }}.
+Proof with mautosolve 3.
   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 mautosolve.
+Lemma exp_eq_sub_compose_typ : forall {Ψ Δ Γ A σ τ i},
+    {{ Ψ ⊢ A : Type@i }} ->
+    {{ Δ ⊢s σ : Ψ }} ->
+    {{ Γ ⊢s τ : Δ }} ->
+    {{ Γ ⊢ A[σ][τ] ≈ A[σ∘τ] : Type@i }}.
+Proof with mautosolve 3.
   intros.
   eapply wf_exp_eq_conv...
 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_sub_typ 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 σ : Ψ }} -> {{ Γ ⊢s τ : Δ }} -> {{ Γ ⊢ Type@i[σ][τ] ≈ Type@i : Type@(S i) }}.
-Proof.
-  mauto.
-Qed.
+Lemma exp_eq_typ_sub_sub : forall {Γ Δ Ψ σ τ i},
+    {{ Δ ⊢s σ : Ψ }} ->
+    {{ Γ ⊢s τ : Δ }} ->
+    {{ Γ ⊢ Type@i[σ][τ] ≈ Type@i : Type@(S i) }}.
+Proof. mauto. Qed.
 
 #[export]
 Hint Resolve exp_eq_typ_sub_sub : mcltt.
 #[export]
- Hint Rewrite -> exp_eq_sub_compose_typ exp_eq_typ_sub_sub using mauto 4 : mcltt.
-
+Hint Rewrite -> @exp_eq_sub_compose_typ @exp_eq_typ_sub_sub using mauto 4 : mcltt.
 
-Lemma vlookup_0_typ : forall {Γ i}, {{ ⊢ Γ }} -> {{ Γ, Type@i ⊢ # 0 : Type@i }}.
-Proof with mautosolve.
+Lemma vlookup_0_typ : forall {Γ i},
+    {{ ⊢ Γ }} ->
+    {{ Γ, Type@i ⊢ # 0 : Type@i }}.
+Proof with mautosolve 4.
   intros.
-  eapply wf_conv...
+  eapply wf_conv; mauto 4.
+  econstructor...
 Qed.
 
-Lemma vlookup_1_typ : forall {Γ i A j}, {{ ⊢ Γ }} -> {{ Γ, Type@i ⊢ A : Type@j }} -> {{ Γ, Type@i, A ⊢ # 1 : Type@i }}.
+Lemma vlookup_1_typ : forall {Γ i A j},
+    {{ Γ, Type@i ⊢ A : Type@j }} ->
+    {{ Γ, Type@i, A ⊢ # 1 : Type@i }}.
 Proof with mautosolve 4.
   intros.
-  assert {{ ⊢ Γ, Type@i }} by mauto 4.
-  assert {{ ⊢ Γ, Type@i, A }} by mauto 4.
+  assert {{ Γ, Type@i ⊢s Wk : Γ }} by mauto 4.
+  assert {{ Γ, Type@i, A ⊢s Wk : Γ, Type@i }} by mauto 4.
   eapply wf_conv...
 Qed.
 
 #[export]
 Hint Resolve vlookup_0_typ vlookup_1_typ : mcltt.
 
-Lemma exp_eq_var_0_sub_typ : forall Γ σ Δ M i, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ M : Type@i }} -> {{ Γ ⊢ #0[σ ,, M] ≈ M : Type@i }}.
+Lemma exp_sub_typ_helper : forall {Γ σ Δ M i},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Γ ⊢ M : Type@i }} ->
+    {{ Γ ⊢ M : Type@i[σ] }}.
+Proof.
+  intros.
+  do 2 (econstructor; mauto 4).
+Qed.
+
+#[export]
+Hint Resolve exp_sub_typ_helper : mcltt.
+
+Lemma exp_eq_var_0_sub_typ : forall {Γ σ Δ M i},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Γ ⊢ M : Type@i }} ->
+    {{ Γ ⊢ #0[σ,,M] ≈ M : Type@i }}.
 Proof with mautosolve 4.
   intros.
-  assert {{ ⊢ Δ }} by mauto 4.
-  assert {{ Γ ⊢ M : Type@i[σ] }} by mauto 4.
-  eapply wf_exp_eq_conv...
+  eapply wf_exp_eq_conv; mauto 3.
+  econstructor...
 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 }}.
+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 mautosolve 4.
   inversion 4 as [? Δ'|]; subst.
-  assert {{ ⊢ Δ' }} by mauto.
+  assert {{ ⊢ Δ' }} by mauto 4.
+  assert {{ Δ', Type@j ⊢s Wk : Δ' }} by mauto 4.
   eapply wf_exp_eq_conv...
 Qed.
 
 #[export]
 Hint Resolve exp_eq_var_0_sub_typ exp_eq_var_1_sub_typ : mcltt.
 #[export]
-  Hint Rewrite -> exp_eq_var_0_sub_typ exp_eq_var_1_sub_typ : mcltt.
+Hint Rewrite -> @exp_eq_var_0_sub_typ @exp_eq_var_1_sub_typ : mcltt.
 
-Lemma exp_eq_var_0_weaken_typ : forall {Γ A i}, {{ ⊢ Γ , A }} -> {{ #0 : Type@i[Wk] ∈ Γ }} -> {{ Γ , A ⊢ #0[Wk] ≈ #1 : Type@i }}.
-Proof with mautosolve.
+Lemma exp_eq_var_0_weaken_typ : forall {Γ A i},
+    {{ ⊢ Γ, A }} ->
+    {{ #0 : Type@i[Wk] ∈ Γ }} ->
+    {{ Γ, A ⊢ #0[Wk] ≈ #1 : Type@i }}.
+Proof with mautosolve 3.
   inversion_clear 1.
   inversion 1 as [? Γ'|]; subst.
   assert {{ ⊢ Γ' }} by mauto.
+  assert {{ Γ', Type@i ⊢s Wk : Γ' }} by mauto 4.
+  assert {{ Γ', Type@i, A ⊢s Wk : Γ', Type@i }} by mauto 4.
   eapply wf_exp_eq_conv...
 Qed.
 
 #[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 mautosolve.
+Lemma sub_extend_typ : forall {Γ σ Δ M i},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Γ ⊢ M : Type@i }} ->
+    {{ Γ ⊢s σ,,M : Δ, Type@i }}.
+Proof with mautosolve 4.
   intros.
-  assert {{ ⊢ Δ }} by mautosolve.
   econstructor...
 Qed.
 
 #[export]
 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 mautosolve.
+Lemma sub_eq_extend_cong_typ : forall {Γ σ σ' Δ M M' i},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Γ ⊢s σ ≈ σ' : Δ }} ->
+    {{ Γ ⊢ M ≈ M' : Type@i }} ->
+    {{ Γ ⊢s σ,,M ≈ σ',,M' : Δ, Type@i }}.
+Proof with mautosolve 4.
   intros.
-  assert {{ ⊢ Δ }} by mautosolve.
-  econstructor...
+  econstructor; mauto 3.
+  eapply wf_exp_eq_conv...
 Qed.
 
-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 mautosolve.
+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 mautosolve 4.
   intros.
   econstructor...
 Qed.
 
-Lemma sub_eq_p_extend_typ : forall {Γ σ Γ' M i}, {{ Γ' ⊢s σ : Γ }} -> {{ Γ' ⊢ M : Type@i }} -> {{ Γ' ⊢s Wk ∘ (σ ,, M) ≈ σ : Γ }}.
-Proof with mautosolve.
+Lemma sub_eq_p_extend_typ : forall {Γ σ Γ' M i},
+    {{ Γ' ⊢s σ : Γ }} ->
+    {{ Γ' ⊢ M : Type@i }} ->
+    {{ Γ' ⊢s Wk ∘ (σ,,M) ≈ σ : Γ }}.
+Proof with mautosolve 4.
   intros.
-  assert {{ ⊢ Γ }} by mautosolve.
-  econstructor; revgoals...
+  assert {{ Γ ⊢ Type@i : Type@(S i) }} by mauto.
+  econstructor; mauto 3.
 Qed.
 
 #[export]
-Hint Resolve sub_eq_extend_cong_typ' sub_eq_extend_compose_typ sub_eq_p_extend_typ : mcltt.
+Hint Resolve sub_eq_extend_cong_typ sub_eq_extend_compose_typ sub_eq_p_extend_typ : mcltt.
 
-Lemma sub_eq_wk_var0_id : forall Γ A i,
+Lemma sub_eq_wk_var0_id : forall {Γ A i},
     {{ Γ ⊢ A : Type@i }} ->
     {{ Γ, A ⊢s Wk,,#0 ≈ Id : Γ, A }}.
-Proof.
+Proof with mautosolve 4.
   intros * ?.
   assert {{ ⊢ Γ, A }} by mauto 3.
   assert {{ Γ, A ⊢s (Wk∘Id),,#0[Id] ≈ Id : Γ, A }} by mauto.
   assert {{ Γ, A ⊢s Wk ≈ Wk∘Id : Γ }} by mauto.
-  assert {{ Γ, A ⊢ #0 ≈ #0[Id] : A[Wk] }} by mauto.
-  mauto 4.
+  enough {{ Γ, A ⊢ #0 ≈ #0[Id] : A[Wk] }}...
 Qed.
 
 #[export]
 Hint Resolve sub_eq_wk_var0_id : mcltt.
 #[export]
-Hint Rewrite -> sub_eq_wk_var0_id using mauto 4 : mcltt.
-
-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 mautosolve.
+Hint Rewrite -> @sub_eq_wk_var0_id using mauto 4 : mcltt.
+
+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 mautosolve 4.
   intros.
   assert {{ Γ ⊢ A[σ][τ] ≈ A[σ∘τ] : Type@i }} by mauto.
   assert {{ Γ ⊢ A[σ∘τ] ≈ A[σ'∘τ'] : Type@i }} by mauto.
-  assert {{ Γ ⊢ A[σ'∘τ'] ≈ A[σ'][τ'] : Type@i }}...
+  enough {{ Γ ⊢ 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.
-  mautosolve.
+(* 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 σ : Δ }} -> {{ Γ ⊢ M[σ] ≈ M'[σ] : ℕ }}.
-Proof.
-  intros. econstructor; mautosolve.
+Lemma exp_eq_sub_cong_nat1 : forall {Δ Γ M M' σ},
+    {{ Δ ⊢ M ≈ M' : ℕ }} ->
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Γ ⊢ M[σ] ≈ M'[σ] : ℕ }}.
+Proof with mautosolve 3.
+  intros.
+  eapply wf_exp_eq_conv...
 Qed.
 
-Lemma exp_eq_sub_cong_nat2' : forall {Δ Γ M σ τ}, {{ Δ ⊢ M : ℕ }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢s σ ≈ τ : Δ }} -> {{ Γ ⊢ M[σ] ≈ M[τ] : ℕ }}.
+Lemma exp_eq_sub_cong_nat2 : forall {Δ Γ M σ τ},
+    {{ Δ ⊢ M : ℕ }} ->
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Γ ⊢s σ ≈ τ : Δ }} ->
+    {{ Γ ⊢ M[σ] ≈ M[τ] : ℕ }}.
 Proof with mautosolve.
   intros.
-  eapply wf_exp_eq_subtyp...
+  eapply wf_exp_eq_conv...
 Qed.
 
-Lemma exp_eq_sub_compose_nat : forall {Ψ Δ Γ M σ τ}, {{ Ψ ⊢ M : ℕ }} -> {{ Δ ⊢s σ : Ψ }} -> {{ Γ ⊢s τ : Δ }} -> {{ Γ ⊢ M[σ][τ] ≈ M[σ∘τ] : ℕ }}.
-Proof with mautosolve.
+Lemma exp_eq_sub_compose_nat : forall {Ψ Δ Γ M σ τ},
+    {{ Ψ ⊢ M : ℕ }} ->
+    {{ Δ ⊢s σ : Ψ }} ->
+    {{ Γ ⊢s τ : Δ }} ->
+    {{ Γ ⊢ M[σ][τ] ≈ M[σ∘τ] : ℕ }}.
+Proof with mautosolve 4.
   intros.
-  eapply wf_exp_eq_subtyp...
+  eapply wf_exp_eq_conv...
 Qed.
 
 #[export]
-Hint Resolve exp_sub_nat exp_eq_sub_cong_nat1 exp_eq_sub_cong_nat2' exp_eq_sub_compose_nat : mcltt.
+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 {Γ Δ Ψ σ τ}, {{ Δ ⊢s σ : Ψ }} -> {{ Γ ⊢s τ : Δ }} -> {{ Γ ⊢ ℕ[σ][τ] ≈ ℕ : Type@0 }}.
-Proof.
-  mauto.
-Qed.
+Lemma exp_eq_nat_sub_sub : forall {Γ Δ Ψ σ τ},
+    {{ Δ ⊢s σ : Ψ }} ->
+    {{ Γ ⊢s τ : Δ }} ->
+    {{ Γ ⊢ ℕ[σ][τ] ≈ ℕ : Type@0 }}.
+Proof. mauto. Qed.
 
 #[export]
 Hint Resolve exp_eq_nat_sub_sub : mcltt.
 
-Lemma exp_eq_nat_sub_sub_to_nat_sub : forall {Γ Δ Ψ Ψ' σ τ σ'}, {{ Δ ⊢s σ : Ψ }} -> {{ Γ ⊢s τ : Δ }} -> {{ Γ ⊢s σ' : Ψ' }} -> {{ Γ ⊢ ℕ[σ][τ] ≈ ℕ[σ'] : Type@0 }}.
-Proof.
-  mauto.
-Qed.
+Lemma exp_eq_nat_sub_sub_to_nat_sub : forall {Γ Δ Ψ Ψ' σ τ σ'},
+    {{ Δ ⊢s σ : Ψ }} ->
+    {{ Γ ⊢s τ : Δ }} ->
+    {{ Γ ⊢s σ' : Ψ' }} ->
+    {{ Γ ⊢ ℕ[σ][τ] ≈ ℕ[σ'] : Type@0 }}.
+Proof. mauto. Qed.
 
 #[export]
 Hint Resolve exp_eq_nat_sub_sub_to_nat_sub : mcltt.
 
-Lemma vlookup_0_nat : forall {Γ}, {{ ⊢ Γ }} -> {{ Γ, ℕ ⊢ # 0 : ℕ }}.
+Lemma vlookup_0_nat : forall {Γ},
+    {{ ⊢ Γ }} ->
+    {{ Γ, ℕ ⊢ # 0 : ℕ }}.
 Proof with mautosolve 4.
   intros.
-  assert {{ ⊢ Γ, ℕ }} by mautosolve 3.
-  assert {{ Γ, ℕ ⊢ # 0 : ℕ[Wk] }}...
+  eapply wf_conv; mauto 4.
+  econstructor...
 Qed.
 
-Lemma vlookup_1_nat : forall {Γ A i}, {{ ⊢ Γ }} -> {{ Γ, ℕ ⊢ A : Type@i }} -> {{ Γ, ℕ, A ⊢ # 1 : ℕ }}.
+Lemma vlookup_1_nat : forall {Γ A i},
+    {{ Γ, ℕ ⊢ A : Type@i }} ->
+    {{ Γ, ℕ, A ⊢ # 1 : ℕ }}.
 Proof with mautosolve 4.
   intros.
-  assert {{ ⊢ Γ, ℕ }} by mautosolve.
-  assert {{ ⊢ Γ, ℕ, A }} by mautosolve.
-  assert {{ Γ, ℕ, A ⊢ #1 : ℕ[Wk][Wk] }} by mauto.
-  assert {{ Γ, ℕ, A ⊢ ℕ[Wk][Wk] ≈ ℕ : Type@0 }}...
+  assert {{ Γ, ℕ ⊢s Wk : Γ }} by mauto 4.
+  assert {{ Γ, ℕ, A ⊢s Wk : Γ, ℕ }} by mauto 4.
+  eapply wf_conv...
 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 mautosolve.
+Lemma exp_sub_nat_helper : forall {Γ σ Δ M},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Γ ⊢ M : ℕ }} ->
+    {{ Γ ⊢ M : ℕ[σ] }}.
+Proof.
   intros.
-  assert {{ ⊢ Δ }} by mauto.
-  assert {{ Γ ⊢ M : ℕ[σ] }} by mautosolve.
-  assert {{ Γ ⊢ #0[σ,, M] ≈ M : ℕ[σ] }} by mautosolve.
-  assert {{ Γ ⊢ ℕ[σ] ≈ ℕ : Type@0 }}...
+  do 2 (econstructor; mauto 4).
 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 mautosolve.
+#[export]
+Hint Resolve exp_sub_nat_helper : mcltt.
+
+Lemma exp_eq_var_0_sub_nat : forall {Γ σ Δ M},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Γ ⊢ M : ℕ }} ->
+    {{ Γ ⊢ #0[σ,,M] ≈ M : ℕ }}.
+Proof with mautosolve 3.
+  intros.
+  eapply wf_exp_eq_conv; mauto 3.
+  econstructor...
+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 mautosolve 4.
   inversion 4 as [? Δ'|]; subst.
-  assert {{ ⊢ Δ' }} by mauto.
-  assert {{ Γ ⊢ #1[σ,, M] ≈ #0[σ] : ℕ[Wk][σ] }} by mauto.
+  assert {{ Γ ⊢ #1[σ,, M] ≈ #0[σ] : ℕ[Wk][σ] }} by mauto 4.
   assert {{ Γ ⊢ ℕ[Wk][σ] ≈ ℕ : Type@0 }}...
 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 mautosolve.
+Lemma exp_eq_var_0_weaken_nat : forall {Γ A},
+    {{ ⊢ Γ, A }} ->
+    {{ #0 : ℕ[Wk] ∈ Γ }} ->
+    {{ Γ, A ⊢ #0[Wk] ≈ #1 : ℕ }}.
+Proof with mautosolve 4.
   inversion 1; subst.
   inversion 1 as [? Γ'|]; subst.
-  assert {{ ⊢ Γ' }} by mauto.
-  assert {{ Γ', ℕ, A ⊢ #0[Wk] ≈ # 1 : ℕ[Wk][Wk] }} by mauto.
+  assert {{ Γ', ℕ, A ⊢ #0[Wk] ≈ # 1 : ℕ[Wk][Wk] }} by mauto 4.
   assert {{ Γ', ℕ, A ⊢ ℕ[Wk][Wk] ≈ ℕ : Type@0 }}...
 Qed.
 
 #[export]
 Hint Resolve exp_eq_var_0_weaken_nat : mcltt.
 
-Lemma sub_extend_nat : forall {Γ σ Δ M}, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ M : ℕ }} -> {{ Γ ⊢s (σ ,, M) : Δ , ℕ }}.
-Proof with mautosolve.
+Lemma sub_extend_nat : forall {Γ σ Δ M},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Γ ⊢ M : ℕ }} ->
+    {{ Γ ⊢s σ,,M : Δ , ℕ }}.
+Proof with mautosolve 3.
   intros.
-  assert {{ ⊢ Δ }} by mauto.
   econstructor...
 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 mautosolve.
+Lemma sub_eq_extend_cong_nat : forall {Γ σ σ' Δ M M'},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Γ ⊢s σ ≈ σ' : Δ }} ->
+    {{ Γ ⊢ M ≈ M' : ℕ }} ->
+    {{ Γ ⊢s σ,,M ≈ σ',,M' : Δ , ℕ }}.
+Proof with mautosolve 4.
   intros.
-  assert {{ ⊢ Δ }} by mauto.
-  econstructor...
+  econstructor; mauto 3.
+  eapply wf_exp_eq_conv...
 Qed.
 
-Lemma sub_eq_extend_compose_nat : forall {Γ τ Γ' σ Γ'' A i M}, {{ Γ' ⊢s σ : Γ'' }} -> {{ Γ'' ⊢ A : Type@i }} -> {{ Γ' ⊢ M : ℕ }} -> {{ Γ ⊢s τ : Γ' }} -> {{ Γ ⊢s (σ ,, M) ∘ τ ≈ ((σ ∘ τ) ,, M[τ]) : Γ'' , ℕ }}.
-Proof with mautosolve.
+Lemma sub_eq_extend_compose_nat : forall {Γ τ Γ' σ Γ'' M},
+    {{ Γ' ⊢s σ : Γ'' }} ->
+    {{ Γ' ⊢ M : ℕ }} ->
+    {{ Γ ⊢s τ : Γ' }} ->
+    {{ Γ ⊢s (σ,,M) ∘ τ ≈ (σ ∘ τ),,M[τ] : Γ'' , ℕ }}.
+Proof with mautosolve 3.
   intros.
   econstructor...
 Qed.
 
-Lemma sub_eq_p_extend_nat : forall {Γ σ Γ' M}, {{ Γ' ⊢s σ : Γ }} -> {{ Γ' ⊢ M : ℕ }} -> {{ Γ' ⊢s Wk ∘ (σ ,, M) ≈ σ : Γ }}.
-Proof with mautosolve.
+Lemma sub_eq_p_extend_nat : forall {Γ σ Γ' M},
+    {{ Γ' ⊢s σ : Γ }} ->
+    {{ Γ' ⊢ M : ℕ }} ->
+    {{ Γ' ⊢s Wk ∘ (σ,,M) ≈ σ : Γ }}.
+Proof with mautosolve 3.
   intros.
-  assert {{ ⊢ Γ }} by mauto.
-  econstructor; revgoals...
+  assert {{ Γ ⊢ ℕ : Type@0 }} by mauto.
+  econstructor...
 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 mautosolve.
+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 mautosolve 4.
   intros.
   assert {{ Γ ⊢ M[σ][τ] ≈ M[σ∘τ] : ℕ }} by mauto.
   assert {{ Γ ⊢ M[σ∘τ] ≈ M[σ'∘τ'] : ℕ }} by mauto.
-  assert {{ Γ ⊢ M[σ'∘τ'] ≈ M[σ'][τ'] : ℕ }}...
+  enough {{ Γ ⊢ 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 mautosolve.
+(* Other lemmas *)
+
+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 mautosolve 4.
   intros.
+  assert {{ Γ ⊢ A[σ∘τ] ≈ A[σ'∘τ'] : Type@i }} by mauto.
   assert {{ Γ ⊢ M[σ][τ] ≈ M[σ∘τ] : A[σ∘τ] }} by mauto.
   assert {{ Γ ⊢ M[σ∘τ] ≈ M[σ'∘τ'] : A[σ∘τ] }} by mauto.
   assert {{ Γ ⊢ M[σ'∘τ'] ≈ M[σ'][τ'] : A[σ'∘τ'] }} by mauto.
-  assert {{ Γ ⊢ M[σ'∘τ'] ≈ M[σ'][τ'] : A[σ∘τ] }}...
+  enough {{ Γ ⊢ M[σ'∘τ'] ≈ M[σ'][τ'] : A[σ∘τ] }} by mauto.
+  eapply wf_exp_eq_conv...
 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.
+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
@@ -530,7 +701,13 @@ Qed.
 #[export]
 Hint Resolve ctx_lookup_wf : mcltt.
 
-Lemma ctxeq_ctx_lookup : forall {Γ Δ A x}, {{ ⊢ Γ ≈ Δ }} -> {{ #x : A ∈ Γ }} -> exists B i, {{ #x : B ∈ Δ }} /\ {{ Γ ⊢ A ≈ B : Type@i }} /\ {{ Δ ⊢ A ≈ B : Type@i }}.
+Lemma ctxeq_ctx_lookup : forall {Γ Δ A x},
+    {{ ⊢ Γ ≈ Δ }} ->
+    {{ #x : A ∈ Γ }} ->
+    exists B i,
+      {{ #x : B ∈ Δ }} /\
+        {{ Γ ⊢ A ≈ B : Type@i }} /\
+        {{ Δ ⊢ A ≈ B : Type@i }}.
 Proof with mautosolve.
   intros * HΓΔ Hx; gen Δ.
   induction Hx as [|* ? IHHx]; inversion_clear 1 as [|? ? ? ? ? HΓΔ'];
@@ -540,8 +717,23 @@ Qed.
 #[export]
 Hint Resolve ctxeq_ctx_lookup : mcltt.
 
-Lemma sub_id_extend : forall {Γ M A i}, {{ Γ ⊢ A : Type@i }} -> {{ Γ ⊢ M : A }} -> {{ Γ ⊢s Id,,M : Γ, A }}.
-Proof with mautosolve.
+Lemma sub_id_on_typ : forall {Γ M A i},
+    {{ Γ ⊢ A : Type@i }} ->
+    {{ Γ ⊢ M : A }} ->
+    {{ Γ ⊢ M : A[Id] }}.
+Proof with mautosolve 4.
+  intros.
+  eapply wf_conv...
+Qed.
+
+#[export]
+Hint Resolve sub_id_on_typ : mcltt.
+
+Lemma sub_id_extend : forall {Γ M A i},
+    {{ Γ ⊢ A : Type@i }} ->
+    {{ Γ ⊢ M : A }} ->
+    {{ Γ ⊢s Id,,M : Γ, A }}.
+Proof with mautosolve 4.
   intros.
   econstructor...
 Qed.
@@ -549,40 +741,51 @@ Qed.
 #[export]
 Hint Resolve sub_id_extend : mcltt.
 
-Lemma sub_eq_p_id_extend : forall {Γ M A i}, {{ Γ ⊢ A : Type@i }} -> {{ Γ ⊢ M : A }} -> {{ Γ ⊢s Wk∘(Id ,, M) ≈ Id : Γ }}.
-Proof with mautosolve.
+Lemma sub_eq_p_id_extend : forall {Γ M A i},
+    {{ Γ ⊢ A : Type@i }} ->
+    {{ Γ ⊢ M : A }} ->
+    {{ Γ ⊢s Wk ∘ (Id,,M) ≈ Id : Γ }}.
+Proof with mautosolve 4.
   intros.
   econstructor...
 Qed.
 
 #[export]
 Hint Resolve sub_eq_p_id_extend : mcltt.
+#[export]
+Hint Rewrite -> @sub_eq_p_id_extend using mauto 4 : mcltt.
 
-Lemma sub_q : forall {Γ A i σ Δ}, {{ Δ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ , A[σ] ⊢s q σ : Δ , A }}.
-Proof with mautosolve.
+Lemma sub_q : forall {Γ A i σ Δ},
+    {{ Δ ⊢ A : Type@i }} ->
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Γ, A[σ] ⊢s q σ : Δ, A }}.
+Proof with mautosolve 3.
   intros.
-  assert {{ Γ ⊢ A[σ] : Type@i }} by mauto.
-  assert {{ ⊢ Γ, A[σ] }} by mauto 3.
-  assert {{ Γ, A[σ] ⊢s Wk : Γ }} by mauto.
-  assert {{ Γ, A[σ] ⊢ # 0 : A[σ][Wk] }} by mauto...
+  assert {{ Γ ⊢ A[σ] : Type@i }} by mauto 4.
+  assert {{ Γ, A[σ] ⊢s Wk : Γ }} by mauto 4.
+  assert {{ Γ, A[σ] ⊢ # 0 : A[σ][Wk] }} by mauto 4.
+  econstructor; mauto 3.
+  eapply wf_conv...
 Qed.
 
-Lemma sub_q_typ : forall {Γ σ Δ i}, {{ Γ ⊢s σ : Δ }} -> {{ Γ , Type@i ⊢s q σ : Δ , Type@i }}.
-Proof with mautosolve.
+Lemma sub_q_typ : forall {Γ σ Δ i},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Γ, Type@i ⊢s q σ : Δ, Type@i }}.
+Proof with mautosolve 4.
   intros.
   assert {{ ⊢ Γ }} by mauto 3.
-  assert {{ ⊢ Δ }} by mauto 3.
   assert {{ Γ, Type@i ⊢s Wk : Γ }} by mauto 4.
   assert {{ Γ, Type@i ⊢s σ ∘ Wk : Δ }} by mauto 4.
   assert {{ Γ, Type@i ⊢ # 0 : Type@i[Wk] }} by mauto 4.
   assert {{ Γ, Type@i ⊢ # 0 : Type@i }}...
 Qed.
 
-Lemma sub_q_nat : forall {Γ σ Δ}, {{ Γ ⊢s σ : Δ }} -> {{ Γ , ℕ ⊢s q σ : Δ , ℕ }}.
-Proof with mautosolve.
+Lemma sub_q_nat : forall {Γ σ Δ},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Γ, ℕ ⊢s q σ : Δ, ℕ }}.
+Proof with mautosolve 4.
   intros.
   assert {{ ⊢ Γ }} by mauto 3.
-  assert {{ ⊢ Δ }} by mauto 3.
   assert {{ Γ, ℕ ⊢s Wk : Γ }} by mauto 4.
   assert {{ Γ, ℕ ⊢s σ ∘ Wk : Δ }} by mauto 4.
   assert {{ Γ, ℕ ⊢ # 0 : ℕ[Wk] }} by mauto 4.
@@ -592,81 +795,97 @@ 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 mautosolve.
+Lemma exp_eq_var_1_sub_q_sigma_nat : forall {Γ A i σ Δ},
+    {{ Δ, ℕ ⊢ A : Type@i }} ->
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Γ, ℕ, A[q σ] ⊢ #1[q (q σ)] ≈ #1 : ℕ }}.
+Proof with mautosolve 4.
   intros.
-  assert {{ ⊢ Δ }} by mauto 4.
-  assert {{ ⊢ Δ, ℕ }} by mauto 3.
-  assert {{ ⊢ Γ }} by mauto 4.
-  assert {{ ⊢ Γ, ℕ }} by mauto 3.
   assert {{ Γ, ℕ ⊢s q σ : Δ, ℕ }} by mauto.
   assert {{ ⊢ Γ, ℕ, A[q σ] }} by mauto 3.
   assert {{ Δ, ℕ ⊢ #0 : ℕ }} by mauto.
   assert {{ Γ, ℕ, A[q σ] ⊢ #0 : A[q σ][Wk] }} by mauto 4.
   assert {{ Γ, ℕ, A[q σ] ⊢ A[q σ∘Wk] ≈ A[q σ][Wk] : Type@i }} by mauto 4.
-  assert {{ Γ, ℕ, A[q σ] ⊢ #0 : A[q σ∘Wk] }} by mauto 3.
-  assert {{ Γ, ℕ, A[q σ] ⊢s Wk : Γ, ℕ }} by mauto.
-  assert {{ Γ, ℕ, A[q σ] ⊢s q σ∘Wk : Δ, ℕ }} by mauto.
-  assert {{ Γ, ℕ, A[q σ] ⊢ #1[q (q σ)] ≈ #0[q σ∘Wk] : ℕ }} by 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 σ] ⊢ #1[q (q σ)] ≈ #1 : ℕ }}...
+  assert {{ Γ, ℕ, A[q σ] ⊢ #0 : A[q σ∘Wk] }} by (eapply wf_conv; mauto 4).
+  assert {{ Γ, ℕ, A[q σ] ⊢s q σ∘Wk : Δ, ℕ }} by mauto 4.
+  assert {{ Γ, ℕ, A[q σ] ⊢ #1[q (q σ)] ≈ #0[q σ∘Wk] : ℕ }} by mauto 4.
+  assert {{ Γ, ℕ, A[q σ] ⊢ #0[q σ∘Wk] ≈ #0[q σ][Wk] : ℕ }} by mauto 4.
+  assert {{ Γ, ℕ ⊢s σ∘Wk : Δ }} by mauto 4.
+  assert {{ Γ, ℕ ⊢ #0 : ℕ[σ∘Wk] }} by (eapply wf_conv; mauto 4).
+  assert {{ Γ, ℕ ⊢ #0[q σ] ≈ #0 : ℕ }} by mauto 4.
+  assert {{ Γ, ℕ, A[q σ] ⊢ #0[q σ][Wk] ≈ #0[Wk] : ℕ }} by mauto 4.
+  econstructor...
 Qed.
 
 #[export]
 Hint Resolve exp_eq_var_1_sub_q_sigma_nat : mcltt.
 
-Lemma sub_id_extend_zero : forall {Γ}, {{ ⊢ Γ }} -> {{ Γ ⊢s Id,,zero : Γ, ℕ }}.
-Proof.
-  mauto.
-Qed.
+Lemma sub_id_extend_zero : forall {Γ},
+    {{ ⊢ Γ }} ->
+    {{ Γ ⊢s Id,,zero : Γ, ℕ }}.
+Proof. mauto. Qed.
 
-Lemma sub_weak_compose_weak_extend_succ_var_1 : forall {Γ A i}, {{ Γ, ℕ ⊢ A : Type@i }} -> {{ Γ, ℕ, A ⊢s Wk∘Wk,,succ #1 : Γ, ℕ }}.
+Lemma sub_weak_compose_weak_extend_succ_var_1 : forall {Γ A i},
+    {{ Γ, ℕ ⊢ A : Type@i }} ->
+    {{ Γ, ℕ, A ⊢s (Wk ∘ Wk),,succ #1 : Γ, ℕ }}.
 Proof with mautosolve 4.
   intros.
-  assert {{ ⊢ Γ, ℕ }} by mauto.
-  assert {{ ⊢ Γ }} by mauto.
   assert {{ Γ, ℕ, A ⊢s Wk : Γ, ℕ }} by mauto 4.
-  assert {{ Γ, ℕ, A ⊢s Wk∘Wk : Γ }} by mauto 4.
-  eapply sub_extend_nat...
+  enough {{ Γ, ℕ, A ⊢s Wk ∘ Wk : Γ }}...
 Qed.
 
-Lemma sub_eq_id_extend_nat_compose_sigma : forall {Γ M σ Δ}, {{ Γ ⊢s σ : Δ }} -> {{ Δ ⊢ M : ℕ }} -> {{ Γ ⊢s (Id,,M)∘σ ≈ σ,,M[σ] : Δ, ℕ }}.
-Proof with mautosolve.
+Lemma sub_eq_id_extend_nat_compose_sigma : forall {Γ M σ Δ},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Δ ⊢ M : ℕ }} ->
+    {{ Γ ⊢s (Id,,M) ∘ σ ≈ σ,,M[σ] : Δ, ℕ }}.
+Proof with mautosolve 4.
   intros.
-  assert {{ Γ ⊢s (Id ,, M)∘σ ≈ Id∘σ ,, M[σ] : Δ, ℕ }} by (eapply sub_eq_extend_compose_nat; mautosolve).
-  assert {{ Γ ⊢s Id∘σ ,, M[σ] ≈ σ ,, M[σ] : Δ, ℕ }} by (eapply sub_eq_extend_cong_nat'; mauto)...
+  assert {{ Γ ⊢s (Id,,M) ∘ σ ≈ (Id ∘ σ),,M[σ] : Δ, ℕ }} by mauto 4.
+  enough {{ Γ ⊢s (Id ∘ σ),,M[σ] ≈ σ,,M[σ] : Δ, ℕ }} by mauto 4.
+  eapply sub_eq_extend_cong_nat...
 Qed.
 
-Lemma sub_eq_id_extend_compose_sigma : forall {Γ M A σ Δ i}, {{ Γ ⊢s σ : Δ }} -> {{ Δ ⊢ A : Type@i }} -> {{ Δ ⊢ M : A }} -> {{ Γ ⊢s (Id,,M)∘σ ≈ σ,,M[σ] : Δ, A }}.
+Lemma sub_eq_id_extend_compose_sigma : forall {Γ M A σ Δ i},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Δ ⊢ A : Type@i }} ->
+    {{ Δ ⊢ M : A }} ->
+    {{ Γ ⊢s (Id,,M) ∘ σ ≈ σ,,M[σ] : Δ, A }}.
 Proof with mautosolve 4.
   intros.
   assert {{ Δ ⊢s Id : Δ }} by mauto.
   assert {{ Δ ⊢ M : A[Id] }} by mauto.
-  assert {{ Γ ⊢s (Id ,, M)∘σ ≈ Id∘σ ,, M[σ] : Δ, A }} by mauto 3.
+  assert {{ Γ ⊢s (Id,,M) ∘ σ ≈ (Id ∘ σ),,M[σ] : Δ, A }} by mauto 3.
   assert {{ Γ ⊢ M[σ] : A[Id][σ] }} by mauto.
   assert {{ Γ ⊢ A[Id][σ] ≈ A[Id∘σ] : Type@i }} by mauto.
   assert {{ Γ ⊢ M[σ] : A[Id∘σ] }} by mauto 4.
-  assert {{ Γ ⊢ M[σ] ≈ M[σ] : A[Id∘σ] }}...
+  enough {{ Γ ⊢ 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 : forall {Γ M A i σ Δ}, {{ Γ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ M : A }} -> {{ Γ ⊢s (σ∘Wk)∘(Id,,M) ≈ σ : Δ }}.
+Lemma sub_eq_sigma_compose_weak_id_extend : forall {Γ M A i σ Δ},
+    {{ Γ ⊢ A : Type@i }} ->
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Γ ⊢ M : A }} ->
+    {{ Γ ⊢s (σ ∘ Wk) ∘ (Id,,M) ≈ σ : Δ }}.
 Proof with mautosolve.
   intros.
   assert {{ Γ ⊢s Id,,M : Γ, A }} by mauto.
-  assert {{ Γ ⊢s (σ∘Wk)∘(Id,,M) ≈ σ∘(Wk∘(Id ,, M)) : Δ }} by mauto 4.
-  assert {{ Γ ⊢s Wk ∘ (Id,, M) ≈ Id : Γ }} by mauto.
-  assert {{ Γ ⊢s σ∘(Wk∘(Id ,, M)) ≈ σ∘Id : Δ }}...
+  assert {{ Γ ⊢s (σ ∘ Wk) ∘ (Id,,M) ≈ σ ∘ (Wk ∘ (Id,,M)) : Δ }} by mauto 4.
+  assert {{ Γ ⊢s Wk ∘ (Id,,M) ≈ Id : Γ }} by mauto.
+  enough {{ Γ ⊢s σ∘ (Wk∘ (Id,,M)) ≈ σ ∘ Id : Δ }} by mauto.
+  econstructor...
 Qed.
 
 #[export]
 Hint Resolve sub_eq_sigma_compose_weak_id_extend : mcltt.
 
-Lemma sub_eq_q_sigma_id_extend : forall Γ M A i σ Δ, {{ Δ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ M : A[σ] }} -> {{ Γ ⊢s q σ∘(Id,,M) ≈ σ,,M : Δ, A }}.
+Lemma sub_eq_q_sigma_id_extend : forall {Γ M A i σ Δ},
+    {{ Δ ⊢ A : Type@i }} ->
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Γ ⊢ M : A[σ] }} ->
+    {{ Γ ⊢s q σ ∘ (Id,,M) ≈ σ,,M : Δ, A }}.
 Proof with mautosolve 4.
   intros.
   assert {{ ⊢ Γ }} by mauto 3.
@@ -675,48 +894,55 @@ Proof with mautosolve 4.
   assert {{ Γ ⊢s Id,,M : Γ, A[σ] }} by mauto.
   assert {{ Γ, A[σ] ⊢s Wk : Γ }} by mauto.
   assert {{ Γ, A[σ] ⊢ #0 : A[σ][Wk] }} by mauto.
-  assert {{ Γ, A[σ] ⊢ #0 : A[σ∘Wk] }} by mauto 3.
-  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 {{ Γ, A[σ] ⊢ #0 : A[σ∘Wk] }} by (eapply wf_conv; mauto 3).
+  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 4.
   assert {{ Γ ⊢ #0[Id,,M] ≈ M : A[σ][Id] }} by mauto 3.
   assert {{ Γ ⊢ #0[Id,,M] ≈ M : A[σ] }} by mauto.
-  assert {{ Γ ⊢ #0[Id,,M] ≈ M : A[(σ∘Wk)∘(Id ,, M)] }}...
+  enough {{ Γ ⊢ #0[Id,,M] ≈ M : A[(σ ∘ Wk) ∘ (Id,,M)] }} by mauto.
+  eapply wf_exp_eq_conv...
 Qed.
 
 #[export]
 Hint Resolve sub_eq_q_sigma_id_extend : mcltt.
 #[export]
- Hint Rewrite -> sub_eq_q_sigma_id_extend using mauto 4 : mcltt.
+Hint Rewrite -> @sub_eq_q_sigma_id_extend using mauto 4 : mcltt.
 
-Lemma sub_eq_p_q_sigma : forall {Γ A i σ Δ}, {{ Δ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ, A[σ] ⊢s Wk∘q σ ≈ σ∘Wk : Δ }}.
+Lemma sub_eq_p_q_sigma : forall {Γ A i σ Δ},
+    {{ Δ ⊢ A : Type@i }} ->
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Γ, A[σ] ⊢s Wk ∘ q σ ≈ σ ∘ Wk : Δ }}.
 Proof with mautosolve 3.
   intros.
-  assert {{ ⊢ Γ }} by mauto 3.
   assert {{ Γ, A[σ] ⊢s Wk : Γ }} by mauto 4.
-  assert {{ Γ, A[σ] ⊢ #0 : A[σ][Wk] }} by mauto.
-  assert {{ Γ, A[σ] ⊢ #0 : A[σ∘Wk] }}...
+  assert {{ Γ, A[σ] ⊢ #0 : A[σ][Wk] }} by mauto 3.
+  enough {{ Γ, A[σ] ⊢ #0 : A[σ ∘ Wk] }} by mauto.
+  eapply wf_conv...
 Qed.
 
 #[export]
 Hint Resolve sub_eq_p_q_sigma : mcltt.
 
-Lemma sub_eq_p_q_sigma_nat : forall {Γ σ Δ}, {{ Γ ⊢s σ : Δ }} -> {{ Γ, ℕ ⊢s Wk∘q σ ≈ σ∘Wk : Δ }}.
+Lemma sub_eq_p_q_sigma_nat : forall {Γ σ Δ},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Γ, ℕ ⊢s Wk ∘ q σ ≈ σ ∘ Wk : Δ }}.
 Proof with mautosolve.
   intros.
-  assert {{ ⊢ Γ }} by mauto 3.
   assert {{ Γ, ℕ ⊢ #0 : ℕ }}...
 Qed.
 
 #[export]
 Hint Resolve sub_eq_p_q_sigma_nat : mcltt.
 
-Lemma sub_eq_p_p_q_q_sigma_nat : forall {Γ A i σ Δ}, {{ Δ, ℕ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ, ℕ, A[q σ] ⊢s Wk∘(Wk∘q (q σ)) ≈ (σ∘Wk)∘Wk : Δ }}.
+Lemma sub_eq_p_p_q_q_sigma_nat : forall {Γ A i σ Δ},
+    {{ Δ, ℕ ⊢ A : Type@i }} ->
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Γ, ℕ, A[q σ] ⊢s Wk ∘ (Wk ∘ q (q σ)) ≈ (σ ∘ Wk) ∘ Wk : Δ }}.
 Proof with mautosolve 3.
   intros.
-  assert {{ ⊢ Γ, ℕ }} by mauto 3.
   assert {{ Γ, ℕ ⊢ A[q σ] : Type@i }} by mauto.
-  assert {{ ⊢ Γ, ℕ, A[q σ] }} by mauto 2.
+  assert {{ ⊢ Γ, ℕ, A[q σ] }} by mauto 3.
   assert {{ ⊢ Δ, ℕ }} by mauto 3.
   assert {{ Γ, ℕ, A[q σ] ⊢s Wk∘q (q σ) ≈ q σ ∘ Wk : Δ, ℕ }} by mauto.
   assert {{ Γ, ℕ, A[q σ] ⊢s Wk∘(Wk∘q (q σ)) ≈ Wk ∘ (q σ ∘ Wk) : Δ }} by mauto 3.
@@ -724,34 +950,37 @@ Proof with mautosolve 3.
   assert {{ Γ, ℕ ⊢s q σ : Δ, ℕ }} by mauto.
   assert {{ Γ, ℕ, A[q σ] ⊢s Wk ∘ (q σ ∘ Wk) ≈ (Wk ∘ q σ) ∘ Wk : Δ }} by mauto 4.
   assert {{ Γ, ℕ ⊢s Wk ∘ q σ ≈ σ ∘ Wk : Δ }} by mauto.
-  assert {{ Γ, ℕ, A[q σ] ⊢s (Wk ∘ q σ) ∘ Wk ≈ (σ ∘ Wk) ∘ Wk : Δ }}...
+  enough {{ Γ, ℕ, 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 : forall {Γ A i σ Δ}, {{ Δ, ℕ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ, ℕ, A[q σ] ⊢s q σ∘(Wk∘Wk,,succ #1) ≈ (Wk∘Wk,,succ #1)∘q (q σ) : Δ, ℕ }}.
+Lemma sub_eq_q_sigma_compose_weak_weak_extend_succ_var_1 : forall {Γ A i σ Δ},
+    {{ Δ, ℕ ⊢ A : Type@i }} ->
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Γ, ℕ, A[q σ] ⊢s q σ ∘ ((Wk ∘ Wk),,succ #1) ≈ ((Wk ∘ Wk),,succ #1) ∘ q (q σ) : Δ, ℕ }}.
 Proof with mautosolve 4.
   intros.
-  assert {{ ⊢ Δ }} by mauto 3.
   assert {{ ⊢ Δ, ℕ, A }} by mauto 3.
   assert {{ ⊢ Γ, ℕ }} by mauto 3.
   assert {{ Γ, ℕ ⊢s Wk : Γ }} by mauto 3.
   assert {{ Γ, ℕ ⊢s σ∘Wk : Δ }} by mauto 3.
   assert {{ Γ, ℕ ⊢ A[q σ] : Type@i }} by mauto 3.
   set (Γ' := {{{ Γ, ℕ, A[q σ] }}}).
-  set (WkWksucc := {{{ Wk∘Wk ,, succ #1 }}}).
+  set (WkWksucc := {{{ (Wk∘Wk),,succ #1 }}}).
   assert {{ ⊢ Γ' }} by mauto 2.
   assert {{ Γ' ⊢s Wk∘Wk : Γ }} by mauto 4.
   assert {{ Γ' ⊢s WkWksucc : Γ, ℕ }} by mauto.
   assert {{ Γ, ℕ ⊢ #0 : ℕ }} by mauto.
-  assert {{ Γ' ⊢s q σ∘WkWksucc ≈ (σ∘Wk)∘WkWksucc ,, #0[WkWksucc] : Δ, ℕ }} by mautosolve 3.
+  assert {{ Γ' ⊢s q σ∘WkWksucc ≈ ((σ∘Wk)∘WkWksucc),,#0[WkWksucc] : Δ, ℕ }} by mautosolve 3.
   assert {{ Γ' ⊢ #1 : ℕ[Wk][Wk] }} by mauto.
   assert {{ Γ' ⊢ ℕ[Wk][Wk] ≈ ℕ : Type@0 }} by mauto 3.
   assert {{ Γ' ⊢ #1 : ℕ }} by mauto 2.
   assert {{ Γ' ⊢ succ #1 : ℕ }} by mauto.
   assert {{ Γ' ⊢s Wk∘WkWksucc : Γ }} by mauto 4.
-  assert {{ Γ' ⊢s Wk∘WkWksucc ≈ Wk∘Wk : Γ }} by mauto.
+  assert {{ Γ' ⊢s Wk∘WkWksucc ≈ Wk∘Wk : Γ }} by mauto 4.
+  assert {{ Γ ⊢s σ ≈ σ : Δ }} by mauto.
   assert {{ Γ' ⊢s σ∘(Wk∘WkWksucc) ≈ σ∘(Wk∘Wk) : Δ }} by mauto 3.
   assert {{ Γ' ⊢s (σ∘Wk)∘WkWksucc ≈ σ∘(Wk∘Wk) : Δ }} by mauto 3.
   assert {{ Γ' ⊢s σ∘(Wk∘Wk) ≈ (σ∘Wk)∘Wk : Δ }} by mauto 4.
@@ -768,30 +997,25 @@ Proof with mautosolve 4.
   assert {{ Γ' ⊢ succ #1 ≈ (succ #1)[q (q σ)] : ℕ }} by mauto 4.
   assert {{ Γ' ⊢ #0[WkWksucc] ≈ (succ #1)[q (q σ)] : ℕ }} by mauto 2.
   assert {{ Γ' ⊢s (σ∘Wk)∘WkWksucc : Δ }} by mauto 3.
-  assert {{ Γ' ⊢s (σ∘Wk)∘WkWksucc ,, #0[WkWksucc] ≈ (Wk∘Wk)∘q (q σ) ,, (succ #1)[q (q σ)] : Δ, ℕ }} by mauto 3.
+  assert {{ Γ' ⊢s ((σ∘Wk)∘WkWksucc),,#0[WkWksucc] ≈ ((Wk∘Wk)∘q (q σ)),,(succ #1)[q (q σ)] : Δ, ℕ }} by mauto 3.
   assert {{ Δ, ℕ, A ⊢ #1 : ℕ[Wk][Wk] }} by mauto 4.
-  assert {{ ⊢ Δ, ℕ }} by mauto 2.
-  assert {{ ⊢ Δ, ℕ, A }} by mauto 2.
   assert {{ Δ, ℕ, A ⊢ ℕ[Wk][Wk] ≈ ℕ : Type@0 }} by mauto 3.
-  assert {{ Δ, ℕ, A ⊢ #1 : ℕ }} by mauto 3.
   assert {{ Δ, ℕ, A ⊢ succ #1 : ℕ }} by mauto.
-  assert {{ Γ' ⊢s (Wk∘Wk)∘q (q σ) ,, (succ #1)[q (q σ)] ≈ WkWksucc∘q (q σ) : Δ, ℕ }}...
+  enough {{ Γ' ⊢s ((Wk∘Wk)∘q (q σ)),,(succ #1)[q (q σ)] ≈ WkWksucc∘q (q σ) : Δ, ℕ }}...
 Qed.
 
 #[export]
 Hint Resolve sub_eq_q_sigma_compose_weak_weak_extend_succ_var_1 : mcltt.
 
-Fact wf_subtyping_refl : forall {Γ A i},
+Fact wf_subtyp_refl : forall {Γ A i},
     {{ Γ ⊢ A : Type@i }} ->
     {{ Γ ⊢ A ⊆ A }}.
-Proof.
-  mauto.
-Qed.
+Proof. mauto. Qed.
 
 #[export]
-Hint Resolve wf_subtyping_refl : mcltt.
+Hint Resolve wf_subtyp_refl : mcltt.
 
-Lemma wf_subtyping_ge : forall {Γ i j},
+Lemma wf_subtyp_ge : forall {Γ i j},
     {{ ⊢ Γ }} ->
     i <= j ->
     {{ Γ ⊢ Type@i ⊆ Type@j }}.
@@ -800,47 +1024,50 @@ Proof.
 Qed.
 
 #[export]
-Hint Resolve wf_subtyping_ge : mcltt.
+Hint Resolve wf_subtyp_ge : mcltt.
 
-Lemma wf_subtyping_sub : forall Δ A A',
+Lemma wf_subtyp_sub : forall {Δ A A'},
     {{ Δ ⊢ A ⊆ A' }} ->
     forall Γ σ,
     {{ Γ ⊢s σ : Δ }} ->
     {{ Γ ⊢ A[σ] ⊆ A'[σ] }}.
 Proof.
   induction 1; intros; mauto 4.
-  - transitivity {{{ Type@i}}}; [mauto |].
-    transitivity {{{ Type@j}}}; [| mauto].
+  - transitivity {{{ Type@i }}}; [econstructor; mauto 4 |].
+    transitivity {{{ Type@j }}}; [| econstructor; mauto 4].
     mauto 3.
-  - transitivity {{{ Π (A[σ]) (B [ q σ ]) }}}; [ mauto |].
-    transitivity {{{ Π (A'[σ]) (B' [ q σ ]) }}}; [ | mauto].
+  - transitivity {{{ Π (A[σ]) (B[q σ]) }}}; [econstructor; mauto |].
+    transitivity {{{ Π (A'[σ]) (B'[q σ]) }}}; [ | econstructor; mauto 4].
     eapply wf_subtyp_pi with (i := i); mauto 4.
 Qed.
 
 #[export]
-Hint Resolve wf_subtyping_sub : mcltt.
-
+Hint Resolve wf_subtyp_sub : mcltt.
 
-Lemma wf_subtyp_univ_weaken : forall Γ i j A,
+Lemma wf_subtyp_univ_weaken : forall {Γ i j A},
     {{ Γ ⊢ Type@i ⊆ Type@j }} ->
-    {{ ⊢ Γ , A }} ->
-    {{ Γ , A ⊢ Type@i ⊆ Type@j }}.
+    {{ ⊢ Γ, A }} ->
+    {{ Γ, A ⊢ Type@i ⊆ Type@j }}.
 Proof.
   intros.
-  eapply wf_subtyping_sub with (σ := {{{ Wk }}}) in H.
-  - transitivity {{{ Type@i[Wk] }}}; [mauto |].
+  eapply wf_subtyp_sub with (σ := {{{ Wk }}}) in H.
+  - transitivity {{{ Type@i[Wk] }}}; [econstructor; mauto |].
     etransitivity; mauto.
   - mauto.
 Qed.
 
-
-Lemma ctx_sub_ctx_lookup : forall Γ Δ, {{ ⊢ Δ ⊆ Γ }} -> forall A x, {{ #x : A ∈ Γ }} -> exists B, {{ #x : B ∈ Δ }} /\ {{ Δ ⊢ B ⊆ A }}.
-Proof.
-  induction 1; intros; progressive_inversion.
-  dependent destruction H3.
-  - eexists; split; mauto.
-  - edestruct IHwf_ctx_sub as [? [? ?]]; try eassumption.
-    eexists; split; mauto.
+Lemma ctx_sub_ctx_lookup : forall {Γ Δ},
+    {{ ⊢ Δ ⊆ Γ }} ->
+    forall {A x},
+      {{ #x : A ∈ Γ }} ->
+      exists B,
+        {{ #x : B ∈ Δ }} /\
+          {{ Δ ⊢ B ⊆ A }}.
+Proof with (do 2 eexists; repeat split; mautosolve).
+  induction 1; intros * Hx; progressive_inversion.
+  dependent destruction Hx.
+  - idtac...
+  - edestruct IHwf_ctx_sub as [? []]; try eassumption...
 Qed.
 
 #[export]
diff --git a/theories/Core/Syntactic/SystemOpt.v b/theories/Core/Syntactic/SystemOpt.v
index 5f49fc6d..c1daad97 100644
--- a/theories/Core/Syntactic/SystemOpt.v
+++ b/theories/Core/Syntactic/SystemOpt.v
@@ -3,18 +3,85 @@ From Mcltt Require Import Base LibTactics.
 From Mcltt.Core Require Export CtxEq Presup System CoreTypeInversions.
 Import Syntax_Notations.
 
+Add Parametric Morphism i Γ : (wf_exp Γ)
+    with signature wf_exp_eq Γ {{{ Type@i }}} ==> eq ==> iff as wf_exp_morphism_iff3.
+Proof with mautosolve.
+  split; intros; gen_presups...
+Qed.
+
+Add Parametric Morphism i Γ : (wf_exp_eq Γ)
+    with signature wf_exp_eq Γ {{{ Type@i }}} ==> eq ==> eq ==> iff as wf_exp_eq_morphism_iff3.
+Proof with mautosolve.
+  split; intros; gen_presups...
+Qed.
+
+Add Parametric Morphism Γ i : (wf_subtyp Γ)
+    with signature (wf_exp_eq Γ {{{Type@i}}}) ==> eq ==> iff as wf_subtyp_morphism_iff1.
+Proof.
+  split; intros; gen_presups;
+    etransitivity; mauto 4.
+Qed.
+
+Add Parametric Morphism Γ j : (wf_subtyp Γ)
+    with signature eq ==> (wf_exp_eq Γ {{{Type@j}}}) ==> iff as wf_subtyp_morphism_iff2.
+Proof.
+  split; intros; gen_presups;
+    etransitivity; mauto 3.
+Qed.
+
 #[local]
 Ltac impl_opt_constructor :=
   intros;
   gen_presups;
   mautosolve 4.
 
+Corollary wf_subtyp_refl' : forall Γ M M' i,
+    {{ Γ ⊢ M ≈ M' : Type@i }} ->
+    {{ Γ ⊢ M ⊆ M' }}.
+Proof.
+  impl_opt_constructor.
+Qed.
+
+#[export]
+Hint Resolve wf_subtyp_refl' : mcltt.
+#[export]
+Remove Hints wf_subtyp_refl : mcltt.
+
+Corollary wf_conv' : forall Γ M A i A',
+    {{ Γ ⊢ M : A }} ->
+    {{ Γ ⊢ A ≈ A' : Type@i }} ->
+    {{ Γ ⊢ M : A' }}.
+Proof.
+  impl_opt_constructor.
+Qed.
+
+#[export]
+Hint Resolve wf_conv' : mcltt.
+#[export]
+Remove Hints wf_conv : mcltt.
+
+Corollary wf_exp_eq_conv' : forall Γ M M' A A' i,
+   {{ Γ ⊢ M ≈ M' : A }} ->
+   {{ Γ ⊢ A ≈ A' : Type@i }} ->
+   {{ Γ ⊢ M ≈ M' : A' }}.
+Proof.
+  impl_opt_constructor.
+Qed.
+
+#[export]
+Hint Resolve wf_exp_eq_conv' : mcltt.
+#[export]
+Remove Hints wf_exp_eq_conv : mcltt.
+
 Corollary wf_ctx_eq_extend' : forall {Γ Δ A A' i},
     {{ ⊢ Γ ≈ Δ }} ->
     {{ Γ ⊢ A ≈ A' : Type@i }} ->
     {{ ⊢ Γ , A ≈ Δ , A' }}.
 Proof.
-  impl_opt_constructor.
+  intros.
+  assert {{ Δ ⊢ A ≈ A' : Type@i }} by mauto.
+  gen_presups.
+  mautosolve 4.
 Qed.
 
 #[export]