From 274b625edc72ee6bf58aeaf25a45177ade1c1460 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Mon, 16 Sep 2024 12:18:09 -0400
Subject: [PATCH 01/23] fixing presupposition

---
 theories/Core/Syntactic/Presup.v             | 18 +++++++++++++++++-
 theories/Core/Syntactic/System/Definitions.v |  2 +-
 2 files changed, 18 insertions(+), 2 deletions(-)

diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index 6f70f993..e7353396 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -63,10 +63,26 @@ Proof with mautosolve 4.
     try (rename M0 into N); try (rename MZ into NZ); try (rename MS into NS);
     try (rename M'0 into N'); try (rename MZ' into NZ'); try (rename MS' into NS');
     try (rename M' into N').
-  (* presup_exp cases *)
+  (** presup_exp cases *)
   - eexists.
     assert {{ Γ ⊢ B : Type@(max i i0) }} by mauto using lift_exp_max_left.
     assert {{ Γ, B ⊢ C : Type@(max i i0) }} by mauto using lift_exp_max_right...
+  - eexists.
+    eapply exp_sub_typ; [eassumption |].
+    assert {{ Γ ⊢s Id ,, M1 : Γ, B}} by mauto 4.
+    assert {{ Γ ⊢s Id ,, M1 ,, M2 : Γ, B , B[Wk]}}.
+    {
+      econstructor; mauto 3.
+      Search (a_sub (a_sub _ _) _).
+      rewrite exp_eq_sub_compose_typ.
+      rewrite
+    }
+
+    by mauto 4.
+
+    econstructor.
+    2:mauto 4.
+    eapply wf_sub.
 
   (* presup_exp_eq cases *)
   - assert {{ Γ ⊢s Id ,, N ≈ Id ,, N' : Γ, ℕ }} by mauto 4.
diff --git a/theories/Core/Syntactic/System/Definitions.v b/theories/Core/Syntactic/System/Definitions.v
index 2232e631..c8d14e34 100644
--- a/theories/Core/Syntactic/System/Definitions.v
+++ b/theories/Core/Syntactic/System/Definitions.v
@@ -96,7 +96,7 @@ with wf_exp : ctx -> typ -> exp -> Prop :=
      {{ Γ ⊢ 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] }} )
