From 1829f6bc6528d994db2afb12535f8b550fe5cf76 Mon Sep 17 00:00:00 2001
From: Jason Hu <fdhzs2010@hotmail.com>
Date: Mon, 30 Sep 2024 16:12:33 -0400
Subject: [PATCH] Feature/fix presup (#223)

* fixing presupposition

* working on presup

* need to figure this out

* update

* one more case

* one more lemma

* I am so dead...

* move out lemmas

* more progress

* finish one lemma

* long way to go

* outline the proof

* outline the proof

* one simple case

* keep completing

* more proofs

* the most complicated case

* more proofs

* more proofs

* more proofs

* finish proofs

* add presup

* finish all syntactic proofs
---
 theories/Core/Syntactic/Presup.v             | 1121 ++++++++++++++++++
 theories/Core/Syntactic/System/Definitions.v |   16 +-
 theories/Core/Syntactic/System/Lemmas.v      |  125 ++
 theories/_CoqProject                         |   10 +-
 4 files changed, 1259 insertions(+), 13 deletions(-)

diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index 4fb4f72..7ecbe02 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -49,6 +49,7 @@ Ltac gen_presup_IH presup_exp presup_exp_eq presup_sub_eq presup_subtyp H :=
   | _ => gen_presup_ctx H
   end.
 
+
 Lemma presup_exp : forall {Γ M A}, {{ Γ ⊢ M : A }} -> {{ ⊢ Γ }} /\ exists i, {{ Γ ⊢ A : Type@i }}
 with presup_exp_eq : forall {Γ M M' A}, {{ Γ ⊢ M ≈ M' : A }} -> {{ ⊢ Γ }} /\ {{ Γ ⊢ M : A }} /\ {{ Γ ⊢ M' : A }} /\ exists i, {{ Γ ⊢ A : Type@i }}
 with presup_sub_eq : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Γ }} /\ {{ Γ ⊢s σ : Δ }} /\ {{ Γ ⊢s σ' : Δ }} /\ {{ ⊢ Δ }}
@@ -68,6 +69,49 @@ Proof with mautosolve 4.
     assert {{ Γ ⊢ B : Type@(max i i0) }} by mauto using lift_exp_max_left.
     assert {{ Γ, B ⊢ C : Type@(max i i0) }} by mauto using lift_exp_max_right...
 
+  - eexists.
+    eapply exp_sub_typ; [eassumption |].
+    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.
+    }
+
+    econstructor; mauto 3.
+    + econstructor; mauto 4.
+    + eapply wf_conv; mauto 2.
+      * eapply exp_sub_typ; mauto 3.
+        econstructor; mauto 4.
+      * 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.
+
   (** presup_exp_eq cases *)
   - assert {{ Γ ⊢s Id ,, N ≈ Id ,, N' : Γ, ℕ }} by mauto 4.
     assert {{ Γ ⊢ B[Id ,, N] ≈ B[Id ,, N'] : Type@i }} by mauto.
@@ -235,6 +279,1083 @@ Proof with mautosolve 4.
     assert {{ Γ, B ⊢ C[q Wk ∘ Id0] ≈ C[Id] : Type@i }} by mauto 4.
     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.
+
   - assert {{ Γ ⊢s Wk∘(σ ,, N') ≈ σ : Δ }} by mauto.
     assert {{ Γ ⊢ B[Wk∘(σ ,, N')] ≈ B[σ] : Type@i }} by mauto.
     assert {{ ⊢ Δ, B }} by mauto.
diff --git a/theories/Core/Syntactic/System/Definitions.v b/theories/Core/Syntactic/System/Definitions.v
index 2232e63..cac0e5d 100644
--- a/theories/Core/Syntactic/System/Definitions.v
+++ b/theories/Core/Syntactic/System/Definitions.v
@@ -95,8 +95,8 @@ with wf_exp : ctx -> typ -> exp -> Prop :=
      {{ Γ ⊢ M2 : A }} ->
      {{ Γ ⊢ N : Eq A M1 M2 }} ->
      {{ Γ , A , A[Wk], Eq (A[Wk][Wk]) #1 #0 ⊢ B : Type@j }} ->
-     {{ Γ , A ⊢ BR : M [Id,,#0,,refl (A[Wk]) #0 ] }} ->
-     {{ Γ ⊢ eqrec N as Eq A M1 M2 return B | refl -> BR end : M[Id,,M1,,M2,,N] }} )
+     {{ Γ , 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 :
   `( {{ Γ ⊢s σ : Δ }} ->
@@ -252,10 +252,10 @@ with wf_exp_eq : ctx -> typ -> exp -> exp -> Prop :=
      {{ Δ ⊢ M2 : A }} ->
      {{ Δ ⊢ N : Eq A M1 M2 }} ->
      {{ Δ , A , A[Wk], Eq (A[Wk][Wk]) #1 #0 ⊢ B : Type@j }} ->
-     {{ Δ , A ⊢ BR : M [Id,,#0,,refl (A[Wk]) #0 ] }} ->
+     {{ Δ , 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
-         : M[σ,,M1[σ],,M2[σ],,N[σ]] }} )
+         : B[σ,,M1[σ],,M2[σ],,N[σ]] }} )
 | wf_exp_eq_eq_cong :
   `( {{ Γ ⊢ A ≈ A' : Type@i }} ->
      {{ Γ ⊢ M ≈ M' : A }} ->
@@ -274,19 +274,19 @@ with wf_exp_eq : ctx -> typ -> exp -> exp -> Prop :=
      {{ Γ ⊢ M2 ≈ M2' : A }} ->
      {{ Γ ⊢ N ≈ N' : Eq A M1 M2 }} ->
      {{ Γ , A , A[Wk], Eq (A[Wk][Wk]) #1 #0 ⊢ B ≈ B' : Type@j }} ->
-     {{ Γ , A ⊢ BR ≈ BR' : M [Id,,#0,,refl (A[Wk]) #0 ] }} ->
+     {{ Γ , 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
-         : M[Id,,M1,,M2,,N] }} )
+         : 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 : M [Id,,#0,,refl (A[Wk]) #0 ] }} ->
+     {{ Γ , 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]
-         : M[Id,,M,,M,,refl A M] }} )
+         : B[Id,,M,,M,,refl A M] }} )
 
 | wf_exp_eq_var :
   `( {{ ⊢ Γ }} ->
diff --git a/theories/Core/Syntactic/System/Lemmas.v b/theories/Core/Syntactic/System/Lemmas.v
index 2148760..a6f9c3d 100644
--- a/theories/Core/Syntactic/System/Lemmas.v
+++ b/theories/Core/Syntactic/System/Lemmas.v
@@ -1085,3 +1085,128 @@ Qed.
 
 #[export]
 Hint Resolve ctx_sub_ctx_lookup : mcltt.
+
+
+Lemma sub_lookup_var0 : forall Δ Γ σ M1 M2 B i,
+    {{Δ ⊢s σ : Γ}} ->
+    {{Γ ⊢ B : Type@i}} ->
+    {{Δ ⊢ M1 : B[σ]}} ->
+    {{Δ ⊢ M2 : B[σ]}} ->
+    {{Δ ⊢ #0[σ,,M1,,M2] ≈ M2 : B[σ]}}.
+Proof.
+  intros.
+  assert {{ Γ , B ⊢ B[Wk] : Type@i }} by mauto.
+  assert {{ Δ ⊢s σ ,, M1 : Γ, B}} by mauto 4.
+  assert {{ Δ ⊢ B[Wk][σ,,M1] : Type @ i }} by mauto 4.
+  assert {{ Δ ⊢ B[Wk][σ,,M1] ≈ B[σ] : Type @ i }}.
+  {
+    transitivity {{{B[Wk ∘ (σ,,M1)]}}}.
+    - eapply exp_eq_sub_compose_typ; mauto 4.
+    - eapply exp_eq_sub_cong_typ2'; mauto 4.
+  }
+  eapply wf_exp_eq_conv;
+    [eapply wf_exp_eq_var_0_sub with (A := {{{B[Wk]}}}) | |];
+    mauto 4.
+Qed.
+
+Lemma id_sub_lookup_var0 : forall Γ M1 M2 B i,
+    {{Γ ⊢ B : Type@i}} ->
+    {{Γ ⊢ M1 : B}} ->
+    {{Γ ⊢ M2 : B}} ->
+    {{Γ ⊢ #0[Id,,M1,,M2] ≈ M2 : B}}.
+Proof.
+  intros.
+  eapply wf_exp_eq_conv;
+    [eapply sub_lookup_var0 | |];
+    mauto 3.
+Qed.
+
+Lemma sub_lookup_var1 : forall Δ Γ σ M1 M2 B i,
+    {{Δ ⊢s σ : Γ}} ->
+    {{Γ ⊢ B : Type@i}} ->
+    {{Δ ⊢ M1 : B[σ]}} ->
+    {{Δ ⊢ M2 : B[σ]}} ->
+    {{Δ ⊢ #1[σ,,M1,,M2] ≈ M1 : B[σ]}}.
+Proof.
+  intros.
+  assert {{ Γ , B ⊢ B[Wk] : Type@i }} by mauto.
+  assert {{ Δ ⊢s σ ,, M1 : Γ, B}} by mauto 4.
+  assert {{ Δ ⊢ B[Wk][σ,,M1] : Type @ i }} by mauto 4.
+  assert {{ Δ ⊢ B[Wk][σ,,M1] ≈ B[σ] : Type @ i }}.
+  {
+    transitivity {{{B[Wk ∘ (σ,,M1)]}}}.
+    - eapply exp_eq_sub_compose_typ; mauto 4.
+    - eapply exp_eq_sub_cong_typ2'; mauto 4.
+  }
+  transitivity {{{#0[σ,,M1]}}}.
+  - eapply wf_exp_eq_conv;
+      [eapply wf_exp_eq_var_S_sub | |];
+      mauto 4.
+  - eapply wf_exp_eq_conv;
+    [eapply wf_exp_eq_var_0_sub with (A := B) | |];
+    mauto 2.
+    mauto.
+Qed.
+
+Lemma id_sub_lookup_var1 : forall Γ M1 M2 B i,
+    {{Γ ⊢ B : Type@i}} ->
+    {{Γ ⊢ M1 : B}} ->
+    {{Γ ⊢ M2 : B}} ->
+    {{Γ ⊢ #1[Id,,M1,,M2] ≈ M1 : B}}.
+Proof.
+  intros.
+  eapply wf_exp_eq_conv;
+    [eapply sub_lookup_var1 | |];
+    mauto 3.
+Qed.
+
+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] }}.
+Proof with mautosolve 4.
+  intros.
+  assert {{ Γ, B[σ] ⊢s q σ : Δ, B }} by mauto.
+  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[σ], 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 σ] ⊢ #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.
+Qed.
diff --git a/theories/_CoqProject b/theories/_CoqProject
index eba34f6..3486db8 100644
--- a/theories/_CoqProject
+++ b/theories/_CoqProject
@@ -58,19 +58,19 @@
 # ./Core/Soundness/Weakening.v
 # ./Core/Soundness/Weakening/Definition.v
 # ./Core/Soundness/Weakening/Lemmas.v
-# ./Core/Syntactic/CoreInversions.v
-# ./Core/Syntactic/CoreTypeInversions.v
-# ./Core/Syntactic/Corollaries.v
+./Core/Syntactic/CoreInversions.v
+./Core/Syntactic/CoreTypeInversions.v
+./Core/Syntactic/Corollaries.v
 ./Core/Syntactic/CtxEq.v
 ./Core/Syntactic/CtxSub.v
 ./Core/Syntactic/ExpNoConfusion.v
-# ./Core/Syntactic/Presup.v
+./Core/Syntactic/Presup.v
 ./Core/Syntactic/Syntax.v
 ./Core/Syntactic/System.v
 ./Core/Syntactic/System/Definitions.v
 ./Core/Syntactic/System/Lemmas.v
 ./Core/Syntactic/System/Tactics.v
-# ./Core/Syntactic/SystemOpt.v
+./Core/Syntactic/SystemOpt.v
 # ./Entrypoint.v
 # ./Extraction/Evaluation.v
 # ./Extraction/NbE.v