diff --git a/theories/Core/Syntactic/CtxSub.v b/theories/Core/Syntactic/CtxSub.v
index e086a91..a042352 100644
--- a/theories/Core/Syntactic/CtxSub.v
+++ b/theories/Core/Syntactic/CtxSub.v
@@ -55,13 +55,21 @@ Module ctxsub_judg.
     5,6: inversion_clear HΓΔ; econstructor; mautosolve 4.
 
     (** eqrec related cases *)
-    1-3:assert {{ ⊢ Δ, B ⊆ Γ, B }} by mauto;
-      assert {{ Γ, B ⊢ B[Wk] : Type@i }} by mauto;
-      assert {{ Δ, B ⊢ B[Wk] : Type@i }} by mauto;
+    1-3: assert {{ ⊢ Δ, B ⊆ Γ, B }} by mauto;
+      assert {{ Γ, B ⊢s Wk : Γ }} by mauto 3;
+      assert {{ Γ, B ⊢ B[Wk] : Type@i }} by mauto 3;
+      assert {{ Γ, B, B[Wk] ⊢s Wk : Γ, B }} by mauto 4;
+      assert {{ Γ, B, B[Wk] ⊢s Wk∘Wk : Γ }} by mauto 3;
+      assert {{ Δ, B ⊢s Wk : Δ }} by mauto 3;
+      assert {{ Δ, B ⊢ B[Wk] : Type@i }} by mauto 3;
+      assert {{ Δ, B, B[Wk] ⊢s Wk : Δ, B }} by mauto 4;
+      assert {{ Δ, B, B[Wk] ⊢s Wk∘Wk : Δ }} by mauto 3;
+      assert {{ Δ, B, B[Wk] ⊢ B[Wk∘Wk] : Type@i }} by mauto 3;
+      assert {{ Δ, B, B[Wk] ⊢ B[Wk∘Wk] : Type@i }} by mauto 3;
       assert {{ ⊢ Δ, B, B[Wk] ⊆ Γ, B, B[Wk] }} by (econstructor; mauto 4);