+     {{ Γ ⊢ eqrec N as Eq A M1 M2 return B | refl -> BR end : B[Id,,M1,,M2,,N] }} )
 
 | wf_exp_sub :
   `( {{ Γ ⊢s σ : Δ }} ->

From 628d4657ab55f990405616a15faaf48621b5ef56 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Tue, 17 Sep 2024 10:52:00 -0400
Subject: [PATCH 02/23] working on presup

---
 theories/Core/Syntactic/Presup.v | 74 +++++++++++++++++++++++++++++---
 1 file changed, 69 insertions(+), 5 deletions(-)

diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index e7353396..6726dfb3 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -49,6 +49,29 @@ Ltac gen_presup_IH presup_exp presup_exp_eq presup_sub_eq presup_subtyp H :=
   | _ => gen_presup_ctx H
   end.
 
+Lemma sub_lookup_var0 : forall Γ M1 M2 A B i j,
+    {{Γ ⊢ A : Type@i}} ->
+    {{Γ ⊢ B : Type@j}} ->
+    {{Γ ⊢ M1 : A}} ->
+    {{Γ ⊢ M2 : B}} ->
+    {{Γ ⊢ #0[Id,,M1,,M2] ≈ M2 : B}}.
+Proof.
+  intros.
+  assert {{ Γ , A ⊢ B[Wk] : Type@j }} by mauto.
+  assert {{ Γ ⊢s Id ,, M1 : Γ, A}} by mauto 4.
+  assert {{ Γ ⊢ B[Wk][Id,,M1] ≈ B : Type @ j }}.
+  {
+    transitivity {{{B[Wk ∘ (Id,,M1)]}}};
+      [| transitivity {{{B[Id]}}}];
+      mauto 3.
+    - 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 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 σ' : Δ }} /\ {{ ⊢ Δ }}
@@ -70,17 +93,58 @@ Proof with mautosolve 4.
   - 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.
-      Search (a_sub (a_sub _ _) _).
-      rewrite exp_eq_sub_compose_typ.
-      rewrite
+      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 with (A := B); mauto 2.
+
+              transitivity {{{#0[Id,,M1]}}};
+                [eapply wf_exp_eq_var_S_sub |
+                eapply wf_exp_eq_conv; eapply wf_exp_eq_var_0_sub].
+
+
+
+
+           2:{
+             eapply wf_exp_eq_conv;
+             [eapply wf_exp_eq_var_0_sub | |];
+             mauto 2; mauto 4.
+           }
+
 
-    by mauto 4.
+              mauto 4.
+             eapply wf_conv.
 
-    econstructor.
+    mauto 4.
     2:mauto 4.
     eapply wf_sub.
 

From d1256bcd9019ca0dd0c5bf1995731cde3f566f51 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Tue, 17 Sep 2024 11:05:29 -0400
Subject: [PATCH 03/23] need to figure this out

---
 theories/Core/Syntactic/Presup.v | 34 ++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index 6726dfb3..5f55b6cf 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -72,6 +72,34 @@ Proof.
     mauto 4.
 Qed.
 
+Lemma sub_lookup_var1 : forall Γ M1 M2 A B i j,
+    {{Γ ⊢ A : Type@i}} ->
+    {{Γ ⊢ B : Type@j}} ->
+    {{Γ ⊢ M1 : A}} ->
+    {{Γ ⊢ M2 : B}} ->
+    {{Γ ⊢ #1[Id,,M1,,M2] ≈ M1 : A}}.
+Proof.
+  intros.
+  assert {{ Γ , A ⊢ B[Wk] : Type@j }} by mauto.
+  assert {{ Γ ⊢s Id ,, M1 : Γ, A}} by mauto 4.
+  assert {{ Γ ⊢ B[Wk][Id,,M1] ≈ B : Type @ j }}.
+  {
+    transitivity {{{B[Wk ∘ (Id,,M1)]}}};
+      [| transitivity {{{B[Id]}}}];
+      mauto 3.
+    - eapply exp_eq_sub_compose_typ; mauto 4.
+    - eapply exp_eq_sub_cong_typ2'; mauto 4.
+  }
+  transitivity {{{#0[Id,,M1]}}}.
+  - eapply wf_exp_eq_conv;
+      [eapply wf_exp_eq_var_S_sub | |];
+      mauto 4.
+    admit.
+  - eapply wf_exp_eq_conv;
+    [eapply wf_exp_eq_var_0_sub with (A := A) | |];
+    mauto 4.
+Qed.
+
 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 σ' : Δ }} /\ {{ ⊢ Δ }}
@@ -125,6 +153,12 @@ Proof with mautosolve 4.
         etransitivity.
         -- eapply wf_exp_eq_eq_sub; mauto.
         -- econstructor; mauto 3.
+           2:{
+             eapply wf_exp_eq_conv;
+             [eapply sub_lookup_var0 with (A:=B) (B:=B) | |];
+               mauto 4.
+           }
+
            ++ eapply wf_exp_eq_conv with (A := B); mauto 2.
 
               transitivity {{{#0[Id,,M1]}}};

From d92022dcdf383492a0314e37d448032d1d699236 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Wed, 18 Sep 2024 10:42:07 -0400
Subject: [PATCH 04/23] update

---
 theories/Core/Syntactic/Presup.v             | 102 +++++++++++--------
 theories/Core/Syntactic/System/Definitions.v |   6 +-
 2 files changed, 61 insertions(+), 47 deletions(-)

diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index 5f55b6cf..54c20460 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -49,17 +49,16 @@ Ltac gen_presup_IH presup_exp presup_exp_eq presup_sub_eq presup_subtyp H :=
   | _ => gen_presup_ctx H
   end.
 
-Lemma sub_lookup_var0 : forall Γ M1 M2 A B i j,
-    {{Γ ⊢ A : Type@i}} ->
-    {{Γ ⊢ B : Type@j}} ->
-    {{Γ ⊢ M1 : A}} ->
+Lemma sub_lookup_var0 : forall Γ M1 M2 B i,
+    {{Γ ⊢ B : Type@i}} ->
+    {{Γ ⊢ M1 : B}} ->
     {{Γ ⊢ M2 : B}} ->
     {{Γ ⊢ #0[Id,,M1,,M2] ≈ M2 : B}}.
 Proof.
   intros.
-  assert {{ Γ , A ⊢ B[Wk] : Type@j }} by mauto.
-  assert {{ Γ ⊢s Id ,, M1 : Γ, A}} by mauto 4.
-  assert {{ Γ ⊢ B[Wk][Id,,M1] ≈ B : Type @ j }}.
+  assert {{ Γ , B ⊢ B[Wk] : Type@i }} by mauto.
+  assert {{ Γ ⊢s Id ,, M1 : Γ, B}} by mauto 4.
+  assert {{ Γ ⊢ B[Wk][Id,,M1] ≈ B : Type @ i }}.
   {
     transitivity {{{B[Wk ∘ (Id,,M1)]}}};
       [| transitivity {{{B[Id]}}}];
@@ -72,17 +71,16 @@ Proof.
     mauto 4.
 Qed.
 
-Lemma sub_lookup_var1 : forall Γ M1 M2 A B i j,
-    {{Γ ⊢ A : Type@i}} ->
-    {{Γ ⊢ B : Type@j}} ->
-    {{Γ ⊢ M1 : A}} ->
+Lemma sub_lookup_var1 : forall Γ M1 M2 B i,
+    {{Γ ⊢ B : Type@i}} ->
+    {{Γ ⊢ M1 : B}} ->
     {{Γ ⊢ M2 : B}} ->
-    {{Γ ⊢ #1[Id,,M1,,M2] ≈ M1 : A}}.
+    {{Γ ⊢ #1[Id,,M1,,M2] ≈ M1 : B}}.
 Proof.
   intros.
-  assert {{ Γ , A ⊢ B[Wk] : Type@j }} by mauto.
-  assert {{ Γ ⊢s Id ,, M1 : Γ, A}} by mauto 4.
-  assert {{ Γ ⊢ B[Wk][Id,,M1] ≈ B : Type @ j }}.
+  assert {{ Γ , B ⊢ B[Wk] : Type@i }} by mauto.
+  assert {{ Γ ⊢s Id ,, M1 : Γ, B}} by mauto 4.
+  assert {{ Γ ⊢ B[Wk][Id,,M1] ≈ B : Type @ i }}.
   {
     transitivity {{{B[Wk ∘ (Id,,M1)]}}};
       [| transitivity {{{B[Id]}}}];
@@ -94,9 +92,8 @@ Proof.
   - eapply wf_exp_eq_conv;
       [eapply wf_exp_eq_var_S_sub | |];
       mauto 4.
-    admit.
   - eapply wf_exp_eq_conv;
-    [eapply wf_exp_eq_var_0_sub with (A := A) | |];
+    [eapply wf_exp_eq_var_0_sub with (A := B) | |];
     mauto 4.
 Qed.
 
@@ -153,36 +150,15 @@ Proof with mautosolve 4.
         etransitivity.
         -- eapply wf_exp_eq_eq_sub; mauto.
         -- econstructor; mauto 3.
-           2:{
+           ++
              eapply wf_exp_eq_conv;
-             [eapply sub_lookup_var0 with (A:=B) (B:=B) | |];
+             [eapply sub_lookup_var1 with (B:=B) | |];
+               mauto 4.
+           ++ eapply wf_exp_eq_conv;
+             [eapply sub_lookup_var0 with (B:=B) | |];
                mauto 4.
-           }
-
-           ++ eapply wf_exp_eq_conv with (A := B); mauto 2.
-
-              transitivity {{{#0[Id,,M1]}}};
-                [eapply wf_exp_eq_var_S_sub |
-                eapply wf_exp_eq_conv; eapply wf_exp_eq_var_0_sub].
-
-
-
-
-           2:{
-             eapply wf_exp_eq_conv;
-             [eapply wf_exp_eq_var_0_sub | |];
-             mauto 2; mauto 4.
-           }
-
-
-              mauto 4.
-             eapply wf_conv.
-
-    mauto 4.
-    2:mauto 4.
-    eapply wf_sub.
 
-  (* presup_exp_eq cases *)
+  (** presup_exp_eq cases *)
   - assert {{ Γ ⊢s Id ,, N ≈ Id ,, N' : Γ, ℕ }} by mauto 4.
     assert {{ Γ ⊢ B[Id ,, N] ≈ B[Id ,, N'] : Type@i }} by mauto.
     assert {{ Γ ⊢ B[Id ,, N] ≈ B'[Id ,, N'] : Type@i }} by mauto 4.
@@ -349,6 +325,44 @@ 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).
+
+    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].
+
+      mau
+      
+      etransitivity;
+        [econstructor; mauto |].
+
+
+      econstructor.
+
+      assert
+
+
   - 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 c8d14e34..5696f460 100644
--- a/theories/Core/Syntactic/System/Definitions.v
+++ b/theories/Core/Syntactic/System/Definitions.v
@@ -255,7 +255,7 @@ with wf_exp_eq : ctx -> typ -> exp -> exp -> Prop :=
      {{ Δ , A ⊢ BR : M [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 }} ->
@@ -277,7 +277,7 @@ with wf_exp_eq : ctx -> typ -> exp -> exp -> Prop :=
      {{ Γ , A ⊢ BR ≈ BR' : M [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 }} ->
@@ -286,7 +286,7 @@ with wf_exp_eq : ctx -> typ -> exp -> exp -> Prop :=
      {{ Γ , A ⊢ BR : M [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 :
   `( {{ ⊢ Γ }} ->

From 35459049031b0aa3ef35188d4b8e1805b6582a37 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Wed, 18 Sep 2024 17:27:20 -0400
Subject: [PATCH 05/23] one more case

---
 theories/Core/Syntactic/Presup.v | 143 +++++++++++++++++++++++++------
 1 file changed, 116 insertions(+), 27 deletions(-)

diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index 54c20460..21a770e4 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -49,20 +49,20 @@ Ltac gen_presup_IH presup_exp presup_exp_eq presup_sub_eq presup_subtyp H :=
   | _ => gen_presup_ctx H
   end.
 
-Lemma sub_lookup_var0 : forall Γ M1 M2 B i,
+Lemma sub_lookup_var0 : forall Δ Γ σ M1 M2 B i,
+    {{Δ ⊢s σ : Γ}} ->
     {{Γ ⊢ B : Type@i}} ->
-    {{Γ ⊢ M1 : B}} ->
-    {{Γ ⊢ M2 : B}} ->
-    {{Γ ⊢ #0[Id,,M1,,M2] ≈ M2 : B}}.
+    {{Δ ⊢ M1 : B[σ]}} ->
+    {{Δ ⊢ M2 : B[σ]}} ->
+    {{Δ ⊢ #0[σ,,M1,,M2] ≈ M2 : B[σ]}}.
 Proof.
   intros.
   assert {{ Γ , B ⊢ B[Wk] : Type@i }} by mauto.
-  assert {{ Γ ⊢s Id ,, M1 : Γ, B}} by mauto 4.
-  assert {{ Γ ⊢ B[Wk][Id,,M1] ≈ B : Type @ i }}.
+  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 ∘ (Id,,M1)]}}};
-      [| transitivity {{{B[Id]}}}];
-      mauto 3.
+    transitivity {{{B[Wk ∘ (σ,,M1)]}}}.
     - eapply exp_eq_sub_compose_typ; mauto 4.
     - eapply exp_eq_sub_cong_typ2'; mauto 4.
   }
