From 6b95ab22a44ed7df4bc3ed205a7ccbf2b30dcc10 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Mon, 9 Dec 2024 22:58:06 -0800
Subject: [PATCH 01/11] finished semantic well-formedness of equality type

---
 theories/Core/Soundness/EqualityCases.v       | 41 +++++++++++++-
 theories/Core/Soundness/FunctionCases.v       |  7 +--
 .../Core/Soundness/LogicalRelation/Lemmas.v   | 56 ++++++++++++++++++-
 theories/LibTactics.v                         |  8 ++-
 4 files changed, 100 insertions(+), 12 deletions(-)

diff --git a/theories/Core/Soundness/EqualityCases.v b/theories/Core/Soundness/EqualityCases.v
index ffb6363..48ae372 100644
--- a/theories/Core/Soundness/EqualityCases.v
+++ b/theories/Core/Soundness/EqualityCases.v
@@ -18,7 +18,46 @@ Lemma glu_rel_eq : forall Γ A i M N,
     {{ Γ ⊩ N : A }} ->
     {{ Γ ⊩ Eq A M N : Type@i }}.
 Proof.
-Admitted.
+  intros * HA HM HN.
+  assert {{ ⊩ Γ }} as [SbΓ] by mauto.
+  assert {{ Γ ⊢ A : Type@i }} by mauto.
+  assert {{ Γ ⊢ M : A }} by mauto.
+  assert {{ Γ ⊢ N : A }} by mauto.
+  invert_glu_rel_exp HA.
+  invert_glu_rel_exp HM.
+  invert_glu_rel_exp HN.
+
+  eapply glu_rel_exp_of_typ; mauto 3.
+  intros.
+  assert {{ Δ ⊢s σ : Γ }} by mauto 4.
+  split; mauto 3.
+  applying_glu_rel_judge.
+  saturate_glu_typ_from_el.
+  unify_glu_univ_lvl i.
+  deepexec glu_univ_elem_per_univ ltac:(fun H => pose proof H).
+  match_by_head per_univ ltac:(fun H => destruct H).
+  do 2 deepexec glu_univ_elem_per_elem ltac:(fun H => pose proof H; fail_at_if_dup ltac:(4)).
+
+  eexists; repeat split; mauto.
+  - eexists. per_univ_elem_econstructor; mauto. reflexivity.
+  - intros.
+    match_by_head1 glu_univ_elem invert_glu_univ_elem.
+    handle_per_univ_elem_irrel.
+    handle_functional_glu_univ_elem.
+    econstructor; mauto 3;
+      intros Δ' τ **;
+      assert {{ Δ' ⊢s τ : Δ }} by mauto 2;
+      assert {{ Δ' ⊢s σ ∘ τ ® ρ ∈ SbΓ }} by (eapply glu_ctx_env_sub_monotone; eassumption);
+      assert {{ Δ' ⊢s σ ∘ τ : Γ }} by mauto 2;
+      applying_glu_rel_judge;
+      handle_functional_glu_univ_elem;
+      unify_glu_univ_lvl i.
+    + bulky_rewrite.
+    + assert {{ Δ' ⊢ M[σ][τ] ≈ M[σ ∘ τ] : A[σ ∘ τ] }} by mauto.
+      bulky_rewrite.
+    + assert {{ Δ' ⊢ N[σ][τ] ≈ N[σ ∘ τ] : A[σ ∘ τ] }} by mauto.
+      bulky_rewrite.
+Qed.
 
 #[export]
   Hint Resolve glu_rel_eq : mctt.
diff --git a/theories/Core/Soundness/FunctionCases.v b/theories/Core/Soundness/FunctionCases.v
index 60e5005..a42bcbb 100644
--- a/theories/Core/Soundness/FunctionCases.v
+++ b/theories/Core/Soundness/FunctionCases.v
@@ -47,12 +47,7 @@ Proof.
   intros.
   assert {{ Δ ⊢s σ : Γ }} by mauto 4.
   split; mauto 3.
-  destruct_glu_rel_exp_with_sub.
-  simplify_evals.
-  match_by_head glu_univ_elem ltac:(fun H => directed invert_glu_univ_elem H).
-  handle_functional_glu_univ_elem.
-  unfold univ_glu_exp_pred' in *.
-  destruct_conjs.
+  applying_glu_rel_judge.
   rename m into a.
   assert {{ Γ ⊨ Π A B : Type@i }} as [env_relΓ]%rel_exp_of_typ_inversion1 by mauto 3 using completeness_fundamental_exp.
   assert {{ Γ, A ⊨ B : Type@i }} as [env_relΓA]%rel_exp_of_typ_inversion1 by mauto 3 using completeness_fundamental_exp.
diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
index 87419b8..18b639f 100644
--- a/theories/Core/Soundness/LogicalRelation/Lemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -464,6 +464,19 @@ Proof.
   eapply glu_univ_elem_exp_lower_max_left; mauto.
 Qed.
 
+Lemma glu_univ_elem_exp_conv' : forall {i j a P P' El El' Γ A M m},
+    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    {{ DG a ∈ glu_univ_elem j ↘ P' ↘ El' }} ->
+    {{ Γ ⊢ M : A ® m ∈ El }} ->
+    {{ Γ ⊢ A ® P' }} ->
+    {{ Γ ⊢ M : A ® m ∈ El' }}.
+Proof.
+  intros.
+  eapply glu_univ_elem_exp_conv; only 2: exact H; eauto.
+  mauto 2.
+Qed.
+
+
 Lemma glu_univ_elem_per_subtyp_typ_escape : forall {i a a' P P' El El' Γ A A'},
     {{ Sub a <: a' at i }} ->
     {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
@@ -1144,29 +1157,32 @@ Ltac destruct_glu_rel_by_assumption sub_glu_rel H :=
         mark_with H' 1
     end;
   unmark_all_with 1.
+
 Ltac destruct_glu_rel_exp_with_sub :=
   repeat
     match goal with
     | H : (forall Δ σ ρ, {{ Δ ⊢s σ ® ρ ∈ ?sub_glu_rel }} -> glu_rel_exp_with_sub _ _ _ _ _ _) |- _ =>
-        destruct_glu_rel_by_assumption sub_glu_rel H; mark H
+        destruct_glu_rel_by_assumption sub_glu_rel H; fail_if_dup; mark H
     | H : glu_rel_exp_with_sub _ _ _ _ _ _ |- _ =>
         dependent destruction H
     end;
   unmark_all.
+
 Ltac destruct_glu_rel_sub_with_sub :=
   repeat
     match goal with
     | H : (forall Δ σ ρ, {{ Δ ⊢s σ ® ρ ∈ ?sub_glu_rel }} -> glu_rel_sub_with_sub _ _ _ _ _) |- _ =>
-        destruct_glu_rel_by_assumption sub_glu_rel H; mark H
+        destruct_glu_rel_by_assumption sub_glu_rel H; fail_if_dup; mark H
     | H : glu_rel_exp_with_sub _ _ _ _ _ _ |- _ =>
         dependent destruction H
     end;
   unmark_all.
+
 Ltac destruct_glu_rel_typ_with_sub :=
   repeat
     match goal with
     | H : (forall Δ σ ρ, {{ Δ ⊢s σ ® ρ ∈ ?sub_glu_rel }} -> glu_rel_typ_with_sub _ _ _ _ _) |- _ =>
-        destruct_glu_rel_by_assumption sub_glu_rel H; mark H
+        destruct_glu_rel_by_assumption sub_glu_rel H; fail_if_dup; mark H
     | H : glu_rel_exp_with_sub _ _ _ _ _ _ |- _ =>
         dependent destruction H
     end;
@@ -1315,3 +1331,37 @@ Qed.
 
 #[export]
 Hint Resolve glu_rel_sub_wf_sub : mctt.
+
+
+Ltac saturate_glu_typ_from_el1 :=
+  match goal with
+  | H : glu_univ_elem _ _ ?El _, H1 : ?El _ _ _ _ |- _ =>
+      pose proof (glu_univ_elem_trm_typ _ _ _ _ H _ _ _ _ H1);
+      fail_if_dup
+  end.
+
+Ltac saturate_glu_typ_from_el :=
+  fail_if_dup;
+  repeat saturate_glu_typ_from_el1.
+
+Ltac unify_glu_univ_lvl1 i :=
+  match goal with
+  | H1 : glu_univ_elem _ _ ?El _, H2 : glu_univ_elem i ?P _ _, H3 : ?P _ _, H4 : ?El _ _ _ _
+    |- _ =>
+      pose proof (glu_univ_elem_exp_conv' H1 H2 H4 H3);
+      fail_if_dup
+  end.
+
+Ltac unify_glu_univ_lvl i :=
+  fail_if_dup;
+  repeat unify_glu_univ_lvl1 i.
+
+Ltac applying_glu_rel_judge :=
+  destruct_glu_rel_exp_with_sub;
+  destruct_glu_rel_sub_with_sub;
+  simplify_evals;
+  match_by_head glu_univ_elem ltac:(fun H => directed invert_glu_univ_elem H);
+  handle_functional_glu_univ_elem;
+  unfold univ_glu_exp_pred' in *;
+  destruct_conjs;
+  clear_dups.
diff --git a/theories/LibTactics.v b/theories/LibTactics.v
index 8236038..a2c3393 100644
--- a/theories/LibTactics.v
+++ b/theories/LibTactics.v
@@ -271,7 +271,9 @@ Ltac deepexec lem tac :=
             || deepexec constr:(proj2 lem) tac
   | forall _ : ?T, _ =>
       exvar T ltac:(fun x =>
-                      lazymatch type of T with
+                      let TT := type of T in
+                      let TT := eval simpl in TT in
+                      lazymatch TT with
                       | Prop => match goal with
                             | H : _ |- _ => unify x H; deepexec constr:(lem x) tac
                             | _ => deepexec constr:(lem x) tac
@@ -297,7 +299,9 @@ Ltac cutexec lem C tac :=
                         unify x C;
                         tac lem
                       else
-                        lazymatch type of T with
+                        let TT := type of T in
+                        let TT := eval simpl in TT in
+                        lazymatch TT with
                          | Prop => match goal with
                                | H : _ |- _ => unify x H; cutexec constr:(lem x) C tac
                                | _ => cutexec constr:(lem x) C tac

From 02435106a910cb21b6444cde02a8fbf089ba8eac Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Sun, 15 Dec 2024 10:36:40 -0800
Subject: [PATCH 02/11] Closes #272

---
 theories/Core/Soundness/LogicalRelation/Definitions.v |  6 ++++++
 theories/Core/Soundness/LogicalRelation/Lemmas.v      | 11 +++--------
 theories/Core/Soundness/NatCases.v                    |  8 ++++----
 theories/Core/Soundness/UniverseCases.v               |  6 +++---
 4 files changed, 16 insertions(+), 15 deletions(-)

diff --git a/theories/Core/Soundness/LogicalRelation/Definitions.v b/theories/Core/Soundness/LogicalRelation/Definitions.v
index 11d2d8d..240a75e 100644
--- a/theories/Core/Soundness/LogicalRelation/Definitions.v
+++ b/theories/Core/Soundness/LogicalRelation/Definitions.v
@@ -415,6 +415,12 @@ Variant glu_rel_sub_with_sub Δ τ (Sb : glu_sub_pred) σ ρ : Prop :=
 Definition glu_rel_ctx Γ : Prop := exists Sb, {{ EG Γ ∈ glu_ctx_env ↘ Sb }}.
 Arguments glu_rel_ctx Γ/.
 
+Definition glu_rel_exp_resp_sub_env i Sb M A :=
+  forall Δ σ ρ,
+    {{ Δ ⊢s σ ® ρ ∈ Sb }} ->
+    glu_rel_exp_with_sub i Δ M A σ ρ.
+Arguments glu_rel_exp_resp_sub_env i Sb M A/.
+
 Definition glu_rel_exp Γ M A : Prop :=
   exists Sb,
     {{ EG Γ ∈ glu_ctx_env ↘ Sb }} /\
diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
index 18b639f..4e86989 100644
--- a/theories/Core/Soundness/LogicalRelation/Lemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -1205,18 +1205,13 @@ Proof.
   mauto.
 Qed.
 
-Definition glu_rel_exp_clean_inversion2_result i Sb M A :=
-  forall Δ σ ρ,
-    {{ Δ ⊢s σ ® ρ ∈ Sb }} ->
-    glu_rel_exp_with_sub i Δ M A σ ρ.
-
 Lemma glu_rel_exp_clean_inversion2 : forall {i Γ Sb M A},
     {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
     {{ Γ ⊩ A : Type@i }} ->
     {{ Γ ⊩ M : A }} ->
-    glu_rel_exp_clean_inversion2_result i Sb M A.
+    glu_rel_exp_resp_sub_env i Sb M A.
 Proof.
-  unfold glu_rel_exp_clean_inversion2_result.
+  simpl.
   intros * ? HA HM.
   eapply glu_rel_exp_clean_inversion1 in HA; [| eassumption].
   eapply glu_rel_exp_clean_inversion1 in HM; [| eassumption].
@@ -1234,7 +1229,7 @@ Qed.
 
 Ltac invert_glu_rel_exp H :=
   (unshelve eapply (glu_rel_exp_clean_inversion2 _ _) in H; shelve_unifiable; [eassumption | eassumption |];
-   unfold glu_rel_exp_clean_inversion2_result in H)
+   simpl in H)
   + (unshelve eapply (glu_rel_exp_clean_inversion1 _) in H; shelve_unifiable; [eassumption |];
      destruct H as [])
   + (inversion H; subst).
diff --git a/theories/Core/Soundness/NatCases.v b/theories/Core/Soundness/NatCases.v
index 3d3f306..75fffeb 100644
--- a/theories/Core/Soundness/NatCases.v
+++ b/theories/Core/Soundness/NatCases.v
@@ -51,7 +51,7 @@ Hint Resolve glu_rel_exp_sub_nat : mctt.
 Lemma glu_rel_exp_clean_inversion2'' : forall {Γ Sb M},
     {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
     {{ Γ ⊩ M : ℕ }} ->
-    glu_rel_exp_clean_inversion2_result 0 Sb M {{{ ℕ }}}.
+    glu_rel_exp_resp_sub_env 0 Sb M {{{ ℕ }}}.
 Proof.
   intros * ? HM.
   assert {{ Γ ⊩ ℕ : Type@0 }} by mauto 3.
@@ -60,11 +60,11 @@ Qed.
 
 Ltac invert_glu_rel_exp H ::=
   (unshelve eapply (glu_rel_exp_clean_inversion2'' _) in H; shelve_unifiable; [eassumption |];
-   unfold glu_rel_exp_clean_inversion2_result in H)
+   unfold glu_rel_exp_resp_sub_env in H)
   + (unshelve eapply (glu_rel_exp_clean_inversion2' _) in H; shelve_unifiable; [eassumption |];
-     unfold glu_rel_exp_clean_inversion2_result in H)
+     unfold glu_rel_exp_resp_sub_env in H)
   + (unshelve eapply (glu_rel_exp_clean_inversion2 _ _) in H; shelve_unifiable; [eassumption | eassumption |];
-     unfold glu_rel_exp_clean_inversion2_result in H)
+     unfold glu_rel_exp_resp_sub_env in H)
   + (unshelve eapply (glu_rel_exp_clean_inversion1 _) in H; shelve_unifiable; [eassumption |];
      destruct H as [])
   + (inversion H; subst).
diff --git a/theories/Core/Soundness/UniverseCases.v b/theories/Core/Soundness/UniverseCases.v
index b9aa78d..a64d42e 100644
--- a/theories/Core/Soundness/UniverseCases.v
+++ b/theories/Core/Soundness/UniverseCases.v
@@ -46,7 +46,7 @@ Hint Resolve glu_rel_exp_typ : mctt.
 Lemma glu_rel_exp_clean_inversion2' : forall {i Γ Sb M},
     {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
     {{ Γ ⊩ M : Type@i }} ->
-    glu_rel_exp_clean_inversion2_result (S i) Sb M {{{ Type@i }}}.
+    glu_rel_exp_resp_sub_env (S i) Sb M {{{ Type@i }}}.
 Proof.
   intros * ? HM.
   assert {{ Γ ⊩ Type@i : Type@(S i) }} by mauto 3.
@@ -55,9 +55,9 @@ Qed.
 
 Ltac invert_glu_rel_exp H ::=
   (unshelve eapply (glu_rel_exp_clean_inversion2' _) in H; shelve_unifiable; [eassumption |];
-   unfold glu_rel_exp_clean_inversion2_result in H)
+   simpl in H)
   + (unshelve eapply (glu_rel_exp_clean_inversion2 _ _) in H; shelve_unifiable; [eassumption | eassumption |];
-     unfold glu_rel_exp_clean_inversion2_result in H)
+     simpl in H)
   + (unshelve eapply (glu_rel_exp_clean_inversion1 _) in H; shelve_unifiable; [eassumption |];
      destruct H as [])
   + (inversion H; subst).

From c04989587d541cd05efca295a46f5e475c2b8c27 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Sun, 15 Dec 2024 11:00:39 -0800
Subject: [PATCH 03/11] proved semantic rule for refl

---
 theories/Core/Soundness/EqualityCases.v       | 30 +++++++++++++++++--
 .../Core/Soundness/LogicalRelation/Lemmas.v   | 24 +++++++++++++++
 2 files changed, 51 insertions(+), 3 deletions(-)

diff --git a/theories/Core/Soundness/EqualityCases.v b/theories/Core/Soundness/EqualityCases.v
index 48ae372..e4ec7f7 100644
--- a/theories/Core/Soundness/EqualityCases.v
+++ b/theories/Core/Soundness/EqualityCases.v
@@ -62,12 +62,36 @@ Qed.
 #[export]
   Hint Resolve glu_rel_eq : mctt.
 
-Lemma glu_rel_eq_refl : forall Γ A i M,
-    {{ Γ ⊩ A : Type@i }} ->
+Lemma glu_rel_eq_refl : forall Γ A M,
     {{ Γ ⊩ M : A }} ->
     {{ Γ ⊩ refl A M : Eq A M M }}.
 Proof.
-Admitted.
+  intros * HM.
+  assert {{ ⊩ Γ }} as [SbΓ] by mauto.
+  assert {{ Γ ⊢ M : A }} by mauto.
+  invert_glu_rel_exp HM.
+  assert {{ Γ ⊢ A : Type@x }} by mauto.
+  eexists; split; eauto.
+  exists x; intros.
+  assert {{ Δ ⊢s σ : Γ }} by mauto 4.
+  applying_glu_rel_judge.
+  saturate_glu_typ_from_el.
+  deepexec glu_univ_elem_per_univ ltac:(fun H => pose proof H).
+  match_by_head per_univ ltac:(fun H => destruct H).
+  deepexec glu_univ_elem_per_elem ltac:(fun H => pose proof H; fail_at_if_dup ltac:(4)).
+  saturate_glu_info.
+  eexists; repeat split; mauto.
+  - glu_univ_elem_econstructor; mauto 3; reflexivity.
+  - do 2 try econstructor; mauto 3;
+      try (intros Δ' τ **;
+             assert {{ Δ' ⊢s τ : Δ }} by mauto 2;
+           assert {{ Δ' ⊢s σ ∘ τ ® ρ ∈ SbΓ }} by (eapply glu_ctx_env_sub_monotone; eassumption);
+           assert {{ Δ' ⊢s σ ∘ τ : Γ }} by mauto 2;
+           assert {{ Δ' ⊢ M[σ][τ] ≈ M[σ ∘ τ] : A[σ ∘ τ] }} by mauto;
+           applying_glu_rel_judge;
+           saturate_glu_typ_from_el;
+           bulky_rewrite).
+Qed.
 
 #[export]
   Hint Resolve glu_rel_eq_refl : mctt.
diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
index 4e86989..0c1b6b4 100644
--- a/theories/Core/Soundness/LogicalRelation/Lemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -1234,6 +1234,7 @@ Ltac invert_glu_rel_exp H :=
      destruct H as [])
   + (inversion H; subst).
 
+
 Lemma glu_rel_exp_to_wf_exp : forall {Γ A M},
     {{ Γ ⊩ M : A }} ->
     {{ Γ ⊢ M : A }}.
@@ -1360,3 +1361,26 @@ Ltac applying_glu_rel_judge :=
   unfold univ_glu_exp_pred' in *;
   destruct_conjs;
   clear_dups.
+
+
+Lemma glu_rel_exp_preserves_lvl : forall Γ Sb M A i,
+    {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
+    (forall Δ σ ρ,
+        {{ Δ ⊢s σ ® ρ ∈ Sb }} ->
+        glu_rel_exp_with_sub i Δ M A σ ρ) ->
+    {{ Γ ⊢ A : Type@i }}.
+Proof.
+  intros.
+  assert (exists env_relΓ, {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ env_relΓ }}) as [env_relΓ] by mauto 3.
+  assert (exists ρ ρ', initial_env Γ ρ /\ initial_env Γ ρ' /\ {{ Dom ρ ≈ ρ' ∈ env_relΓ }}) as [ρ] by mauto 3 using per_ctx_then_per_env_initial_env.
+  destruct_conjs.
+  functional_initial_env_rewrite_clear.
+  assert {{ Γ ⊢s Id ® ρ ∈ Sb }} by (eapply initial_env_glu_rel_exp; mauto 3).
+  destruct_glu_rel_exp_with_sub.
+  saturate_glu_typ_from_el.
+  saturate_glu_info.
+  mauto 3.
+Qed.
+
+#[export]
+Hint Resolve glu_rel_exp_preserves_lvl : mctt.

From 7ba0096861310d4ad6987294ac23f6f6edf164a8 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Sun, 15 Dec 2024 11:01:44 -0800
Subject: [PATCH 04/11] minor improvement

---
 theories/Core/Soundness/EqualityCases.v | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/theories/Core/Soundness/EqualityCases.v b/theories/Core/Soundness/EqualityCases.v
index e4ec7f7..5062213 100644
--- a/theories/Core/Soundness/EqualityCases.v
+++ b/theories/Core/Soundness/EqualityCases.v
@@ -83,14 +83,14 @@ Proof.
   eexists; repeat split; mauto.
   - glu_univ_elem_econstructor; mauto 3; reflexivity.
   - do 2 try econstructor; mauto 3;
-      try (intros Δ' τ **;
-             assert {{ Δ' ⊢s τ : Δ }} by mauto 2;
-           assert {{ Δ' ⊢s σ ∘ τ ® ρ ∈ SbΓ }} by (eapply glu_ctx_env_sub_monotone; eassumption);
-           assert {{ Δ' ⊢s σ ∘ τ : Γ }} by mauto 2;
-           assert {{ Δ' ⊢ M[σ][τ] ≈ M[σ ∘ τ] : A[σ ∘ τ] }} by mauto;
-           applying_glu_rel_judge;
-           saturate_glu_typ_from_el;
-           bulky_rewrite).
+    intros Δ' τ **;
+      assert {{ Δ' ⊢s τ : Δ }} by mauto 2;
+    assert {{ Δ' ⊢s σ ∘ τ ® ρ ∈ SbΓ }} by (eapply glu_ctx_env_sub_monotone; eassumption);
+    assert {{ Δ' ⊢s σ ∘ τ : Γ }} by mauto 2;
+    assert {{ Δ' ⊢ M[σ][τ] ≈ M[σ ∘ τ] : A[σ ∘ τ] }} by mauto;
+    applying_glu_rel_judge;
+    saturate_glu_typ_from_el;
+    bulky_rewrite.
 Qed.
 
 #[export]

From c01fbc90ac6b741fcc0872bf138e48f6fd28b5eb Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Sun, 15 Dec 2024 22:33:17 -0800
Subject: [PATCH 05/11] improve one automation

---
 theories/Core/Soundness/FunctionCases.v       |  2 +-
 .../Core/Soundness/LogicalRelation/Lemmas.v   |  8 ++--
 theories/Core/Soundness/SubtypingCases.v      | 44 ++++++++++++++++++-
 theories/Core/Soundness/UniverseCases.v       | 13 +++---
 4 files changed, 55 insertions(+), 12 deletions(-)

diff --git a/theories/Core/Soundness/FunctionCases.v b/theories/Core/Soundness/FunctionCases.v
index a42bcbb..6c39f92 100644
--- a/theories/Core/Soundness/FunctionCases.v
+++ b/theories/Core/Soundness/FunctionCases.v
@@ -47,7 +47,7 @@ Proof.
   intros.
   assert {{ Δ ⊢s σ : Γ }} by mauto 4.
   split; mauto 3.
-  applying_glu_rel_judge.
+  apply_glu_rel_judge.
   rename m into a.
   assert {{ Γ ⊨ Π A B : Type@i }} as [env_relΓ]%rel_exp_of_typ_inversion1 by mauto 3 using completeness_fundamental_exp.
   assert {{ Γ, A ⊨ B : Type@i }} as [env_relΓA]%rel_exp_of_typ_inversion1 by mauto 3 using completeness_fundamental_exp.
diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
index 0c1b6b4..d7733d4 100644
--- a/theories/Core/Soundness/LogicalRelation/Lemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -650,7 +650,7 @@ Proof.
     handle_functional_glu_univ_elem.
     trivial.
 Qed.
-
+xb
 Lemma glu_univ_elem_per_subtyp_trm_conv : forall {i j k a a' P P' El El' Γ A A' M m},
     {{ Sub a <: a' at i }} ->
     {{ DG a ∈ glu_univ_elem j ↘ P ↘ El }} ->
@@ -1227,12 +1227,13 @@ Proof.
   eapply glu_univ_elem_exp_conv; revgoals; mauto 3.
 Qed.
 
+#[global]
 Ltac invert_glu_rel_exp H :=
   (unshelve eapply (glu_rel_exp_clean_inversion2 _ _) in H; shelve_unifiable; [eassumption | eassumption |];
    simpl in H)
   + (unshelve eapply (glu_rel_exp_clean_inversion1 _) in H; shelve_unifiable; [eassumption |];
      destruct H as [])
-  + (inversion H; subst).
+  + (inversion H as [? [? [? ?]]]; subst).
 
 
 Lemma glu_rel_exp_to_wf_exp : forall {Γ A M},
@@ -1352,7 +1353,8 @@ Ltac unify_glu_univ_lvl i :=
   fail_if_dup;
   repeat unify_glu_univ_lvl1 i.
 
-Ltac applying_glu_rel_judge :=
+Ltac apply_glu_rel_judge :=
+  destruct_glu_rel_typ_with_sub;
   destruct_glu_rel_exp_with_sub;
   destruct_glu_rel_sub_with_sub;
   simplify_evals;
diff --git a/theories/Core/Soundness/SubtypingCases.v b/theories/Core/Soundness/SubtypingCases.v
index 3f88be3..6abdda9 100644
--- a/theories/Core/Soundness/SubtypingCases.v
+++ b/theories/Core/Soundness/SubtypingCases.v
@@ -54,18 +54,58 @@ Qed.
 #[export]
 Hint Resolve glu_rel_sub_subtyp : mctt.
 
+
+#[local]
+Lemma glu_rel_exp_conv' : forall {Γ M A A' i},
+    {{ Γ ⊩ M : A }} ->
+    {{ Γ ⊢ A ≈ A' : Type@i }} -> (** proof trick, will discharge. see the next lemma. *)
+    {{ Γ ⊢ A ≈ A' : Type@i }} ->
+    {{ Γ ⊩ M : A' }}.
+Proof.
+  intros * [? [? [k ?]]] [env_relΓ [? [? ?]]]%completeness_fundamental_exp_eq ?.
+  econstructor; split; [eassumption |].
+  exists (max i k); intros.
+  assert {{ Δ ⊢s σ : Γ }} by mauto 4.
+
+  destruct_glu_rel_exp_with_sub.
+  assert {{ Dom ρ ≈ ρ ∈ env_relΓ }} by (eapply glu_ctx_env_per_env; mauto).
+  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+  destruct_by_head rel_typ.
+  match_by_head eval_exp ltac:(fun H => directed dependent destruction H).
+  destruct_by_head rel_exp.
+  saturate_refl.
+  invert_per_univ_elems.
+  apply_equiv_left.
+  destruct_all.
+  handle_per_univ_elem_irrel.
+  assert (i <= max i k) by lia.
+  assert (k <= max i k) by lia.
+  assert {{ Δ ⊢ A'[σ] ≈ A[σ] : Type@(max i k) }} by mauto 4.
+  eapply mk_glu_rel_exp_with_sub''; intuition mauto using per_univ_elem_cumu_max_left, per_univ_elem_cumu_max_right.
+  bulky_rewrite.
+  eapply glu_univ_elem_exp_cumu_ge; try eassumption.
+  eapply glu_univ_elem_resp_per_univ; eauto.
+  symmetry. mauto.
+Qed.
+
 Lemma glu_rel_exp_conv : forall {Γ M A A' i},
     {{ Γ ⊩ M : A }} ->
-    {{ Γ ⊩ A' : Type@i }} ->
     {{ Γ ⊢ A ≈ A' : Type@i }} ->
     {{ Γ ⊩ M : A' }}.
 Proof.
-  mauto 3.
+  eauto using glu_rel_exp_conv'.
 Qed.
 
 #[export]
 Hint Resolve glu_rel_exp_conv : mctt.
 
+Add Parametric Morphism i Γ M : (glu_rel_exp Γ M)
+    with signature (wf_exp_eq Γ {{{Type@i}}}) ==> iff as foo.
+Proof.
+  split; mauto 3.
+Qed.
+
+
 Lemma glu_rel_sub_conv : forall {Γ σ Δ Δ'},
     {{ Γ ⊩s σ : Δ }} ->
     {{ ⊩ Δ' }} ->
diff --git a/theories/Core/Soundness/UniverseCases.v b/theories/Core/Soundness/UniverseCases.v
index a64d42e..a8f1c86 100644
--- a/theories/Core/Soundness/UniverseCases.v
+++ b/theories/Core/Soundness/UniverseCases.v
@@ -53,14 +53,15 @@ Proof.
   eapply glu_rel_exp_clean_inversion2 in HM; mauto 3.
 Qed.
 
-Ltac invert_glu_rel_exp H ::=
+#[local]
+  Ltac invert_glu_rel_exp_old H :=
+  invert_glu_rel_exp H.
+
+#[global]
+  Ltac invert_glu_rel_exp H :=
   (unshelve eapply (glu_rel_exp_clean_inversion2' _) in H; shelve_unifiable; [eassumption |];
    simpl in H)
-  + (unshelve eapply (glu_rel_exp_clean_inversion2 _ _) in H; shelve_unifiable; [eassumption | eassumption |];
-     simpl in H)
-  + (unshelve eapply (glu_rel_exp_clean_inversion1 _) in H; shelve_unifiable; [eassumption |];
-     destruct H as [])
-  + (inversion H; subst).
+  + invert_glu_rel_exp_old H.
 
 Lemma glu_rel_exp_sub_typ : forall {Γ σ Δ i A},
     {{ Γ ⊩s σ : Δ }} ->

From d6221576a605117694d238d478368974b465bcb2 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Sun, 15 Dec 2024 22:40:07 -0800
Subject: [PATCH 06/11] typo

---
 theories/Core/Soundness/LogicalRelation/Lemmas.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
index d7733d4..b9680f2 100644
--- a/theories/Core/Soundness/LogicalRelation/Lemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -650,7 +650,7 @@ Proof.
     handle_functional_glu_univ_elem.
     trivial.
 Qed.
-xb
+
 Lemma glu_univ_elem_per_subtyp_trm_conv : forall {i j k a a' P P' El El' Γ A A' M m},
     {{ Sub a <: a' at i }} ->
     {{ DG a ∈ glu_univ_elem j ↘ P ↘ El }} ->

From aaff934597abd9711cde3f589084d7bd9e74c711 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Tue, 17 Dec 2024 20:11:23 -0800
Subject: [PATCH 07/11] more tactic setups

---
 theories/Core/Soundness/EqualityCases.v       | 20 +++++--------
 .../Soundness/LogicalRelation/Definitions.v   |  7 +++++
 .../Core/Soundness/LogicalRelation/Lemmas.v   | 30 +++++++++++++++++--
 3 files changed, 43 insertions(+), 14 deletions(-)

diff --git a/theories/Core/Soundness/EqualityCases.v b/theories/Core/Soundness/EqualityCases.v
index 5062213..c757feb 100644
--- a/theories/Core/Soundness/EqualityCases.v
+++ b/theories/Core/Soundness/EqualityCases.v
@@ -20,18 +20,14 @@ Lemma glu_rel_eq : forall Γ A i M N,
 Proof.
   intros * HA HM HN.
   assert {{ ⊩ Γ }} as [SbΓ] by mauto.
-  assert {{ Γ ⊢ A : Type@i }} by mauto.
-  assert {{ Γ ⊢ M : A }} by mauto.
-  assert {{ Γ ⊢ N : A }} by mauto.
-  invert_glu_rel_exp HA.
-  invert_glu_rel_exp HM.
-  invert_glu_rel_exp HN.
+  saturate_syn_judge.
+  invert_sem_judge.
 
   eapply glu_rel_exp_of_typ; mauto 3.
   intros.
   assert {{ Δ ⊢s σ : Γ }} by mauto 4.
   split; mauto 3.
-  applying_glu_rel_judge.
+  apply_glu_rel_judge.
   saturate_glu_typ_from_el.
   unify_glu_univ_lvl i.
   deepexec glu_univ_elem_per_univ ltac:(fun H => pose proof H).
@@ -49,7 +45,7 @@ Proof.
       assert {{ Δ' ⊢s τ : Δ }} by mauto 2;
       assert {{ Δ' ⊢s σ ∘ τ ® ρ ∈ SbΓ }} by (eapply glu_ctx_env_sub_monotone; eassumption);
       assert {{ Δ' ⊢s σ ∘ τ : Γ }} by mauto 2;
-      applying_glu_rel_judge;
+      apply_glu_rel_judge;
       handle_functional_glu_univ_elem;
       unify_glu_univ_lvl i.
     + bulky_rewrite.
@@ -68,13 +64,13 @@ Lemma glu_rel_eq_refl : forall Γ A M,
 Proof.
   intros * HM.
   assert {{ ⊩ Γ }} as [SbΓ] by mauto.
-  assert {{ Γ ⊢ M : A }} by mauto.
-  invert_glu_rel_exp HM.
+  saturate_syn_judge.
+  invert_sem_judge.
   assert {{ Γ ⊢ A : Type@x }} by mauto.
   eexists; split; eauto.
   exists x; intros.
   assert {{ Δ ⊢s σ : Γ }} by mauto 4.
-  applying_glu_rel_judge.
+  apply_glu_rel_judge.
   saturate_glu_typ_from_el.
   deepexec glu_univ_elem_per_univ ltac:(fun H => pose proof H).
   match_by_head per_univ ltac:(fun H => destruct H).
@@ -88,7 +84,7 @@ Proof.
     assert {{ Δ' ⊢s σ ∘ τ ® ρ ∈ SbΓ }} by (eapply glu_ctx_env_sub_monotone; eassumption);
     assert {{ Δ' ⊢s σ ∘ τ : Γ }} by mauto 2;
     assert {{ Δ' ⊢ M[σ][τ] ≈ M[σ ∘ τ] : A[σ ∘ τ] }} by mauto;
-    applying_glu_rel_judge;
+    apply_glu_rel_judge;
     saturate_glu_typ_from_el;
     bulky_rewrite.
 Qed.
diff --git a/theories/Core/Soundness/LogicalRelation/Definitions.v b/theories/Core/Soundness/LogicalRelation/Definitions.v
index 240a75e..d576923 100644
--- a/theories/Core/Soundness/LogicalRelation/Definitions.v
+++ b/theories/Core/Soundness/LogicalRelation/Definitions.v
@@ -430,6 +430,13 @@ Definition glu_rel_exp Γ M A : Prop :=
         glu_rel_exp_with_sub i Δ M A σ ρ.
 Arguments glu_rel_exp Γ M A/.
 
+
+Definition glu_rel_sub_resp_sub_env Sb Sb' τ :=
+  forall Δ σ ρ,
+    {{ Δ ⊢s σ ® ρ ∈ Sb }} ->
+    glu_rel_sub_with_sub Δ τ Sb' σ ρ.
+Arguments glu_rel_sub_resp_sub_env Sb Sb' τ/.
+
 Definition glu_rel_sub Γ τ Γ' : Prop :=
   exists Sb Sb',
     {{ EG Γ ∈ glu_ctx_env ↘ Sb }} /\
diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
index b9680f2..6c31df4 100644
--- a/theories/Core/Soundness/LogicalRelation/Lemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -1292,9 +1292,9 @@ Lemma glu_rel_sub_clean_inversion3 : forall {Γ Sb τ Γ' Sb'},
     {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
     {{ EG Γ' ∈ glu_ctx_env ↘ Sb' }} ->
     {{ Γ ⊩s τ : Γ' }} ->
-    forall (Δ : ctx) (σ : sub) (ρ : env), Sb Δ σ ρ -> glu_rel_sub_with_sub Δ τ Sb' σ ρ.
+    glu_rel_sub_resp_sub_env Sb Sb' τ.
 Proof.
-  intros * ? ? Hglu.
+  simpl. intros * ? ? Hglu.
   eapply glu_rel_sub_clean_inversion2 in Hglu; [| eassumption].
   destruct_conjs.
   handle_functional_glu_ctx_env.
@@ -1386,3 +1386,29 @@ Qed.
 
 #[export]
 Hint Resolve glu_rel_exp_preserves_lvl : mctt.
+
+
+
+Ltac saturate_syn_judge1 :=
+  match goal with
+  | H : {{ ^?Γ ⊩ ^?M : ^?A }} |- _ =>
+      assert {{ Γ ⊢ M : A }} by mauto; fail_if_dup
+  | H : {{ ^?Γ ⊩s ^?τ : ^?Γ' }} |- _ =>
+      assert {{ Γ ⊢s τ : Γ' }} by mauto; fail_if_dup
+  end.
+
+#[global]
+  Ltac saturate_syn_judge :=
+  repeat saturate_syn_judge1.
+
+Ltac invert_sem_judge1 :=
+  match goal with
+  | H : {{ ^?Γ ⊩ ^?M : ^?A }} |- _ =>
+      invert_glu_rel_exp H
+  | H : {{ ^?Γ ⊩s ^?τ : ^?Γ' }} |- _ =>
+      invert_glu_rel_sub H
+  end.
+
+#[global]
+  Ltac invert_sem_judge :=
+  repeat invert_sem_judge1.

From f91cebd941003bcf54a5d44ad8f99fb3b962b6fa Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Tue, 17 Dec 2024 20:12:30 -0800
Subject: [PATCH 08/11] to export

---
 theories/Core/Soundness/LogicalRelation/Lemmas.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
index 6c31df4..72875c2 100644
--- a/theories/Core/Soundness/LogicalRelation/Lemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -1227,7 +1227,7 @@ Proof.
   eapply glu_univ_elem_exp_conv; revgoals; mauto 3.
 Qed.
 
-#[global]
+#[export]
 Ltac invert_glu_rel_exp H :=
   (unshelve eapply (glu_rel_exp_clean_inversion2 _ _) in H; shelve_unifiable; [eassumption | eassumption |];
    simpl in H)
@@ -1397,7 +1397,7 @@ Ltac saturate_syn_judge1 :=
       assert {{ Γ ⊢s τ : Γ' }} by mauto; fail_if_dup
   end.
 
-#[global]
+#[export]
   Ltac saturate_syn_judge :=
   repeat saturate_syn_judge1.
 
@@ -1409,6 +1409,6 @@ Ltac invert_sem_judge1 :=
       invert_glu_rel_sub H
   end.
 
-#[global]
+#[export]
   Ltac invert_sem_judge :=
   repeat invert_sem_judge1.

From a55fc6760ced90032bc1a93267a06c897dfa5504 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Tue, 17 Dec 2024 20:23:06 -0800
Subject: [PATCH 09/11] revert

---
 theories/Core/Soundness/EqualityCases.v | 62 +++++++++++++++++++++++++
 1 file changed, 62 insertions(+)

diff --git a/theories/Core/Soundness/EqualityCases.v b/theories/Core/Soundness/EqualityCases.v
index c757feb..4885ea5 100644
--- a/theories/Core/Soundness/EqualityCases.v
+++ b/theories/Core/Soundness/EqualityCases.v
@@ -101,6 +101,68 @@ Lemma glu_rel_eq_eqrec : forall Γ A i M1 M2 B j BR N,
     {{ Γ, A ⊩ BR : B[Id,,#0,,refl A[Wk] #0] }} ->
     {{ Γ ⊩ N : Eq A M1 M2 }} ->
     {{ Γ ⊩ eqrec N as Eq A M1 M2 return B | refl -> BR end : B[Id,,M1,,M2,,N] }}.
+Proof.
+  intros * HA HM1 HM2 HB HBR HN.
+  assert {{ ⊩ Γ }} by mauto.
+  assert {{ ⊩ Γ }} as [SbΓ] by mauto.
+  saturate_syn_judge.
+
+  assert {{ Γ ⊩s Id,,M1 : Γ, A }} by (eapply glu_rel_sub_extend; mauto 3; bulky_rewrite).
+  assert {{ ⊩ Γ , A }} by mauto.
+  assert {{ ⊩ Γ , A }} as [SbΓA] by mauto.
+  assert {{ Γ ⊩s Id,,M1,,M2 : Γ, A, A[Wk] }} by (eapply glu_rel_sub_extend; mauto 4).
+  assert {{ ⊩ Γ , A, A[Wk] }} by mauto.
+  assert {{ ⊩ Γ , A, A[Wk] }} as [SbΓAA] by mauto.
+  assert {{ Γ ⊩s Id,,M1,,M2,,N : Γ, A, A[Wk], Eq A[Wk ∘ Wk] #1 #0 }}.
+  {
+    eapply glu_rel_sub_extend; mauto 4.
+    eapply glu_rel_eq.
+    - mauto.
+    - rewrite <- @exp_eq_sub_compose_typ with (i := i); mauto 3.
+    - rewrite <- @exp_eq_sub_compose_typ with (i := i); mauto 3.
+  }
+  saturate_syn_judge.
+
+  invert_sem_judge1.
+  invert_sem_judge1.
+  invert_sem_judge1.
+  invert_sem_judge1.
+  invert_sem_judge1.
+  invert_sem_judge1.
+  invert_sem_judge1.
+  invert_sem_judge1.
+
+
+Ltac invert_glu_rel_sub H :=
+  (unshelve eapply (glu_rel_sub_clean_inversion3 _ _) in H; shelve_unifiable; [eassumption | eassumption |])
+  + (unshelve eapply (glu_rel_sub_clean_inversion2 _) in H; shelve_unifiable; [eassumption |];
+     destruct H as [? []])
+  + (unshelve eapply (glu_rel_sub_clean_inversion1 _) in H; shelve_unifiable; [eassumption |];
+     destruct H as [? []])
+  + (inversion H; subst).
+
+unshelve eapply (glu_rel_sub_clean_inversion3 _ _) in H10; shelve_unifiable.
+eassumption.
+eassumption.
+invert_glu_rel_sub H10.
+
+
+  invert_sem_judge1.
+
+  eexists; split; eauto.
+  exists j; intros.
+  assert {{ Δ ⊢s σ : Γ }} by mauto 4.
+  apply_glu_rel_judge.
+  repeat invert_glu_rel1.
+  saturate_glu_typ_from_el.
+  unify_glu_univ_lvl i.
+  deepexec (glu_univ_elem_per_univ i) ltac:(fun H => pose proof H).
+  match_by_head per_univ ltac:(fun H => destruct H).
+  do 2 deepexec (glu_univ_elem_per_elem i) ltac:(fun H => pose proof H; fail_at_if_dup ltac:(4)).
+  saturate_glu_info.
+
+  econstructor.
+
 Admitted.
 
 #[export]

From ce7f979fb96d4bb8e86df2c0241be14daf588dcf Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Tue, 17 Dec 2024 20:55:04 -0800
Subject: [PATCH 10/11] Revert "revert"

This reverts commit a55fc6760ced90032bc1a93267a06c897dfa5504.
---
 theories/Core/Soundness/EqualityCases.v | 62 -------------------------
 1 file changed, 62 deletions(-)

diff --git a/theories/Core/Soundness/EqualityCases.v b/theories/Core/Soundness/EqualityCases.v
index 4885ea5..c757feb 100644
--- a/theories/Core/Soundness/EqualityCases.v
+++ b/theories/Core/Soundness/EqualityCases.v
@@ -101,68 +101,6 @@ Lemma glu_rel_eq_eqrec : forall Γ A i M1 M2 B j BR N,
     {{ Γ, A ⊩ BR : B[Id,,#0,,refl A[Wk] #0] }} ->
     {{ Γ ⊩ N : Eq A M1 M2 }} ->
     {{ Γ ⊩ eqrec N as Eq A M1 M2 return B | refl -> BR end : B[Id,,M1,,M2,,N] }}.
-Proof.
-  intros * HA HM1 HM2 HB HBR HN.
-  assert {{ ⊩ Γ }} by mauto.
-  assert {{ ⊩ Γ }} as [SbΓ] by mauto.
-  saturate_syn_judge.
-
-  assert {{ Γ ⊩s Id,,M1 : Γ, A }} by (eapply glu_rel_sub_extend; mauto 3; bulky_rewrite).
-  assert {{ ⊩ Γ , A }} by mauto.
-  assert {{ ⊩ Γ , A }} as [SbΓA] by mauto.
-  assert {{ Γ ⊩s Id,,M1,,M2 : Γ, A, A[Wk] }} by (eapply glu_rel_sub_extend; mauto 4).
-  assert {{ ⊩ Γ , A, A[Wk] }} by mauto.
-  assert {{ ⊩ Γ , A, A[Wk] }} as [SbΓAA] by mauto.
-  assert {{ Γ ⊩s Id,,M1,,M2,,N : Γ, A, A[Wk], Eq A[Wk ∘ Wk] #1 #0 }}.
-  {
-    eapply glu_rel_sub_extend; mauto 4.
-    eapply glu_rel_eq.
-    - mauto.
-    - rewrite <- @exp_eq_sub_compose_typ with (i := i); mauto 3.
-    - rewrite <- @exp_eq_sub_compose_typ with (i := i); mauto 3.
-  }
-  saturate_syn_judge.
-
-  invert_sem_judge1.
-  invert_sem_judge1.
-  invert_sem_judge1.
-  invert_sem_judge1.
-  invert_sem_judge1.
-  invert_sem_judge1.
-  invert_sem_judge1.
-  invert_sem_judge1.
-
-
-Ltac invert_glu_rel_sub H :=
-  (unshelve eapply (glu_rel_sub_clean_inversion3 _ _) in H; shelve_unifiable; [eassumption | eassumption |])
-  + (unshelve eapply (glu_rel_sub_clean_inversion2 _) in H; shelve_unifiable; [eassumption |];
-     destruct H as [? []])
-  + (unshelve eapply (glu_rel_sub_clean_inversion1 _) in H; shelve_unifiable; [eassumption |];
-     destruct H as [? []])
-  + (inversion H; subst).
-
-unshelve eapply (glu_rel_sub_clean_inversion3 _ _) in H10; shelve_unifiable.
-eassumption.
-eassumption.
-invert_glu_rel_sub H10.
-
-
-  invert_sem_judge1.
-
-  eexists; split; eauto.
-  exists j; intros.
-  assert {{ Δ ⊢s σ : Γ }} by mauto 4.
-  apply_glu_rel_judge.
-  repeat invert_glu_rel1.
-  saturate_glu_typ_from_el.
-  unify_glu_univ_lvl i.
-  deepexec (glu_univ_elem_per_univ i) ltac:(fun H => pose proof H).
-  match_by_head per_univ ltac:(fun H => destruct H).
-  do 2 deepexec (glu_univ_elem_per_elem i) ltac:(fun H => pose proof H; fail_at_if_dup ltac:(4)).
-  saturate_glu_info.
-
-  econstructor.
-
 Admitted.
 
 #[export]

From cf6ce42fd17e49b256537196a990364283ea3c6f Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Tue, 17 Dec 2024 20:55:14 -0800
Subject: [PATCH 11/11] revert

---
 theories/Core/Soundness/LogicalRelation/Lemmas.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
index 72875c2..6c31df4 100644
--- a/theories/Core/Soundness/LogicalRelation/Lemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -1227,7 +1227,7 @@ Proof.
   eapply glu_univ_elem_exp_conv; revgoals; mauto 3.
 Qed.
 
-#[export]
+#[global]
 Ltac invert_glu_rel_exp H :=
   (unshelve eapply (glu_rel_exp_clean_inversion2 _ _) in H; shelve_unifiable; [eassumption | eassumption |];
    simpl in H)
@@ -1397,7 +1397,7 @@ Ltac saturate_syn_judge1 :=
       assert {{ Γ ⊢s τ : Γ' }} by mauto; fail_if_dup
   end.
 
-#[export]
+#[global]
   Ltac saturate_syn_judge :=
   repeat saturate_syn_judge1.
 
@@ -1409,6 +1409,6 @@ Ltac invert_sem_judge1 :=
       invert_glu_rel_sub H
   end.
 
-#[export]
+#[global]
   Ltac invert_sem_judge :=
   repeat invert_sem_judge1.