-      assert {{ Γ, B, B[Wk] ⊢ Eq (B[Wk][Wk]) #1 #0 : Type@i }} by (econstructor; mauto 4);
-      assert {{ Δ, B, B[Wk] ⊢ Eq (B[Wk][Wk]) #1 #0 : Type@i }} by (econstructor; mauto 4);
-      assert {{ ⊢ Δ, B, B[Wk], Eq (B[Wk][Wk]) #1 #0 ⊆ Γ, B, B[Wk], Eq (B[Wk][Wk]) #1 #0 }} by mauto;
+      assert {{ Γ, B, B[Wk] ⊢ Eq B[Wk∘Wk] #1 #0 : Type@i }} by (econstructor; mauto 3; eapply wf_conv; mauto 4);
+      assert {{ Δ, B, B[Wk] ⊢ Eq B[Wk∘Wk] #1 #0 : Type@i }} by (econstructor; mauto 3; eapply wf_conv; mauto 4);
+      assert {{ ⊢ Δ, B, B[Wk], Eq B[Wk∘Wk] #1 #0 ⊆ Γ, B, B[Wk], Eq B[Wk∘Wk] #1 #0 }} by mauto 3;
       econstructor; mauto 2.
 
     - (** ctxsub_exp_eq_helper variable case *)
diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index 6b697d7..278cac8 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -3,6 +3,1286 @@ From Mcltt.Core Require Import Base.
 From Mcltt.Core.Syntactic Require Export CtxEq.
 Import Syntax_Notations.
 
+Lemma presup_exp_eq_natrec_cong_right : forall {Γ i A A' MZ' MS' M M'},
+    {{ Γ, ℕ ⊢ A : Type@i }} ->
+    {{ Γ, ℕ ⊢ A' : Type@i }} ->
+    {{ Γ, ℕ ⊢ A ≈ A' : Type@i }} ->
+    {{ Γ ⊢ MZ' : A[Id,,zero] }} ->
+    {{ Γ, ℕ, A ⊢ MS' : A[Wk∘Wk,,succ #1] }} ->
+    {{ Γ ⊢ M : ℕ }} ->
+    {{ Γ ⊢ M' : ℕ }} ->
+    {{ Γ ⊢ M ≈ M' : ℕ }} ->
+    {{ Γ ⊢ rec M' return A' | zero -> MZ' | succ -> MS' end : A[Id,,M] }}.
+Proof.
+  intros.
+  assert {{ ⊢ Γ }} by mauto 2.
+  assert {{ Γ ⊢s Id,,M : Γ, ℕ }} by mauto 3.
+  assert {{ Γ ⊢s Id,,M' : Γ, ℕ }} by mauto 3.
+  assert {{ Γ ⊢s Id,,M ≈ Id,,M' : Γ, ℕ }} by mauto 3.
+  assert {{ Γ ⊢ A[Id,,M] ≈ A'[Id,,M'] : Type@i }} by (transitivity {{{ A[Id,,M'] }}}; mauto 2).
+  assert {{ Γ ⊢s Id,,zero : Γ, ℕ }} by mauto 3.
+  assert {{ Γ ⊢ MZ' : A'[Id,,zero] }} by mauto 4.
+  assert {{ Γ, ℕ, A ⊢s Wk∘Wk,,succ #1 : Γ, ℕ }} by mauto 3.
+  assert {{ Γ, ℕ, A ⊢ MS' : A'[Wk∘Wk,,succ #1] }} by mauto 4.
+  assert {{ ⊢ Γ, ℕ, A ≈ Γ, ℕ, A' }} by mauto 4.
+  assert {{ Γ, ℕ, A' ⊢ MS' : A'[Wk∘Wk,,succ #1] }} by mauto 3.
+  eapply wf_conv; mauto 2.
+Qed.
+
+#[local]
+Hint Resolve presup_exp_eq_natrec_cong_right : mcltt.
+
+Lemma presup_exp_eq_natrec_sub_left : forall {Γ σ Δ i A MZ MS M},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Δ , ℕ ⊢ A : Type@i }} ->
+    {{ Δ ⊢ MZ : A[Id,,zero] }} ->
+    {{ Δ, ℕ, A ⊢ MS : A[Wk∘Wk,,succ #1] }} ->
+    {{ Δ ⊢ M : ℕ }} ->
+    {{ Γ ⊢ rec M return A | zero -> MZ | succ -> MS end[σ] : A[σ,,M[σ]] }}.
+Proof.
+  intros.
+  assert {{ ⊢ Δ }} by mauto 2.
+  assert {{ Γ ⊢s σ,,M[σ] : Δ, ℕ }} by mauto 3.
+  assert {{ Γ ⊢ A[σ,,M[σ]] : Type@i }} by mauto 2.
+  assert {{ Δ ⊢s Id,,M : Δ, ℕ }} by mauto 3.
+  assert {{ Γ ⊢s (Id,,M)∘σ ≈ σ,,M[σ] : Δ, ℕ }} by mauto 2.
+  assert {{ Γ ⊢ A[(Id,,M)∘σ] ≈ A[σ,,M[σ]] : Type@i }} by mauto 3.
+  assert {{ Γ ⊢ A[Id,,M][σ] ≈ A[σ,,M[σ]] : Type@i }} by mauto 3.
+  eapply wf_conv; mauto 3.
+Qed.
+
+#[local]
+Hint Resolve presup_exp_eq_natrec_sub_left : mcltt.
+
+Lemma presup_exp_eq_natrec_sub_right : forall {Γ σ Δ i A MZ MS M},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Δ , ℕ ⊢ A : Type@i }} ->
+    {{ Δ ⊢ MZ : A[Id,,zero] }} ->
+    {{ Δ, ℕ, A ⊢ MS : A[Wk∘Wk,,succ #1] }} ->
+    {{ Δ ⊢ M : ℕ }} ->
+    {{ Γ ⊢ rec M[σ] return A[q σ] | zero -> MZ[σ] | succ -> MS[q (q σ)] end : A[σ,,M[σ]] }}.
+Proof.
+  intros.
+  assert {{ ⊢ Γ }} by mauto 2.
+  assert {{ ⊢ Δ }} by mauto 2.
+  assert {{ Γ, ℕ ⊢s q σ : Δ, ℕ }} by mauto 2.
+  assert {{ Γ, ℕ, A[q σ] ⊢s q (q σ) : Δ, ℕ, A }} by mauto 2.
+  assert {{ Γ, ℕ ⊢ A[q σ] : Type@i }} by mauto 3.
+  (* Possible lemma? *)
+  assert (forall N, {{ Γ ⊢ N : ℕ }} -> {{ Γ ⊢ A[q σ][Id,,N] : Type@i }} /\ {{ Γ ⊢ A[q σ][Id,,N] ≈ A[σ,,N] : Type@i }}).
+  {
+    intros.
+    assert {{ Γ ⊢ N : ℕ[σ] }} by mauto 3.
+    assert {{ Γ ⊢s Id,,N : Γ, ℕ }} by mauto 3.
+    assert {{ Γ ⊢s q σ∘(Id,,N) ≈ σ,,N : Δ, ℕ }} by mauto 3.
+    assert {{ Γ ⊢s σ,,N : Δ, ℕ }} by mauto 2.
+    assert {{ Γ ⊢ A[q σ∘(Id,,N)] ≈ A[σ,,N] : Type@i }} by mauto 3.
+    split; mauto 3.
+  }
+  (* Assertion for M *)
+  assert {{ Γ ⊢ M[σ] : ℕ }} by mauto 3.
+  (* Assertion for type *)
+  assert ({{ Γ ⊢ A[q σ][Id,,M[σ]] : Type@i }} /\ {{ Γ ⊢ A[q σ][Id,,M[σ]] ≈ A[σ,,M[σ]] : Type@i }}) as [] by mauto 3.
+  (* Assertion for MZ *)
+  assert {{ Δ ⊢ zero : ℕ }} by mauto 2.
+  assert {{ Δ ⊢s Id,,zero : Δ, ℕ }} by mauto 2.
+  assert {{ Γ ⊢ zero[σ] ≈ zero : ℕ }} by mauto 2.
+  assert {{ Γ ⊢s σ,,zero[σ] ≈ σ,,zero : Δ, ℕ }} by mauto 3.
+  assert {{ Γ ⊢s (Id,,zero)∘σ ≈ σ,,zero : Δ, ℕ }} by mauto 3.
+  assert ({{ Γ ⊢ A[q σ][Id,,zero] : Type@i }} /\ {{ Γ ⊢ A[q σ][Id,,zero] ≈ A[σ,,zero] : Type@i }}) as [] by mauto 3.
+  assert {{ Γ ⊢ A[(Id,,zero)∘σ] ≈ A[σ,,zero] : Type@i }} by mauto 3.
+  assert {{ Γ ⊢ A[q σ][Id,,zero] ≈ A[Id,,zero][σ] : Type@i }} by (etransitivity; [| symmetry]; mauto 3).
+  assert {{ Γ ⊢ MZ[σ] : A[q σ][Id,,zero] }} by mauto 4.
+  (* Assertion for MS *)
+  assert {{ Δ, ℕ, A ⊢s Wk∘Wk,,succ #1 : Δ, ℕ }} by mauto 2.
+  assert {{ Γ, ℕ, A[q σ] ⊢s Wk∘Wk,,succ #1 : Γ, ℕ }} by mauto 2.
+  assert {{ Γ, ℕ, A[q σ] ⊢s q σ∘(Wk∘Wk,,succ #1) ≈ (Wk∘Wk,,succ #1)∘q (q σ) : Δ, ℕ }} by mauto 2.
+  assert {{ Γ, ℕ, A[q σ] ⊢ A[q σ][Wk∘Wk,,succ #1] ≈ A[Wk∘Wk,,succ #1][q (q σ)] : Type@i }} by mauto 2.
+  assert {{ Γ, ℕ, A[q σ] ⊢ MS[q (q σ)] : A[q σ][Wk∘Wk,,succ #1] }} by (eapply wf_conv; mauto 2).
+  (* Final *)
+  eapply wf_conv; mauto 3.
+Qed.
+
+#[local]
+Hint Resolve presup_exp_eq_natrec_sub_right : mcltt.
+
+Lemma presup_exp_eq_beta_succ_right : forall {Γ i A MZ MS M},
+    {{ Γ, ℕ ⊢ A : Type@i }} ->
+    {{ Γ ⊢ MZ : A[Id,,zero] }} ->
+    {{ Γ, ℕ, A ⊢ MS : A[Wk∘Wk,,succ #1] }} ->
+    {{ Γ ⊢ M : ℕ }} ->
+    {{ Γ ⊢ MS[Id,,M,,rec M return A | zero -> MZ | succ -> MS end] : A[Id,,succ M] }}.
+Proof.
+  intros.
+  set (WkWksucc := {{{ Wk∘Wk,,succ #1 }}}).
+  set (recM := {{{ rec M return A | zero -> MZ | succ -> MS end }}}).
+  set (IdMrecM := {{{ Id,,M,,recM }}}).
+  assert {{ ⊢ Γ }} by mauto 2.
+  (* Assertion for type *)
+  assert {{ Γ ⊢ ℕ : Type@0 }} by mauto 3.
+  assert {{ Γ ⊢ recM : A[Id,,M] }} by mauto 4.
+  assert {{ Γ, ℕ ⊢s Wk : Γ }} by mauto 3.
+  assert {{ Γ, ℕ, A ⊢s Wk : Γ, ℕ }} by mauto 3.
+  assert {{ Γ, ℕ, A ⊢s Wk∘Wk : Γ }} by mauto 2.
+  assert {{ Γ ⊢s WkWksucc∘IdMrecM ≈ (Wk∘Wk)∘IdMrecM,,(succ #1)[IdMrecM] : Γ, ℕ }}
+    by (eapply sub_eq_extend_compose_nat; mauto 3).
+  assert {{ Γ ⊢s IdMrecM : Γ, ℕ, A }} by mauto 3.
+  assert {{ Γ ⊢s (Wk∘Wk)∘IdMrecM : Γ }} by mauto 2.
+  assert {{ Γ ⊢s (Wk∘Wk)∘IdMrecM ≈ Wk∘(Wk∘IdMrecM) : Γ }} by mauto 2.
+  assert {{ Γ ⊢s Id,,M : Γ, ℕ }} by mauto 2.
+  assert {{ Γ ⊢s Wk∘(Wk∘IdMrecM) ≈ Wk∘(Id,,M) : Γ }} by mauto 4.
+  assert {{ Γ ⊢s (Wk∘Wk)∘IdMrecM ≈ Id : Γ }} by mauto 4.
+  assert {{ Γ ⊢ #1[IdMrecM] ≈ #0[Id,,M] : ℕ }} by mauto 3.
+  assert {{ Γ ⊢ #1[IdMrecM] ≈ M : ℕ }} by mauto 4.
+  assert {{ Γ ⊢ succ #1[IdMrecM] ≈ succ M : ℕ }} by mauto 2.
+  assert {{ Γ ⊢ (succ #1)[IdMrecM] ≈ succ M : ℕ }} by mauto 4.
+  assert {{ Γ ⊢s (Wk∘Wk)∘IdMrecM,,(succ #1)[IdMrecM] ≈ Id,,succ M : Γ , ℕ }} by mauto 2.
+  assert {{ Γ ⊢s WkWksucc∘IdMrecM : Γ, ℕ }} by mauto 3.
+  assert {{ Γ ⊢s Id,,succ M : Γ, ℕ }} by mauto 3.
+  assert {{ Γ ⊢s WkWksucc∘IdMrecM ≈ Id,,succ M : Γ , ℕ }} by mauto 2.
+  assert {{ Γ ⊢ A[WkWksucc∘IdMrecM] ≈ A[Id,,succ M] : Type@i }} by mauto 2.
+  enough {{ Γ ⊢ A[WkWksucc][IdMrecM] ≈ A[Id,,succ M] : Type@i }}; mauto 4.
+Qed.
+
+#[local]
+Hint Resolve presup_exp_eq_beta_succ_right : mcltt.
+
+Lemma presup_exp_eq_fn_cong_right : forall {Γ i A A' j B M'},
+    {{ Γ ⊢ A : Type@i }} ->
+    {{ Γ ⊢ A' : Type@i }} ->
+    {{ Γ ⊢ A ≈ A' : Type@i }} ->
+    {{ Γ, A ⊢ B : Type@j }} ->
+    {{ Γ , A ⊢ M' : B }} ->
+    {{ Γ ⊢ λ A' M' : Π A B }}.
+Proof.
+  intros.
+  assert {{ ⊢ Γ }} by mauto 2.
+  assert {{ Γ ⊢ A : Type@(max i j) }} by mauto 2 using lift_exp_max_left.
+  assert {{ Γ ⊢ A ≈ A' : Type@(max i j) }} by mauto 2 using lift_exp_eq_max_left.
+  assert {{ Γ, A ⊢ B : Type@(max i j) }} by mauto 2 using lift_exp_max_right.
+  assert {{ Γ ⊢ Π A B ≈ Π A' B : Type@(max i j) }} by mauto 3.
+  assert {{ Γ, A' ⊢ M' : B }} by mauto 4.
+  assert {{ Γ ⊢ Π A B : Type@(max i j) }} by mauto 2.
+  enough {{ Γ ⊢ λ A' M' : Π A' B }}; mauto 3.
+Qed.
+
+#[local]
+Hint Resolve presup_exp_eq_fn_cong_right : mcltt.
+
+Lemma presup_exp_eq_fn_sub_right : forall {Γ σ Δ i A j B M},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Δ ⊢ A : Type@i }} ->
+    {{ Δ, A ⊢ B : Type@j }} ->
+    {{ Δ, A ⊢ M : B }} ->
+    {{ Γ ⊢ λ A[σ] M[q σ] : (Π A B)[σ] }}.
+Proof.
+  intros.
+  assert {{ Δ ⊢ A : Type@(max i j) }} by mauto 2 using lift_exp_max_left.
+  assert {{ Δ, A ⊢ B : Type@(max i j) }} by mauto 2 using lift_exp_max_right.
+  assert {{ Γ ⊢ A[σ] : Type@(max i j) }} by mauto 2.
+  assert {{ Γ, A[σ] ⊢ B[q σ] : Type@(max i j) }} by mauto 3.
+  assert {{ Γ ⊢ Π A[σ] B[q σ] : Type@(max i j) }} by mauto 2.
+  assert {{ Γ ⊢ Π A[σ] B[q σ] ≈ Π A[σ] B[q σ] : Type@(max i j) }} by mauto 2.
+  assert {{ Γ, A[σ] ⊢ M[q σ] : B[q σ] }} by mauto 3.
+  assert {{ Γ ⊢ λ A[σ] M[q σ] : Π A[σ] B[q σ] }} by mauto 3.
+  eapply wf_conv; mauto 3.
+Qed.
+
+#[local]
+Hint Resolve presup_exp_eq_fn_sub_right : mcltt.
+
+Lemma presup_exp_eq_app_cong_right : forall {Γ i A B M' N N'},
+    {{ Γ ⊢ A : Type@i }} ->
+    {{ Γ , A ⊢ B : Type@i }} ->
+    {{ Γ ⊢ M' : Π A B }} ->
+    {{ Γ ⊢ N : A }} ->
+    {{ Γ ⊢ N' : A }} ->
+    {{ Γ ⊢ N ≈ N' : A }} ->
+    {{ Γ ⊢ M' N' : B[Id,,N] }}.
+Proof.
+  intros.
+  assert {{ ⊢ Γ }} by mauto 2.
+  assert {{ Γ ⊢s Id ≈ Id : Γ }} by mauto 2.
+  assert {{ Γ ⊢ A ≈ A[Id] : Type@i }} by mauto 3.
+  assert {{ Γ ⊢ N ≈ N' : A[Id] }} by mauto 2.
+  assert {{ Γ ⊢s Id,,N ≈ Id,,N' : Γ, A }} by mauto 2.
+  assert {{ Γ ⊢ B[Id,,N] ≈ B[Id,,N'] : Type@i }} by mauto 3.
+  eapply wf_conv; mauto 3.
+Qed.
+
+#[local]
+Hint Resolve presup_exp_eq_app_cong_right : mcltt.
+
+Lemma presup_exp_eq_app_sub_left : forall {Γ σ Δ i A B M N},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Δ ⊢ A : Type@i }} ->
+    {{ Δ , A ⊢ B : Type@i }} ->
+    {{ Δ ⊢ M : Π A B }} ->
+    {{ Δ ⊢ N : A }} ->
+    {{ Γ ⊢ (M N)[σ] : B[σ,,N[σ]] }}.
+Proof.
+  intros.
+  assert {{ ⊢ Δ }} by mauto 2.
+  assert {{ Γ, A[σ] ⊢s q σ : Δ, A }} by mauto 2.
+  assert {{ Γ ⊢ M[σ] : (Π A B)[σ] }} by mauto 3.
+  assert {{ Γ ⊢ Π A[σ] B[q σ] : Type@i }} by mauto 4.
+  assert {{ Γ ⊢ M[σ] : Π A[σ] B[q σ] }} by mauto 3.
+  assert {{ Δ ⊢ N : A[Id] }} by mauto 2.
+  assert {{ Γ ⊢s (Id,,N)∘σ ≈ Id∘σ,,N[σ] : Δ, A }} by mauto 3.
+  assert {{ Γ ⊢s (Id,,N)∘σ ≈ σ,,N[σ] : Δ, A }} by mauto 3.
+  assert {{ Δ ⊢s Id,,N : Δ, A }} by mauto 3.
+  assert {{ Γ ⊢s (Id,,N)∘σ : Δ, A }} by mauto 3.
+  assert {{ Γ ⊢ B[(Id,,N)∘σ] ≈ B[σ,,N[σ]] : Type@i }} by mauto 2.
+  assert {{ Γ ⊢s σ,,N[σ] : Δ, A }} by mauto 3.
+  assert {{ Γ ⊢ B[σ,,N[σ]] : Type@i }} by mauto 2.
+  assert {{ Γ ⊢ B[Id,,N][σ] ≈ B[σ,,N[σ]] : Type@i }} by mauto 3.
+  eapply wf_conv; mauto 3.
+Qed.
+
+#[local]
+Hint Resolve presup_exp_eq_app_sub_left : mcltt.
+
+Lemma presup_exp_eq_app_sub_right : forall {Γ σ Δ i A B M N},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Δ ⊢ A : Type@i }} ->
+    {{ Δ , A ⊢ B : Type@i }} ->
+    {{ Δ ⊢ M : Π A B }} ->
+    {{ Δ ⊢ N : A }} ->
+    {{ Γ ⊢ M[σ] N[σ] : B[σ,,N[σ]] }}.
+Proof.
+  intros.
+  assert {{ Γ ⊢ A[σ] : Type@i }} by mauto 3.
+  assert {{ Γ, A[σ] ⊢s q σ : Δ, A }} by mauto 2.
+  assert {{ Γ, A[σ] ⊢ B[q σ] : Type@i }} by mauto 2.
+  assert {{ Γ ⊢ M[σ] : Π A[σ] B[q σ] }} by (eapply wf_conv; mauto 2).
+  assert {{ Γ ⊢ N[σ] : A[σ] }} by mauto 2.
+  assert {{ Γ ⊢s q σ∘(Id,,N[σ]) ≈ σ,,N[σ] : Δ, A }} by mauto 2.
+  assert {{ Γ ⊢s Id,,N[σ] : Γ, A[σ] }} by mauto 2.
+  assert {{ Γ ⊢s q σ∘(Id,,N[σ]) : Δ, A }} by mauto 2.
+  assert {{ Γ ⊢ B[q σ∘(Id,,N[σ])] ≈ B[σ,,N[σ]] : Type@i }} by mauto 2.
+  assert {{ Γ ⊢ B[q σ][Id,,N[σ]] : Type@i }} by mauto 2.
+  assert {{ Γ ⊢ B[q σ][Id,,N[σ]] ≈ B[σ,,N[σ]] : Type@i }} by mauto 3.
+  eapply wf_conv; mauto 3.
+Qed.
+
+#[local]
+Hint Resolve presup_exp_eq_app_sub_right : mcltt.
+
+Lemma presup_exp_eq_pi_eta_right : forall {Γ i A B M},
+    {{ Γ ⊢ A : Type@i }} ->
+    {{ Γ , A ⊢ B : Type@i }} ->
+    {{ Γ ⊢ M : Π A B }} ->
+    {{ Γ ⊢ λ A (M[Wk] #0) : Π A B }}.
+Proof.
+  intros.
+  assert {{ Γ, A ⊢s Wk : Γ }} by mauto 3.
+  assert {{ Γ, A, A[Wk] ⊢s q Wk : Γ, A }} by mauto 3.
+  assert {{ Γ, A ⊢ A[Wk] : Type@i }} by mauto 2.
+  assert {{ Γ, A, A[Wk] ⊢ B[q Wk] : Type@i }} by mauto 3.
+  assert {{ Γ, A ⊢ M[Wk] : Π A[Wk] B[q Wk] }} by (eapply wf_conv; mauto 3).
+  assert {{ Γ, A ⊢ #0 : A[Wk] }} by mauto 3.
+  assert {{ Γ, A ⊢s q Wk∘(Id,,#0) ≈ Id : Γ, A }} by mauto 4.
+  assert {{ Γ, A ⊢s Id,,#0 : Γ, A, A[Wk] }} by mauto 2.
+  assert {{ Γ, A ⊢ B[q Wk][Id,,#0] ≈ B[Id] : Type@i }} by (transitivity {{{ B[q Wk∘(Id,,#0)] }}}; mauto 3).
+  econstructor; mauto 3.
+  eapply wf_conv; mauto 3.
+Qed.
+
+#[local]
+Hint Resolve presup_exp_eq_pi_eta_right : mcltt.
+
+Lemma presup_exp_eq_prop_eq_var0 : forall {Γ i A},
+  {{ Γ ⊢ A : Type@i }} ->
+  {{ Γ, A, A[Wk] ⊢ #0 : A[Wk∘Wk] }}.
+Proof.
+  intros.
+  assert {{ ⊢ Γ, A }} by mauto 3.
+  assert {{ Γ, A ⊢s Wk : Γ }} by mauto 2.
+  assert {{ ⊢ Γ, A, A[Wk] }} by mauto 3.
+  mauto 3.
+Qed.
+
+#[export]
+Hint Resolve presup_exp_eq_prop_eq_var0 : mcltt.
+
+Lemma presup_exp_eq_prop_eq_var1 : forall {Γ i A},
+  {{ Γ ⊢ A : Type@i }} ->
+  {{ Γ, A, A[Wk] ⊢ #1 : A[Wk∘Wk] }}.
+Proof.
+  intros.
+  assert {{ ⊢ Γ, A }} by mauto 3.
+  assert {{ Γ, A ⊢s Wk : Γ }} by mauto 2.
+  assert {{ ⊢ Γ, A, A[Wk] }} by mauto 3.
+  mauto 4.
+Qed.
+
+#[export]
+Hint Resolve presup_exp_eq_prop_eq_var1 : mcltt.
+
+Lemma presup_exp_eq_prop_eq_wf : forall {Γ i A},
+  {{ Γ ⊢ A : Type@i }} ->
+  {{ Γ, A, A[Wk] ⊢ Eq A[Wk∘Wk] #1 #0 : Type@i }}.
+Proof.
+  intros.
+  assert {{ ⊢ Γ, A }} by mauto 3.
+  assert {{ Γ, A ⊢s Wk : Γ }} by mauto 2.
+  assert {{ ⊢ Γ, A, A[Wk] }} by mauto 3.
+  assert {{ Γ, A, A[Wk] ⊢s Wk∘Wk : Γ }} by mauto 3.
+  assert {{ Γ, A, A[Wk] ⊢ A[Wk∘Wk] : Type@i }} by mauto 3.
+  mauto 4.
+Qed.
+
+#[export]
+Hint Resolve presup_exp_eq_prop_eq_wf : mcltt.
+
+Lemma presup_exp_eq_prop_eq_sub_helper2 : forall {Γ σ Δ i A M1 M2},
+  {{ Γ ⊢s σ : Δ }} ->
+  {{ Δ ⊢ A : Type@i }} ->
+  {{ Δ ⊢ M1 : A }} ->
+  {{ Δ ⊢ M2 : A }} ->
+  {{ Γ ⊢s σ,,M1[σ],,M2[σ] : Δ, A, A[Wk] }}.
+Proof.
+  intros.
+  assert {{ ⊢ Δ, A }} by mauto 3.
+  assert {{ Δ, A ⊢s Wk : Δ }} by mauto 2.
+  assert {{ Γ ⊢s σ,,M1[σ] : Δ, A }} by mauto 3.
+  assert {{ Γ ⊢ A[Wk][σ,,M1[σ]] ≈ A[σ] : Type@i }} by mauto 3.
+  assert {{ Γ ⊢ M2[σ] : A[σ] }} by mauto 2.
+  assert {{ Γ ⊢ A[Wk][σ,,M1[σ]] : Type@i }} by mauto 3.
+  assert {{ Γ ⊢ M2[σ] : A[Wk][σ,,M1[σ]] }} by mauto 3.
+  mauto 4.
+Qed.
+
+#[export]
+Hint Resolve presup_exp_eq_prop_eq_sub_helper2 : mcltt.
+
+Lemma presup_exp_eq_prop_eq_typ_sub2_eq : forall {Γ σ Δ i A M1 M2},
+  {{ Γ ⊢s σ : Δ }} ->
+  {{ Δ ⊢ A : Type@i }} ->
+  {{ Δ ⊢ M1 : A }} ->
+  {{ Δ ⊢ M2 : A }} ->
+  {{ Γ ⊢ (Eq A[Wk∘Wk] #1 #0)[σ,,M1[σ],,M2[σ]] ≈ (Eq A M1 M2)[σ] : Type@i }}.
+Proof.
+  intros.
+  assert {{ ⊢ Δ, A }} by mauto 3.
+  assert {{ Δ, A ⊢s Wk : Δ }} by mauto 2.
+  assert {{ Γ ⊢ M1[σ] : A[σ] }} by mauto 2.
+  assert {{ Γ ⊢s σ,,M1[σ] : Δ, A }} by mauto 2.
+  assert {{ Δ, A ⊢ A[Wk] : Type@i }} by mauto 2.
+  assert {{ Γ ⊢ A[Wk][σ,,M1[σ]] : Type@i }} by mauto 3.
+  assert {{ Γ ⊢ A[Wk][σ,,M1[σ]] ≈ A[σ] : Type@i }} by mauto 2.
+  assert {{ Γ ⊢ M2[σ] : A[σ] }} by mauto 2.
+  assert {{ Γ ⊢ M2[σ] : A[Wk][σ,,M1[σ]] }} by mauto 3.
+  assert {{ Γ ⊢s σ,,M1[σ],,M2[σ] : Δ, A, A[Wk] }} by mauto 2.
+  assert {{ Δ, A, A[Wk] ⊢s Wk∘Wk : Δ }} by mauto 4.
+  assert {{ Δ, A, A[Wk] ⊢ A[Wk∘Wk] : Type@i }} by mauto 2.
+  assert {{ Γ ⊢ A[Wk∘Wk][σ,,M1[σ],,M2[σ]] : Type@i }} by mauto 2.
+  enough {{ Γ ⊢ Eq A[Wk∘Wk][σ,,M1[σ],,M2[σ]] #1[σ,,M1[σ],,M2[σ]] #0[σ,,M1[σ],,M2[σ]] ≈ Eq A[σ] M1[σ] M2[σ] : Type@i }}
+    by (etransitivity; [| etransitivity]; [| eassumption |]; econstructor; mauto 2).
+  assert {{ Γ ⊢ A[σ] : Type@i }} by mauto 2.
+  econstructor; mauto 2; eapply wf_exp_eq_conv; mauto 4 using sub_lookup_var0, sub_lookup_var1.
+Qed.
+
+#[export]
+Hint Resolve presup_exp_eq_prop_eq_typ_sub2_eq : mcltt.
+
+Lemma presup_exp_eq_prop_eq_sub_helper3 : forall {Γ σ Δ i A M1 M2 N},
+  {{ Γ ⊢s σ : Δ }} ->
+  {{ Δ ⊢ A : Type@i }} ->
+  {{ Δ ⊢ M1 : A }} ->
+  {{ Δ ⊢ M2 : A }} ->
+  {{ Δ ⊢ N : Eq A M1 M2 }} ->
+  {{ Γ ⊢s σ,,M1[σ],,M2[σ],,N[σ] : Δ, A, A[Wk], Eq A[Wk∘Wk] #1 #0 }}.
+Proof.
+  intros.
+  assert {{ Γ ⊢s σ,,M1[σ],,M2[σ] : Δ, A, A[Wk] }} by mauto 3.
+  assert {{ Δ, A, A[Wk] ⊢ Eq A[Wk∘Wk] #1 #0 : Type@i }} by mauto 2.
+  assert {{ Γ ⊢ (Eq A[Wk∘Wk] #1 #0)[σ,,M1[σ],,M2[σ]] : Type@i }} by mauto 2.
+  assert {{ Γ ⊢ N[σ] : (Eq A[Wk∘Wk] #1 #0)[σ,,M1[σ],,M2[σ]] }} by (eapply wf_conv; mauto 3).
+  mauto 3.
+Qed.
+
+#[export]
+Hint Resolve presup_exp_eq_prop_eq_sub_helper3 : mcltt.
+
+Lemma presup_exp_eq_prop_eq_id_sub_helper2 : forall {Γ i A M1 M2},
+  {{ Γ ⊢ A : Type@i }} ->
+  {{ Γ ⊢ M1 : A }} ->
+  {{ Γ ⊢ M2 : A }} ->
+  {{ Γ ⊢s Id,,M1,,M2 : Γ, A, A[Wk] }}.
+Proof.
+  intros.
+  assert {{ ⊢ Γ }} by mauto 2.
+  assert {{ Γ ⊢s Id : Γ }} by mauto 2.
+  assert {{ Γ ⊢s Id,,M1 : Γ, A }} by mauto 2.
+  assert {{ ⊢ Γ, A }} by mauto 3.
+  assert {{ Γ, A ⊢ A[Wk] : Type@i }} by mauto 3.
+  assert {{ Γ ⊢ A[Wk][Id,,M1] : Type@i }} by mauto 2.
+  assert {{ Γ ⊢ A[Wk][Id,,M1] ≈ A : Type@i }} by mauto 2.
+  assert {{ Γ ⊢ M2 : A[Wk][Id,,M1] }} by mauto 3.
+  mauto 2.
+Qed.
+
+#[export]
+Hint Resolve presup_exp_eq_prop_eq_id_sub_helper2 : mcltt.
+
+Lemma presup_exp_eq_prop_eq_typ_id_sub2_eq : forall {Γ i A M1 M2},
+  {{ Γ ⊢ A : Type@i }} ->
+  {{ Γ ⊢ M1 : A }} ->
+  {{ Γ ⊢ M2 : A }} ->
+  {{ Γ ⊢ (Eq A[Wk∘Wk] #1 #0)[Id,,M1,,M2] ≈ Eq A M1 M2 : Type@i }}.
+Proof.
+  intros.
+  assert {{ ⊢ Γ, A }} by mauto 3.
+  assert {{ Γ, A ⊢s Wk : Γ }} by mauto 2.
+  assert {{ Γ ⊢s Id,,M1 : Γ, A }} by mauto 2.
+  assert {{ Γ, A ⊢ A[Wk] : Type@i }} by mauto 2.
+  assert {{ Γ ⊢ A[Wk][Id,,M1] : Type@i }} by mauto 3.
+  assert {{ Γ ⊢ A[Wk][Id,,M1] ≈ A : Type@i }} by mauto 2.
+  assert {{ Γ ⊢ M2 : A[Wk][Id,,M1] }} by mauto 3.
+  assert {{ Γ ⊢s Id,,M1,,M2 : Γ, A, A[Wk] }} by mauto 2.
+  assert {{ Γ, A, A[Wk] ⊢s Wk∘Wk : Γ }} by mauto 4.
+  assert {{ Γ, A, A[Wk] ⊢ A[Wk∘Wk] : Type@i }} by mauto 2.
+  assert {{ Γ ⊢ A[Wk∘Wk][Id,,M1,,M2] : Type@i }} by mauto 2.
+  transitivity {{{ Eq A[Wk∘Wk][Id,,M1,,M2] #1[Id,,M1,,M2] #0[Id,,M1,,M2] }}}; [econstructor; mautosolve 2 |].
+  econstructor; mauto 2; eapply wf_exp_eq_conv; mauto 4 using id_sub_lookup_var0, id_sub_lookup_var1.
+Qed.
+
+#[export]
+Hint Resolve presup_exp_eq_prop_eq_typ_id_sub2_eq : mcltt.
+
+Lemma presup_exp_eq_prop_eq_id_sub_helper3 : forall {Γ i A M1 M2 N},
+  {{ Γ ⊢ A : Type@i }} ->
+  {{ Γ ⊢ M1 : A }} ->
+  {{ Γ ⊢ M2 : A }} ->
+  {{ Γ ⊢ N : Eq A M1 M2 }} ->
+  {{ Γ ⊢s Id,,M1,,M2,,N : Γ, A, A[Wk], Eq A[Wk∘Wk] #1 #0 }}.
+Proof.
+  intros.
+  assert {{ Γ ⊢s Id,,M1,,M2 : Γ, A, A[Wk] }} by mauto 3.
+  assert {{ Γ, A, A[Wk] ⊢ Eq A[Wk∘Wk] #1 #0 : Type@i }} by mauto 2.
+  assert {{ Γ ⊢ (Eq A[Wk∘Wk] #1 #0)[Id,,M1,,M2] : Type@i }} by mauto 2.
+  assert {{ Γ ⊢ N : (Eq A[Wk∘Wk] #1 #0)[Id,,M1,,M2] }} by (eapply wf_conv; mauto 3).
+  mauto 3.
+Qed.
+
+#[export]
+Hint Resolve presup_exp_eq_prop_eq_id_sub_helper3 : mcltt.
+
+Lemma presup_exp_eq_refl_sub_right : forall {Γ σ Δ i A M},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Δ ⊢ A : Type@i }} ->
+    {{ Δ ⊢ M : A }} ->
+    {{ Γ ⊢ refl A[σ] M[σ] : (Eq A M M)[σ] }}.
+Proof.
+  intros.
+  assert {{ ⊢ Δ }} by mauto 2.
+  assert {{ Γ ⊢ A[σ] : Type@i }} by mauto 2.
+  assert {{ Γ ⊢ M[σ] : A[σ] }} by mauto 2.
+  assert {{ Γ ⊢ (Eq A M M)[σ] : Type@i }} by mauto 3.
+  assert {{ Γ ⊢ (Eq A M M)[σ] ≈ Eq A[σ] M[σ] M[σ] : Type@i }} by mauto 3.
+  eapply wf_conv; mauto 2.
+Qed.
+
+#[local]
+Hint Resolve presup_exp_eq_refl_sub_right : mcltt.
+
+Lemma presup_exp_eq_eqrec_sub_left : forall {Γ σ Δ i A M1 M2 j B N BR},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Δ ⊢ A : Type@i }} ->
+    {{ Δ ⊢ M1 : A }} ->
+    {{ Δ ⊢ M2 : A }} ->
+    {{ Δ, A, A[Wk], Eq A[Wk∘Wk] #1 #0 ⊢ B : Type@j }} ->
+    {{ Δ, A ⊢ BR : B[Id,,#0,,refl A[Wk] #0] }} ->
+    {{ Δ ⊢ N : Eq A M1 M2 }} ->
+    {{ Γ ⊢ eqrec N as Eq A M1 M2 return B | refl -> BR end[σ] : B[σ,,M1[σ],,M2[σ],,N[σ]] }}.
+Proof.
+  intros.
+  set (IdM1 := {{{ Id,,M1 }}}).
+  set (IdM1M2 := {{{ IdM1,,M2 }}}).
+  set (IdM1M2N := {{{ IdM1M2,,N }}}).
+  set (σM1 := {{{ σ,,M1[σ] }}}).
+  set (σM1M2 := {{{ σM1,,M2[σ] }}}).
+  set (σM1M2N := {{{ σM1M2,,N[σ] }}}).
+  eapply wf_conv; mauto 3.
+  transitivity {{{ B[IdM1M2N∘σ] }}}; [mauto 3 |].
+  eapply exp_eq_sub_cong_typ2'; mauto 3.
+  assert {{ Γ ⊢ (Eq A[Wk∘Wk] #1 #0)[σM1M2] : Type@i }} by mauto 4.
+  assert {{ Δ ⊢ N : (Eq A[Wk∘Wk] #1 #0)[IdM1M2] }} by (eapply wf_conv; mauto 4).
+  transitivity {{{ (IdM1M2∘σ),,N[σ] }}}; [econstructor; mautosolve 2 | symmetry].
+  assert {{ Γ ⊢ N[σ] : (Eq A M1 M2)[σ] }} by mauto 2.
+  assert {{ Γ ⊢ (Eq A[Wk∘Wk] #1 #0)[σM1M2] ≈ (Eq A M1 M2)[σ] : Type@i }} by mauto 2.
+  assert {{ Γ ⊢ N[σ] : (Eq A[Wk∘Wk] #1 #0)[σM1M2] }} by mauto 3.
+  enough {{ Γ ⊢s σM1M2 ≈ IdM1M2∘σ : Δ, A, A[Wk] }} by (econstructor; mauto 3).
+  assert {{ ⊢ Δ, A }} by mauto 2.
+  assert {{ Δ, A ⊢s Wk : Δ }} by mauto 2.
+  assert {{ Δ, A ⊢ A[Wk] : Type@i }} by mauto 2.
+  assert {{ Γ ⊢ M1[σ] : A[σ] }} by mauto 2.
+  assert {{ Γ ⊢ A[Wk][σM1] : Type@i }} by mauto 3.
+  assert {{ Γ ⊢ A[Wk][σM1] ≈ A[σ] : Type@i }} by mauto 2.
+  assert {{ Γ ⊢ M2[σ] : A[Wk][σM1] }} by (eapply wf_conv; mauto 2).
+  assert {{ Δ ⊢ A[Wk][IdM1] : Type@i }} by mauto 3.
+  assert {{ Δ ⊢ A[Wk][IdM1] ≈ A : Type@i }} by mauto 2.
+  assert {{ Δ ⊢ M2 : A[Wk][IdM1] }} by (eapply wf_conv; mauto 2).
+  transitivity {{{ (IdM1∘σ),,M2[σ] }}}; econstructor; mautosolve 3.
+Qed.
+
+#[local]
+Hint Resolve presup_exp_eq_eqrec_sub_left : mcltt.
+
+Lemma presup_exp_eq_eqrec_sub_right : forall {Γ σ Δ i A M1 M2 j B N BR},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Δ ⊢ A : Type@i }} ->
+    {{ Δ ⊢ M1 : A }} ->
+    {{ Δ ⊢ M2 : A }} ->
+    {{ Δ, A, A[Wk], Eq A[Wk∘Wk] #1 #0 ⊢ B : Type@j }} ->
+    {{ Δ, A ⊢ BR : B[Id,,#0,,refl A[Wk] #0] }} ->
+    {{ Δ ⊢ N : Eq A M1 M2 }} ->
+    {{ Γ ⊢ eqrec N[σ] as Eq A[σ] M1[σ] M2[σ] return B[q (q (q σ))] | refl -> BR[q σ] end : B[σ,,M1[σ],,M2[σ],,N[σ]] }}.
+Proof.
+  intros.
+  assert {{ Δ ⊢s Id,,M1 : Δ, A }} by mauto 4.
+  assert {{ ⊢ Δ, A }} by mauto 2.
+  assert {{ Δ , A ⊢ A[Wk] : Type@i }} by mauto 3.
+  assert {{ ⊢ Δ, A, A[Wk] }} by mauto 3.
+  assert {{ Δ, A, A[Wk] ⊢s Wk∘Wk : Δ }} by mauto 4.
+  assert {{ Δ , A , A[Wk] ⊢ A[Wk∘Wk] : Type@i }} by mauto 2.
+  assert {{ Γ ⊢ A[Wk][σ,,M1[σ]] : Type@i}} by mauto 4.
+  assert {{ Γ ⊢ A[σ] : Type@i }} by mauto 2.
+  assert {{ Γ ⊢ M1[σ] : A[σ] }} by mauto 2.
+  assert {{ Γ ⊢ M2[σ] : A[σ] }} by mauto 2.
+  assert {{ Γ ⊢ A[Wk][σ,,M1[σ]] ≈ A[σ] : Type@i}}.
+  {
+    transitivity {{{ A[Wk∘(σ,,M1[σ])] }}};
+      [| eapply exp_eq_sub_cong_typ2']; mauto 4.
+  }
+  assert {{ Γ ⊢ M2[σ] : A[Wk][σ,,M1[σ]] }} by mauto 3.
+  assert {{ Γ ⊢s σ,, M1[σ] : Δ, A }} by mauto 2.
+  assert {{ Γ ⊢s σ,,M1[σ],,M2[σ] : Δ, A, A[Wk] }} by mauto 2.
+  assert {{ Δ, A, A[Wk] ⊢ Eq A[Wk∘Wk] #1 #0 : Type@i }} by mauto 2.
+
+  assert {{ Δ, A ⊢s Wk : Δ }} by mauto 2.
+  assert {{ Δ, A, A[Wk] ⊢s Wk : Δ, A }} by mauto 2.
+  assert {{Γ ⊢ A[Wk∘Wk][σ,,M1[σ],,M2[σ]] ≈ A[σ] : Type@i}}
+    by (transitivity {{{ A[Wk][Wk][σ,,M1[σ],,M2[σ]] }}}; mauto 4).
+  assert {{ Γ ⊢ N[σ] : (Eq A M1 M2)[σ] }} by mauto 3.
+  assert {{ Γ ⊢ #1[σ,,M1[σ],,M2[σ]] ≈ M1[σ] : A[Wk∘Wk][σ,,M1[σ],,M2[σ]] }}
+    by (eapply wf_exp_eq_conv; [eapply sub_lookup_var1 | |]; mauto 3).
+  assert {{ Γ ⊢ #0[σ,,M1[σ],,M2[σ]] ≈ M2[σ] : A[Wk∘Wk][σ,,M1[σ],,M2[σ]] }}
+    by (eapply wf_exp_eq_conv; [eapply sub_lookup_var0 | |]; mauto 3).
+  assert {{ Γ ⊢ N[σ] : (Eq A[Wk∘Wk] #1 #0)[σ,,M1[σ],,M2[σ]] }}
+    by (eapply wf_conv; mauto 2; mauto 3).
+  assert {{ Γ ⊢s σ,,M1[σ],,M2[σ],,N[σ] : Δ, A, A[Wk], Eq A[Wk∘Wk] #1 #0 }} by mauto 2.
+  assert {{ Γ, A[σ] ⊢s q σ : Δ, A }} by mauto 2.
+  assert {{ Γ, A[σ] ⊢s Wk : Γ }} by mauto 3.
+  assert {{ Γ, A[σ] ⊢ A[σ][Wk] : Type@i }} by mauto 2.
+  assert {{ ⊢ Γ, A[σ], A[σ][Wk] }} by mauto 3.
+  assert {{ Γ, A[σ], A[σ][Wk] ⊢s Wk : Γ, A[σ] }} by mauto 2.
+  assert {{ Γ, A[σ], A[σ][Wk] ⊢ A[σ][Wk∘Wk] : Type@i }} by mauto 3.
+  assert {{ Γ, A[σ], A[σ][Wk] ⊢ Eq A[σ][Wk∘Wk] # 1 # 0 : Type@i }} by (econstructor; mauto 2).
+  assert {{ Γ, A[σ] ⊢ A[Wk][q σ] ≈ A[σ][Wk] : Type@i }} by mauto 3.
+  assert {{ ⊢ Γ, A[σ], A[Wk][q σ] ≈ Γ, A[σ], A[σ][Wk] }} by (econstructor; mauto 3).
+  assert {{ Γ, A[σ], A[σ][Wk] ⊢s q (q σ) : Δ, A, A[Wk] }} by mauto 3.
+  assert {{ Γ, A[σ], A[σ][Wk] ⊢ A[Wk][q σ∘Wk] : Type@i }} by mauto 3.
+  assert {{ Γ, A[σ], A[σ][Wk] ⊢ A[Wk][q σ∘Wk] ≈ A[σ][Wk∘Wk] : Type@i }}.
+  {
+    transitivity {{{ A[Wk][q σ][Wk] }}}; [mauto 3 |].
+    transitivity {{{ A[σ][Wk][Wk] }}}; [| mauto 2].
+    eapply exp_eq_sub_cong_typ1; mauto 3.
+  }
+  assert {{ Γ, A[σ],A[σ][Wk] ⊢ A[Wk∘Wk][q (q σ)] ≈ A[σ][Wk∘Wk] : Type@i }}.
+  {
+    transitivity {{{ A[Wk][q σ∘Wk] }}}; [| eassumption].
+    transitivity {{{ A[Wk][Wk][q (q σ)] }}}; [eapply exp_eq_sub_cong_typ1; mauto 3 |].
+    transitivity {{{ A[Wk][Wk∘q (q σ)] }}}; [mauto 2 |].
+    eapply exp_eq_sub_cong_typ2'; mauto 3.
+  }
+  assert {{ Γ, A[σ], A[σ][Wk] ⊢ Eq A[σ][Wk∘Wk] #0 #0 : Type@i }} by (econstructor; mauto 2).
+  assert {{ Γ, A[σ], A[σ][Wk] ⊢ (Eq A[Wk∘Wk] #1 #0)[q (q σ)] ≈ Eq A[σ][Wk∘Wk] #1 #0 : Type@i }}.
+  {
+    transitivity {{{ Eq (A[Wk∘Wk][q (q σ)]) (#1[q (q σ)]) (#0[q (q σ)]) }}};
+      [econstructor; mauto 2 |].
+    econstructor; mauto 2.
+    - eapply wf_exp_eq_conv;
+        [eapply ctxeq_exp_eq; [eassumption | eapply exp_eq_var_1_sub_q_sigma] | |];
+        mauto 2.
+    - eapply wf_exp_eq_conv.
+      econstructor; [mauto 2 | eauto | eapply wf_conv; mauto 2].
+      + mauto 2.
+      + mauto 3.
+  }
+  assert {{ Γ, A[σ], A[σ][Wk], Eq A[σ][Wk∘Wk] #1 #0 ⊢s q (q (q σ)) : Δ, A, A[Wk], Eq A[Wk∘Wk] #1 #0 }}.
+  {
+    eapply ctxeq_sub; [| eapply sub_q]; mauto 2.
+    econstructor; mauto 3.
+  }
+  assert {{ Γ, A[σ] ⊢ #0 : A[σ][Wk] }} by mauto 3.
+  assert {{ Γ, A[σ] ⊢s Id,,#0 : Γ, A[σ], A[σ][Wk] }} by mauto 4.
+  assert {{ Γ, A[σ] ⊢ A[σ][Wk∘Wk][Id,,#0] ≈ A[σ][Wk] : Type@i }}
+    by (transitivity {{{ A[σ][Wk][Wk][Id,,#0] }}}; [symmetry |]; mauto 3).
+
+  assert {{ Γ, A[σ] ⊢s Id,,#0,,refl A[σ][Wk] #0 : Γ, A[σ], A[σ][Wk], Eq A[σ][Wk∘Wk] #1 #0 }}.
+  {
+    econstructor; mauto 2.
+    eapply wf_conv;
+      [econstructor | |];
+      mauto 2.
+    symmetry.
+    etransitivity; [econstructor; mauto 3 |].
+    econstructor; eauto.
+    - eapply wf_exp_eq_conv; mauto 2.
+      transitivity {{{#0[Id]}}}; mauto 2.
+      eapply wf_exp_eq_conv; [econstructor | |]; mauto 3.
+    - eapply wf_exp_eq_conv; [econstructor | |]; mauto 3.
+      transitivity {{{ A[σ][Wk] }}}; mauto 3.
+  }
+  assert {{ Γ, A[σ] ⊢s q (q σ) ∘ (Id,,#0) ≈ q σ,,#0 : Δ, A, A[Wk] }}.
+  {
+    eapply sub_eq_q_sigma_id_extend; mauto 2.
+    eapply wf_conv; mauto 2.
+  }
+  assert {{ Γ, A[σ] ⊢ #0 : A[σ][Wk∘Wk][Id,,#0] }} by (eapply wf_conv; mauto 2).
+  assert {{ Γ, A[σ] ⊢ #0[Id,,#0] ≈ #0 : A[σ][Wk][Id] }} by (econstructor; mauto 3).
+  assert {{ Γ, A[σ] ⊢ #0[Id,,#0] ≈ #0 : A[σ][Wk] }} by mauto 3.
+  assert {{ Γ, A[σ] ⊢ #0[Id,,#0] ≈ #0 : A[σ][Wk∘Wk][Id,,#0] }} by (eapply wf_exp_eq_conv; mauto 2).
+  assert {{ Γ, A[σ] ⊢ (Eq A[σ][Wk∘Wk] #0 #0)[Id,,#0] ≈ Eq A[σ][Wk] #0 #0 : Type@i }}
+    by (etransitivity; econstructor; mauto 2).
+  assert {{ Γ, A[σ] ⊢s (q (q σ)∘Wk)∘(Id,,#0,,refl A[σ][Wk] #0) : Δ, A, A[Wk] }}.
+  {
+    econstructor; [eassumption |].
+    econstructor; mauto 3.
+  }
+  assert {{ Γ, A[σ] ⊢s (q (q σ)∘Wk)∘(Id,,#0,,refl A[σ][Wk] #0) ≈ q (q σ)∘(Id,,#0) : Δ, A, A[Wk] }}.
+  {
+    transitivity {{{ q (q σ)∘(Wk∘(Id,,#0,,refl A[σ][Wk] #0)) }}}; [mauto 4 |].
+    econstructor; mauto 2.
+    eapply wf_sub_eq_p_extend with (A:={{{ Eq A[σ][Wk∘Wk] #0 #0 }}}); mauto 2.
+    eapply wf_conv; mauto 3.
+  }
+  assert {{ Γ, A[σ] ⊢s (q (q σ) ∘ Wk) ∘ (Id,,#0,,refl A[σ][Wk] #0) ≈ q σ,,#0 : Δ, A, A[Wk] }} by mauto 4.
+  assert {{ Γ, A[σ] ⊢ A[σ][Wk∘Wk][Id,,#0] ≈ A[Wk][q σ] : Type@i }} by mauto 3.
+  assert {{ Γ, A[σ] ⊢ #0 : A[Wk][q σ] }} by mauto 3.
+  assert {{ Γ, A[σ] ⊢ A[Wk∘Wk][q σ,,#0] ≈ A[Wk][q σ] : Type@i }}
+    by (transitivity {{{ A[Wk][Wk][q σ,,#0] }}}; [eapply exp_eq_sub_cong_typ1 |]; mauto 3).
+  assert {{Γ, A[σ] ⊢s q σ,,#0 : Δ, A, A[Wk] }} by mauto 2.
+  assert {{Γ, A[σ] ⊢ A[Wk∘Wk][q σ,,#0] : Type@i}} by mauto 2.
+  assert {{Γ, A[σ] ⊢ A[Wk∘Wk][q σ,,#0] ≈ A[σ][Wk] : Type@i}} by mauto 2.
+  assert {{ Γ, A[σ] ⊢ #0[q σ,,#0] ≈ # 0 : A[σ][Wk] }} by (eapply wf_exp_eq_conv; mauto 2).
+  assert {{ Γ, A[σ] ⊢ #0[q σ,,#0] ≈ # 0 : A[Wk∘Wk][q σ,,#0] }} by mauto 3.
+
+  assert {{ Γ, A[σ] ⊢s σ∘Wk : Δ }} by mauto 2.
+  assert {{ Γ, A[σ] ⊢ A[σ][Wk] ≈ A[σ ∘ Wk] : Type@i }} by mauto 2.
+  assert {{ Γ, A[σ] ⊢ #0 : A[σ∘Wk] }} by mauto 3.
+
+  assert {{ Γ, A[σ] ⊢ #1[q σ,,#0] ≈ #0 : A[σ][Wk] }}
+    by (eapply wf_exp_eq_conv; [eapply sub_lookup_var1 | |]; mauto 2).
+  assert {{ Γ, A[σ] ⊢ #1[q σ,,#0] ≈ #0 : A[Wk∘Wk][q σ,,#0] }} by mauto 3.
+
+  assert {{ ⊢ Γ, A[σ], A[σ][Wk], Eq A[σ][Wk∘Wk] #1 #0 }} by mauto 2.
+  assert {{ Γ, A[σ] ⊢s q (q (q σ))∘(Id,,#0,,refl A[σ][Wk] #0) ≈ (q (q σ)∘(Id,,#0)),,refl A[σ][Wk] #0 : Δ, A, A[Wk], Eq A[Wk∘Wk] #1 #0 }}.
+  {
+    etransitivity;
+      [eapply wf_sub_eq_extend_compose; mauto 2; mauto 3 |].
+
+    - eapply wf_conv; mauto 2.
+      + mauto 4.
+      + symmetry.
+        transitivity {{{ (Eq A[Wk∘Wk] #1 #0)[q (q σ)][Wk] }}};
+          [mauto 4 |].
+        eapply exp_eq_sub_cong_typ1; mauto 2.
+    - econstructor; mauto 2.
+
+      eapply wf_exp_eq_conv; mauto 3.
+      + econstructor; mauto 3.
+        eapply wf_conv; [econstructor | |]; mauto 3.
+      + etransitivity; mauto 2.
+        symmetry.
+        etransitivity; [| etransitivity].
+        * eapply exp_eq_sub_cong_typ2'; mauto 2.
+        * econstructor; mauto 2.
+        * econstructor; mauto 2.
+  }
+
+  assert {{ Γ, A[σ] ⊢ A[Wk∘Wk][q (q σ)∘(Id,,#0)] ≈ A[Wk][q σ] : Type@i }} by (etransitivity; mauto 3).
+  assert {{ Γ, A[σ] ⊢ A[Wk∘Wk][q (q σ)∘(Id,,#0)] ≈ A[σ][Wk] : Type@i }} by mauto 2.
+
+  assert {{ Γ, A[σ] ⊢ #0[q (q σ)∘(Id,,#0)] ≈ #0 : A[σ][Wk] }}.
+  {
+    transitivity {{{ #0[q σ,,#0] }}}; [| eassumption].
+    eapply wf_exp_eq_conv; [econstructor; [| eassumption] | |]; mauto 3.
+  }
+  assert {{ Γ, A[σ] ⊢ #0[q (q σ)∘(Id,,#0)] ≈ #0 : A[Wk∘Wk][q (q σ)∘(Id,,#0)] }}
+    by (eapply wf_exp_eq_conv; mauto 3).
+
+  assert {{ Γ, A[σ] ⊢ #1[q (q σ)∘(Id,,#0)] ≈ #0 : A[σ][Wk] }}.
+  {
+    transitivity {{{ #1[q σ,,#0] }}}; [| eassumption].
+    eapply wf_exp_eq_conv; [econstructor; [| eassumption] | |]; mauto 3.
+  }
+  assert {{ Γ, A[σ] ⊢ #1[q (q σ)∘(Id,,#0)] ≈ #0 : A[Wk∘Wk][q (q σ) ∘ (Id,,#0)] }}
+    by (eapply wf_exp_eq_conv; mauto 3).
+
+  assert {{ Γ, A[σ] ⊢s q (q (q σ))∘(Id,,#0,,refl A[σ][Wk] #0) ≈ q σ,,#0,,refl A[σ][Wk] #0 : Δ, A, A[Wk], Eq A[Wk∘Wk] #1 #0 }}.
+  {
+    etransitivity; [eassumption |].
+    econstructor; mauto 2.
+    eapply exp_eq_refl.
+    eapply wf_conv; mauto 3.
+    symmetry.
+    etransitivity; econstructor; mauto 2.
+  }
+
+  assert {{ Γ, A[σ] ⊢s Id ∘ q σ : Δ, A }} by mauto 3.
+  assert {{ Γ, A[σ] ⊢s Id ∘ q σ ≈ q σ : Δ, A }} by mauto 2.
+  assert {{ Γ, A[σ] ⊢ #0[q σ] ≈ #0 : A[σ ∘ Wk] }} by mauto 2.
+  assert {{ Γ, A[σ] ⊢ #0[q σ] ≈ #0 : A[σ][Wk] }} by mauto 3.
+  assert {{ Γ, A[σ] ⊢ #0[q σ] ≈ #0 : A[Wk][q σ] }} by (eapply wf_exp_eq_conv; mauto 2).
+  assert {{ Γ, A[σ] ⊢s (Id,,#0)∘q σ : Δ, A, A[Wk] }} by (econstructor; mauto 3).
+  assert {{ Γ, A[σ] ⊢s (Id,,#0)∘q σ ≈ q σ,,#0 : Δ, A, A[Wk] }}.
+  {
+    etransitivity.
+    - eapply wf_sub_eq_extend_compose; mauto 3.
+    - econstructor; mauto 3.
+      eapply wf_exp_eq_conv; mauto 2.
+      eapply exp_eq_sub_cong_typ2'; mauto 2.
+  }
+
+  assert {{ Δ, A ⊢ A[Wk∘Wk][Id,,#0] ≈ A[Wk] : Type@i }}
+    by (transitivity {{{ A[Wk][Wk][Id,,#0] }}}; [eapply exp_eq_sub_cong_typ1 |]; mauto 3).
+  assert {{ Δ, A ⊢ #0[Id,,#0] ≈ #0 : A[Wk] }} by (eapply wf_exp_eq_conv; [econstructor | |]; mauto 3).
+  assert {{ Δ, A ⊢ A[Wk∘Wk][Id,,#0] : Type@i }} by (eapply exp_sub_typ; mauto 3).
+  assert {{ Δ, A ⊢ #0[Id,,#0] ≈ #0 : A[Wk∘Wk][Id,,#0] }} by (eapply wf_exp_eq_conv; mauto 2).
+  assert {{ Δ, A ⊢ #1[Id,,#0] ≈ #0 : A[Wk] }}.
+  {
+    transitivity {{{ #0[Id] }}}; mauto 3.
+    eapply wf_exp_eq_conv; [econstructor | |]; mauto 3.
+    eapply wf_conv; mauto 3.
+    symmetry; mauto 3.
+  }
+  assert {{ Δ, A ⊢ #1[Id,,#0] ≈ #0 : A[Wk∘Wk][Id,,#0] }} by (eapply wf_exp_eq_conv; mauto 2).
+
+  assert {{ Δ, A ⊢ refl A[Wk] #0 : (Eq A[Wk∘Wk] #1 #0)[Id,,#0] }}.
+  {
+    eapply wf_conv; [mauto 3 | |].
+    - mauto 4.
+    - symmetry.
+      etransitivity; econstructor; mauto 3.
+  }
+
+  assert {{ Γ, A[σ] ⊢ (Eq A[Wk] #0 #0)[q σ] ≈ Eq A[σ][Wk] #0 #0 : Type@i }}
+    by (etransitivity; [econstructor; mauto 2 |]; mauto 3).
+  assert {{ Γ, A[σ] ⊢ A[Wk∘Wk][(Id,,#0)∘q σ] ≈ A[σ][Wk] : Type@i }} by mauto 3.
+  assert {{ Γ, A[σ] ⊢ #1[(Id,,#0)∘q σ] ≈ #0 : A[σ][Wk] }}
+    by (transitivity {{{ #1[q σ,,#0] }}}; [eapply wf_exp_eq_conv |]; mauto 2; econstructor; mauto 3).
+  assert {{ Γ, A[σ] ⊢ #1[(Id,,#0)∘q σ] ≈ #0 : A[Wk∘Wk][(Id,,#0)∘q σ] }} by (eapply wf_exp_eq_conv; mauto 2).
+
+  assert {{ Γ, A[σ] ⊢ #0[(Id,,#0)∘q σ] ≈ #0 : A[σ][Wk] }}.
+  {
+    transitivity {{{ #0[q σ,,#0] }}};
+      [eapply wf_exp_eq_conv; [| | eassumption] |]; mauto 2.
+    econstructor; mauto 3.
+  }
+  assert {{ Γ, A[σ] ⊢ #0[(Id,,#0)∘q σ] ≈ #0 : A[Wk∘Wk][(Id,,#0)∘q σ] }} by (eapply wf_exp_eq_conv; mauto 2).
+
+  assert {{ Γ, A[σ] ⊢ (Eq A[Wk∘Wk] #1 #0)[(Id,,#0)∘q σ] ≈ Eq A[σ][Wk] #0 #0 : Type@i }}
+    by (etransitivity; econstructor; mauto 2).
+
+  assert {{ Γ, A[σ] ⊢s (Id,,#0,,refl A[Wk] #0) ∘ q σ ≈ q σ,,#0,,refl A[σ][Wk] #0 : Δ, A, A[Wk], Eq A[Wk∘Wk] #1 #0 }}.
+  {
+    etransitivity.
+    - eapply wf_sub_eq_extend_compose; mauto 3.
+    - econstructor; mauto 2.
+      etransitivity.
+      + eapply wf_exp_eq_conv;
+          [eapply wf_exp_eq_refl_sub; mauto 3 |
+            eapply exp_sub_typ; mauto 3 |].
+        mauto 3.
+      + eapply wf_exp_eq_conv;
+          [econstructor | |];
+          mauto 2.
+        etransitivity; mauto 2.
+  }
+
+  assert {{ Δ, A ⊢s Id,,#0,,refl A[Wk] #0 : Δ, A, A[Wk], Eq A[Wk∘Wk] #1 #0 }} by (econstructor; mauto 3).
+
+  assert {{ Γ ⊢s Id,,M1[σ] : Γ,A[σ]}} by mauto 2.
+  assert {{ Γ ⊢ A[σ][Wk][Id,,M1[σ]] ≈ A[σ] : Type@i}}.
+  {
+    etransitivity;
+      [eapply exp_eq_sub_compose_typ; mauto 3 |];
+      transitivity {{{ A[σ][Id] }}}; mauto 2.
+    symmetry.
+    eapply exp_eq_sub_cong_typ2'; mauto 3.
+  }
+  assert {{ Γ ⊢ M2[σ] : A[σ][Wk][Id,,M1[σ]] }} by (eapply wf_conv; revgoals; mauto 2).
+  assert {{ Γ ⊢s Id,,M1[σ],,M2[σ] : Γ, A[σ], A[σ][Wk] }} by mauto 2.
+
+  assert {{ Γ ⊢ A[σ][Wk∘Wk][Id,,M1[σ],,M2[σ]] ≈ A[σ] : Type@i }} by mauto 2.
+
+  assert {{ Γ ⊢ #1[Id,,M1[σ],,M2[σ]] ≈ M1[σ] : A[σ] }}.
+  {
+    transitivity {{{#0[Id,,M1[σ]]}}};
+      [eapply wf_exp_eq_conv | eapply wf_exp_eq_conv; econstructor];
+      mauto 3.
+  }
+  assert {{ Γ ⊢ #1[Id,,M1[σ],,M2[σ]] ≈ M1[σ] : A[σ][Wk∘Wk][Id,,M1[σ],,M2[σ]] }} by (eapply wf_exp_eq_conv; mauto 2).
+
+  assert {{ Γ ⊢ #0[Id,,M1[σ],,M2[σ]] ≈ M2[σ] : A[σ] }} by (eapply wf_exp_eq_conv; mauto 2).
+  assert {{ Γ ⊢ #0[Id,,M1[σ],,M2[σ]] ≈ M2[σ] : A[σ][Wk∘Wk][Id,,M1[σ],,M2[σ]] }} by (eapply wf_exp_eq_conv; mauto 2).
+
+  assert {{ Γ ⊢ (Eq A[σ][Wk∘Wk] #1 #0)[Id,,M1[σ],,M2[σ]] ≈ Eq A[σ] M1[σ] M2[σ] : Type@i }}
+    by (etransitivity; econstructor; mauto 2).
+  assert {{ Γ ⊢ (Eq A M1 M2)[σ] ≈ Eq A[σ] M1[σ] M2[σ] : Type@i }} by mauto 2.
+  assert {{ Γ ⊢ N[σ] : (Eq A[σ][Wk∘Wk] #1 #0)[Id,,M1[σ],,M2[σ]] }}
+    by (eapply wf_conv; mauto 2; transitivity {{{ (Eq A M1 M2)[σ] }}}; [| etransitivity]; mauto 2).
+
+  assert {{ Γ ⊢s Id,,M1[σ],,M2[σ],,N[σ] : Γ, A[σ], A[σ][Wk], Eq A[σ][Wk∘Wk] #1 #0}} by mauto 3.
+
+  assert {{ Γ, A[σ], A[σ][Wk] ⊢ A[Wk][q σ∘Wk] ≈ A[σ][Wk∘Wk] : Type@i }} by mauto 3.
+
+  assert {{ Γ, A[σ], A[σ][Wk] ⊢ #0 : A[Wk][q σ∘Wk] }} by (eapply wf_conv; mauto 3).
+
+  assert {{ Γ, A[σ], A[σ][Wk], Eq A[σ][Wk∘Wk] #1 #0 ⊢s q (q σ)∘Wk : Δ,A,A[Wk] }} by mauto 3.
+  assert {{ Γ, A[σ], A[σ][Wk], Eq A[σ][Wk∘Wk] #1 #0 ⊢ (Eq A[Wk∘Wk] #1 #0)[q (q σ)∘Wk] ≈ (Eq A[σ][Wk∘Wk] #1 #0)[Wk] : Type@i }}.
+  {
+    transitivity {{{ (Eq A[Wk∘Wk] #1 #0)[q (q σ)][Wk] }}};
+      [symmetry;
+       eapply exp_eq_sub_compose_typ; mauto 3 |].
+    eapply exp_eq_sub_cong_typ1; mauto 3.
+  }
+
+  assert {{ Γ, A[σ], A[σ][Wk], Eq A[σ][Wk∘Wk] #1 #0 ⊢ #0 : (Eq A[Wk∘Wk] #1 #0)[q (q σ)∘Wk] }}
+    by (eapply wf_conv; mauto 2).
+
+  assert {{ Γ ⊢s (q σ∘Wk)∘(Id,,M1[σ],,M2[σ]) : Δ, A }} by (econstructor; mauto 2).
+  assert {{ Γ ⊢s (q σ∘Wk)∘(Id,,M1[σ],,M2[σ]) ≈ σ,,M1[σ] : Δ, A }}.
+  {
+    etransitivity; [eapply wf_sub_eq_compose_assoc; mauto 3 |].
+    etransitivity;
+      [eapply wf_sub_eq_compose_cong;
+       [eapply wf_sub_eq_p_extend with (A:={{{A[σ][Wk]}}}) | eapply sub_eq_refl] |];
+      mauto 3.
+  }
+
+  assert {{ Γ ⊢ A[Wk][(q σ∘Wk)∘(Id,,M1[σ],,M2[σ])] ≈ A[σ] : Type@i }}.
+  {
+    transitivity {{{ A[Wk][σ,,M1[σ]] }}};
+      [eapply exp_eq_sub_cong_typ2' |]; mauto 3.
+  }
+  assert {{ Γ ⊢ #0[Id,,M1[σ],,M2[σ]] ≈ M2[σ] : A[Wk][(q σ∘Wk)∘(Id,,M1[σ],,M2[σ])] }} by (eapply wf_exp_eq_conv; revgoals; mauto 2).
+  assert {{ Γ ⊢s q (q σ)∘(Id,,M1[σ],,M2[σ]) ≈ σ,,M1[σ],,M2[σ] : Δ, A, A[Wk] }}
+    by (etransitivity; [eapply wf_sub_eq_extend_compose; mauto 2 | econstructor; mauto 2]).
+  assert {{ Γ ⊢s (q (q σ)∘Wk)∘(Id,,M1[σ],,M2[σ],,N[σ]) : Δ, A, A[Wk] }} by mauto 2.
+  assert {{ Γ ⊢s (q (q σ) ∘ Wk) ∘ (Id,,M1[σ],,M2[σ],,N[σ]) ≈ σ,,M1[σ],,M2[σ] : Δ, A, A[Wk] }}.
+  {
+    etransitivity;
+      [eapply wf_sub_eq_compose_assoc; mauto 2 |].
+    etransitivity;
+      [eapply wf_sub_eq_compose_cong;
+       [eapply wf_sub_eq_p_extend with (A:={{{ Eq A[σ][Wk∘Wk] #1 #0 }}}) | eapply sub_eq_refl]  |];
+      mauto 3.
+  }
+
+  assert {{ Γ ⊢ (Eq A[Wk∘Wk] #1 #0)[σ,,M1[σ],,M2[σ]] ≈ Eq A[σ] M1[σ] M2[σ] : Type@i }}
+    by (etransitivity; econstructor; mauto 3).
+  assert {{ Γ ⊢ (Eq A[Wk∘Wk] #1 #0)[(q (q σ)∘Wk)∘(Id,,M1[σ],,M2[σ],,N[σ])] ≈ Eq A[σ] M1[σ] M2[σ] : Type@i }}.
+  {
+    transitivity {{{ (Eq A[Wk∘Wk] #1 #0)[σ,,M1[σ],,M2[σ]] }}};
+      [eapply exp_eq_sub_cong_typ2' |]; mauto 3.
+  }
+  assert {{ Γ ⊢ #0[Id,,M1[σ],,M2[σ],,N[σ]] ≈ N[σ] : (Eq A[Wk∘Wk] #1 #0)[(q (q σ)∘Wk)∘(Id,,M1[σ],,M2[σ],,N[σ])] }}
+    by (eapply wf_exp_eq_conv with (A:={{{ Eq A[σ] M1[σ] M2[σ] }}}); [econstructor | |]; mauto 3).
+  assert {{ Γ ⊢s q (q (q σ))∘(Id,,M1[σ],,M2[σ],,N[σ]) ≈ σ,,M1[σ],,M2[σ],,N[σ] : Δ, A, A[Wk], Eq A[Wk∘Wk] #1 #0 }}.
+  {
+    etransitivity; [eapply wf_sub_eq_extend_compose; mauto 2 |].
+    econstructor; mauto 2.
+  }
+
+  assert {{Γ, A[σ] ⊢s (Id,,#0,,refl A[Wk] #0) ∘ q σ ≈ q (q (q σ))∘(Id,,#0,,refl A[σ][Wk] #0) : Δ, A, A[Wk], Eq A[Wk∘Wk] #1 #0}}
+    by mauto 3.
+
+  eapply wf_conv; [econstructor | |]; mauto 3.
+  - eapply wf_conv; mauto 2; mauto 3.
+  - etransitivity;
+      [eapply exp_eq_sub_compose_typ | eapply exp_eq_sub_cong_typ2'];
+      mauto 3.
+Qed.
+
+#[local]
+Hint Resolve presup_exp_eq_eqrec_sub_right : mcltt.
+
+Lemma presup_exp_eq_refl_cong_right : forall {Γ i A A' M M'},
+    {{ Γ ⊢ A : Type@i }} ->
+    {{ Γ ⊢ A' : Type@i }} ->
+    {{ Γ ⊢ A ≈ A' : Type@i }} ->
+    {{ Γ ⊢ M : A }} ->
+    {{ Γ ⊢ M' : A }} ->
+    {{ Γ ⊢ M ≈ M' : A }} ->
+    {{ Γ ⊢ refl A' M' : Eq A M M }}.
+Proof.
+  intros.
+  eapply wf_conv; mauto 3.
+  symmetry; mauto 3.
+Qed.
+
+#[local]
+Hint Resolve presup_exp_eq_refl_cong_right : mcltt.
+
+Lemma presup_exp_eq_eqrec_cong_right : forall {Γ i A A' M1 M1' M2 M2' j B B' BR BR' N N'},
+    {{ Γ ⊢ A : Type@i }} ->
+    {{ Γ ⊢ M1 : A }} ->
+    {{ Γ ⊢ M2 : A }} ->
+    {{ Γ ⊢ A' : Type@i }} ->
+    {{ Γ ⊢ A ≈ A' : Type@i }} ->
+    {{ Γ ⊢ M1' : A }} ->
+    {{ Γ ⊢ M1 ≈ M1' : A }} ->
+    {{ Γ ⊢ M2' : A }} ->
+    {{ Γ ⊢ M2 ≈ M2' : A }} ->
+    {{ Γ, A, A[Wk], Eq A[Wk∘Wk] #1 #0 ⊢ B : Type@j }} ->
+    {{ Γ, A, A[Wk], Eq A[Wk∘Wk] #1 #0 ⊢ B' : Type@j }} ->
+    {{ Γ, A, A[Wk], Eq A[Wk∘Wk] #1 #0 ⊢ B ≈ B' : Type@j }} ->
+    {{ Γ, A ⊢ BR : B[Id,,#0,,refl A[Wk] #0] }} ->
+    {{ Γ, A ⊢ BR' : B[Id,,#0,,refl A[Wk] #0] }} ->
+    {{ Γ, A ⊢ BR ≈ BR' : B[Id,,#0,,refl A[Wk] #0] }} ->
+    {{ Γ ⊢ N : Eq A M1 M2 }} ->
+    {{ Γ ⊢ N' : Eq A M1 M2 }} ->
+    {{ Γ ⊢ N ≈ N' : Eq A M1 M2 }} ->
+    {{ Γ ⊢ eqrec N' as Eq A' M1' M2' return B' | refl -> BR' end : B[Id,,M1,,M2,,N] }}.
+Proof.
+  intros.
+  assert {{ ⊢ Γ }} by mauto 4.
+  assert {{ Γ ⊢s Id,,M1 : Γ, A}} by mauto 4.
+  assert {{ ⊢ Γ, A }} by mauto 4.
+  assert {{ Γ, A ⊢ A[Wk] : Type@i }} by mauto 4.
+  assert {{ ⊢ Γ, A, A[Wk] }} by mauto 4.
+  assert {{ Γ, A, A[Wk] ⊢s Wk∘Wk : Γ }} by mauto 4.
+  assert {{ Γ, A, A[Wk] ⊢ A[Wk∘Wk] : Type@i }} by mauto 2.
+  assert {{ Γ ⊢ A[Wk][Id,,M1] ≈ A : Type@i }} by mauto 2.
+  assert {{ Γ ⊢s Id,,M1,,M2 : Γ, A, A[Wk]}} by mauto 2.
+  assert {{ Γ ⊢ A[Wk∘Wk][Id,,M1,,M2] ≈ A : Type@i }}.
+  {
+    eapply exp_eq_sub_compose_double_weaken_id_double_extend_typ; revgoals; try eassumption.
+    eapply wf_conv; mauto 3.
+  }
+  assert {{ Γ, A, A[Wk] ⊢ Eq A[Wk∘Wk] # 1 # 0 : Type@i }} by (econstructor; mauto 3; eapply var_compose_subs; mauto 2).
+  assert {{ Γ ⊢ #1[Id,,M1,,M2] ≈ M1 : A[Wk∘Wk][Id,,M1,,M2] }}
+    by (eapply wf_exp_eq_conv; mauto 2 using id_sub_lookup_var1).
+  assert {{ Γ ⊢ #0[Id,,M1,,M2] ≈ M2 : A[Wk∘Wk][Id,,M1,,M2] }}
+    by (eapply wf_exp_eq_conv; mauto 2 using id_sub_lookup_var0).
+  assert {{ Γ ⊢ N : (Eq A[Wk∘Wk] #1 #0)[Id,,M1,,M2]}}.
+  {
+    eapply wf_conv; mauto 2.
+    symmetry; mauto 2.
+  }
+  assert {{ Γ ⊢s Id,,M1,,M2,,N : Γ, A , A[Wk], Eq A[Wk∘Wk] #1 #0}} by mauto 2.
+  assert {{ Γ ⊢ Eq A' M1' M2' : Type@i }} by mauto 4.
+  assert {{ Γ ⊢ Eq A' M1' M2' ≈ Eq A M1 M2 : Type @ i }} by mauto 3.
+
+  assert {{ ⊢ Γ, A ≈ Γ, A' }} by mauto 3.
+  assert {{ Γ , A ⊢ A'[Wk] : Type@i }} by mauto 3.
+  assert {{ Γ , A' ⊢ A'[Wk] : Type@i }} by mauto 2.
+  assert {{ Γ, A ⊢ A[Wk] ≈ A'[Wk] : Type@i }} by mauto 3.
+  assert {{ Γ, A' ⊢ A[Wk] ≈ A'[Wk] : Type@i }} by mauto 2.
+  assert {{ ⊢ Γ, A, A[Wk] ≈ Γ, A', A'[Wk] }} by mauto 3.
+
+  assert {{ Γ, A', A'[Wk] ⊢ Eq A[Wk∘Wk] # 1 # 0 : Type@i }} by mauto 2.
+  assert {{ Γ, A', A'[Wk] ⊢ Eq A'[Wk∘Wk] # 1 # 0 : Type@i }} by (econstructor; mauto 3).
+  assert {{ Γ, A, A[Wk] ⊢ Eq A'[Wk∘Wk] # 1 # 0 : Type@i }} by mauto 3.
+  assert {{ Γ, A, A[Wk] ⊢ Eq A[Wk∘Wk] #1 #0 ≈ Eq A'[Wk∘Wk] #1 #0 : Type@i }} by (econstructor; mauto 3).
+
+  assert {{ ⊢ Γ, A, A[Wk], Eq A[Wk∘Wk] #1 #0 ≈ Γ, A', A'[Wk], Eq A'[Wk∘Wk] #1 #0 }} by mauto 3.
+
+  assert {{ Γ, A ⊢ Eq A[Wk] #0 #0 : Type@i }} by (econstructor; mauto 2).
+  assert {{ Γ, A ⊢ Eq A'[Wk] #0 #0 ≈ Eq A[Wk] #0 #0 : Type@i }} by (econstructor; mauto 3).
+
+  assert {{ Γ, A ⊢ refl A'[Wk] #0 : Eq A[Wk] #0 #0 }}
+    by (eapply wf_conv; [econstructor | |]; mauto 3).
+  assert {{ Γ, A ⊢ refl A[Wk] #0 : Eq A[Wk] #0 #0 }} by mauto 3.
+  assert {{ Γ, A ⊢ refl A[Wk] #0 ≈ refl A'[Wk] #0 : Eq A[Wk] #0 #0 }} by mauto 3.
+  assert {{ Γ, A ⊢s Id,,#0 : Γ, A, A[Wk] }} by mauto 3.
+  assert {{ Γ, A ⊢s Wk : Γ }} by mauto 2.
+  assert {{ Γ, A, A[Wk] ⊢ #1 : A[Wk∘Wk] }} by mauto 2.
+  assert {{ Γ, A ⊢s Wk∘(Id,,#0) : Γ, A }} by (econstructor; mauto 2).
+  assert {{ Γ, A ⊢ A[Wk∘Wk][Id,,#0] ≈ A[Wk] : Type@i }}.
+  {
+    transitivity {{{ A[Wk][Wk][Id,,#0] }}}; [| mauto 3].
+    eapply exp_eq_sub_cong_typ1; mauto 2.
+    symmetry; mauto 3.
+  }
+  assert {{ Γ, A ⊢ #1[Id,,#0] ≈ #0 : A[Wk] }}.
+  {
+    transitivity {{{ #0[Id] }}}.
+    - eapply wf_exp_eq_conv;
+        [eapply wf_exp_eq_var_S_sub with (A:={{{A[Wk]}}}) | |];
+        mauto 3.
+    - mauto 3.
+  }
+  assert {{ Γ, A ⊢ #1[Id,,#0] ≈ #0 : A[Wk∘Wk][Id,,#0] }} by (eapply wf_exp_eq_conv; mauto 2).
+  assert {{ Γ, A ⊢ #0[Id,,#0] ≈ #0 : A[Wk] }}.
+  {
+    eapply wf_exp_eq_conv;
+      [eapply wf_exp_eq_var_0_sub with (A:={{{A[Wk]}}}) | |];
+      mauto 3.
+  }
+  assert {{ Γ, A ⊢ #0[Id,,#0] ≈ #0 : A[Wk∘Wk][Id,,#0] }} by (eapply wf_exp_eq_conv; mauto 2).
+  assert {{ Γ, A ⊢ (Eq A[Wk∘Wk] #1 #0)[Id,,#0] ≈ Eq A[Wk] #0 #0 : Type@i }}
+    by (etransitivity; econstructor; mauto 3).
+  assert {{ Γ, A ⊢ refl A'[Wk] #0 : (Eq A[Wk∘Wk] #1 #0)[Id,,#0] }} by (eapply wf_conv; mauto 2).
+  assert {{ Γ, A ⊢ refl A[Wk] #0 : (Eq A[Wk∘Wk] #1 #0)[Id,,#0] }} by (eapply wf_conv; mauto 2).
+  assert {{ Γ, A ⊢s Id,,#0,,refl A'[Wk] #0 : Γ, A, A[Wk], Eq A[Wk∘Wk] #1 #0 }} by mauto 2.
+  assert {{ Γ, A ⊢s Id,,#0,,refl A[Wk] #0 : Γ, A, A[Wk], Eq A[Wk∘Wk] #1 #0 }} by mauto 2.
+
+  assert {{ Γ, A ⊢s Id,,#0,,refl A[Wk] #0 ≈ Id,,#0,,refl A'[Wk] #0 : Γ, A, A[Wk], Eq A[Wk∘Wk] #1 #0 }}
+    by (econstructor; [| | eapply wf_exp_eq_conv]; mauto 2).
+
+  assert {{ Γ, A ⊢ B[Id,,#0,,refl A[Wk] #0] ≈ B'[Id,,#0,,refl A'[Wk] #0] : Type@j }}.
+  {
+    etransitivity;
+      [eapply exp_eq_sub_cong_typ2' |
+        eapply exp_eq_sub_cong_typ1];
+      mauto 3.
+  }
+
+  assert {{ Γ ⊢ M1 ≈ M1' : A[Id] }} by (eapply wf_exp_eq_conv; mauto 3).
+  assert {{ Γ ⊢s Id,,M1 ≈ Id,,M1' : Γ, A }} by mauto 2.
+  assert {{ Γ ⊢ M2 ≈ M2' : A[Wk][Id,,M1] }} by (eapply wf_exp_eq_conv; mauto 2).
+  assert {{ Γ ⊢s Id,,M1,,M2 ≈ Id,,M1',,M2' : Γ, A, A[Wk] }} by mauto 2.
+
+  assert {{ Γ ⊢ (Eq A[Wk∘Wk] #1 #0)[Id,,M1,,M2] ≈ Eq A M1 M2 : Type@i }} by mauto 2.
+  assert {{ Γ ⊢s Id,,M1,,M2,,N ≈ Id,,M1',,M2',,N' : Γ, A, A[Wk], Eq (A[Wk∘Wk]) #1 #0 }}
+    by (econstructor; [| | eapply wf_exp_eq_conv]; mauto 2).
+
+  assert {{ Γ ⊢s Id,,M1' : Γ, A}} by mauto 2.
+  assert {{ Γ ⊢ A[Wk][Id,,M1'] ≈ A : Type@i }}.
+  {
+    transitivity {{{A[Wk ∘ (Id,,M1')]}}};
+      [| transitivity {{{A[Id]}}}];
+      mauto 2.
+    eapply exp_eq_sub_cong_typ2'; mauto 2.
+  }
+  assert {{ Γ ⊢ M2' : A[Wk][Id,,M1'] }} by (eapply wf_conv; mauto 2).
+  assert {{ Γ ⊢s Id,,M1',,M2' : Γ, A, A[Wk]}} by mauto 2.
+
+  assert {{ Γ ⊢ (Eq A[Wk∘Wk] #1 #0)[Id,,M1',,M2'] ≈ Eq A M1 M2 : Type@i }}
+    by (transitivity {{{ Eq A M1' M2' }}}; [mauto 2 | econstructor; mauto 2]).
+  assert {{ Γ ⊢ N' : (Eq A[Wk∘Wk] #1 #0)[Id,,M1',,M2'] }} by (eapply wf_conv; mauto 2).
+  assert {{ Γ ⊢s Id,,M1',,M2',,N' : Γ, A, A[Wk], Eq A[Wk∘Wk] #1 #0 }} by mauto 2.
+
+  eapply wf_conv;
+    [econstructor; mauto 3 | mauto 2 | ].
+  - eapply ctxeq_exp; eauto.
+    eapply wf_conv;
+      mauto 2.
+  - etransitivity;
+      [eapply exp_eq_sub_cong_typ2' |
+        eapply exp_eq_sub_cong_typ1];
+      mauto 2.
+Qed.
+
+#[local]
+Hint Resolve presup_exp_eq_eqrec_cong_right : mcltt.
+
+Lemma presup_exp_eq_eqrec_beta_right : forall {Γ i A M j B BR},
+    {{ Γ ⊢ A : Type@i }} ->
+    {{ Γ ⊢ M : A }} ->
+    {{ Γ , A , A[Wk], Eq A[Wk∘Wk] #1 #0 ⊢ B : Type@j }} ->
+    {{ Γ , A ⊢ BR : B[Id,,#0,,refl A[Wk] #0] }} ->
+    {{ Γ ⊢ BR[Id,,M] : B[Id,,M,,M,,refl A M] }}.
+Proof.
+  intros.
+  assert {{ Γ ⊢s Id,,M : Γ, A }} by mauto 4.
+  assert {{ Γ, A ⊢ A[Wk] : Type@i }} by mauto 4.
+  assert {{ Γ, A, A[Wk] ⊢s Wk : Γ, A }} by mauto 4.
+  assert {{ Γ, A, A[Wk] ⊢s Wk∘Wk : Γ }} by mauto 4.
+  assert {{ Γ, A, A[Wk] ⊢ A[Wk∘Wk] : Type@i }} by mauto 4.
+  assert {{ Γ ⊢ A[Wk][Id,,M] ≈ A : Type@i }} by mauto 3.
+  assert {{ Γ ⊢s Id,,M,,M : Γ, A, A[Wk] }} by mauto 2.
+  assert {{ Γ ⊢ A[Wk∘Wk][Id,,M,,M] ≈ A : Type@i }}.
+  {
+    eapply exp_eq_sub_compose_double_weaken_id_double_extend_typ; mauto 2.
+    eapply wf_conv; mauto 2.
+  }
+  assert {{ Γ, A, A[Wk] ⊢ Eq A[Wk∘Wk] # 1 # 0 : Type@i }} by mauto 2.
+  assert {{ Γ ⊢ refl A M : Eq A M M}} by mauto 2.
+  assert {{ Γ ⊢ refl A M : (Eq A[Wk∘Wk] #1 #0)[Id,,M,,M]}}.
+  {
+    eapply wf_conv; mauto 2.
+    symmetry.
+    mauto 3.
+  }
+  assert {{Γ, A ⊢s Id,,#0 : Γ, A, A[Wk] }} by mauto 4.
+
+  assert {{ Γ, A ⊢ refl A[Wk] #0 : Eq A[Wk] #0 #0 }} by mauto 4.
+  assert {{ Γ, A, A[Wk] ⊢ #1 : A[Wk∘Wk] }} by mauto 2.
+  assert {{ ⊢ Γ, A }} by mauto 2.
+  assert {{ Γ, A ⊢s Wk : Γ }} by mauto 2.
+  assert {{ Γ, A ⊢s Wk∘(Id,,#0) : Γ, A }} by mauto 2.
+  assert {{ Γ, A ⊢ A[Wk∘Wk][Id,,#0] ≈ A[Wk] : Type@i }}
+    by (transitivity {{{ A[Wk][Wk][Id,,#0] }}}; [symmetry |]; mauto 3).
+  assert {{ Γ, A ⊢ #1[Id,,#0] ≈ #0 : A[Wk] }}.
+  {
+    transitivity {{{ #0[Id] }}}.
+    - eapply wf_exp_eq_conv;
+        [eapply wf_exp_eq_var_S_sub with (A:={{{A[Wk]}}}) | |];
+        mauto 3.
+    - mauto 3.
+  }
+  assert {{ Γ, A ⊢ #1[Id,,#0] ≈ #0 : A[Wk∘Wk][Id,,#0] }} by (eapply wf_exp_eq_conv; mauto 2).
+  assert {{ Γ, A ⊢ #0[Id,,#0] ≈ #0 : A[Wk] }}.
+  {
+    eapply wf_exp_eq_conv;
+      [eapply wf_exp_eq_var_0_sub with (A:={{{A[Wk]}}}) | |];
+      mauto 3.
+  }
+  assert {{ Γ, A ⊢ #0[Id,,#0] ≈ #0 : A[Wk∘Wk][Id,,#0] }} by (eapply wf_exp_eq_conv; mauto 2).
+  assert {{ Γ, A ⊢ (Eq A[Wk∘Wk] #1 #0)[Id,,#0] ≈ Eq A[Wk] #0 #0 : Type@i }}
+    by (etransitivity; econstructor; mauto 2).
+  assert {{ Γ, A ⊢ refl A[Wk] #0 : (Eq A[Wk∘Wk] #1 #0)[Id,,#0] }} by (eapply wf_conv; mauto 2).
+  assert {{ Γ, A ⊢s Id,,#0,,refl A[Wk] #0 : Γ, A, A[Wk], Eq A[Wk∘Wk] #1 #0 }} by mauto 2.
+
+  assert {{ Γ, A ⊢ #0 : A[Wk][Id] }} by mauto 3.
+
+  assert {{ Γ ⊢ A[Wk][Id∘(Id,,M)] ≈ A : Type@i }}.
+  {
+    transitivity {{{ A[Wk][Id,,M] }}}; mauto 3.
+    eapply exp_eq_sub_cong_typ2'; mauto 3.
+  }
+  assert {{ Γ ⊢s Id : Γ }} by mauto 3.
+  assert {{ Γ ⊢ #0[Id,,M] ≈ M : A }}
+    by (eapply wf_exp_eq_conv with (A:={{{A[Id]}}}); mauto 3).
+  assert {{ Γ ⊢ A[Wk][Id∘(Id,,M)] : Type@i }} by mauto 4.
+  assert {{ Γ ⊢ #0[Id,,M] ≈ M : A[Wk][Id∘(Id,,M)] }} by mauto 3.
+
+  assert {{ Γ ⊢s Id∘(Id,,M),,#0[Id,,M] ≈ Id,,M,,M : (Γ, A), A[Wk] }} by mauto 3.
+  assert {{ Γ ⊢s (Id,,#0)∘(Id,,M) ≈ Id,,M,,M : (Γ, A), A[Wk] }}.
+  {
+    etransitivity;
+      [eapply wf_sub_eq_extend_compose |];
+      mauto 2.
+  }
+
+  assert {{ Γ ⊢ #1[Id,,M,,M] ≈ M : A }}.
+  {
+    transitivity {{{ #0[Id,,M] }}}.
+    - eapply wf_exp_eq_conv;
+        [eapply wf_exp_eq_var_S_sub with (A:={{{ A[Wk] }}}) | |];
+        mauto 4.
+    - mauto 3.
+  }
+  assert {{ Γ ⊢s Wk∘(Id,,M,,M) : Γ, A }} by (eapply wf_sub_conv; mauto 2).
+  assert {{ Γ ⊢s Wk∘(Id,,M,,M) ≈ Id,,M : Γ, A }}
+    by (econstructor; [| | eapply wf_conv]; mauto 2).
+  assert {{ Γ ⊢ A[Wk∘Wk][Id,,M,,M] ≈ A : Type@i }} by mauto 3.
+  assert {{ Γ ⊢ #1[Id,,M,,M] ≈ M : A[Wk∘Wk][Id,,M,,M] }} by (eapply wf_exp_eq_conv; mauto 2).
+
+  assert {{ Γ ⊢ #0[Id,,M,,M] ≈ M : A }}.
+  {
+    eapply wf_exp_eq_conv with (A:={{{A[Wk][Id,,M]}}});
+      [econstructor | |];
+      mauto 4.
+  }
+  assert {{ Γ ⊢ #0[Id,,M,,M] ≈ M : A[Wk∘Wk][Id,,M,,M] }} by (eapply wf_exp_eq_conv; mauto 2).
+
+  assert {{ Γ ⊢ (Eq A[Wk∘Wk] #1 #0)[(Id,,#0)∘(Id,,M)] ≈ Eq A M M : Type@i }}
+    by (etransitivity; [eapply exp_eq_sub_cong_typ2' | ]; mauto 2).
+
+  assert {{ Γ ⊢ (Eq A[Wk∘Wk] #1 #0)[Id,,#0][Id,,M] ≈ Eq A M M : Type@i }}
+    by (etransitivity; mauto 4).
+  assert {{ Γ ⊢ Eq A M M : Type@i }} by mauto 2.
+
+  assert {{ Γ ⊢ #0[Id,,M] ≈ M : A }} by eassumption.
+  assert {{ Γ ⊢ #0[Id,,M] ≈ M : A[Wk][Id,,M] }} by (eapply wf_exp_eq_conv; mauto 2).
+
+  assert {{ Γ ⊢ (refl A[Wk] #0)[Id,,M] ≈ refl A M : Eq A M M }}.
+  {
+    etransitivity.
+    - eapply wf_exp_eq_conv;
+        [eapply wf_exp_eq_refl_sub | | ]; mauto 4.
+    - eapply wf_exp_eq_conv; [econstructor | | econstructor]; mauto 3.
+  }
+
+  assert {{ Γ ⊢ (refl A[Wk] #0)[Id,,M] ≈ refl A M : (Eq A[Wk∘Wk] #1 #0)[(Id,,#0)∘(Id,,M)] }}
+    by (eapply wf_exp_eq_conv; mauto 3).
+
+  eapply wf_conv; mauto 3.
+  etransitivity.
+  - eapply exp_eq_sub_compose_typ; mauto 2.
+  - symmetry.
+    eapply exp_eq_sub_cong_typ2'; mauto 2.
+    symmetry.
+    etransitivity;
+      [eapply wf_sub_eq_extend_compose |];
+      mauto 2.
+Qed.
+
+#[local]
+Hint Resolve presup_exp_eq_eqrec_beta_right : mcltt.
+
+Lemma presup_exp_eq_var_0_sub_left : forall {Γ σ Δ i A M},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Δ ⊢ A : Type@i }} ->
+    {{ Γ ⊢ M : A[σ] }} ->
+    {{ Γ ⊢ #0[σ,,M] : A[σ] }}.
+Proof.
+  intros.
+  assert {{ ⊢ Δ, A }} by mauto 3.
+  assert {{ Δ, A ⊢ #0 : A[Wk] }} by mauto 2.
+  eapply wf_conv; mauto 3.
+Qed.
+
+#[local]
+Hint Resolve presup_exp_eq_var_0_sub_left : mcltt.
+
+Lemma presup_exp_eq_var_S_sub_left : forall {Γ σ Δ i A M B x},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Δ ⊢ A : Type@i }} ->
+    {{ Γ ⊢ M : A[σ] }} ->
+    {{ #x : B ∈ Δ }} ->
+    {{ Γ ⊢ #(S x)[σ,,M] : B[σ] }}.
+Proof.
+  intros.
+  assert {{ ⊢ Δ }} by mauto 2.
+  assert {{ ⊢ Δ, A }} by mauto 2.
+  assert (exists j, {{ Δ ⊢ B : Type@j }}) as [j] by mauto 2.
+  assert {{ Δ, A ⊢ #(S x) : B[Wk] }} by mauto 3.
+  eapply wf_conv; mauto 3.
+Qed.
+
+#[local]
+Hint Resolve presup_exp_eq_var_S_sub_left : mcltt.
+
+Lemma presup_exp_eq_sub_cong_right : forall {Γ σ σ' Δ i A M M'},
+    {{ Δ ⊢ A : Type@i }} ->
+    {{ Δ ⊢ M : A }} ->
+    {{ Δ ⊢ M' : A }} ->
+    {{ Δ ⊢ M ≈ M' : A }} ->
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Γ ⊢s σ' : Δ }} ->
+    {{ Γ ⊢s σ ≈ σ' : Δ }} ->
+    {{ Γ ⊢ M'[σ'] : A[σ] }}.
+Proof.
+  intros.
+  eapply wf_conv; mauto 2.
+  eapply exp_eq_sub_cong_typ2'; mauto 2.
+Qed.
+
+#[local]
+Hint Resolve presup_exp_eq_sub_cong_right : mcltt.
+
+Lemma presup_exp_eq_sub_compose_right : forall {Γ τ Γ' σ Γ'' i A M},
+    {{ Γ ⊢s τ : Γ' }} ->
+    {{ Γ' ⊢s σ : Γ'' }} ->
+    {{ Γ'' ⊢ A : Type@i }} ->
+    {{ Γ'' ⊢ M : A }} ->
+    {{ Γ ⊢ M[σ][τ] : A[σ ∘ τ] }}.
+Proof.
+  intros.
+  eapply wf_conv; mauto 3.
+Qed.
+
+#[local]
+Hint Resolve presup_exp_eq_sub_compose_right : mcltt.
+
 #[local]
 Ltac gen_presup_ctx H :=
   match type of H with
@@ -54,1306 +1334,29 @@ Lemma presup_exp_eq : forall {Γ M M' A}, {{ Γ ⊢ M ≈ M' : A }} -> {{ ⊢ Γ
 with presup_sub_eq : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Γ }} /\ {{ Γ ⊢s σ : Δ }} /\ {{ Γ ⊢s σ' : Δ }} /\ {{ ⊢ Δ }}
 with presup_subtyp : forall {Γ M M'}, {{ Γ ⊢ M ⊆ M' }} -> {{ ⊢ Γ }} /\ exists i, {{ Γ ⊢ M : Type@i }} /\ {{ Γ ⊢ M' : Type@i }}.
 Proof with mautosolve 4.
-  1: set (WkWksucc := {{{ Wk∘Wk ,, succ #1 }}}).
   all: inversion_clear 1; (on_all_hyp: gen_presup_IH presup_exp_eq presup_sub_eq presup_subtyp);
     clear presup_exp_eq presup_sub_eq presup_subtyp;
-    repeat split; mauto 4;
-    try (rename B into C); try (rename B' into C'); try (rename A0 into B); try (rename A' into B');
-    try (rename N into L); try (rename N' into L');
-    try (rename M0 into N); try (rename MZ into NZ); try (rename MS into NS);
-    try (rename M'0 into N'); try (rename MZ' into NZ'); try (rename MS' into NS');
-    try (rename M' into N').
+    repeat split; try mautosolve 3;
+    try (eexists; unshelve solve [mauto 4 using lift_exp_max_left, lift_exp_max_right]; constructor).
 
-  (** presup_exp_eq cases *)
-  - assert {{ Γ ⊢s Id ,, N ≈ Id ,, N' : Γ, ℕ }} by mauto 4.
-    assert {{ Γ ⊢ B[Id ,, N] ≈ B[Id ,, N'] : Type@i }} by mauto 3.
-    assert {{ Γ ⊢ B[Id ,, N] ≈ B'[Id ,, N'] : Type@i }} by mauto 4.
-    assert {{ Γ ⊢ NZ' : B'[Id ,, zero] }} by (eapply wf_conv; mauto 3).
-    assert {{ Γ, ℕ, B ⊢ NS' : B'[WkWksucc] }} by (eapply wf_conv; mauto 3).
-    assert {{ Γ, ℕ, B' ⊢ NS' : B'[WkWksucc] }} by mauto 4.
-    assert {{ Γ ⊢ rec N' return B' | zero -> NZ' | succ -> NS' end : B'[Id ,, N'] }} by mauto 3.
-    eapply wf_conv...
-
-  - assert {{ Γ ⊢ B[(Id,,N)][σ] ≈ B[(Id,,N)∘σ] : Type@i }} by mauto 3.
-    assert {{ Γ ⊢s (Id,,N)∘σ ≈ σ,,N[σ] : Δ, ℕ }} by mauto 3.
-    assert {{ Γ ⊢ B[(Id,,N)∘σ] ≈ B[σ,,N[σ]] : Type@i }} by mauto 4.
-    eapply wf_conv...
-
-  - assert {{ Γ ⊢s Id,,N[σ] : Γ, ℕ }} by mauto 4.
-    assert {{ Γ, ℕ ⊢s q σ : Δ, ℕ }} by mauto 2.
-    assert {{ Γ, ℕ ⊢ B[q σ] : Type@i }} by mauto 2.
-    assert {{ Γ ⊢ B[q σ][(Id,,N[σ])] ≈ B[q σ∘(Id,,N[σ])] : Type@i }} by mauto 2.
-    assert {{ Γ ⊢s q σ∘(Id,,N[σ]) ≈ σ,,N[σ] : Δ, ℕ }} by mauto 3.
-    assert {{ Γ ⊢ B[q σ∘(Id,,N[σ])] ≈ B[σ,,N[σ]] : Type@i }} by mauto 3.
-    assert {{ Γ ⊢ B[q σ][Id,,N[σ]] ≈ B[σ,,N[σ]] : Type@i }} by mauto 3.
-    assert {{ Γ ⊢ NZ[σ] : B[Id ,, zero][σ] }} by mauto 3.
-    assert {{ Γ ⊢ ℕ ≈ ℕ[σ] : Type@0 }} by mauto 3.
-    assert {{ Γ ⊢ zero : ℕ[σ] }} by mauto 3.
-    assert {{ Γ ⊢s q σ∘(Id ,, zero) ≈ σ ,, zero : Δ, ℕ }} by mauto 3.
-    assert {{ Γ ⊢s σ ≈ Id∘σ : Δ }} by mauto 3.
-    assert {{ Γ ⊢s σ ,, zero ≈ Id∘σ ,, zero[σ] : Δ, ℕ }} by mauto 4.
-    assert {{ Γ ⊢s Id∘σ ,, zero[σ] ≈ (Id ,, zero)∘σ : Δ, ℕ }} by mauto.
-    assert {{ Γ ⊢s Id ,, zero : Γ, ℕ }} by mauto 2.
-    assert {{ Γ ⊢s q σ∘(Id ,, zero) ≈ (Id ,, zero)∘σ : Δ, ℕ }} by mauto 3.
-    assert {{ Γ ⊢ B[q σ∘(Id ,, zero)] ≈ B[(Id ,, zero)∘σ] : Type@i }} by mauto 3.
-    assert {{ Γ ⊢ B[q σ][Id ,, zero] ≈ B[Id ,, zero][σ] : Type@i }} by mauto 3.
-    assert {{ Γ ⊢ NZ[σ] : B[q σ][Id ,, zero] }} by mauto 4.
-    set (Γ' := {{{ Γ, ℕ, B[q σ] }}}).
-    assert {{ Γ' ⊢s q (q σ) : Δ, ℕ, B }} by mauto 2.
-    assert {{ Γ' ⊢s q σ∘WkWksucc ≈ WkWksucc∘q (q σ) : Δ, ℕ }} by mauto 2.
-    assert {{ Γ' ⊢s WkWksucc : Γ, ℕ }} by mauto 2.
-    assert {{ Γ' ⊢ B[WkWksucc][q (q σ)] ≈ B[q σ][WkWksucc] : Type@i }} by mauto 4.
-    assert {{ Γ' ⊢ NS[q (q σ)] : B[q σ][WkWksucc] }} by mauto 4.
-    eapply wf_conv...
-
-  - eexists...
-
-  - set (recN := {{{ rec N return B | zero -> NZ | succ -> NS end }}}).
-    set (IdNrecN := {{{ Id ,, N ,, recN }}}).
-    assert {{ Γ ⊢ ℕ : Type@0 }} by mauto 3.
-    assert {{ Γ ⊢ recN : B[Id ,, N] }} by mauto 4.
-    assert {{ Γ, ℕ ⊢s Wk : Γ }} by mauto 2.
-    assert {{ Γ, ℕ, B ⊢s Wk : Γ, ℕ }} by mauto 2.
-    assert {{ Γ, ℕ, B ⊢s Wk∘Wk : Γ }} by mauto 2.
-    assert {{ Γ ⊢s WkWksucc∘IdNrecN ≈ (Wk∘Wk)∘IdNrecN ,, (succ #1)[IdNrecN] : Γ, ℕ }}
-      by (eapply sub_eq_extend_compose_nat; mauto 3).
-    assert {{ Γ ⊢s IdNrecN : Γ, ℕ, B }} by mauto 3.
-    assert {{ Γ ⊢s (Wk∘Wk)∘IdNrecN : Γ }} by mauto 2.
-    assert {{ Γ ⊢s (Wk∘Wk)∘IdNrecN ≈ Wk∘(Wk∘IdNrecN) : Γ }} by mauto 2.
-    assert {{ Γ ⊢s Id,,N : Γ, ℕ }} by mauto 2.
-    assert {{ Γ ⊢s Wk∘(Wk∘IdNrecN) ≈ Wk∘(Id,,N) : Γ }} by mauto 4.
-    assert {{ Γ ⊢s (Wk∘Wk)∘IdNrecN ≈ Id : Γ }} by mauto 4.
-    assert {{ Γ ⊢ #1[IdNrecN] ≈ #0[Id ,, N] : ℕ }} by mauto 3.
-    assert {{ Γ ⊢ #1[IdNrecN] ≈ N : ℕ }} by mauto 4.
-    assert {{ Γ ⊢ succ #1[IdNrecN] ≈ succ N : ℕ }} by mauto 2.
-    assert {{ Γ ⊢ (succ #1)[IdNrecN] ≈ succ N : ℕ }} by mauto 4.
-    assert {{ Γ ⊢s (Wk∘Wk)∘IdNrecN ,, (succ #1)[IdNrecN] ≈ Id ,, succ N : Γ , ℕ }} by mauto 2.
-    assert {{ Γ ⊢s WkWksucc∘IdNrecN : Γ, ℕ }} by mauto 3.
-    assert {{ Γ ⊢s Id,,succ N : Γ, ℕ }} by mauto 3.
-    assert {{ Γ ⊢s WkWksucc∘IdNrecN ≈ Id ,, succ N : Γ , ℕ }} by mauto 2.
-    assert {{ Γ ⊢ B[WkWksucc∘IdNrecN] ≈ B[Id,,succ N] : Type@i }} by mauto 2.
-    enough {{ Γ ⊢ B[WkWksucc][IdNrecN] ≈ B[Id,,succ N] : Type@i }}...
-
-  - eexists...
-
-  - mauto.
-
-  - mauto.
-
-  - assert {{ Γ ⊢ B : Type@(max i i0) }} by mauto 2 using lift_exp_max_left.
-    assert {{ Γ ⊢ B ≈ B' : Type@(max i i0) }} by mauto 2 using lift_exp_eq_max_left.
-    assert {{ Γ, B ⊢ C : Type@(max i i0) }} by mauto 2 using lift_exp_max_right.
-    assert {{ Γ ⊢ Π B C ≈ Π B' C : Type@(max i i0) }} by mauto 3.
-    assert {{ Γ, B' ⊢ N' : C }} by mauto 4.
-    enough {{ Γ ⊢ λ B' N' : Π B' C }}...
-
-  - assert {{ Γ ⊢ B : Type@(max i i0) }} by mauto 2 using lift_exp_max_left.
-    assert {{ Γ, B ⊢ C : Type@(max i i0) }} by mauto 2 using lift_exp_max_right...
-
-  - assert {{ Δ ⊢ B : Type@(max i i0) }} by mauto 2 using lift_exp_max_left.
-    assert {{ Δ, B ⊢ C : Type@(max i i0) }} by mauto 2 using lift_exp_max_right.
-    assert {{ Γ ⊢ B[σ] : Type@(max i i0) }} by mauto 2.
-    assert {{ Γ, B[σ] ⊢ C[q σ] : Type@(max i i0) }} by mauto 3.
-    assert {{ Γ ⊢ Π B[σ] C[q σ] : Type@(max i i0) }} by mauto 2.
-    assert {{ Γ ⊢ Π B[σ] C[q σ] ≈ Π B[σ] C[q σ] : Type@(max i i0) }} by mauto 2.
-    assert {{ Γ, B[σ] ⊢ N[q σ] : C[q σ] }} by mauto 3.
-    assert {{ Γ ⊢ λ B[σ] N[q σ] : Π B[σ] C[q σ] }} by mauto 3.
-    eapply wf_conv...
-
-  - assert {{ Δ ⊢ B : Type@(max i i0) }} by mauto 2 using lift_exp_max_left.
-    assert {{ Δ, B ⊢ C : Type@(max i i0) }} by mauto 2 using lift_exp_max_right.
-    enough {{ Δ ⊢ Π B C : Type@(max i i0) }}...
-
-  - assert {{ Γ ⊢s Id ≈ Id : Γ }} by mauto 2.
-    assert {{ Γ ⊢ B ≈ B[Id] : Type@i }} by mauto 3.
-    assert {{ Γ ⊢ L ≈ L' : B[Id] }} by mauto 4.
-    assert {{ Γ ⊢s Id ,, L ≈ Id ,, L' : Γ, B }} by mauto 2.
-    assert {{ Γ ⊢ C[Id ,, L] ≈ C[Id ,, L'] : Type@i }} by mauto 3.
-    eapply wf_conv...
-
-  - assert {{ Γ ⊢ N[σ] : Π B[σ] C[q σ] }} by (eapply wf_conv; mauto).
-    assert {{ Δ ⊢ L : B[Id] }} by mauto 4.
-    assert {{ Γ ⊢s (Id ,, L)∘σ ≈ Id∘σ ,, L[σ] : Δ, B }} by mauto 3.
-    assert {{ Γ ⊢s (Id ,, L)∘σ ≈ σ ,, L[σ] : Δ, B }} by mauto 3.
-    assert {{ Δ ⊢s Id ,, L : Δ, B }} by mauto 3.
-    assert {{ Γ ⊢s (Id ,, L)∘σ : Δ, B }} by mauto 3.
-    assert {{ Γ ⊢ C[(Id ,, L)∘σ] ≈ C[σ ,, L[σ]] : Type@i }} by mauto 2.
-    assert {{ Γ ⊢ C[Id ,, L][σ] ≈ C[σ ,, L[σ]] : Type@i }} by mauto 3.
-    eapply wf_conv...
-
-  - assert {{ Γ ⊢ B[σ] : Type@i }} by mauto 2.
-    assert {{ Γ, B[σ] ⊢s q σ : Δ, B }} by mauto 2.
-    assert {{ Γ, B[σ] ⊢ C[q σ] : Type@i }} by mauto 2.
-    assert {{ Γ ⊢ N[σ] : Π B[σ] C[q σ] }} by (eapply wf_conv; mauto 2).
-    assert {{ Γ ⊢ L[σ] : B[σ] }} by mauto 2.
-    assert {{ Γ ⊢s q σ∘(Id ,, L[σ]) ≈ σ ,, L[σ] : Δ, B }} by mauto 2.
-    assert {{ Γ ⊢s Id ,, L[σ] : Γ, B[σ] }} by mauto 2.
-    assert {{ Γ ⊢s q σ∘(Id ,, L[σ]) : Δ, B }} by mauto 2.
-    assert {{ Γ ⊢ C[q σ∘(Id ,, L[σ])] ≈ C[σ ,, L[σ]] : Type@i }} by mauto 2.
-    assert {{ Γ ⊢ C[q σ][(Id ,, L[σ])] ≈ C[σ ,, L[σ]] : Type@i }} by mauto 3.
-    eapply wf_conv...
+  all: try (econstructor; mautosolve 4).
 
-  - eexists...
-
-  - set (Id0 := {{{ Id ,, #0 }}}).
-    assert {{ Γ, B ⊢s Wk : Γ }} by mauto 2.
-    assert {{ Γ, B ⊢ B[Wk] : Type@i }} by mauto 2.
-    assert {{ Γ, B, B[Wk] ⊢s Wk : Γ, B }} by mauto 3.
-    assert {{ Γ, B, B[Wk] ⊢s q Wk : Γ, B }} by mauto 2.
-    assert {{ Γ, B, B[Wk] ⊢ C[q Wk] : Type@i }} by mauto 2.
-    assert {{ Γ, B ⊢ M[Wk] : (Π B C)[Wk] }} by mauto 2.
-    assert {{ Γ, B ⊢ M[Wk] : Π B[Wk] C[q Wk] }} by mauto 4.
-    assert {{ Γ, B ⊢ #0 : B[Wk] }} by mauto 2.
-    assert {{ Γ, B ⊢s Id0 : Γ, B, B[Wk] }} by mauto 2.
-    assert {{ Γ, B ⊢ M[Wk] #0 : C[q Wk][Id0] }} by mauto 2.
-    assert {{ Γ, B ⊢ M[Wk] #0 : C[q Wk ∘ Id0] }} by (eapply wf_conv; mauto 3).
-    assert {{ Γ, B ⊢ B[Wk][Id] ≈ B[Wk] : Type@i }} by mauto 2.
-    assert {{ Γ, B ⊢ #0 : B[Wk][Id] }} by mauto 2.
-    assert {{ Γ, B, B[Wk] ⊢s Wk∘Wk : Γ }} by mauto 2.
-    assert {{ Γ, B ⊢s (Wk∘Wk)∘Id0 : Γ }} by mauto 2.
-    assert {{ Γ, B ⊢s Id ≈ Wk∘Id0 : Γ, B }} by mauto 3.
-    assert {{ Γ, B ⊢s Wk∘Id ≈ Wk∘(Wk∘Id0) : Γ }} by mauto 3.
-    assert {{ Γ, B ⊢s Wk∘Id ≈ (Wk∘Wk)∘Id0 : Γ }} by mauto 4.
-    assert {{ Γ, B, B[Wk] ⊢ #0 : B[Wk][Wk] }} by mauto 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 3.
-    assert {{ Γ, B ⊢s (Wk∘Wk)∘Id0 ≈ Wk∘(Wk∘Id0) : Γ }} by mauto 2.
-    assert {{ Γ, B ⊢s (Wk∘Wk)∘Id0 ≈ Wk∘Id : Γ }} by mauto 2.
-    assert {{ Γ, B ⊢ #0[Id0] ≈ #0 : B[Wk][Id] }} by mauto 3.
-    assert {{ Γ, B ⊢ #0 ≈ #0[Id] : B[Wk][Id] }} by mauto 3.
-    assert {{ Γ, B ⊢ #0[Id0] ≈ #0[Id] : B[Wk][Id] }} by mauto 2.
-    assert {{ Γ, B ⊢ #0[Id0] ≈ #0[Id] : B[Wk∘Id] }} by (eapply wf_exp_eq_conv; mauto 4).
-    assert {{ Γ, B ⊢ B[Wk∘Id] ≈ B[(Wk∘Wk)∘Id0] : Type@i }} by mauto 3.
-    assert {{ Γ, B ⊢ #0[Id0] ≈ #0[Id] : B[(Wk∘Wk)∘Id0] }} by mauto 3.
-    assert {{ Γ, B ⊢s (Wk∘Wk)∘Id0 ,, #0[Id0] ≈ Wk∘Id ,, #0[Id] : Γ, B }} by mauto 2.
-    assert {{ Γ, B ⊢s Wk∘Id ,, #0[Id] ≈ Id : Γ, B }} by mauto 4.
-    assert {{ Γ, B ⊢s q Wk ∘ Id0 ≈ Id : Γ, B }} by mauto 3.
-    assert {{ Γ, B ⊢ C[q Wk ∘ Id0] ≈ C[Id] : Type@i }} by mauto 3.
-    enough {{ Γ, B ⊢ M[Wk] #0 : C }}...
-
-  - econstructor...
-  - eapply wf_conv...
-  - assert {{ Γ ⊢s σ ,, M1[σ] : Δ, B}} by mauto.
-    assert {{ Δ , B ⊢ B[Wk] : Type@i }} by mauto 4.
-    assert {{ Δ , B , B[Wk] ⊢ B[Wk][Wk] : Type@i }} by mauto 4.
-    assert {{ Γ ⊢ B[Wk][σ ,, M1[σ]] : Type@i}} by mauto.
-    assert {{ Γ ⊢ B[Wk][σ ,, M1[σ]] ≈ B[σ] : Type@i}}.
-    {
-      transitivity {{{B[Wk ∘ (σ,,M1[σ])]}}};
-        [mauto | eapply exp_eq_sub_cong_typ2'; mauto].
-    }
-    assert {{ Γ ⊢ M2[σ] : B[Wk][σ ,, M1[σ]]}}.
-    {
-      eapply wf_conv with (A:={{{B[σ]}}});
-        mauto 2.
-    }
-    assert {{ Γ ⊢s σ ,, M1[σ] ,, M2[σ] : Δ, B, B[Wk]}} by mauto 4.
-    assert {{ Δ, B, B[Wk] ⊢ Eq (B[Wk][Wk]) # 1 # 0 : Type@i }} by (econstructor; mauto 4).
-
-    assert {{Γ ⊢ B[Wk][Wk][σ,,M1[σ],,M2[σ]] ≈ B[σ] : Type@i}}.
-    {
-      transitivity {{{B[Wk][Wk ∘ (σ,,M1[σ],,M2[σ])]}}};
-        [mauto 4 | transitivity {{{B[Wk][σ,,M1[σ]]}}}];
-        [| transitivity {{{B[Wk ∘ (σ,,M1[σ])]}}};
-           [mauto 4 | ]];
-        eapply exp_eq_sub_cong_typ2';
-        mauto 4.
-    }
-
-    eapply wf_conv;
-      [econstructor | |]; mauto 3.
-    + eapply exp_sub_typ; try eassumption.
-      econstructor; mauto 2.
-      eapply wf_conv; mauto 2.
-      transitivity {{{Eq (B[σ]) (M1[σ]) (M2[σ])}}};
-        [mauto 4 | symmetry].
-      etransitivity;
-        [econstructor; mauto |].
-
-      econstructor; eauto.
-      * eapply wf_exp_eq_conv; mauto 4 using sub_lookup_var1.
-      * eapply wf_exp_eq_conv;
-          [eapply sub_lookup_var0 with (B:=B)| |];
-          mauto 4.
-
-    + assert {{ Δ ⊢s Id ,, M1 : Δ, B}} by mauto 4.
-      assert {{ Δ , B ⊢ B[Wk] : Type@i }} by mauto 4.
-      assert {{ Δ , B , B[Wk] ⊢ B[Wk][Wk] : Type@i }} by mauto 4.
-      assert {{ Δ ⊢ B[Wk][Id,,M1] ≈ B : Type@i }}.
-      {
-        transitivity {{{B[Wk ∘ (Id,,M1)]}}};
-          [| transitivity {{{B[Id]}}}];
-          mauto 3.
-        eapply exp_eq_sub_cong_typ2'; mauto 3.
-      }
-      assert {{ Δ ⊢s Id ,, M1 ,, M2 : Δ, B , B[Wk]}}.
-      {
-        econstructor; mauto 3.
-        eapply wf_conv; mauto 2.
-      }
-      assert {{ Δ ⊢ B[Wk][Wk][Id ,, M1 ,, M2] ≈ B : Type@i }}.
-      {
-        transitivity {{{B[Wk][Wk ∘ (Id ,, M1 ,, M2)]}}};
-          [| transitivity {{{B[Wk][Id ,, M1]}}}];
-          mauto 4.
-        eapply exp_eq_sub_cong_typ2'; mauto 4.
-        eapply wf_sub_eq_p_extend; mauto 4.
-      }
-      assert {{ Δ ⊢L : (Eq (B[Wk][Wk]) #1 #0) [ Id ,, M1 ,, M2]}}.
-      {
-        eapply wf_conv; mauto 2.
-        symmetry.
-        etransitivity.
-        - eapply wf_exp_eq_eq_sub; mauto.
-        - econstructor; mauto 3.
-          + eapply wf_exp_eq_conv;
-              [eapply id_sub_lookup_var1 with (B:=B) | |];
-              mauto 4.
-          + eapply wf_exp_eq_conv;
-              [eapply id_sub_lookup_var0 with (B:=B) | |];
-              mauto 4.
-      }
-      assert {{ Δ ⊢s Id ,, M1 ,, M2 ,, L : Δ, B , B[Wk], Eq (B[Wk][Wk]) #1 #0}} by mauto 4.
-
-      transitivity {{{ C[(Id,,M1,,M2,,L) ∘ σ ] }}};
-        [eapply exp_eq_sub_compose_typ | eapply exp_eq_sub_cong_typ2'];
-        mauto 3.
-
-      transitivity {{{(Id,,M1,,M2) ∘ σ ,, L[σ]}}};
-        [econstructor; mauto 3 |].
-      econstructor; mauto 3.
-      * transitivity {{{(Id,,M1) ∘ σ ,, M2[σ]}}}.
-        econstructor; mauto 4.
-        econstructor; mauto 3.
-        eapply exp_eq_refl.
-        eapply wf_conv; mauto 3.
-        eapply exp_eq_sub_cong_typ2'; mauto 3.
-      * eapply exp_eq_refl.
-        eapply wf_conv; mauto 3.
-
-  - assert {{ Δ ⊢s Id ,, M1 : Δ, B}} by mauto 4.
-    assert {{ Δ , B ⊢ B[Wk] : Type@i }} by mauto 4.
-    assert {{ Δ , B , B[Wk] ⊢ B[Wk][Wk] : Type@i }} by mauto 4.
-    assert {{ Γ ⊢ B[Wk][σ ,, M1[σ]] : Type@i}} by mauto.
-    assert {{ Γ ⊢ B[σ] : Type @ i }} by mauto 3.
-    assert {{ Γ ⊢ M1[σ] : B[σ] }} by mauto 3.
-    assert {{ Γ ⊢ M2[σ] : B[σ] }} by mauto 3.
-    assert {{ Γ ⊢ B[Wk][σ ,, M1[σ]] ≈ B[σ] : Type@i}}.
-    {
-      transitivity {{{B[Wk ∘ (σ,,M1[σ])]}}};
-        [| eapply exp_eq_sub_cong_typ2']; mauto 4.
-    }
-    assert {{ Γ ⊢ M2[σ] : B[Wk][σ ,, M1[σ]]}} by mauto 3.
-    assert {{ Γ ⊢s σ,, M1[σ] : Δ,B}} by mauto 3.
-    assert {{ Γ ⊢s σ ,, M1[σ] ,, M2[σ] : Δ, B, B[Wk]}} by mauto 3.
-    assert {{ Δ, B, B[Wk] ⊢ Eq (B[Wk][Wk]) # 1 # 0 : Type@i }} by (econstructor; mauto 4).
-
-    assert {{Γ ⊢ B[Wk][Wk][σ,,M1[σ],,M2[σ]] ≈ B[σ] : Type@i}}.
-    {
-      transitivity {{{B[Wk][Wk ∘ (σ,,M1[σ],,M2[σ])]}}};
-        [mauto 4 | transitivity {{{B[Wk][σ,,M1[σ]]}}}];
-        mauto 2.
-      eapply exp_eq_sub_cong_typ2';
-        mauto 4.
-    }
-    assert {{ Γ ⊢ L[σ] : (Eq B M1 M2)[σ] }} by mauto 3.
-    assert {{ Γ ⊢ L[σ] : Eq (B[σ]) (M1[σ]) (M2[σ]) }} by (eapply wf_conv; mauto 3).
-    assert {{ Γ ⊢ #1[σ,,M1[σ],,M2[σ]] ≈ M1[σ] : B[Wk][Wk][σ,,M1[σ],,M2[σ]] }}.
-    {
-      eapply wf_exp_eq_conv;
-        [eapply sub_lookup_var1 with (B:=B) | |];
-        mauto 4.
-    }
-    assert {{ Γ ⊢ #0[σ,,M1[σ],,M2[σ]] ≈ M2[σ] : B[Wk][Wk][σ,,M1[σ],,M2[σ]] }}.
-    {
-      eapply wf_exp_eq_conv;
-        [eapply sub_lookup_var0 with (B:=B) | |];
-        mauto 4.
-    }
-    assert {{ Γ ⊢ L[σ] : (Eq (B[Wk][Wk]) #1 #0)[σ,,M1[σ],,M2[σ]] }}.
-    {
-      eapply wf_conv; mauto 2.
-      symmetry.
-      etransitivity.
-      - eapply wf_exp_eq_eq_sub; mauto.
-      - econstructor; mauto 3.
-    }
-    assert {{ Γ ⊢s σ,,M1[σ],,M2[σ],,L[σ] : Δ,B,B[Wk],Eq (B[Wk][Wk]) #1 #0}} by mauto 3.
-    assert {{Γ, B[σ] ⊢s q σ : Δ, B}} by mauto 4.
-    assert {{Γ, B[σ] ⊢ B[σ][Wk] : Type@i}} by mauto 4.
-    assert {{Γ, B[σ], B[σ][Wk] ⊢ B[σ][Wk][Wk] : Type@i}} by mauto.
-    assert {{Γ, B[σ], B[σ][Wk] ⊢ Eq (B[σ][Wk][Wk]) # 1 # 0 : Type@i }} by (econstructor; mauto 3; mauto).
-    assert {{Γ, B[σ] ⊢ B[Wk][q σ] ≈ B[σ][Wk] : Type@i}}.
-    {
-      transitivity {{{B[Wk ∘ q σ]}}};
-        [mauto 3 | transitivity {{{B[σ ∘ Wk]}}}];
-        [eapply exp_eq_sub_cong_typ2'; mauto 3 | mauto].
-    }
-    assert {{⊢ Γ, B[σ], B[Wk][q σ] ≈ Γ, B[σ], B[σ][Wk]}} by (econstructor; mauto 3).
-    assert {{Γ, B[σ], B[σ][Wk] ⊢s q (q σ) : Δ, B, B[Wk]}}.
-    {
-      eapply ctxeq_sub; [| eapply sub_q]; mauto 2.
-    }
-    assert {{Γ, B[σ],B[σ][Wk] ⊢ B[Wk][q σ ∘ Wk] : Type@i}} by mauto.
-    assert {{Γ, B[σ],B[σ][Wk] ⊢ B[Wk][q σ ∘ Wk] ≈ B[σ][Wk][Wk] : Type@i}}.
-    {
-      transitivity {{{B[Wk][q σ][Wk]}}};
-        [mauto |].
-      eapply exp_eq_sub_cong_typ1; mauto 3.
-    }
-    assert {{Γ, B[σ],B[σ][Wk] ⊢ B[Wk][Wk][q (q σ)] ≈ B[σ][Wk][Wk] : Type@i}}.
-    {
-      transitivity {{{B[Wk][Wk ∘ q (q σ)]}}};
-        [mauto 4| transitivity {{{B[Wk][q σ ∘ Wk]}}}];
-        [eapply exp_eq_sub_cong_typ2'; mauto 4 | trivial].
-    }
-    assert {{Γ, B[σ], B[σ][Wk] ⊢ #1 : B[σ][Wk][Wk]}} by mauto.
-    assert {{Γ, B[σ], B[σ][Wk] ⊢ Eq (B[σ][Wk][Wk]) #0 #0 : Type@i}} by (econstructor; mauto 3).
-    assert {{Γ, B[σ], B[σ][Wk] ⊢ (Eq (B[Wk][Wk]) #1 #0)[q (q σ)] ≈ Eq (B[σ][Wk][Wk]) #1 #0 : Type@i}}.
-    {
-      transitivity {{{Eq (B[Wk][Wk][q (q σ)]) (#1[q (q σ)]) (#0[q (q σ)])}}};
-        [econstructor; mauto 4 |].
-      econstructor; mauto 2.
-      - eapply wf_exp_eq_conv;
-          [eapply ctxeq_exp_eq;[eassumption | eapply exp_eq_var_1_sub_q_sigma] | |];
-          mauto 2.
-      - eapply wf_exp_eq_conv.
-        econstructor; [mauto 4 | eauto | eapply wf_conv; mauto].
-        + mauto 2.
-        + mauto 4.
-    }
-    assert {{Γ, B[σ], B[σ][Wk], Eq (B[σ][Wk][Wk]) #1 #0 ⊢s q (q (q σ)) : Δ, B, B[Wk], Eq (B[Wk][Wk]) #1 #0}}.
-    {
-      eapply ctxeq_sub; [| eapply sub_q]; mauto 2.
-      econstructor; mauto 3.
-    }
-    assert {{Γ, B[σ] ⊢s Id,,#0 : Γ, B[σ], B[σ][Wk]}} by mauto 4.
-    assert {{Γ, B[σ] ⊢ B[σ][Wk][Wk][Id,,#0] ≈ B[σ][Wk] : Type@i}}.
-    {
-      transitivity {{{B[σ][Wk][Wk ∘ (Id,,#0)]}}};
-        [mauto 4 |].
-      transitivity {{{B[σ][Wk][Id]}}};
-        [| mauto 3].
-      eapply exp_eq_sub_cong_typ2'; mauto 4.
-    }
-
-    assert {{Γ, B[σ] ⊢s Id,,#0,,refl (B[σ][Wk]) #0 : Γ, B[σ], B[σ][Wk], Eq (B[σ][Wk][Wk]) #1 #0}}.
-    {
-      econstructor; mauto 3.
-      eapply wf_conv;
-        [econstructor | |];
-        mauto 2.
-      - mauto 3.
-      - symmetry.
-        etransitivity; [econstructor; mauto 3 |].
-        econstructor; eauto.
-        + eapply wf_exp_eq_conv; mauto 2.
-          transitivity {{{#0[Id]}}}.
-          * eapply wf_exp_eq_conv; [econstructor | |];
-              mauto 3.
-            mauto 4.
-          * eapply wf_exp_eq_conv; mauto 4.
-        + eapply wf_exp_eq_conv;
-            [econstructor | |].
-          * mauto 3.
-          * mauto 2.
-          * mauto 4.
-          * mauto 2.
-          * etransitivity; mauto 2.
-    }
-    assert {{Γ, B[σ] ⊢s q (q σ) ∘ (Id,,#0) ≈ q σ,,#0 : Δ, B, B[Wk]}}.
-    {
-      eapply sub_eq_q_sigma_id_extend;
-        mauto 2.
-      eapply wf_conv; mauto 3.
-    }
-    assert {{Γ, B[σ] ⊢ #0 : B[σ][Wk][Wk][Id,,#0]}} by (eapply wf_conv; mauto 3).
-    assert {{Γ, B[σ] ⊢ #0[Id,,#0] ≈ #0 : B[σ][Wk][Id]}} by (econstructor; mauto 3).
-    assert {{Γ, B[σ] ⊢ #0[Id,,#0] ≈ #0 : B[σ][Wk]}} by mauto 3.
-    assert {{Γ, B[σ] ⊢ #0[Id,,#0] ≈ #0 : B[σ][Wk][Wk][Id,,#0]}} by mauto 4.
-    assert {{Γ, B[σ] ⊢ (Eq (B[σ][Wk][Wk]) #0 #0)[Id,,#0] ≈ Eq (B[σ][Wk]) #0 #0 : Type@i}}.
-    {
-      etransitivity; econstructor; mauto 3.
-    }
-    assert {{Γ, B[σ] ⊢s (q (q σ) ∘ Wk) ∘ (Id,,#0,,refl (B[σ][Wk]) #0) : Δ, B, B[Wk]}}.
-    {
-      econstructor; mauto 3.
-      econstructor; mauto 3.
-    }
-    assert {{Γ, B[σ] ⊢s (q (q σ) ∘ Wk) ∘ (Id,,#0,,refl (B[σ][Wk]) #0)
-                  ≈ q (q σ) ∘ (Id,,#0) : Δ, B, B[Wk]}}.
-    {
-      transitivity {{{q (q σ) ∘ (Wk ∘ (Id,,#0,,refl (B[σ][Wk]) #0))}}};
-        [mauto 4 |].
-      econstructor; mauto 3.
-      eapply wf_sub_eq_p_extend with (A:={{{Eq (B[σ][Wk][Wk]) #0 #0}}}); mauto 2.
-
-      eapply wf_conv;
-        [econstructor; mauto 3 | eapply exp_sub_typ; mauto 3 |].
-
-      symmetry.
-      etransitivity;
-        [econstructor; mauto 3 |].
-      econstructor; mauto 3.
-    }
-    assert {{Γ, B[σ] ⊢s (q (q σ) ∘ Wk) ∘ (Id,,#0,,refl (B[σ][Wk]) #0)
-                  ≈ q σ,,#0 : Δ, B, B[Wk]}} by mauto 4.
-    assert {{Γ, B[σ] ⊢ B[σ][Wk][Wk][Id,,#0] ≈ B[Wk][q σ] : Type@i}} by mauto 3.
-    assert {{Γ, B[σ] ⊢ B[Wk][Wk][q σ,,#0] ≈ B[Wk][q σ] : Type@i}}.
-    {
-      transitivity {{{B[Wk][Wk ∘ (q σ,,#0)]}}};
-        [eapply exp_eq_sub_compose_typ; mauto 4 |].
-      symmetry.
-      eapply exp_eq_sub_cong_typ2'; mauto 3.
-      symmetry.
-      mauto 4.
-    }
-    assert {{Γ, B[σ] ⊢s q σ,,#0 : Δ, B, B[Wk] }} by (econstructor; mauto 3).
-    assert {{Γ, B[σ] ⊢ B[Wk][Wk][q σ,,#0] : Type@i}} by mauto 3.
-    assert {{Γ, B[σ] ⊢ B[Wk][Wk][q σ,,#0] ≈ B[σ][Wk] : Type@i}} by mauto 4.
-    assert {{ Γ, B[σ] ⊢ #0[q σ,,#0] ≈ # 0 : B[σ][Wk] }}.
-    {
-      eapply wf_exp_eq_conv;
-        [econstructor | |];
-        mauto 2.
-      mauto 3.
-    }
-    assert {{ Γ, B[σ] ⊢ #0[q σ,,#0] ≈ # 0 : B[Wk][Wk][q σ,,#0] }} by mauto 3.
-
-    assert {{ Γ, B[σ] ⊢s σ ∘ Wk : Δ }} by mauto 4.
-    assert {{ Γ, B[σ] ⊢ # 0 : B[σ][Wk] }} by mauto 2.
-    assert {{ Γ, B[σ] ⊢ B[σ][Wk] ≈ B[σ ∘ Wk] : Type@i }} by mauto 4.
-    assert {{ Γ, B[σ] ⊢ # 0 : B[σ ∘ Wk] }} by mauto 3.
-
-    assert {{ Γ, B[σ] ⊢ #1[q σ,,#0] ≈ # 0 : B[σ][Wk] }}.
-    {
-      eapply wf_exp_eq_conv with (A:={{{B[σ ∘ Wk]}}});
-        [eapply sub_lookup_var1; eauto | |];
-        mauto 2.
-    }
-    assert {{ Γ, B[σ] ⊢ #1[q σ,,#0] ≈ # 0 : B[Wk][Wk][q σ,,#0] }} by mauto 3.
-
-    assert {{Γ, B[σ] ⊢s q (q (q σ)) ∘ (Id,,#0,,refl (B[σ][Wk]) #0)
-                  ≈ (q (q σ) ∘ (Id,,#0)),,refl (B[σ][Wk]) #0
-          : Δ, B, B[Wk], Eq (B[Wk][Wk]) # 1 # 0}}.
-    {
-      etransitivity;
-        [eapply wf_sub_eq_extend_compose; mauto 2; mauto 4 |].
-
-      - eapply wf_conv; mauto 3.
-        + mauto.
-        + symmetry.
-          transitivity {{{(Eq (B[Wk][Wk]) #1 #0)[q (q σ)][Wk]}}};
-            [mauto |].
-          eapply exp_eq_sub_cong_typ1; mauto 4.
-      - econstructor; mauto 3.
-
-        eapply wf_exp_eq_conv.
-        econstructor; mauto 3.
-        + eapply wf_conv; [econstructor | |]; mauto 3.
-        + eapply exp_sub_typ; mauto 3.
-        + etransitivity; eauto.
-          symmetry.
-          etransitivity; [| etransitivity].
-          * eapply exp_eq_sub_cong_typ2'; mauto 3.
-          * econstructor; mauto 4.
-          * econstructor; mauto 2.
-    }
-
-    assert {{⊢ Δ, B, B[Wk]}} by mauto 3.
-    assert {{Δ, B, B[Wk] ⊢ #0 : B[Wk][Wk]}} by mauto 4.
-    assert {{Δ, B, B[Wk] ⊢ #1 : B[Wk][Wk]}} by mauto 4.
-    assert {{Γ, B[σ] ⊢ B[Wk][Wk][q (q σ) ∘ (Id,,#0)] ≈ B[Wk][q σ] : Type@i}} by mauto 4.
-    assert {{Γ, B[σ] ⊢ B[Wk][Wk][q (q σ) ∘ (Id,,#0)] ≈ B[σ][Wk] : Type@i}} by mauto 4.
-
-    assert {{ Γ, B[σ] ⊢ #0[q (q σ) ∘ (Id,,#0)] ≈ # 0 : B[σ][Wk] }}.
-    {
-      transitivity {{{#0[q σ,,#0]}}}.
-      - symmetry.
-        eapply wf_exp_eq_conv;
-          [econstructor | |]; mauto 2.
-      - eauto.
-    }
-    assert {{ Γ, B[σ] ⊢ #0[q (q σ) ∘ (Id,,#0)] ≈ # 0 : B[Wk][Wk][q (q σ) ∘ (Id,,#0)] }} by
-      (eapply wf_exp_eq_conv; mauto 3).
-
-    assert {{ Γ, B[σ] ⊢ #1[q (q σ) ∘ (Id,,#0)] ≈ # 0 : B[σ][Wk] }}.
-    {
-      transitivity {{{#1[q σ,,#0]}}}.
-      - symmetry.
-        eapply wf_exp_eq_conv;
-          [econstructor | |]; mauto 2.
-      - eauto.
-    }
-    assert {{ Γ, B[σ] ⊢ #1[q (q σ) ∘ (Id,,#0)] ≈ # 0 : B[Wk][Wk][q (q σ) ∘ (Id,,#0)] }} by
-      (eapply wf_exp_eq_conv; mauto 3).
-
-    assert {{Γ, B[σ] ⊢s q (q (q σ)) ∘ (Id,,#0,,refl (B[σ][Wk]) #0)
-                  ≈ q σ,,#0,,refl (B[σ][Wk]) #0 : Δ, B, B[Wk], Eq (B[Wk][Wk]) # 1 # 0}}.
-    {
-      etransitivity; eauto.
-      econstructor; mauto 3.
-      eapply exp_eq_refl.
-      eapply wf_conv; mauto 3.
-      symmetry.
-      etransitivity.
-      - econstructor; mauto 2.
-      - econstructor; mauto 2.
-    }
-
-    assert {{Γ, B[σ] ⊢s Id ∘ q σ : Δ, B}} by mauto 3.
-    assert {{Γ, B[σ] ⊢s Id ∘ q σ ≈ q σ : Δ, B}} by mauto 3.
-    assert {{Γ, B[σ] ⊢ #0[q σ] ≈ #0 : B[σ ∘ Wk]}} by mauto 3.
-    assert {{Γ, B[σ] ⊢ #0[q σ] ≈ #0 : B[σ][Wk]}} by mauto 3.
-    assert {{Γ, B[σ] ⊢ #0[q σ] ≈ #0 : B[Wk][q σ]}} by mauto 4.
-    assert {{Γ, B[σ] ⊢s (Id,,#0) ∘ q σ : Δ, B, B[Wk]}} by (econstructor; mauto 3).
-    assert {{Γ, B[σ] ⊢s (Id,,#0) ∘ q σ ≈ q σ,,#0 : Δ, B, B[Wk]}}.
-    {
-      etransitivity.
-      - eapply wf_sub_eq_extend_compose; mauto 3.
-      - econstructor; mauto 3.
-        eapply wf_exp_eq_conv; mauto 2.
-        eapply exp_eq_sub_cong_typ2'; mauto 3.
-    }
-
-    assert {{Δ, B ⊢ B[Wk][Wk][Id,,#0] ≈ B[Wk] : Type@i }}.
-    {
-      transitivity {{{B[Wk][Wk ∘ (Id,,#0)]}}}; [ |transitivity{{{B[Wk][Id]}}}].
-      - eapply exp_eq_sub_compose_typ; mauto 3.
-      - eapply exp_eq_sub_cong_typ2'; mauto 3.
-        econstructor; mauto 3.
-      - mauto 3.
-    }
-    assert {{Δ, B ⊢ #0[Id ,, #0] ≈ #0 : B[Wk]}}.
-    {
-      eapply wf_exp_eq_conv;
-      [econstructor | |]; mauto 3.
-    }
-    assert {{Δ, B ⊢ B[Wk][Wk][Id,,#0] : Type@i }} by (eapply exp_sub_typ; mauto 3).
-    assert {{Δ, B ⊢ #0[Id ,, #0] ≈ #0 : B[Wk][Wk][Id,,#0]}} by (eapply wf_exp_eq_conv; mauto 2).
-    assert {{Δ, B ⊢ #1[Id ,, #0] ≈ #0 : B[Wk]}}.
-    {
-      transitivity {{{#0[Id]}}}; mauto 3.
-      eapply wf_exp_eq_conv;
-        [econstructor | |]; mauto 3.
-      eapply wf_conv; mauto 3.
-      symmetry.
-      mauto 3.
-    }
-    assert {{Δ, B ⊢ #1[Id ,, #0] ≈ #0 : B[Wk][Wk][Id,,#0]}} by (eapply wf_exp_eq_conv; mauto 2).
-
-    assert {{Δ, B ⊢ refl (B[Wk]) #0 : (Eq (B[Wk][Wk]) #1 #0)[Id ,, #0]}}.
-    {
-      eapply wf_conv; mauto 3.
-      - mauto 4.
-      - symmetry.
-        etransitivity.
-        + econstructor; mauto 3.
-        + econstructor; mauto 3.
-    }
-
-    assert {{ Γ, B[σ] ⊢ (Eq B[Wk] #0 #0)[q σ] ≈ Eq B[σ][Wk] #0 #0 : Type@i }}.
-    {
-      etransitivity;
-        [econstructor; mauto 2 |];
-        mauto 3.
-    }
-
-    assert {{ Γ, B[σ] ⊢ B[Wk][Wk][(Id,,#0)∘q σ] ≈ B[σ][Wk] : Type@i }} by mauto 3.
-
-    assert {{ Γ, B[σ] ⊢ #1[(Id,,#0)∘q σ] ≈ #0 : B[σ][Wk] }}.
-    {
-      transitivity {{{#1[q σ,,#0]}}};
-        [eapply wf_exp_eq_conv |];
-        mauto 3.
-    }
-    assert {{ Γ, B[σ] ⊢ #1[(Id,,#0)∘q σ] ≈ #0 : B[Wk][Wk][(Id,,#0)∘q σ] }} by mauto 4.
-
-    assert {{ Γ, B[σ] ⊢ #0[(Id,,#0)∘q σ] ≈ #0 : B[σ][Wk] }}.
-    {
-      transitivity {{{#0[q σ,,#0]}}};
-        [eapply wf_exp_eq_conv |];
-        mauto 3.
-    }
-    assert {{ Γ, B[σ] ⊢ #0[(Id,,#0)∘q σ] ≈ #0 : B[Wk][Wk][(Id,,#0)∘q σ] }} by mauto 4.
-
-    assert {{ Γ, B[σ] ⊢ (Eq B[Wk][Wk] #1 #0)[(Id,,#0)∘q σ] ≈ Eq B[σ][Wk] #0 #0 : Type@i }}.
-    {
-      etransitivity; econstructor; mauto 2.
-    }
-
-    assert {{Γ, B[σ] ⊢s (Id,,#0,,refl (B[Wk]) #0) ∘ q σ
-                  ≈ q σ,,#0,,refl (B[σ][Wk]) #0 : Δ, B, B[Wk], Eq (B[Wk][Wk]) # 1 # 0}}.
-    {
-      etransitivity.
-      - eapply wf_sub_eq_extend_compose; mauto 3.
-      - econstructor; mauto 2.
-        etransitivity.
-        + eapply wf_exp_eq_conv;
-            [eapply wf_exp_eq_refl_sub; mauto 3 |
-             eapply exp_sub_typ; mauto 3 |].
-          mauto 3.
-        + eapply wf_exp_eq_conv;
-            [econstructor | |];
-            mauto 2.
-          etransitivity; mauto 2.
-    }
-
-    assert {{ Δ, B ⊢s Id,,#0,,refl B[Wk] #0 : ((Δ, B), B[Wk]), Eq B[Wk][Wk] #1 #0 }} by mauto 4.
-
-    assert {{ Γ ⊢s Id,,M1[σ] : Γ,B[σ]}} by mauto 2.
-    assert {{ Γ ⊢ B[σ][Wk][Id ,, M1[σ]] ≈ B[σ] : Type@i}}.
-    {
-      etransitivity;
-        [eapply exp_eq_sub_compose_typ; mauto 3 |];
-        transitivity {{{B[σ][Id]}}}; mauto 2.
-      symmetry.
-      eapply exp_eq_sub_cong_typ2';
-        mauto 3.
-    }
-    assert {{ Γ ⊢ M2[σ] : B[σ][Wk][Id ,, M1[σ]]}} by mauto 4.
-    assert {{ Γ ⊢s Id ,, M1[σ] ,, M2[σ] : Γ, B[σ], B[σ][Wk]}} by mauto 3.
-
-    assert {{ Γ ⊢ B[σ][Wk][Wk][Id,,M1[σ],,M2[σ]] ≈ B[σ] : Type@i }}.
-    {
-      etransitivity;
-        [eapply exp_eq_sub_compose_typ; mauto 3 |];
-        transitivity {{{B[σ][Wk][Id,,M1[σ]]}}}; mauto 3.
-      symmetry.
-      eapply exp_eq_sub_cong_typ2';
-        mauto 3.
-    }
-
-    assert {{ Γ ⊢ #1[Id,,M1[σ],,M2[σ]] ≈ M1[σ] : B[σ] }}.
-    {
-      transitivity {{{#0[Id,,M1[σ]]}}};
-        [eapply wf_exp_eq_conv | eapply wf_exp_eq_conv; econstructor];
-        mauto 3.
-    }
-    assert {{ Γ ⊢ #1[Id,,M1[σ],,M2[σ]] ≈ M1[σ] : B[σ][Wk][Wk][Id,,M1[σ],,M2[σ]] }} by mauto 4.
-
-    assert {{ Γ ⊢ #0[Id,,M1[σ],,M2[σ]] ≈ M2[σ] : B[σ] }}
-      by (eapply wf_exp_eq_conv; mauto 3).
-    assert {{ Γ ⊢ #0[Id,,M1[σ],,M2[σ]] ≈ M2[σ] : B[σ][Wk][Wk][Id,,M1[σ],,M2[σ]] }} by mauto 4.
-
-    assert {{ Γ ⊢ (Eq B[σ][Wk][Wk] #1 #0)[Id ,, M1[σ] ,, M2[σ]] ≈ Eq B[σ] M1[σ] M2[σ] : Type@i }}
-      by (etransitivity; econstructor; mauto 3).
-    assert {{ Γ ⊢ L[σ] : (Eq B[σ][Wk][Wk] #1 #0)[Id ,, M1[σ] ,, M2[σ]] }} by mauto 4.
-
-    assert {{ Γ ⊢s Id ,, M1[σ] ,, M2[σ] ,, L[σ] : Γ, B[σ], B[σ][Wk], Eq B[σ][Wk][Wk] #1 #0}} by mauto 3.
-
-    assert {{ (Γ, B[σ]), B[σ][Wk] ⊢ B[Wk][q σ∘Wk] ≈ B[σ][Wk][Wk] : Type@i }}.
-    {
-      transitivity {{{B[Wk][q σ][Wk]}}};
-        [symmetry;
-         eapply exp_eq_sub_compose_typ; mauto 3 |].
-      eapply exp_eq_sub_cong_typ1; mauto 3.
-    }
-
-    assert {{ (Γ, B[σ]), B[σ][Wk] ⊢ #0 : B[Wk][q σ∘Wk] }}
-      by (eapply wf_conv; mauto 3).
-
-    assert {{ ((Γ, B[σ]), B[σ][Wk]), Eq B[σ][Wk][Wk] #1 #0 ⊢s q (q σ)∘Wk : Δ,B,B[Wk] }} by mauto 4.
-    assert {{ ((Γ, B[σ]), B[σ][Wk]), Eq B[σ][Wk][Wk] #1 #0 ⊢ (Eq B[Wk][Wk] #1 #0)[q (q σ)∘Wk] ≈ (Eq B[σ][Wk][Wk] #1 #0)[Wk] : Type@i }}.
-    {
-      transitivity {{{(Eq B[Wk][Wk] #1 #0)[q (q σ)][Wk]}}};
-        [symmetry;
-         eapply exp_eq_sub_compose_typ; mauto 3 |].
-      eapply exp_eq_sub_cong_typ1; mauto 3.
-    }
-
-
-    assert {{ Δ,B,B[Wk] ⊢ Eq B[Wk][Wk] #1 #0 : Type@i }} by mauto 3.
-    assert {{ ((Γ, B[σ]), B[σ][Wk]), Eq B[σ][Wk][Wk] #1 #0 ⊢ #0 : (Eq B[Wk][Wk] #1 #0)[q (q σ)∘Wk] }}.
-    {
-      eapply wf_conv; mauto 3.
-    }
-
-    assert {{ Γ ⊢s (q σ ∘ Wk) ∘ (Id,,M1[σ],,M2[σ]) : Δ, B }}
-             by (econstructor; mauto 4).
-    assert {{ Γ ⊢s (q σ ∘ Wk) ∘ (Id,,M1[σ],,M2[σ]) ≈ σ,,M1[σ] : Δ, B }}.
-    {
-      etransitivity;
-        [eapply wf_sub_eq_compose_assoc; mauto 3 |].
-      etransitivity;
-        [eapply wf_sub_eq_compose_cong;
-         [eapply wf_sub_eq_p_extend with (A:={{{B[σ][Wk]}}}) | eapply sub_eq_refl]  |];
-        mauto 3.
-    }
-
-    assert {{ Γ ⊢ B[Wk][(q σ∘Wk)∘(Id,,M1[σ],,M2[σ])] ≈ B[σ] : Type@i }}.
-    {
-      transitivity {{{B[Wk][σ,,M1[σ]]}}};
-        [eapply exp_eq_sub_cong_typ2' |]; mauto 3.
-    }
-    assert {{ Γ ⊢ #0[Id,,M1[σ],,M2[σ]] ≈ M2[σ] : B[Wk][(q σ∘Wk)∘(Id,,M1[σ],,M2[σ])] }} by mauto 4.
-    assert {{ Γ ⊢s q (q σ) ∘ (Id,,M1[σ],,M2[σ]) ≈ σ,,M1[σ],,M2[σ] : Δ, B, B[Wk] }}.
-    {
-      etransitivity;
-        [eapply wf_sub_eq_extend_compose; mauto 4 |].
-      econstructor; mauto 2.
-    }
-    assert {{ Γ ⊢s (q (q σ)∘Wk)∘(Id,,M1[σ],,M2[σ],,L[σ]) : (Δ, B), B[Wk] }}
-      by (econstructor; mauto 4).
-    assert {{ Γ ⊢s (q (q σ) ∘ Wk) ∘ (Id,,M1[σ],,M2[σ],,L[σ]) ≈ σ,,M1[σ],,M2[σ] : Δ, B, B[Wk] }}.
-    {
-      etransitivity;
-        [eapply wf_sub_eq_compose_assoc; mauto 3 |].
-      etransitivity;
-        [eapply wf_sub_eq_compose_cong;
-         [eapply wf_sub_eq_p_extend with (A:={{{Eq B[σ][Wk][Wk] #1 #0}}}) | eapply sub_eq_refl]  |];
-        mauto 3.
-    }
-
-    assert {{ Γ ⊢ (Eq B[Wk][Wk] #1 #0)[σ,,M1[σ],,M2[σ]] ≈ Eq B[σ] M1[σ] M2[σ] : Type@i }}.
-    {
-      etransitivity;
-        econstructor; mauto 3.
-    }
-    assert {{ Γ ⊢ (Eq B[Wk][Wk] #1 #0)[(q (q σ)∘Wk)∘(Id,,M1[σ],,M2[σ],,L[σ])] ≈ Eq B[σ] M1[σ] M2[σ] : Type@i }}.
-    {
-      transitivity {{{(Eq B[Wk][Wk] #1 #0)[σ,,M1[σ],,M2[σ]]}}};
-        [eapply exp_eq_sub_cong_typ2' |]; mauto 3.
-    }
-    assert {{ Γ ⊢ #0[Id,,M1[σ],,M2[σ],,L[σ]] ≈ L[σ] : (Eq B[Wk][Wk] #1 #0)[(q (q σ)∘Wk)∘(Id,,M1[σ],,M2[σ],,L[σ])] }}.
-    {
-      eapply wf_exp_eq_conv with (A:={{{Eq B[σ] M1[σ] M2[σ]}}});
-        econstructor; mauto 3.
-    }
-    assert {{ Γ ⊢s q (q (q σ)) ∘ (Id,,M1[σ],,M2[σ],,L[σ]) ≈ σ,,M1[σ],,M2[σ],,L[σ] : Δ, B, B[Wk], Eq B[Wk][Wk] #1 #0 }}.
-    {
-      etransitivity;
-        [eapply wf_sub_eq_extend_compose; mauto 4 |].
-      econstructor; mauto 2.
-    }
-
-    assert {{Γ, B[σ] ⊢s (Id,,#0,,refl (B[Wk]) #0) ∘ q σ
-                  ≈ q (q (q σ)) ∘ (Id,,#0,,refl (B[σ][Wk]) #0)
-          : Δ, B, B[Wk], Eq (B[Wk][Wk]) # 1 # 0}} by mauto 3.
-
-    eapply wf_conv;
-    [econstructor | |];
-      mauto 2.
-    + eapply wf_conv; mauto 3.
-    + etransitivity;
-        [eapply exp_eq_sub_compose_typ | eapply exp_eq_sub_cong_typ2'];
-        mauto 3.
-
-  - eexists.
-    eapply exp_sub_typ; mauto 2.
-    assert {{ Δ ⊢s Id ,, M1 : Δ, B}} by mauto 4.
-    assert {{ Δ , B ⊢ B[Wk] : Type@i }} by mauto 4.
-    assert {{ Δ , B , B[Wk] ⊢ B[Wk][Wk] : Type@i }} by mauto 4.
-    assert {{ Γ ⊢ B[Wk][σ ,, M1[σ]] : Type@i}} by mauto.
-    assert {{ Γ ⊢ B[σ] : Type @ i }} by mauto 3.
-    assert {{ Γ ⊢ M1[σ] : B[σ] }} by mauto 3.
-    assert {{ Γ ⊢ M2[σ] : B[σ] }} by mauto 3.
-    assert {{ Γ ⊢ B[Wk][σ ,, M1[σ]] ≈ B[σ] : Type@i}}.
-    {
-      transitivity {{{B[Wk ∘ (σ,,M1[σ])]}}};
-        [| eapply exp_eq_sub_cong_typ2']; mauto 4.
-    }
-    assert {{ Γ ⊢ M2[σ] : B[Wk][σ ,, M1[σ]]}} by mauto 3.
-    assert {{ Γ ⊢s σ,, M1[σ] : Δ,B}} by mauto 3.
-    assert {{ Γ ⊢s σ ,, M1[σ] ,, M2[σ] : Δ, B, B[Wk]}} by mauto 3.
-    assert {{ Δ, B, B[Wk] ⊢ Eq (B[Wk][Wk]) # 1 # 0 : Type@i }} by (econstructor; mauto 4).
-
-    assert {{Γ ⊢ B[Wk][Wk][σ,,M1[σ],,M2[σ]] ≈ B[σ] : Type@i}}.
-    {
-      transitivity {{{B[Wk][Wk ∘ (σ,,M1[σ],,M2[σ])]}}};
-        [mauto 4 | transitivity {{{B[Wk][σ,,M1[σ]]}}}];
-        mauto 2.
-      eapply exp_eq_sub_cong_typ2';
-        mauto 4.
-    }
-    assert {{ Γ ⊢ L[σ] : (Eq B M1 M2)[σ] }} by mauto 3.
-    assert {{ Γ ⊢ L[σ] : Eq (B[σ]) (M1[σ]) (M2[σ]) }} by (eapply wf_conv; mauto 3).
-    assert {{ Γ ⊢ L[σ] : (Eq (B[Wk][Wk]) #1 #0)[σ,,M1[σ],,M2[σ]] }}.
-    {
-      eapply wf_conv; mauto 2.
-      symmetry.
-      etransitivity.
-      - eapply wf_exp_eq_eq_sub; mauto.
-      - econstructor; mauto 3.
-        + eapply wf_exp_eq_conv;
-            [eapply sub_lookup_var1 with (B:=B) | |];
-            mauto 4.
-        + eapply wf_exp_eq_conv;
-            [eapply sub_lookup_var0 with (B:=B) | |];
-            mauto 4.
-    }
-    mauto 3.
-
-  - eapply wf_conv; [mauto 3 | mauto 2 |].
-    symmetry. mauto 3.
-
-  - assert {{ Γ ⊢s Id ,, M1 : Γ, B}} by mauto 4.
-    assert {{ Γ , B ⊢ B[Wk] : Type@i }} by mauto 4.
-    assert {{ Γ , B , B[Wk] ⊢ B[Wk][Wk] : Type@i }} by mauto 4.
-    assert {{ Γ ⊢ B[Wk][Id,,M1] ≈ B : Type@i }}.
-    {
-      transitivity {{{B[Wk ∘ (Id,,M1)]}}};
-        [| transitivity {{{B[Id]}}}];
-        mauto 3.
-      eapply exp_eq_sub_cong_typ2'; mauto 3.
-    }
-    assert {{ Γ ⊢s Id ,, M1 ,, M2 : Γ, B , B[Wk]}}.
-    {
-      econstructor; mauto 3.
-      eapply wf_conv; mauto 2.
-    }
-    assert {{ Γ ⊢ B[Wk][Wk][Id ,, M1 ,, M2] ≈ B : Type@i }}.
-    {
-      transitivity {{{B[Wk][Wk ∘ (Id ,, M1 ,, M2)]}}};
-        [| transitivity {{{B[Wk][Id ,, M1]}}}];
-        mauto 4.
-      eapply exp_eq_sub_cong_typ2'; mauto 4.
-      eapply wf_sub_eq_p_extend; mauto 4.
-    }
-    assert {{ Γ, B, B[Wk] ⊢ Eq (B[Wk][Wk]) # 1 # 0 : Type@i }} by (econstructor; mauto 4).
-    assert {{ Γ ⊢ #1[Id,,M1,,M2] ≈ M1 : B[Wk][Wk][Id,,M1,,M2] }}.
-    {
-      eapply wf_exp_eq_conv;
-        [eapply id_sub_lookup_var1 with (B:=B) | |];
-        mauto 4.
-    }
-    assert {{ Γ ⊢ #0[Id,,M1,,M2] ≈ M2 : B[Wk][Wk][Id,,M1,,M2] }}.
-    {
-      eapply wf_exp_eq_conv;
-        [eapply id_sub_lookup_var0 with (B:=B) | |];
-        mauto 4.
-    }
-    assert {{ Γ ⊢L : (Eq (B[Wk][Wk]) #1 #0) [ Id ,, M1 ,, M2]}}.
-    {
-      eapply wf_conv; mauto 2.
-      symmetry.
-      etransitivity.
-      - eapply wf_exp_eq_eq_sub; mauto.
-      - econstructor; mauto 3.
-    }
-    assert {{ Γ ⊢s Id ,, M1 ,, M2 ,, L : Γ, B , B[Wk], Eq (B[Wk][Wk]) #1 #0}} by mauto 4.
-    assert {{ Γ ⊢ Eq B' M1' M2' : Type @ i }} by mauto 4.
-    assert {{ Γ ⊢ Eq B' M1' M2' ≈ Eq B M1 M2 : Type @ i }} by (symmetry; mauto 3).
-
-    assert {{ ⊢ Γ, B ≈ Γ, B' }} by mauto 3.
-    assert {{ Γ , B ⊢ B'[Wk] : Type@i }} by mauto 4.
-    assert {{ Γ , B' ⊢ B'[Wk] : Type@i }} by mauto 4.
-    assert {{ Γ, B ⊢ B[Wk] ≈ B'[Wk] : Type@i }} by mauto 3.
-    assert {{ Γ, B' ⊢ B[Wk] ≈ B'[Wk] : Type@i }} by mauto 3.
-    assert {{ ⊢ Γ, B, B[Wk] ≈ Γ, B', B'[Wk] }} by mauto 4.
-
-    assert {{ Γ, B', B'[Wk] ⊢ Eq (B[Wk][Wk]) # 1 # 0 : Type@i }} by mauto 3.
-    assert {{ Γ, B', B'[Wk] ⊢ Eq (B'[Wk][Wk]) # 1 # 0 : Type@i }} by (econstructor; mauto 4).
-    assert {{ Γ, B, B[Wk] ⊢ Eq (B'[Wk][Wk]) # 1 # 0 : Type@i }} by mauto 3.
-    assert {{ (Γ, B), B[Wk] ⊢ Eq B[Wk][Wk] #1 #0 ≈ Eq B'[Wk][Wk] #1 #0 : Type@i }} by (econstructor; mauto 4).
-
-    assert {{ ⊢ Γ, B, B[Wk], Eq (B[Wk][Wk]) #1 #0 ≈ Γ, B', B'[Wk], Eq (B'[Wk][Wk]) #1 #0 }} by mauto 3.
-
-    assert {{ Γ, B ⊢ Eq B[Wk] #0 #0 : Type@i }} by (econstructor; mauto 2).
-    assert {{ Γ, B ⊢ Eq B'[Wk] #0 #0 ≈ Eq B[Wk] #0 #0 : Type@i }} by (econstructor; mauto 3).
-
-    assert {{ Γ, B ⊢ refl B'[Wk] #0 : Eq (B[Wk]) #0 #0 }}.
-    {
-      eapply wf_conv;
-      [econstructor | |]; mauto 3.
-    }
-    assert {{ Γ, B ⊢ refl B[Wk] #0 : Eq (B[Wk]) #0 #0 }} by mauto 4.
-    assert {{ Γ, B ⊢ refl B[Wk] #0 ≈ refl B'[Wk] #0 : Eq (B[Wk]) #0 #0 }} by mauto 3.
-    assert {{ Γ, B ⊢s Id,,#0 : Γ, B, B[Wk] }} by mauto 3.
-    assert {{ (Γ, B), B[Wk] ⊢ #1 : B[Wk][Wk] }} by mauto 4.
-    assert {{ Γ, B ⊢s Wk∘(Id,,#0) : Γ, B }} by (econstructor; mauto 3).
-    assert {{ Γ, B ⊢ B[Wk][Wk][Id,,#0] ≈ B[Wk] : Type@i }}.
-    {
-      transitivity {{{B[Wk][Wk ∘ (Id,,#0)]}}};
-        [eapply exp_eq_sub_compose_typ |
-         transitivity {{{B[Wk][Id]}}} ];
-        mauto 3.
-      eapply exp_eq_sub_cong_typ2'; mauto 3.
-    }
-    assert {{ Γ, B ⊢ #1[Id,,#0] ≈ #0 : B[Wk] }}.
-    {
-      transitivity {{{#0[Id]}}}.
-      - eapply wf_exp_eq_conv;
-          [eapply wf_exp_eq_var_S_sub with (A:={{{B[Wk]}}}) | |];
-          mauto 3.
-      - mauto 3.
-    }
-    assert {{ Γ, B ⊢ #1[Id,,#0] ≈ #0 : B[Wk][Wk][Id,,#0] }} by mauto 4.
-    assert {{ Γ, B ⊢ #0[Id,,#0] ≈ #0 : B[Wk] }}.
-    {
-      eapply wf_exp_eq_conv;
-        [eapply wf_exp_eq_var_0_sub with (A:={{{B[Wk]}}}) | |];
-        mauto 3.
-    }
-    assert {{ Γ, B ⊢ #0[Id,,#0] ≈ #0 : B[Wk][Wk][Id,,#0] }} by mauto 4.
-    assert {{ Γ, B ⊢ (Eq B[Wk][Wk] #1 #0)[Id,,#0] ≈ Eq (B[Wk]) #0 #0 : Type@i }}.
-    {
-      etransitivity; econstructor; mauto 3.
-    }
-    assert {{ Γ, B ⊢ refl B'[Wk] #0 : (Eq B[Wk][Wk] #1 #0)[Id,,#0] }} by mauto 4.
-    assert {{ Γ, B ⊢ refl B[Wk] #0 : (Eq B[Wk][Wk] #1 #0)[Id,,#0] }} by mauto 4.
-    assert {{ Γ, B ⊢s Id,,#0,,refl B'[Wk] #0 : Γ, B, B[Wk], Eq (B[Wk][Wk]) #1 #0 }} by mauto 4.
-    assert {{ Γ, B ⊢s Id,,#0,,refl B[Wk] #0 : Γ, B, B[Wk], Eq (B[Wk][Wk]) #1 #0 }} by mauto 4.
-
-    assert {{ Γ, B ⊢s Id,,#0,,refl B[Wk] #0 ≈ Id,,#0,,refl B'[Wk] #0 : Γ, B, B[Wk], Eq (B[Wk][Wk]) #1 #0 }}
-      by (econstructor; mauto 4).
-
-    assert {{ Γ, B ⊢ C[Id,,#0,,refl B[Wk] #0] ≈ C'[Id,,#0,,refl B'[Wk] #0] : Type@j }}.
-    {
-      etransitivity;
-        [eapply exp_eq_sub_cong_typ2' |
-          eapply exp_eq_sub_cong_typ1];
-        mauto 3.
-    }
-
-    assert {{ Γ ⊢ M1 ≈ M1' : B[Id] }} by (eapply wf_exp_eq_conv; mauto 3).
-    assert {{ Γ ⊢s Id,,M1 ≈ Id,,M1' : Γ, B }} by mauto 3.
-    assert {{ Γ ⊢ M2 ≈ M2' : B[Wk][Id,,M1] }} by (eapply wf_exp_eq_conv; mauto 3).
-    assert {{ Γ ⊢s Id,,M1,,M2 ≈ Id,,M1',,M2' : Γ, B, B[Wk] }} by mauto 3.
-
-    assert {{ Γ ⊢ (Eq B[Wk][Wk] #1 #0)[Id,,M1,,M2] ≈ Eq B M1 M2 : Type@i }}.
-    {
-      etransitivity;
-        econstructor; mauto 3.
-    }
-    assert {{ Γ ⊢s Id,,M1,,M2,,L ≈ Id,,M1',,M2',,L' : Γ, B, B[Wk], Eq (B[Wk][Wk]) #1 #0 }}
-      by (econstructor; mauto 4).
-
-    assert {{ Γ ⊢s Id ,, M1' : Γ, B}} by mauto 4.
-    assert {{ Γ ⊢ B[Wk][Id,,M1'] ≈ B : Type@i }}.
-    {
-      transitivity {{{B[Wk ∘ (Id,,M1')]}}};
-        [| transitivity {{{B[Id]}}}];
-        mauto 3.
-      eapply exp_eq_sub_cong_typ2'; mauto 3.
-    }
-    assert {{ Γ ⊢ M2' : B[Wk][Id,,M1'] }} by mauto 4.
-    assert {{ Γ ⊢s Id,,M1',,M2' : Γ, B, B[Wk]}} by mauto 3.
-
-    assert {{ Γ ⊢ (Eq B[Wk][Wk] #1 #0)[Id,,M1',,M2'] ≈ Eq B M1 M2 : Type@i }}.
-    {
-      etransitivity;
-        [eapply exp_eq_sub_cong_typ2' | ];
-        cycle 1.
-      - eauto.
-      - symmetry. eauto.
-      - eauto.
-      - eauto.
-    }
-    assert {{ Γ ⊢ L' : (Eq B[Wk][Wk] #1 #0)[Id,,M1',,M2'] }} by mauto 4.
-    assert {{ Γ ⊢s Id,,M1',,M2',,L' : ((Γ, B), B[Wk]), Eq B[Wk][Wk] #1 #0 }} by mauto 3.
-
-    eapply wf_conv;
-      [econstructor; mauto 3 | mauto 2 | ].
-    + eapply ctxeq_exp; eauto.
-      eapply wf_conv;
-        mauto 2.
-    + etransitivity;
-        [eapply exp_eq_sub_cong_typ2' |
-          eapply exp_eq_sub_cong_typ1];
-        mauto 3.
-
-  - eexists.
-    eapply exp_sub_typ; mauto 2.
-    assert {{ Γ ⊢s Id ,, M1 : Γ, B}} by mauto 4.
-    assert {{ Γ , B ⊢ B[Wk] : Type@i }} by mauto 4.
-    assert {{ Γ , B , B[Wk] ⊢ B[Wk][Wk] : Type@i }} by mauto 4.
-    assert {{ Γ ⊢ B[Wk][Id,,M1] ≈ B : Type@i }}.
-    {
-      transitivity {{{B[Wk ∘ (Id,,M1)]}}};
-        [| transitivity {{{B[Id]}}}];
-        mauto 3.
-      eapply exp_eq_sub_cong_typ2'; mauto 3.
-    }
-    assert {{ Γ ⊢s Id ,, M1 ,, M2 : Γ, B , B[Wk]}}.
-    {
-      econstructor; mauto 3.
-      eapply wf_conv; mauto 2.
-    }
-    assert {{ Γ ⊢ B[Wk][Wk][Id ,, M1 ,, M2] ≈ B : Type@i }}.
-    {
-      transitivity {{{B[Wk][Wk ∘ (Id ,, M1 ,, M2)]}}};
-        [| transitivity {{{B[Wk][Id ,, M1]}}}];
-        mauto 4.
-      eapply exp_eq_sub_cong_typ2'; mauto 4.
-      eapply wf_sub_eq_p_extend; mauto 4.
-    }
-    assert {{ Γ, B, B[Wk] ⊢ Eq (B[Wk][Wk]) # 1 # 0 : Type@i }} by (econstructor; mauto 4).
-    assert {{ Γ ⊢ L : (Eq (B[Wk][Wk]) #1 #0) [ Id ,, M1 ,, M2]}}.
-    {
-      eapply wf_conv; mauto 2.
-      symmetry.
-      etransitivity.
-      - eapply wf_exp_eq_eq_sub; mauto.
-      - econstructor; mauto 3.
-        + eapply wf_exp_eq_conv;
-            [eapply id_sub_lookup_var1 with (B:=B) | |];
-            mauto 4.
-        + eapply wf_exp_eq_conv;
-            [eapply id_sub_lookup_var0 with (B:=B) | |];
-            mauto 4.
-    }
-    mauto 3.
-
-  - clear HAi1 HAi2.
-    assert {{ Γ ⊢s Id ,, N : Γ, B}} by mauto 4.
-    assert {{ Γ , B ⊢ B[Wk] : Type@i }} by mauto 4.
-    assert {{ Γ , B , B[Wk] ⊢ B[Wk][Wk] : Type@i }} by mauto 4.
-    assert {{ Γ ⊢ B[Wk][Id,,N] ≈ B : Type@i }}.
-    {
-      transitivity {{{B[Wk ∘ (Id,,N)]}}};
-        [| transitivity {{{B[Id]}}}];
-        mauto 3.
-      eapply exp_eq_sub_cong_typ2'; mauto 3.
-    }
-    assert {{ Γ ⊢s Id ,, N ,, N : Γ, B , B[Wk]}}.
-    {
-      econstructor; mauto 3.
-      eapply wf_conv; mauto 2.
-    }
-    assert {{ Γ ⊢ B[Wk][Wk][Id ,, N ,, N] ≈ B : Type@i }}.
-    {
-      transitivity {{{B[Wk][Wk ∘ (Id ,, N ,, N)]}}};
-        [| transitivity {{{B[Wk][Id ,, N]}}}];
-        mauto 4.
-      eapply exp_eq_sub_cong_typ2'; mauto 4.
-      eapply wf_sub_eq_p_extend; mauto 4.
-    }
-    assert {{ Γ, B, B[Wk] ⊢ Eq (B[Wk][Wk]) # 1 # 0 : Type@i }} by (econstructor; mauto 4).
-    assert {{ Γ ⊢ refl B N : Eq B N N}} by mauto 3.
-    assert {{ Γ ⊢ refl B N : (Eq (B[Wk][Wk]) #1 #0) [ Id ,, N ,, N]}}.
-    {
-      eapply wf_conv; mauto 2.
-      symmetry.
-      etransitivity.
-      - eapply wf_exp_eq_eq_sub; mauto.
-      - econstructor; mauto 3.
-        + eapply wf_exp_eq_conv;
-            [eapply id_sub_lookup_var1 with (B:=B) | |];
-            mauto 4.
-        + eapply wf_exp_eq_conv;
-            [eapply id_sub_lookup_var0 with (B:=B) | |];
-            mauto 4.
-    }
-    assert {{Γ, B ⊢s Id,, #0 : Γ, B, B[Wk] }} by mauto 3.
-
-    assert {{ Γ, B ⊢ refl B[Wk] #0 : Eq (B[Wk]) #0 #0 }} by mauto 4.
-    assert {{ Γ, B ⊢s Id,,#0 : Γ, B, B[Wk] }} by mauto 3.
-    assert {{ (Γ, B), B[Wk] ⊢ #1 : B[Wk][Wk] }} by mauto 4.
-    assert {{ Γ, B ⊢s Wk∘(Id,,#0) : Γ, B }} by (econstructor; mauto 3).
-    assert {{ Γ, B ⊢ B[Wk][Wk][Id,,#0] ≈ B[Wk] : Type@i }}.
-    {
-      transitivity {{{B[Wk][Wk ∘ (Id,,#0)]}}};
-        [eapply exp_eq_sub_compose_typ |
-         transitivity {{{B[Wk][Id]}}} ];
-        mauto 3.
-      eapply exp_eq_sub_cong_typ2'; mauto 3.
-    }
-    assert {{ Γ, B ⊢ #1[Id,,#0] ≈ #0 : B[Wk] }}.
-    {
-      transitivity {{{#0[Id]}}}.
-      - eapply wf_exp_eq_conv;
-          [eapply wf_exp_eq_var_S_sub with (A:={{{B[Wk]}}}) | |];
-          mauto 3.
-      - mauto 3.
-    }
-    assert {{ Γ, B ⊢ #1[Id,,#0] ≈ #0 : B[Wk][Wk][Id,,#0] }} by mauto 4.
-    assert {{ Γ, B ⊢ #0[Id,,#0] ≈ #0 : B[Wk] }}.
-    {
-      eapply wf_exp_eq_conv;
-        [eapply wf_exp_eq_var_0_sub with (A:={{{B[Wk]}}}) | |];
-        mauto 3.
-    }
-    assert {{ Γ, B ⊢ #0[Id,,#0] ≈ #0 : B[Wk][Wk][Id,,#0] }} by mauto 4.
-    assert {{ Γ, B ⊢ (Eq B[Wk][Wk] #1 #0)[Id,,#0] ≈ Eq (B[Wk]) #0 #0 : Type@i }}.
-    {
-      etransitivity; econstructor; mauto 3.
-    }
-    assert {{ Γ, B ⊢ refl B[Wk] #0 : (Eq B[Wk][Wk] #1 #0)[Id,,#0] }} by mauto 4.
-    assert {{ Γ, B ⊢s Id,,#0,,refl B[Wk] #0 : Γ, B, B[Wk], Eq (B[Wk][Wk]) #1 #0 }} by mauto 4.
-
-    assert {{ Γ, B ⊢ #0 : B[Wk][Id] }} by mauto 3.
-
-    assert {{ Γ ⊢ B[Wk][Id∘(Id,,N)] ≈ B : Type@i }}.
-    {
-      transitivity {{{B[Wk][Id,,N]}}}; mauto 3.
-      eapply exp_eq_sub_cong_typ2'; mauto 3.
-    }
-    assert {{ Γ ⊢ #0[Id,,N] ≈ N : B }}.
-    {
-      eapply wf_exp_eq_conv with (A:={{{B[Id]}}}); mauto 4.
-    }
-    assert {{ Γ ⊢ B[Wk][Id∘(Id,,N)] : Type@i }} by mauto 4.
-    assert {{ Γ ⊢ #0[Id,,N] ≈ N : B[Wk][Id∘(Id,,N)] }} by mauto 3.
-
-    assert {{ Γ ⊢s Id∘(Id,,N),,#0[Id,,N] ≈ Id,,N,,N : (Γ, B), B[Wk] }} by mauto 3.
-    assert {{ Γ ⊢s (Id,,#0)∘(Id,,N) ≈ Id,,N,,N : (Γ, B), B[Wk] }}.
-    {
-      etransitivity;
-        [eapply wf_sub_eq_extend_compose |];
-        mauto 2.
-    }
-
-    assert {{ Γ ⊢ #1[Id,,N,,N] ≈ N : B }}.
-    {
-      transitivity {{{#0[Id,,N]}}}.
-      - eapply wf_exp_eq_conv;
-          [eapply wf_exp_eq_var_S_sub with (A:={{{B[Wk]}}}) | |];
-          mauto 4.
-      - mauto 3.
-    }
-    assert {{ Γ ⊢s Wk∘(Id,,N,,N) : Γ, B }} by mauto 4.
-    assert {{ Γ ⊢s Wk∘(Id,,N,,N) ≈ Id,,N : Γ, B }}
-      by (econstructor; mauto 4).
-    assert {{ Γ ⊢ B[Wk][Wk][Id,,N,,N] ≈ B : Type@i }}.
-    {
-      transitivity {{{B[Wk][Wk ∘ (Id,,N,,N)]}}};
-        [eapply exp_eq_sub_compose_typ |];
-        mauto 3.
-    }
-    assert {{ Γ ⊢ #1[Id,,N,,N] ≈ N : B[Wk][Wk][Id,,N,,N] }} by mauto 4.
-
-    assert {{ Γ ⊢ #0[Id,,N,,N] ≈ N : B }}.
-    {
-      eapply wf_exp_eq_conv with (A:={{{B[Wk][Id,,N]}}});
-        [econstructor | |];
-        mauto 4.
-    }
-    assert {{ Γ ⊢ #0[Id,,N,,N] ≈ N : B[Wk][Wk][Id,,N,,N] }} by mauto 4.
-
-    assert {{ Γ ⊢ (Eq B[Wk][Wk] #1 #0)[(Id,,#0)∘(Id,,N)] ≈ Eq B N N : Type@i }}.
-    {
-      etransitivity;
-        [eapply exp_eq_sub_cong_typ2' | ]; mauto 2.
-      etransitivity;
-        econstructor; mauto 3.
-    }
-
-    assert {{ Γ ⊢ (Eq B[Wk][Wk] #1 #0)[Id,,#0][Id,,N] ≈ Eq B N N : Type@i }}.
-    {
-      etransitivity; eauto.
-      eapply exp_eq_sub_compose_typ; mauto 3.
-    }
-    assert {{ Γ ⊢ Eq B N N : Type@i }} by mauto 3.
-
-    assert {{ Γ ⊢ #0[Id,,N] ≈ N : B }}.
-    {
-      eapply wf_exp_eq_conv with (A:={{{B[Id]}}});
-        [econstructor | |];
-        mauto 4.
-    }
-    assert {{ Γ ⊢ #0[Id,,N] ≈ N : B[Wk][Id,,N] }} by mauto 4.
-
-    assert {{ Γ ⊢ (refl B[Wk] #0)[Id,,N] ≈ refl B N : Eq B N N }}.
-    {
-      etransitivity.
-      - eapply wf_exp_eq_conv;
-          [eapply wf_exp_eq_refl_sub | | ]; mauto 4.
-      - eapply wf_exp_eq_conv; [econstructor | | econstructor]; mauto 3.
-    }
-
-    assert {{ Γ ⊢ (refl B[Wk] #0)[Id,,N] ≈ refl B N : (Eq B[Wk][Wk] #1 #0)[(Id,,#0)∘(Id,,N)] }}
-             by (eapply wf_exp_eq_conv; mauto 4).
-
-    eapply wf_conv; mauto 3.
-    etransitivity.
-    + eapply exp_eq_sub_compose_typ; mauto 2.
-    + symmetry.
-      eapply exp_eq_sub_cong_typ2'; mauto 2.
-      symmetry.
-      etransitivity;
-        [eapply wf_sub_eq_extend_compose |];
-        mauto 2.
-
-  - eexists.
-    eapply exp_sub_typ; mauto 2.
-    assert {{ Γ ⊢s Id ,, N : Γ, B}} by mauto 4.
-    assert {{ Γ , B ⊢ B[Wk] : Type@i }} by mauto 4.
-    assert {{ Γ , B , B[Wk] ⊢ B[Wk][Wk] : Type@i }} by mauto 4.
-    assert {{ Γ ⊢ B[Wk][Id,,N] ≈ B : Type@i }}.
-    {
-      transitivity {{{B[Wk ∘ (Id,,N)]}}};
-        [| transitivity {{{B[Id]}}}];
-        mauto 3.
-      eapply exp_eq_sub_cong_typ2'; mauto 3.
-    }
-    assert {{ Γ ⊢s Id ,, N ,, N : Γ, B , B[Wk]}}.
-    {
-      econstructor; mauto 3.
-      eapply wf_conv; mauto 2.
-    }
-    assert {{ Γ ⊢ B[Wk][Wk][Id ,, N ,, N] ≈ B : Type@i }}.
-    {
-      transitivity {{{B[Wk][Wk ∘ (Id ,, N ,, N)]}}};
-        [| transitivity {{{B[Wk][Id ,, N]}}}];
-        mauto 4.
-      eapply exp_eq_sub_cong_typ2'; mauto 4.
-      eapply wf_sub_eq_p_extend; mauto 4.
-    }
-    assert {{ Γ, B, B[Wk] ⊢ Eq (B[Wk][Wk]) # 1 # 0 : Type@i }} by (econstructor; mauto 4).
-    assert {{ Γ ⊢ refl B N : Eq B N N}} by mauto 3.
-    assert {{ Γ ⊢ refl B N : (Eq (B[Wk][Wk]) #1 #0) [ Id ,, N ,, N]}}.
-    {
-      eapply wf_conv; mauto 2.
-      symmetry.
-      etransitivity.
-      - eapply wf_exp_eq_eq_sub; mauto.
-      - econstructor; mauto 3.
-        + eapply wf_exp_eq_conv;
-            [eapply id_sub_lookup_var1 with (B:=B) | |];
-            mauto 4.
-        + eapply wf_exp_eq_conv;
-            [eapply id_sub_lookup_var0 with (B:=B) | |];
-            mauto 4.
-    }
-    mauto 3.
+  (** presup_exp_eq cases *)
+  - eexists; eapply exp_sub_typ; mauto 4 using lift_exp_max_left, lift_exp_max_right.
 
-  - assert {{ Γ ⊢s Wk∘(σ ,, N') ≈ σ : Δ }} by mauto 3.
-    assert {{ Γ ⊢ B[Wk∘(σ ,, N')] ≈ B[σ] : Type@i }} by mauto 4.
-    assert {{ ⊢ Δ, B }} by mauto 2.
-    assert {{ Δ, B ⊢s Wk : Δ }} by mauto 2.
-    assert {{ Γ ⊢s σ ,, N' : Δ, B }} by mauto 2.
-    assert {{ Γ ⊢ B[Wk][σ ,, N'] ≈ B[σ] : Type@i }} by mauto 3.
-    enough {{ Γ ⊢ #0[σ ,, N'] : B[Wk][σ ,, N'] }}...
-
-  - assert (exists i, {{ Δ ⊢ C : Type@i }}) as [i'] by mauto 2.
-    assert {{ Γ ⊢s Wk∘(σ ,, N) ≈ σ : Δ }} by mauto 2.
-    assert {{ Γ ⊢ C[Wk∘(σ ,, N)] ≈ C[σ] : Type@i' }} by mauto 4.
-    assert {{ Δ, B ⊢s Wk : Δ }} by mauto 3.
-    assert {{ Γ ⊢s σ ,, N : Δ, B }} by mauto 2.
-    assert {{ Γ ⊢ C[Wk][σ ,, N] ≈ C[σ] : Type@i' }} by mauto 3.
-    assert {{ Δ, B ⊢ #(S x) : C[Wk] }} by mauto 4.
-    enough {{ Γ ⊢ #(S x)[σ ,, N] : C[Wk][σ ,, N] }}...
-
-  - assert (exists i, {{ Δ ⊢ C : Type@i }}) as []...
+  - match_by_head1 ctx_lookup ltac:(fun H => directed destruct (presup_ctx_lookup_typ ltac:(eassumption) H))...
 
   (** presup_sub_eq cases *)
-  - econstructor...
-
-  - assert {{ Γ ⊢ B[σ] ≈ B[σ'] : Type@i }} by mauto 2.
-    eapply wf_conv...
-
-  - assert {{ Γ ⊢ N'[Id] : A[Id] }}...
-
-  - assert {{ Γ ⊢ N[σ][τ] : B[σ][τ] }} by mauto 3.
-    eapply wf_conv...
-
-  - econstructor...
-
   - econstructor; mauto 3.
     eapply wf_conv...
 
-  - mauto.
-
   - assert (exists i, {{ Γ0 ⊢ A : Type@i }}) as [] by mauto 2.
     assert {{ Γ ⊢ #0[σ] : A[Wk][σ] }} by mauto 3.
     enough {{ Γ ⊢ #0[σ] : A[Wk∘σ] }} by mauto 4.
     eapply wf_conv...
 
   (** 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_eq @presup_sub_eq @presup_subtyp H.
diff --git a/theories/Core/Syntactic/Syntax.v b/theories/Core/Syntactic/Syntax.v
index 16b4a1c..aa20a43 100644
--- a/theories/Core/Syntactic/Syntax.v
+++ b/theories/Core/Syntactic/Syntax.v
@@ -169,7 +169,7 @@ Module Syntax_Notations.
   Notation "'q' σ" := (q σ) (in custom exp at level 30) : mcltt_scope.
 
   Notation "⋅" := nil (in custom exp at level 0) : mcltt_scope.
-  Notation "x , y" := (cons y x) (in custom exp at level 50, format "x ,  y") : mcltt_scope.
+  Notation "x , y" := (cons y x) (in custom exp at level 50, left associativity, format "x ,  y") : mcltt_scope.
 
   Notation "n{{{ x }}}" := x (at level 0, x custom nf at level 99, format "'n{{{'  x  '}}}'") : mcltt_scope.
   Notation "( x )" := x (in custom nf at level 0, x custom nf at level 60) : mcltt_scope.
diff --git a/theories/Core/Syntactic/System/Definitions.v b/theories/Core/Syntactic/System/Definitions.v
index 2913aad..521e510 100644
--- a/theories/Core/Syntactic/System/Definitions.v
+++ b/theories/Core/Syntactic/System/Definitions.v
@@ -94,9 +94,9 @@ with wf_exp : ctx -> typ -> exp -> Prop :=
   `( {{ Γ ⊢ A : Type@i }} ->
      {{ Γ ⊢ M1 : A }} ->
      {{ Γ ⊢ M2 : A }} ->
+     {{ Γ , A , A[Wk], Eq A[Wk∘Wk] #1 #0 ⊢ B : Type@j }} ->
+     {{ Γ , A ⊢ BR : B[Id,,#0,,refl A[Wk] #0] }} ->
      {{ Γ ⊢ N : Eq A M1 M2 }} ->
-     {{ Γ , A , A[Wk], Eq (A[Wk][Wk]) #1 #0 ⊢ B : Type@j }} ->
-     {{ Γ , A ⊢ BR : B [Id,,#0,,refl (A[Wk]) #0 ] }} ->
      {{ Γ ⊢ eqrec N as Eq A M1 M2 return B | refl -> BR end : B[Id,,M1,,M2,,N] }} )
 
 | wf_exp_sub :
@@ -188,13 +188,13 @@ with wf_exp_eq : ctx -> typ -> exp -> exp -> Prop :=
      {{ Γ ⊢ MZ : A[Id,,zero] }} ->
      {{ Γ , ℕ , A ⊢ MS : A[Wk∘Wk,,succ(#1)] }} ->
      {{ Γ ⊢ M : ℕ }} ->
-     {{ Γ ⊢ rec (succ M) return A | zero -> MZ | succ -> MS end ≈ MS[Id,,M,,rec M return A | zero -> MZ | succ -> MS end] : A[Id,,succ M] }} )
+     {{ Γ ⊢ rec succ M return A | zero -> MZ | succ -> MS end ≈ MS[Id,,M,,rec M return A | zero -> MZ | succ -> MS end] : A[Id,,succ M] }} )
 
 | wf_exp_eq_pi_sub :
   `( {{ Γ ⊢s σ : Δ }} ->
      {{ Δ ⊢ A : Type@i }} ->
      {{ Δ , A ⊢ B : Type@i }} ->
-     {{ Γ ⊢ (Π A B)[σ] ≈ Π (A[σ]) (B[q σ]) : Type@i }} )
+     {{ Γ ⊢ (Π A B)[σ] ≈ Π A[σ] B[q σ] : Type@i }} )
 | wf_exp_eq_pi_cong :
   `( {{ Γ ⊢ A : Type@i }} ->
      {{ Γ ⊢ A ≈ A' : Type@i }} ->
@@ -240,22 +240,22 @@ with wf_exp_eq : ctx -> typ -> exp -> exp -> Prop :=
      {{ Δ ⊢ A : Type@i }} ->
      {{ Δ ⊢ M : A }} ->
      {{ Δ ⊢ N : A }} ->
-     {{ Γ ⊢ (Eq A M N)[σ] ≈ Eq (A[σ]) (M[σ]) (N[σ]) : Type@i }} )
+     {{ Γ ⊢ (Eq A M N)[σ] ≈ Eq A[σ] M[σ] N[σ] : Type@i }} )
 | wf_exp_eq_refl_sub :
   `( {{ Γ ⊢s σ : Δ }} ->
      {{ Δ ⊢ A : Type@i }} ->
      {{ Δ ⊢ M : A }} ->
-     {{ Γ ⊢ (refl A M)[σ] ≈ refl (A[σ]) (M[σ]) : (Eq A M M)[σ] }} )
+     {{ Γ ⊢ (refl A M)[σ] ≈ refl A[σ] M[σ] : (Eq A M M)[σ] }} )
 | wf_exp_eq_eqrec_sub :
   `( {{ Γ ⊢s σ : Δ }} ->
      {{ Δ ⊢ A : Type@i }} ->
      {{ Δ ⊢ M1 : A }} ->
      {{ Δ ⊢ M2 : A }} ->
+     {{ Δ , A , A[Wk], Eq A[Wk∘Wk] #1 #0 ⊢ B : Type@j }} ->
+     {{ Δ , A ⊢ BR : B[Id,,#0,,refl A[Wk] #0] }} ->
      {{ Δ ⊢ N : Eq A M1 M2 }} ->
-     {{ Δ , A , A[Wk], Eq (A[Wk][Wk]) #1 #0 ⊢ B : Type@j }} ->
-     {{ Δ , A ⊢ BR : B [Id,,#0,,refl (A[Wk]) #0 ] }} ->
-     {{ Γ ⊢ (eqrec N as Eq A M1 M2 return B | refl -> BR end)[σ]
-          ≈ eqrec (N[σ]) as Eq (A[σ]) (M1[σ]) (M2[σ]) return B[q (q (q σ))] | refl -> BR[q σ] end
+     {{ Γ ⊢ eqrec N as Eq A M1 M2 return B | refl -> BR end[σ]
+          ≈ eqrec N[σ] as Eq A[σ] M1[σ] M2[σ] return B[q (q (q σ))] | refl -> BR[q σ] end
          : B[σ,,M1[σ],,M2[σ],,N[σ]] }} )
 | wf_exp_eq_eq_cong :
   `( {{ Γ ⊢ A ≈ A' : Type@i }} ->
@@ -273,18 +273,17 @@ with wf_exp_eq : ctx -> typ -> exp -> exp -> Prop :=
      {{ Γ ⊢ A ≈ A' : Type@i }} ->
      {{ Γ ⊢ M1 ≈ M1' : A }} ->
      {{ Γ ⊢ M2 ≈ M2' : A }} ->
+     {{ Γ , A , A[Wk], Eq A[Wk∘Wk] #1 #0 ⊢ B ≈ B' : Type@j }} ->
+     {{ Γ , A ⊢ BR ≈ BR' : B[Id,,#0,,refl A[Wk] #0] }} ->
      {{ Γ ⊢ N ≈ N' : Eq A M1 M2 }} ->
-     {{ Γ , A , A[Wk], Eq (A[Wk][Wk]) #1 #0 ⊢ B ≈ B' : Type@j }} ->
-     {{ Γ , A ⊢ BR ≈ BR' : B [Id,,#0,,refl (A[Wk]) #0 ] }} ->
      {{ Γ ⊢ eqrec N as Eq A M1 M2 return B | refl -> BR end
           ≈ eqrec N' as Eq A' M1' M2' return B' | refl -> BR' end
          : B[Id,,M1,,M2,,N] }} )
 | wf_exp_eq_eqrec_beta :
   `( {{ Γ ⊢ A : Type@i }} ->
      {{ Γ ⊢ M : A }} ->
-     {{ Γ ⊢ N : Eq A M M }} ->
-     {{ Γ , A , A[Wk], Eq (A[Wk][Wk]) #1 #0 ⊢ B : Type@j }} ->
-     {{ Γ , A ⊢ BR : B [Id,,#0,,refl (A[Wk]) #0 ] }} ->
+     {{ Γ , A , A[Wk], Eq A[Wk∘Wk] #1 #0 ⊢ B : Type@j }} ->
+     {{ Γ , A ⊢ BR : B[Id,,#0,,refl A[Wk] #0] }} ->
      {{ Γ ⊢ eqrec refl A M as Eq A M M return B | refl -> BR end
           ≈ BR[Id,,M]
          : B[Id,,M,,M,,refl A M] }} )
diff --git a/theories/Core/Syntactic/System/Lemmas.v b/theories/Core/Syntactic/System/Lemmas.v
index 5cd4407..4931d51 100644
--- a/theories/Core/Syntactic/System/Lemmas.v
+++ b/theories/Core/Syntactic/System/Lemmas.v
@@ -3,9 +3,8 @@ From Mcltt.Core Require Import Base.
 From Mcltt.Core.Syntactic.System Require Import Definitions.
 Import Syntax_Notations.
 
-(** ** Core Presuppositions *)
+(** ** Basic Context Properties *)
 
-(** *** Basic inversion *)
 Lemma ctx_lookup_lt : forall {Γ A x},
     {{ #x : A ∈ Γ }} ->
     x < length Γ.
@@ -15,14 +14,22 @@ Qed.
 #[export]
 Hint Resolve ctx_lookup_lt : mcltt.
 
+Lemma functional_ctx_lookup : forall {Γ A A' x},
+    {{ #x : A ∈ Γ }} ->
+    {{ #x : A' ∈ Γ }} ->
+    A = A'.
+Proof with mautosolve.
+  intros * Hx Hx'; gen A'.
+  induction Hx as [|* ? IHHx]; intros; inversion_clear Hx';
+    f_equal;
+    intuition.
+Qed.
+
 Lemma ctx_decomp : forall {Γ A}, {{ ⊢ Γ , A }} -> {{ ⊢ Γ }} /\ exists i, {{ Γ ⊢ A : Type@i }}.
 Proof with now eauto.
   inversion 1...
 Qed.
 
-#[export]
-Hint Resolve ctx_decomp : mcltt.
-
 Corollary ctx_decomp_left : forall {Γ A}, {{ ⊢ Γ , A }} -> {{ ⊢ Γ }}.
 Proof with easy.
   intros * ?%ctx_decomp...
@@ -36,6 +43,8 @@ Qed.
 #[export]
 Hint Resolve ctx_decomp_left ctx_decomp_right : mcltt.
 
+(** ** Core Presuppositions *)
+
 (** *** Context Presuppositions *)
 
 Lemma presup_ctx_eq : forall {Γ Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ ⊢ Γ }} /\ {{ ⊢ Δ }}.
@@ -277,6 +286,16 @@ Proof. mauto. Qed.
 #[export]
 Hint Resolve sub_eq_refl : mcltt.
 
+Lemma ctx_eq_refl : forall {Γ},
+    {{ ⊢ Γ }} ->
+    {{ ⊢ Γ ≈ Γ }}.
+Proof.
+  induction 1; mauto 4.
+Qed.
+
+#[export]
+Hint Resolve ctx_eq_refl : mcltt.
+
 (** *** Lemmas for [exp] of [{{{ Type@i }}}] *)
 
 Lemma exp_sub_typ : forall {Δ Γ A σ i},
@@ -338,6 +357,75 @@ Qed.
 #[export]
 Hint Resolve exp_eq_sub_cong_typ1 exp_eq_sub_cong_typ2' exp_eq_sub_compose_typ : mcltt.
 
+Lemma exp_eq_sub_compose_weaken_extend_typ : forall {Γ σ Δ i A j B M},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Δ ⊢ A : Type@i }} ->
+    {{ Δ ⊢ B : Type@j }} ->
+    {{ Γ ⊢ M : B[σ] }} ->
+    {{ Γ ⊢ A[Wk][σ,,M] ≈ A[σ] : Type@i }}.
+Proof with mautosolve 3.
+  intros.
+  assert {{ Δ, B ⊢s Wk : Δ }} by mauto 4.
+  transitivity {{{ A[Wk∘(σ,,M)] }}}; [mautosolve 4 |].
+  eapply exp_eq_sub_cong_typ2'...
+Qed.
+
+#[export]
+Hint Resolve exp_eq_sub_compose_weaken_extend_typ : mcltt.
+
+Lemma exp_eq_sub_compose_weaken_id_extend_typ : forall {Γ i A j B M},
+    {{ Γ ⊢ A : Type@i }} ->
+    {{ Γ ⊢ B : Type@j }} ->
+    {{ Γ ⊢ M : B }} ->
+    {{ Γ ⊢ A[Wk][Id,,M] ≈ A : Type@i }}.
+Proof with mautosolve 4.
+  intros.
+  assert {{ Γ ⊢ B[Id] : Type@_ }} by mauto 4.
+  assert {{ Γ ⊢ B ⊆ B[Id] }} by mauto 4.
+  assert {{ Γ ⊢ M : B[Id] }} by mauto 2.
+  transitivity {{{ A[Id] }}}...
+Qed.
+
+#[export]
+Hint Resolve exp_eq_sub_compose_weaken_id_extend_typ : mcltt.
+
+Lemma exp_eq_sub_compose_double_weaken_double_extend_typ : forall {Γ σ Δ i A j B M k C N},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Δ ⊢ A : Type@i }} ->
+    {{ Δ ⊢ B : Type@j }} ->
+    {{ Γ ⊢ M : B[σ] }} ->
+    {{ Δ, B ⊢ C : Type@k }} ->
+    {{ Γ ⊢ N : C[σ,,M] }} ->
+    {{ Γ ⊢ A[Wk∘Wk][σ,,M,,N] ≈ A[σ] : Type@i }}.
+Proof with mautosolve 4.
+  intros.
+  assert {{ Δ, B ⊢s Wk : Δ }} by mauto 4.
+  assert {{ Δ, B, C ⊢s Wk : Δ, B }} by mauto 4.
+  transitivity {{{ A[Wk][Wk][σ,,M,,N] }}}; [eapply exp_eq_sub_cong_typ1; mautosolve 3 |].
+  transitivity {{{ A[Wk][σ,,M] }}}...
+Qed.
+
+#[export]
+Hint Resolve exp_eq_sub_compose_double_weaken_double_extend_typ : mcltt.
+
+Lemma exp_eq_sub_compose_double_weaken_id_double_extend_typ : forall {Γ i A j B M k C N},
+    {{ Γ ⊢ A : Type@i }} ->
+    {{ Γ ⊢ B : Type@j }} ->
+    {{ Γ ⊢ M : B }} ->
+    {{ Γ, B ⊢ C : Type@k }} ->
+    {{ Γ ⊢ N : C[Id,,M] }} ->
+    {{ Γ ⊢ A[Wk∘Wk][Id,,M,,N] ≈ A : Type@i }}.
+Proof with mautosolve 4.
+  intros.
+  assert {{ Γ ⊢ B[Id] : Type@_ }} by mauto 4.
+  assert {{ Γ ⊢ B ⊆ B[Id] }} by mauto 4.
+  assert {{ Γ ⊢ M : B[Id] }} by mauto 2.
+  transitivity {{{ A[Id] }}}...
+Qed.
+
+#[export]
+Hint Resolve exp_eq_sub_compose_double_weaken_id_double_extend_typ : mcltt.
+
 Lemma exp_eq_typ_sub_sub : forall {Γ Δ Ψ σ τ i},
     {{ Δ ⊢s σ : Ψ }} ->
     {{ Γ ⊢s τ : Δ }} ->
@@ -349,20 +437,9 @@ 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.
 
-Lemma functional_ctx_lookup : forall {Γ A A' x},
-    {{ #x : A ∈ Γ }} ->
-    {{ #x : A' ∈ Γ }} ->
-    A = A'.
-Proof with mautosolve.
-  intros * Hx Hx'; gen A'.
-  induction Hx as [|* ? IHHx]; intros; inversion_clear Hx';
-    f_equal;
-    intuition.
-Qed.
-
 Lemma vlookup_0_typ : forall {Γ i},
     {{ ⊢ Γ }} ->
-    {{ Γ, Type@i ⊢ # 0 : Type@i }}.
+    {{ Γ, Type@i ⊢ #0 : Type@i }}.
 Proof with mautosolve 4.
   intros.
   eapply wf_conv; mauto 4.
@@ -371,7 +448,7 @@ Qed.
 
 Lemma vlookup_1_typ : forall {Γ i A j},
     {{ Γ, Type@i ⊢ A : Type@j }} ->
-    {{ Γ, Type@i, A ⊢ # 1 : Type@i }}.
+    {{ Γ, Type@i, A ⊢ #1 : Type@i }}.
 Proof with mautosolve 4.
   intros.
   assert {{ Γ, Type@i ⊢s Wk : Γ }} by mauto 4.
@@ -485,22 +562,6 @@ Qed.
 #[export]
 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},
-    {{ Γ ⊢ A : Type@i }} ->
-    {{ Γ, A ⊢s Wk,,#0 ≈ Id : Γ, A }}.
-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.
-  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 σ : Ψ }} ->
@@ -585,6 +646,75 @@ Proof. mauto. Qed.
 #[export]
 Hint Resolve exp_eq_nat_sub_sub_to_nat_sub : mcltt.
 
+Lemma exp_eq_sub_compose_weaken_extend_nat : forall {Γ σ Δ M i B N},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Δ ⊢ M : ℕ }} ->
+    {{ Δ ⊢ B : Type@i }} ->
+    {{ Γ ⊢ N : B[σ] }} ->
+    {{ Γ ⊢ M[Wk][σ,,N] ≈ M[σ] : ℕ }}.
+Proof with mautosolve 3.
+  intros.
+  assert {{ Δ, B ⊢s Wk : Δ }} by mauto 4.
+  transitivity {{{ M[Wk∘(σ,,N)] }}}; [mauto 4 |].
+  eapply exp_eq_sub_cong_nat2...
+Qed.
+
+#[export]
+Hint Resolve exp_eq_sub_compose_weaken_extend_nat : mcltt.
+
+Lemma exp_eq_sub_compose_weaken_id_extend_nat : forall {Γ M i B N},
+    {{ Γ ⊢ M : ℕ }} ->
+    {{ Γ ⊢ B : Type@i }} ->
+    {{ Γ ⊢ N : B }} ->
+    {{ Γ ⊢ M[Wk][Id,,N] ≈ M : ℕ }}.
+Proof with mautosolve 4.
+  intros.
+  assert {{ Γ ⊢ B[Id] : Type@_ }} by mauto 4.
+  assert {{ Γ ⊢ B ⊆ B[Id] }} by mauto 4.
+  assert {{ Γ ⊢ N : B[Id] }} by mauto 2.
+  transitivity {{{ M[Id] }}}...
+Qed.
+
+#[export]
+Hint Resolve exp_eq_sub_compose_weaken_id_extend_nat : mcltt.
+
+Lemma exp_eq_sub_compose_double_weaken_double_extend_nat : forall {Γ σ Δ M i B N j C L},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Δ ⊢ M : ℕ }} ->
+    {{ Δ ⊢ B : Type@i }} ->
+    {{ Γ ⊢ N : B[σ] }} ->
+    {{ Δ, B ⊢ C : Type@j }} ->
+    {{ Γ ⊢ L : C[σ,,N] }} ->
+    {{ Γ ⊢ M[Wk∘Wk][σ,,N,,L] ≈ M[σ] : ℕ }}.
+Proof with mautosolve 4.
+  intros.
+  assert {{ Δ, B ⊢s Wk : Δ }} by mauto 4.
+  assert {{ Δ, B, C ⊢s Wk : Δ, B }} by mauto 4.
+  transitivity {{{ M[Wk][Wk][σ,,N,,L] }}}; [eapply exp_eq_sub_cong_nat1; mautosolve 3 |].
+  transitivity {{{ M[Wk][σ,,N] }}}...
+Qed.
+
+#[export]
+Hint Resolve exp_eq_sub_compose_double_weaken_double_extend_nat : mcltt.
+
+Lemma exp_eq_sub_compose_double_weaken_id_double_extend_nat : forall {Γ M i B N j C L},
+    {{ Γ ⊢ M : ℕ }} ->
+    {{ Γ ⊢ B : Type@i }} ->
+    {{ Γ ⊢ N : B }} ->
+    {{ Γ, B ⊢ C : Type@j }} ->
+    {{ Γ ⊢ L : C[Id,,N] }} ->
+    {{ Γ ⊢ M[Wk∘Wk][Id,,N,,L] ≈ M : ℕ }}.
+Proof with mautosolve 4.
+  intros.
+  assert {{ Γ ⊢ B[Id] : Type@_ }} by mauto 4.
+  assert {{ Γ ⊢ B ⊆ B[Id] }} by mauto 4.
+  assert {{ Γ ⊢ N : B[Id] }} by mauto 2.
+  transitivity {{{ M[Id] }}}...
+Qed.
+
+#[export]
+Hint Resolve exp_eq_sub_compose_double_weaken_id_double_extend_nat : mcltt.
+
 Lemma vlookup_0_nat : forall {Γ},
     {{ ⊢ Γ }} ->
     {{ Γ, ℕ ⊢ # 0 : ℕ }}.
@@ -724,6 +854,22 @@ Hint Resolve exp_eq_sub_sub_compose_cong_nat : mcltt.
 
 (** *** Other Tedious Lemmas *)
 
+Lemma sub_eq_weaken_var0_id : forall {Γ A i},
+    {{ Γ ⊢ A : Type@i }} ->
+    {{ Γ, A ⊢s Wk,,#0 ≈ Id : Γ, A }}.
+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.
+  enough {{ Γ, A ⊢ #0 ≈ #0[Id] : A[Wk] }}...
+Qed.
+
+#[export]
+Hint Resolve sub_eq_weaken_var0_id : mcltt.
+#[export]
+Hint Rewrite -> @sub_eq_weaken_var0_id using mauto 4 : mcltt.
+
 Lemma exp_eq_sub_sub_compose_cong : forall {Γ Δ Δ' Ψ σ τ σ' τ' M A i},
     {{ Ψ ⊢ A : Type@i }} ->
     {{ Ψ ⊢ M : A }} ->
@@ -786,6 +932,30 @@ Qed.
 #[export]
 Hint Resolve sub_id_extend : mcltt.
 
+Lemma sub_eq_id_on_typ : forall {Γ M M' A i},
+    {{ Γ ⊢ A : Type@i }} ->
+    {{ Γ ⊢ M ≈ M' : A }} ->
+    {{ Γ ⊢ M ≈ M' : A[Id] }}.
+Proof with mautosolve 4.
+  intros.
+  eapply wf_exp_eq_conv...
+Qed.
+
+#[export]
+Hint Resolve sub_eq_id_on_typ : mcltt.
+
+Lemma sub_eq_id_extend_cong : forall {Γ M M' A i},
+    {{ Γ ⊢ A : Type@i }} ->
+    {{ Γ ⊢ M ≈ M' : A }} ->
+    {{ Γ ⊢s Id,,M ≈ Id,,M' : Γ, A }}.
+Proof with mautosolve 4.
+  intros.
+  econstructor; mauto 3.
+Qed.
+
+#[export]
+Hint Resolve sub_eq_id_extend_cong : mcltt.
+
 Lemma sub_eq_p_id_extend : forall {Γ M A i},
     {{ Γ ⊢ A : Type@i }} ->
     {{ Γ ⊢ M : A }} ->
@@ -821,7 +991,6 @@ Proof with mautosolve 4.
   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.
 
@@ -833,7 +1002,6 @@ Proof with mautosolve 4.
   assert {{ ⊢ Γ }} by mauto 3.
   assert {{ Γ, ℕ ⊢s Wk : Γ }} by mauto 4.
   assert {{ Γ, ℕ ⊢s σ ∘ Wk : Δ }} by mauto 4.
-  assert {{ Γ, ℕ ⊢ # 0 : ℕ[Wk] }} by mauto 4.
   assert {{ Γ, ℕ ⊢ # 0 : ℕ }}...
 Qed.
 
@@ -1120,6 +1288,20 @@ Qed.
 #[export]
 Hint Resolve ctx_sub_ctx_lookup : mcltt.
 
+Lemma var_compose_subs : forall {Γ τ Δ σ Ψ i A x},
+    {{ Ψ ⊢ A : Type@i }} ->
+    {{ Δ ⊢s σ : Ψ }} ->
+    {{ Γ ⊢s τ : Δ }} ->
+    {{ #x : A[σ][τ] ∈ Γ }} ->
+    {{ Γ ⊢ #x : A[σ∘τ] }}.
+Proof.
+  intros.
+  eapply wf_conv; mauto 3.
+Qed.
+
+#[export]
+Hint Resolve var_compose_subs : mcltt.
+
 Lemma sub_lookup_var0 : forall Δ Γ σ M1 M2 B i,
     {{Δ ⊢s σ : Γ}} ->
     {{Γ ⊢ B : Type@i}} ->
@@ -1197,88 +1379,72 @@ Lemma exp_eq_var_1_sub_q_sigma : forall {Γ A i B j σ Δ},
     {{ Δ ⊢ B : Type@j }} ->
     {{ Δ, B ⊢ A : Type@i }} ->
     {{ Γ ⊢s σ : Δ }} ->
-    {{ Γ, B[σ], A[q σ] ⊢ #1[q (q σ)] ≈ #1 : B[σ][Wk][Wk] }}.
+    {{ Γ, B[σ], A[q σ] ⊢ #1[q (q σ)] ≈ #1 : B[σ][Wk∘Wk] }}.
 Proof with mautosolve 4.
   intros.
-  assert {{ Γ, B[σ] ⊢s q σ : Δ, B }} by mauto.
+  assert {{ ⊢ Δ }} by mauto 2.
+  assert {{ Γ, B[σ] ⊢s q σ : Δ, B }} by mauto 2.
+  assert {{ ⊢ Γ, B[σ] }} by mauto 3.
   assert {{ ⊢ Γ, B[σ], A[q σ] }} by mauto 3.
-  assert {{ Δ, B ⊢ B[Wk] : Type@j }} by mauto.
-  assert {{ Δ, B ⊢ #0 : B[Wk] }} by mauto.
-  assert {{ Γ, B[σ], A[q σ] ⊢ #0 : A[q σ][Wk] }} by mauto 4.
+  assert {{ Δ, B ⊢ B[Wk] : Type@j }} by mauto 4.
+  assert {{ Δ, B ⊢ #0 : B[Wk] }} by mauto 3.
+  assert {{ Γ, B[σ], A[q σ] ⊢ #0 : A[q σ][Wk] }} by mauto 2.
   assert {{ Γ, B[σ], A[q σ] ⊢ A[q σ∘Wk] ≈ A[q σ][Wk] : Type@i }} by mauto 4.
-  assert {{ Γ, B[σ], A[q σ] ⊢ #0 : A[q σ∘Wk] }} by (eapply wf_conv; mauto 4).
-  assert {{ Γ, B[σ], A[q σ] ⊢s q σ∘Wk : Δ, B }} by mauto 4.
-  assert {{ Γ ⊢ B[σ] : Type@j }} by mauto 3.
-  assert {{ Γ,B[σ] ⊢ B[σ][Wk] : Type@j }} by mauto 4.
-  assert {{Γ, B[σ], A[q σ] ⊢ B[σ][Wk][Wk] : Type@j}} by mauto 4.
-  assert {{Γ, B[σ],A[q σ] ⊢ B[Wk][q σ ∘ Wk] : Type@j}} by mauto.
-  assert {{Γ, B[σ] ⊢ B[Wk][q σ] ≈ B[σ][Wk] : Type@j}}.
-  {
-    transitivity {{{B[Wk ∘ q σ]}}};
-      [mauto 4 | transitivity {{{B[σ ∘ Wk]}}}];
-      [eapply exp_eq_sub_cong_typ2'; mauto 4 | mauto].
-  }
-  assert {{Γ, B[σ],A[q σ] ⊢ B[Wk][q σ ∘ Wk] ≈ B[σ][Wk][Wk] : Type@j}}.
-  {
-    transitivity {{{B[Wk][q σ][Wk]}}};
-      [mauto 4 |].
-    eapply exp_eq_sub_cong_typ1; mauto 3.
-  }
+  assert {{ Γ, B[σ], A[q σ] ⊢s q σ∘Wk : Δ, B }} by mauto 3.
+  assert {{ Γ, B[σ], A[q σ] ⊢ #0 : A[q σ∘Wk] }} by mauto 3.
+  assert {{ Γ ⊢ B[σ] : Type@j }} by mauto 2.
+  assert {{ Γ, B[σ] ⊢s Wk : Γ }} by mauto 2.
+  assert {{ Γ, B[σ], A[q σ] ⊢s Wk : Γ, B[σ] }} by mauto 2.
+  assert {{ Γ, B[σ] ⊢ B[σ][Wk] : Type@j }} by mauto 2.
+  assert {{ Γ, B[σ], A[q σ] ⊢ B[σ][Wk][Wk] : Type@j }} by mauto 2.
+  assert {{ Γ, B[σ] ⊢ B[Wk][q σ] ≈ B[σ][Wk] : Type@j }} by (eapply exp_eq_sub_sub_compose_cong_typ; mauto 3).
+  assert {{Γ, B[σ],A[q σ] ⊢ B[Wk][q σ ∘ Wk] ≈ B[σ][Wk][Wk] : Type@j}} by (transitivity {{{ B[Wk][q σ][Wk] }}}; mauto 3).
   assert {{ Γ, B[σ], A[q σ] ⊢ #1[q (q σ)] ≈ #0[q σ∘Wk] : B[σ][Wk][Wk] }} by mauto 3.
-  assert {{ Γ, B[σ], A[q σ] ⊢ #0[q σ∘Wk] ≈ #0[q σ][Wk] : B[σ][Wk][Wk] }} by mauto 4.
-  assert {{ Γ, B[σ] ⊢s σ∘Wk : Δ }} by mauto 4.
-  assert {{ Γ, B[σ] ⊢ #0 : B[σ∘Wk] }}.
-  {
-    eapply wf_conv with (A:={{{B[σ][Wk]}}}); mauto 2; mauto 4.
-  }
-  assert {{ Γ, B[σ] ⊢ #0[q σ] ≈ #0 : B[σ ∘ Wk] }} by mauto 4.
-  assert {{ Γ, B[σ], A[q σ] ⊢ #0[q σ][Wk] ≈ #0[Wk] : B[σ ∘ Wk][Wk] }} by mauto 4.
-  assert {{ Γ, B[σ], A[q σ] ⊢ B[σ ∘ Wk][Wk] ≈ B[σ][Wk][Wk] : Type@j}}.
-  {
-    eapply exp_eq_sub_cong_typ1; mauto 3.
-    symmetry.
-    mauto 4.
-  }
-  assert {{ Γ, B[σ], A[q σ] ⊢ #0[q σ][Wk] ≈ #0[Wk] : B[σ][Wk][Wk] }} by mauto 4.
-  etransitivity; mauto 2.
-  transitivity {{{#0[q σ][Wk]}}}; mauto 3.
+  assert {{ Γ, B[σ], A[q σ] ⊢ #0[q σ∘Wk] ≈ #0[q σ][Wk] : B[σ][Wk][Wk] }} by mauto 3.
+  assert {{ Γ, B[σ] ⊢s σ∘Wk : Δ }} by mauto 2.
+  assert {{ Γ, B[σ] ⊢ #0 : B[σ∘Wk] }} by mauto 2.
+  assert {{ Γ, B[σ] ⊢ #0[q σ] ≈ #0 : B[σ ∘ Wk] }} by mauto 2.
+  assert {{ Γ, B[σ], A[q σ] ⊢ #0[q σ][Wk] ≈ #0[Wk] : B[σ ∘ Wk][Wk] }} by mauto 3.
+  assert {{ Γ, B[σ], A[q σ] ⊢ B[σ ∘ Wk][Wk] ≈ B[σ][Wk][Wk] : Type@j}} by mauto 4.
+  assert {{ Γ, B[σ], A[q σ] ⊢ #0[q σ][Wk] ≈ #0[Wk] : B[σ][Wk][Wk] }} by mauto 2.
+  assert {{ Γ, B[σ], A[q σ] ⊢ #1[q (q σ)] ≈ #1 : B[σ][Wk][Wk] }} by (do 2 etransitivity; mauto 2).
+  assert {{ Γ, B[σ], A[q σ] ⊢s Wk∘Wk : Γ }} by mauto 2.
+  assert {{ Γ, B[σ], A[q σ] ⊢ B[σ][Wk∘Wk] : Type@j }} by mauto 2.
+  eapply wf_exp_eq_conv; mauto 2.
 Qed.
 
-(** *** Types Presuppositions *)
+(** *** Type Presuppositions *)
 
 Lemma presup_exp_typ : forall {Γ M A},
     {{ Γ ⊢ M : A }} ->
     exists i, {{ Γ ⊢ A : Type@i }}.
 Proof.
   induction 1; assert {{ ⊢ Γ }} by mauto 3; destruct_conjs; mauto 3.
+
   - enough {{ Γ ⊢s Id,,M : Γ, ℕ }}; mauto 3.
+
   - eexists; mauto 4 using lift_exp_max_left, lift_exp_max_right.
+
   - enough {{ Γ ⊢s Id,,N : Γ, A }}; mauto 3.
-  - assert {{ Γ ⊢s Id,,M1 : Γ, A }} by mauto 3.
+
+  - enough {{ Γ ⊢s Id,,M1,,M2,,N : Γ, A, A[Wk], Eq A[Wk∘Wk] #1 #0 }} by mauto 3.
     assert {{ Γ, A ⊢s Wk : Γ }} by mauto 3.
     assert {{ Γ, A ⊢ A[Wk] : Type@i }} by mauto 3.
     assert {{ Γ, A, A[Wk] ⊢s Wk : Γ, A }} by mauto 4.
-    assert {{ Γ, A, A[Wk] ⊢ A[Wk][Wk] : Type@i }} by mauto 3.
-    assert {{ Γ ⊢ A[Wk][Id,,M1] : Type@i }} by mauto 3.
-    assert {{ Γ ⊢ A[Wk][Id,,M1] ≈ A : Type@i }}.
-    {
-      transitivity {{{ A[Wk∘(Id,,M1)] }}}; mauto 3.
-      transitivity {{{ A[Id] }}}; mauto 4.
-    }
-    assert {{ Γ ⊢s Id,,M1,,M2 : Γ, A, A[Wk] }} by mauto 4.
-    assert {{ Γ ⊢ A[Wk][Wk][Id ,, M1 ,, M2] ≈ A : Type@i }}.
-    {
-      transitivity {{{ A[Wk][Wk∘(Id,,M1,,M2)] }}}; mauto 3.
-      transitivity {{{ A[Wk][Id,,M1] }}}; mauto 3.
-      eapply exp_eq_sub_cong_typ2'; mauto 4.
-    }
-    enough {{ Γ ⊢s Id,,M1,,M2,,N : Γ, A, A[Wk], Eq A[Wk][Wk] #1 #0 }} by mauto 3.
-    assert {{ Γ, A, A[Wk] ⊢ Eq A[Wk][Wk] #1 #0 : Type@i }} by (econstructor; mauto 4).
-    econstructor; mauto 3.
-    eapply wf_conv; mauto 2.
-    transitivity {{{ Eq A[Wk][Wk][Id,,M1,,M2] #1[Id,,M1,,M2] #0[Id,,M1,,M2] }}}.
-    + econstructor; mauto 3 using id_sub_lookup_var0, id_sub_lookup_var1.
-    + symmetry; econstructor; mauto 4.
+    assert {{ Γ, A, A[Wk] ⊢ A[Wk∘Wk] : Type@i }} by mauto 3.
+    assert {{ Γ, A, A[Wk] ⊢ Eq A[Wk∘Wk] #1 #0 : Type@i }} by (econstructor; mauto 3; eapply wf_conv; mauto 4).
+
+    assert {{ Γ ⊢s Id,,M1 : Γ, A }} by mauto 3.
+    assert {{ Γ ⊢ M2 : A[Wk][Id,,M1] }} by (eapply wf_conv; [| | symmetry]; mauto 2).
+    assert {{ Γ ⊢s Id,,M1,,M2 : Γ, A, A[Wk] }} by mauto 3.
+    econstructor; [mautosolve 3 | mautosolve 3 |].
+    eapply wf_conv; [| | symmetry]; mauto 3.
+    transitivity {{{ Eq A[Wk∘Wk][Id,,M1,,M2] #1[Id,,M1,,M2] #0[Id,,M1,,M2] }}}.
+    + econstructor; mauto 3 using id_sub_lookup_var0, id_sub_lookup_var1; eapply wf_conv; mauto 4.
+    + assert {{ Γ ⊢ M2 : A }} by eassumption. (* re-assert to help search process *)
+      assert {{ Γ ⊢ M1 : A[Wk∘Wk][Id,,M1,,M2] }} by (eapply wf_conv; [| | symmetry]; mauto 2).
+      assert {{ Γ ⊢ M2 : A[Wk∘Wk][Id,,M1,,M2] }} by (eapply wf_conv; [| | symmetry]; mauto 2).
+      econstructor; mauto 3 using id_sub_lookup_var0, id_sub_lookup_var1.
 Qed.
 
 Lemma presup_exp : forall {Γ M A},
@@ -1288,6 +1454,8 @@ Proof.
   mauto 4 using presup_exp_typ.
 Qed.
 
+(** *** Consistency Helper *)
+
 Lemma no_closed_neutral : forall {A} {W : ne},
     ~ {{ ⋅ ⊢ W : A }}.
 Proof.