@@ -71,30 +71,55 @@ Proof.
     mauto 4.
 Qed.
 
-Lemma sub_lookup_var1 : forall Γ M1 M2 B i,
+Lemma id_sub_lookup_var0 : forall Γ M1 M2 B i,
     {{Γ ⊢ B : Type@i}} ->
     {{Γ ⊢ M1 : B}} ->
     {{Γ ⊢ M2 : B}} ->
-    {{Γ ⊢ #1[Id,,M1,,M2] ≈ M1 : 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 Id ,, M1 : Γ, B}} by mauto 4.
-  assert {{ Γ ⊢ B[Wk][Id,,M1] ≈ B : Type @ i }}.
+  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 ∘ (Id,,M1)]}}};
-      [| transitivity {{{B[Id]}}}];
-      mauto 3.
+    transitivity {{{B[Wk ∘ (σ,,M1)]}}}.
     - eapply exp_eq_sub_compose_typ; mauto 4.
     - eapply exp_eq_sub_cong_typ2'; mauto 4.
   }
-  transitivity {{{#0[Id,,M1]}}}.
+  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 4.
+    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 presup_exp : forall {Γ M A}, {{ Γ ⊢ M : A }} -> {{ ⊢ Γ }} /\ exists i, {{ Γ ⊢ A : Type@i }}
@@ -152,10 +177,10 @@ Proof with mautosolve 4.
         -- econstructor; mauto 3.
            ++
              eapply wf_exp_eq_conv;
-             [eapply sub_lookup_var1 with (B:=B) | |];
+             [eapply id_sub_lookup_var1 with (B:=B) | |];
                mauto 4.
            ++ eapply wf_exp_eq_conv;
-             [eapply sub_lookup_var0 with (B:=B) | |];
+             [eapply id_sub_lookup_var0 with (B:=B) | |];
                mauto 4.
 
   (** presup_exp_eq cases *)
@@ -344,6 +369,16 @@ Proof with mautosolve 4.
     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.
@@ -351,17 +386,71 @@ Proof with mautosolve 4.
       eapply wf_conv; mauto 2.
       transitivity {{{Eq (B[σ]) (M1[σ]) (M2[σ])}}};
         [mauto 4 | symmetry].
-
-      mau
-      
       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.
 
-      econstructor.
-
-      assert
-
+      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 Wk∘(σ ,, N') ≈ σ : Δ }} by mauto.
     assert {{ Γ ⊢ B[Wk∘(σ ,, N')] ≈ B[σ] : Type@i }} by mauto.

From 8bc5ed371b98cb30e5d11af01ee5775852753451 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Thu, 19 Sep 2024 10:30:26 -0400
Subject: [PATCH 06/23] one more lemma

---
 theories/Core/Syntactic/Presup.v             | 151 ++++++++++++++++++-
 theories/Core/Syntactic/System/Definitions.v |   8 +-
 2 files changed, 154 insertions(+), 5 deletions(-)

diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index 21a770e4..1437ad29 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -122,6 +122,58 @@ Proof.
     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.
+
+
 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 σ' : Δ }} /\ {{ ⊢ Δ }}
@@ -450,7 +502,104 @@ Proof with mautosolve 4.
       * 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 {{ Γ ⊢ 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.
+    }
+    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] ⊢ 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] ⊢ (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.
+
+      2:{
+        eapply wf_exp_eq_conv.
+        econstructor. mauto 4. eauto.
+        all:mauto 2.
+        eapply wf_conv; mauto.
+        mauto 4.
+      }
+
+
+      admit.
+    }
+    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.
+    }
+
+    eapply wf_conv.
+    econstructor.
+    all:mauto 3.
+
+    eapply exp_sub_typ; eauto.
+
 
   - assert {{ Γ ⊢s Wk∘(σ ,, N') ≈ σ : Δ }} by mauto.
     assert {{ Γ ⊢ B[Wk∘(σ ,, N')] ≈ B[σ] : Type@i }} by mauto.
diff --git a/theories/Core/Syntactic/System/Definitions.v b/theories/Core/Syntactic/System/Definitions.v
index 5696f460..cac0e5d5 100644
--- a/theories/Core/Syntactic/System/Definitions.v
+++ b/theories/Core/Syntactic/System/Definitions.v
@@ -95,7 +95,7 @@ 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 ] }} ->
+     {{ Γ , 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 :
@@ -252,7 +252,7 @@ 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
          : B[σ,,M1[σ],,M2[σ],,N[σ]] }} )
@@ -274,7 +274,7 @@ 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
          : B[Id,,M1,,M2,,N] }} )
@@ -283,7 +283,7 @@ with wf_exp_eq : ctx -> typ -> exp -> exp -> Prop :=
      {{ Γ ⊢ 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]
          : B[Id,,M,,M,,refl A M] }} )

From 2fc3a072534b0ce1b57ca9547a59aeddad42bf7f Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Thu, 19 Sep 2024 15:12:41 -0400
Subject: [PATCH 07/23] I am so dead...

---
 theories/Core/Syntactic/Presup.v | 85 +++++++++++++++++++++++++-------
 1 file changed, 68 insertions(+), 17 deletions(-)

diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index 1437ad29..baf45268 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -524,7 +524,7 @@ Proof with mautosolve 4.
       transitivity {{{B[Wk][Wk ∘ (σ,,M1[σ],,M2[σ])]}}};
         [mauto 4 | transitivity {{{B[Wk][σ,,M1[σ]]}}}];
         mauto 2.
-        eapply exp_eq_sub_cong_typ2';
+      eapply exp_eq_sub_cong_typ2';
         mauto 4.
     }
     assert {{ Γ ⊢ L[σ] : (Eq B M1 M2)[σ] }} by mauto 3.
@@ -546,12 +546,13 @@ Proof with mautosolve 4.
     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].
+        [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]}}.
@@ -571,34 +572,84 @@ Proof with mautosolve 4.
         [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]) #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.
-
-      2:{
-        eapply wf_exp_eq_conv.
-        econstructor. mauto 4. eauto.
-        all:mauto 2.
-        eapply wf_conv; mauto.
-        mauto 4.
-      }
-
-
-      admit.
+      - 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[σ] ⊢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 4.
+
+      econstructor.
+    }
+
+    (* assert {{Γ, B[σ] ⊢s q (q (q σ)) ∘ (Id,,#0,,refl (B[σ][Wk]) #0) ≈ q (q σ) : Δ, B, B[Wk], Eq (B[Wk][Wk]) # 1 # 0}}. *)
 
-    eapply wf_conv.
-    econstructor.
-    all:mauto 3.
+    eapply wf_conv;
+    [econstructor | |];
+      mauto 3.
+    + eapply wf_conv; mauto 3.
 
-    eapply exp_sub_typ; eauto.
 
 
   - assert {{ Γ ⊢s Wk∘(σ ,, N') ≈ σ : Δ }} by mauto.

From 3db9dfa57589d37c3608c7e5d0d985e9d2825987 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Thu, 19 Sep 2024 15:15:52 -0400
Subject: [PATCH 08/23] move out lemmas

---
 theories/Core/Syntactic/Presup.v        | 124 -----------------------
 theories/Core/Syntactic/System/Lemmas.v | 125 ++++++++++++++++++++++++
 2 files changed, 125 insertions(+), 124 deletions(-)

diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index baf45268..2e3176e7 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -49,130 +49,6 @@ Ltac gen_presup_IH presup_exp presup_exp_eq presup_sub_eq presup_subtyp H :=
   | _ => gen_presup_ctx H
   end.
 
-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.
-
 
 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 }}
diff --git a/theories/Core/Syntactic/System/Lemmas.v b/theories/Core/Syntactic/System/Lemmas.v
index ab7e860c..fa3ec88e 100644
--- a/theories/Core/Syntactic/System/Lemmas.v
+++ b/theories/Core/Syntactic/System/Lemmas.v
@@ -1083,3 +1083,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.

From 43306064981f0e2d1acca37bee40c735682c44de Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Thu, 19 Sep 2024 18:13:27 -0400
Subject: [PATCH 09/23] more progress

---
 theories/Core/Syntactic/Presup.v | 46 +++++++++++++++++++++++++++-----
 1 file changed, 39 insertions(+), 7 deletions(-)

diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index 2e3176e7..19c0d103 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -449,6 +449,7 @@ Proof with mautosolve 4.
         [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 σ)])}}};
@@ -506,20 +507,51 @@ Proof with mautosolve 4.
         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[σ] ⊢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 4.
+      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.
+        + 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.
+
+        + eapply wf_exp_eq_conv.
+          econstructor; mauto 3.
+
+          Search {{{Id,,#0}}}.
+
 
-      econstructor.
     }
 
-    (* assert {{Γ, B[σ] ⊢s q (q (q σ)) ∘ (Id,,#0,,refl (B[σ][Wk]) #0) ≈ q (q σ) : Δ, B, B[Wk], Eq (B[Wk][Wk]) # 1 # 0}}. *)
+    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}}.
+    {
+
+    }
 
     eapply wf_conv;
     [econstructor | |];

From bd5f9dfe8714c891bd2883266f8127d73bc22952 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Thu, 19 Sep 2024 23:06:14 -0400
Subject: [PATCH 10/23] finish one lemma

---
 theories/Core/Syntactic/Presup.v | 121 +++++++++++++++++++++++++++----
 1 file changed, 105 insertions(+), 16 deletions(-)

diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index 19c0d103..f4b265b5 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -477,6 +477,7 @@ Proof with mautosolve 4.
         [| 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.
@@ -511,6 +512,67 @@ Proof with mautosolve 4.
     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
@@ -526,38 +588,65 @@ Proof with mautosolve 4.
             [mauto |].
           eapply exp_eq_sub_cong_typ1; mauto 4.
       - econstructor; mauto 3.
-        + 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 |].
 
+        eapply wf_exp_eq_conv.
+        econstructor; mauto 3.
+        + eapply wf_conv; [econstructor | |]; mauto 3.
+        + eapply exp_sub_typ; mauto 3.
+        + etransitivity; eauto.
           symmetry.
-          etransitivity;
-            [econstructor; mauto 3 |].
-          econstructor; mauto 3.
-
-        + eapply wf_exp_eq_conv.
-          econstructor; mauto 3.
+          etransitivity; [| etransitivity].
+          * eapply exp_eq_sub_cong_typ2'; mauto 3.
+          * econstructor; mauto 4.
+          * econstructor; mauto 2.
+    }
 
-          Search {{{Id,,#0}}}.
+    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.
     }
 
     eapply wf_conv;
     [econstructor | |];
       mauto 3.
     + eapply wf_conv; mauto 3.
-
+      Search (a_compose _ (Syntax.q _)).
 
 
   - assert {{ Γ ⊢s Wk∘(σ ,, N') ≈ σ : Δ }} by mauto.

From adbb55e2042f80e028aff238f970fcb872db01ba Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Fri, 20 Sep 2024 00:39:20 -0400
Subject: [PATCH 11/23] long way to go

---
 theories/Core/Syntactic/Presup.v | 179 ++++++++++++++++++++++++++++++-
 1 file changed, 176 insertions(+), 3 deletions(-)

diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index f4b265b5..052b2f0e 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -642,12 +642,185 @@ Proof with mautosolve 4.
       - 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[σ] ⊢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 |].
+
+          admit.
+        + eapply wf_exp_eq_conv;
+            [econstructor | |];
+            mauto 2.
+          admit.
+    }
+
+    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 3.
-    + eapply wf_conv; mauto 3.
-      Search (a_compose _ (Syntax.q _)).
+      mauto 2.
+    + eapply wf_conv; mauto 3. admit.
+    + admit.
 
+  - 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 {{ Γ ⊢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.
+    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).
+
+    eapply wf_conv;
+      [econstructor; mauto 3 | mauto 2 | ].
+    + admit.
+    + admit.
+    + admit.
+
+  - admit.
+  - admit.
+  - admit.
+  - admit.
 
   - assert {{ Γ ⊢s Wk∘(σ ,, N') ≈ σ : Δ }} by mauto.
     assert {{ Γ ⊢ B[Wk∘(σ ,, N')] ≈ B[σ] : Type@i }} by mauto.

From 366b319b5880fe4ce355fdcc01cf19abfeb08035 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Fri, 20 Sep 2024 00:40:50 -0400
Subject: [PATCH 12/23] outline the proof

---
 theories/Core/Syntactic/Presup.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index 052b2f0e..5106124a 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -820,7 +820,6 @@ Proof with mautosolve 4.
   - admit.
   - admit.
   - admit.
-  - admit.
 
   - assert {{ Γ ⊢s Wk∘(σ ,, N') ≈ σ : Δ }} by mauto.
     assert {{ Γ ⊢ B[Wk∘(σ ,, N')] ≈ B[σ] : Type@i }} by mauto.

From a9d3bb5a154e5c678136ac1c72d4ae73299a4b6d Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Fri, 20 Sep 2024 00:42:54 -0400
Subject: [PATCH 13/23] outline the proof

---
 theories/Core/Syntactic/Presup.v | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index 5106124a..1064c6dc 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -811,11 +811,12 @@ Proof with mautosolve 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).
 
-    eapply wf_conv;
-      [econstructor; mauto 3 | mauto 2 | ].
-    + admit.
-    + admit.
-    + admit.
+    admit.
+    (* eapply wf_conv; *)
+    (*   [econstructor; mauto 3 | mauto 2 | ]. *)
+    (* + admit. *)
+    (* + admit. *)
+    (* + admit. *)
 
   - admit.
   - admit.
@@ -867,7 +868,8 @@ Proof with mautosolve 4.
   - 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.
+Admitted.
+(* Qed. *)
 
 Ltac gen_presup H := gen_presup_IH @presup_exp @presup_exp_eq @presup_sub_eq @presup_subtyp H.
 

From 50238efd52667d7f579d529b8a9512a0c64a5daf Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Fri, 20 Sep 2024 00:51:47 -0400
Subject: [PATCH 14/23] one simple case

---
 theories/Core/Syntactic/Presup.v | 44 +++++++++++++++++++++++++++++++-
 1 file changed, 43 insertions(+), 1 deletion(-)

diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index 1064c6dc..be63c061 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -820,7 +820,49 @@ Proof with mautosolve 4.
 
   - admit.
   - admit.
-  - admit.
+
+  - 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.

From c5fad9deeb3b89260bf8898cb3ed0c9354c6e127 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Fri, 20 Sep 2024 01:00:45 -0400
Subject: [PATCH 15/23] keep completing

---
 theories/Core/Syntactic/Presup.v | 93 +++++++++++++++++++++++++++++++-
 1 file changed, 91 insertions(+), 2 deletions(-)

diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index be63c061..9d0a7186 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -818,8 +818,97 @@ Proof with mautosolve 4.
     (* + admit. *)
     (* + admit. *)
 
-  - admit.
-  - admit.
+  - 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.
+
+  - 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.
+
+    eapply wf_conv; mauto 3.
+    etransitivity.
+    + eapply exp_eq_sub_compose_typ; mauto 2.
+      admit.
+    + symmetry.
+      eapply exp_eq_sub_cong_typ2'; mauto 2.
+      symmetry.
+      admit.
 
   - eexists.
     eapply exp_sub_typ; mauto 2.

From 9850140e04dc7e8c30eb95c8e602294fc317a62a Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Sun, 29 Sep 2024 18:51:26 -0400
Subject: [PATCH 16/23] more proofs

---
 theories/Core/Syntactic/Presup.v | 35 +++++++++++++++++++++++++++++---
 1 file changed, 32 insertions(+), 3 deletions(-)

diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index b6ec2822..6a000d8b 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -694,6 +694,36 @@ Proof with mautosolve 4.
         + 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}}.
     {
@@ -704,12 +734,11 @@ Proof with mautosolve 4.
         + eapply wf_exp_eq_conv;
             [eapply wf_exp_eq_refl_sub; mauto 3 |
              eapply exp_sub_typ; mauto 3 |].
-
-          admit.
+          mauto 3.
         + eapply wf_exp_eq_conv;
             [econstructor | |];
             mauto 2.
-          admit.
+          etransitivity; mauto 2.
     }
 
     assert {{Γ, B[σ] ⊢s (Id,,#0,,refl (B[Wk]) #0) ∘ q σ

From 2255a004510641cd7fdd0fb3050278f4a2933438 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Sun, 29 Sep 2024 23:48:47 -0400
Subject: [PATCH 17/23] the most complicated case

---
 theories/Core/Syntactic/Presup.v | 152 +++++++++++++++++++++++++++++--
 1 file changed, 144 insertions(+), 8 deletions(-)

diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index 6a000d8b..7833f67c 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -406,6 +406,18 @@ Proof with mautosolve 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.
@@ -413,12 +425,6 @@ Proof with mautosolve 4.
       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.
     }
     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.
@@ -741,6 +747,134 @@ Proof with mautosolve 4.
           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.
@@ -748,8 +882,10 @@ Proof with mautosolve 4.
     eapply wf_conv;
     [econstructor | |];
       mauto 2.
-    + eapply wf_conv; mauto 3. admit.
-    + admit.
+    + 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.

From 11175da6fe824c1490937a8684d30c4999893cd1 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Mon, 30 Sep 2024 09:19:29 -0400
Subject: [PATCH 18/23] more proofs

---
 theories/Core/Syntactic/Presup.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index 7833f67c..d505864d 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -983,6 +983,11 @@ Proof with mautosolve 4.
     (* + admit. *)
     (* + admit. *)
     (* + admit. *)
+    assert {{ ⊢ Γ, B ≈ Γ, B' }} by mauto 3.
+    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.
 
   - eexists.
     eapply exp_sub_typ; mauto 2.

From 016fdb0b1fdbd439d6f7673923bd6aacd5c2e87c Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Mon, 30 Sep 2024 10:44:39 -0400
Subject: [PATCH 19/23] more proofs

---
 theories/Core/Syntactic/Presup.v | 78 +++++++++++++++++++++++++++++---
 1 file changed, 72 insertions(+), 6 deletions(-)

diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index d505864d..acb05fd3 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -977,18 +977,84 @@ Proof with mautosolve 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).
 
-    admit.
-    (* eapply wf_conv; *)
-    (*   [econstructor; mauto 3 | mauto 2 | ]. *)
-    (* + admit. *)
-    (* + admit. *)
-    (* + admit. *)
     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.
+    }
+
+    eapply wf_conv;
+      [econstructor; mauto 3 | mauto 2 | ].
+    + eapply ctxeq_exp; eauto.
+      eapply wf_conv;
+        mauto 2.
+    + admit.
+
   - eexists.
     eapply exp_sub_typ; mauto 2.
     assert {{ Γ ⊢s Id ,, M1 : Γ, B}} by mauto 4.

From e228fe333455cdac2f4584979233dd5e0d371f6f Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Mon, 30 Sep 2024 12:27:02 -0400
Subject: [PATCH 20/23] more proofs

---
 theories/Core/Syntactic/Presup.v | 60 ++++++++++++++++++++++++++++----
 1 file changed, 53 insertions(+), 7 deletions(-)

diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index acb05fd3..5bca5ace 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -959,6 +959,18 @@ Proof with mautosolve 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.
@@ -966,12 +978,6 @@ Proof with mautosolve 4.
       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.
     assert {{ Γ ⊢ Eq B' M1' M2' : Type @ i }} by mauto 4.
@@ -1048,12 +1054,52 @@ Proof with mautosolve 4.
         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.
-    + admit.
+    + etransitivity;
+        [eapply exp_eq_sub_cong_typ2' |
+          eapply exp_eq_sub_cong_typ1];
+        mauto 3.
 
   - eexists.
     eapply exp_sub_typ; mauto 2.

From cd11f3c27d4330c217952cbe9b5abcd372677ba4 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Mon, 30 Sep 2024 15:54:01 -0400
Subject: [PATCH 21/23] finish proofs

---
 theories/Core/Syntactic/Presup.v | 129 +++++++++++++++++++++++++++++--
 1 file changed, 124 insertions(+), 5 deletions(-)

diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index 5bca5ace..7ecbe02c 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -1143,7 +1143,8 @@ Proof with mautosolve 4.
     }
     mauto 3.
 
-  - assert {{ Γ ⊢s Id ,, N : Γ, B}} by mauto 4.
+  - 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 }}.
@@ -1184,14 +1185,133 @@ Proof with mautosolve 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.
-      admit.
     + symmetry.
       eapply exp_eq_sub_cong_typ2'; mauto 2.
       symmetry.
-      admit.
+      etransitivity;
+        [eapply wf_sub_eq_extend_compose |];
+        mauto 2.
 
   - eexists.
     eapply exp_sub_typ; mauto 2.
@@ -1282,8 +1402,7 @@ Proof with mautosolve 4.
   - 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.
-Admitted.
-(* Qed. *)
+Qed.
 
 Ltac gen_presup H := gen_presup_IH @presup_exp @presup_exp_eq @presup_sub_eq @presup_subtyp H.
 

From b722bc3276c4ffda484c7ab246af5a655b0f99e3 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Mon, 30 Sep 2024 15:54:52 -0400
Subject: [PATCH 22/23] add presup

---
 theories/_CoqProject | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/_CoqProject b/theories/_CoqProject
index eba34f6e..417ea44a 100644
--- a/theories/_CoqProject
+++ b/theories/_CoqProject
@@ -64,7 +64,7 @@
 ./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

From 3a5c85ecba3f24d11ff6900a0d09219e1cf10197 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Mon, 30 Sep 2024 16:07:32 -0400
Subject: [PATCH 23/23] finish all syntactic proofs

---
 theories/_CoqProject | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/_CoqProject b/theories/_CoqProject
index 417ea44a..3486db82 100644
--- a/theories/_CoqProject
+++ b/theories/_CoqProject
@@ -58,9 +58,9 @@
 # ./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
@@ -70,7 +70,7 @@
 ./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