From 7575614090a4a951ea9ee09693c0f21352538956 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Mon, 23 Dec 2024 19:40:05 -0800
Subject: [PATCH 1/9] reorganize automation

---
 theories/Core/Soundness/EqualityCases.v       | 22 +++++++++++++++++++
 .../Soundness/LogicalRelation/CoreLemmas.v    |  8 +++----
 .../Core/Soundness/LogicalRelation/Lemmas.v   | 20 +++++++++++++++--
 theories/Core/Soundness/Realizability.v       |  2 +-
 theories/Core/Soundness/UniverseCases.v       | 13 ++++++-----
 5 files changed, 52 insertions(+), 13 deletions(-)

diff --git a/theories/Core/Soundness/EqualityCases.v b/theories/Core/Soundness/EqualityCases.v
index c757feb..2322831 100644
--- a/theories/Core/Soundness/EqualityCases.v
+++ b/theories/Core/Soundness/EqualityCases.v
@@ -93,6 +93,28 @@ Qed.
   Hint Resolve glu_rel_eq_refl : mctt.
 
 
+
+Lemma glu_rel_exp_eq_clean_inversion : forall {i Γ Sb M1 M2 A N},
+    {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
+    {{ Γ ⊩ A : Type@i }} ->
+    {{ Γ ⊩ M1 : A }} ->
+    {{ Γ ⊩ M2 : A }} ->
+    {{ Γ ⊩ N : Eq A M1 M2 }} ->
+    glu_rel_exp_resp_sub_env i Sb N {{{Eq A M1 M2}}}.
+Proof.
+  intros * ? HA HM1 HM2 HN.
+  assert {{ Γ ⊩ Eq A M1 M2 : Type@i }} by mauto.
+  eapply glu_rel_exp_clean_inversion2 in HN; eassumption.
+Qed.
+
+
+#[global]
+  Ltac invert_glu_rel_exp H ::=
+  (unshelve eapply (glu_rel_exp_eq_clean_inversion _) in H; shelve_unifiable; try eassumption;
+   simpl in H)
+  + universe_invert_glu_rel_exp H.
+
+
 Lemma glu_rel_eq_eqrec : forall Γ A i M1 M2 B j BR N,
     {{ Γ ⊩ A : Type@i }} ->
     {{ Γ ⊩ M1 : A }} ->
diff --git a/theories/Core/Soundness/LogicalRelation/CoreLemmas.v b/theories/Core/Soundness/LogicalRelation/CoreLemmas.v
index 46bcb2d..80965a5 100644
--- a/theories/Core/Soundness/LogicalRelation/CoreLemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/CoreLemmas.v
@@ -132,7 +132,7 @@ Qed.
 
 #[global]
   Ltac destruct_glu_eq :=
-  match_by_head1 glu_eq ltac:(fun H => destruct H).
+  match_by_head1 glu_eq ltac:(fun H => dependent destruction H).
 
 Lemma glu_univ_elem_trm_resp_typ_exp_eq : forall i P El a,
     {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
@@ -802,12 +802,12 @@ Proof.
       symmetry. trivial.
   - simpl_glu_rel.
     econstructor; eauto.
-    destruct_glu_eq; progressive_invert H20; econstructor; mauto 3; intros.
+    destruct_glu_eq; match_by_head1 per_eq progressive_invert; econstructor; mauto 3; intros.
     + etransitivity; mauto.
     + etransitivity; eauto.
       symmetry. eauto.
     + resp_per_IH.
-    + specialize (H20 (length Δ)).
+    + match_by_head1 per_bot ltac:(fun H => specialize (H (length Δ))).
       destruct_all.
       functional_read_rewrite_clear.
       mauto.
@@ -1064,7 +1064,7 @@ Proof.
       * assert {{ Δ0 ⊢w σ ∘ σ0 : Γ }} by mauto 4.
         bulky_rewrite.
         etransitivity;
-          [| deepexec H14 ltac:(fun H => apply H)].
+          [| deepexec H13 ltac:(fun H => apply H)].
         mauto 4.
   - destruct_conjs.
     split; [mauto 3 |].
diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
index 6c31df4..84ed8ea 100644
--- a/theories/Core/Soundness/LogicalRelation/Lemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -1227,8 +1227,9 @@ Proof.
   eapply glu_univ_elem_exp_conv; revgoals; mauto 3.
 Qed.
 
+
 #[global]
-Ltac invert_glu_rel_exp H :=
+Ltac basic_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 |];
@@ -1236,6 +1237,10 @@ Ltac invert_glu_rel_exp H :=
   + (inversion H as [? [? [? ?]]]; subst).
 
 
+#[global]
+Ltac invert_glu_rel_exp H :=
+  basic_invert_glu_rel_exp H.
+
 Lemma glu_rel_exp_to_wf_exp : forall {Γ A M},
     {{ Γ ⊩ M : A }} ->
     {{ Γ ⊢ M : A }}.
@@ -1304,7 +1309,7 @@ Proof.
 Qed.
 
 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_inversion3 _ _) in H; shelve_unifiable; [eassumption | eassumption |]; simpl in H)
   + (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 |];
@@ -1365,6 +1370,16 @@ Ltac apply_glu_rel_judge :=
   clear_dups.
 
 
+Ltac apply_glu_rel_exp_judge :=
+  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;
+  clear_dups.
+
+
 Lemma glu_rel_exp_preserves_lvl : forall Γ Sb M A i,
     {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
     (forall Δ σ ρ,
@@ -1401,6 +1416,7 @@ Ltac saturate_syn_judge1 :=
   Ltac saturate_syn_judge :=
   repeat saturate_syn_judge1.
 
+#[global]
 Ltac invert_sem_judge1 :=
   match goal with
   | H : {{ ^?Γ ⊩ ^?M : ^?A }} |- _ =>
diff --git a/theories/Core/Soundness/Realizability.v b/theories/Core/Soundness/Realizability.v
index 1d560e6..739bfd2 100644
--- a/theories/Core/Soundness/Realizability.v
+++ b/theories/Core/Soundness/Realizability.v
@@ -325,7 +325,7 @@ Proof.
     saturate_weakening_escape.
     destruct_glu_eq;
       dir_inversion_clear_by_head read_nf.
-    + pose proof (PER_refl1 _ _ _ _ _ H25).
+    + pose proof (PER_refl1 _ _ _ _ _ H21).
       gen_presups.
       assert {{ Γ ⊢w Id : Γ }} by mauto 4.
       assert (P Γ {{{ B[Id] }}}) as HB by mauto 3.
diff --git a/theories/Core/Soundness/UniverseCases.v b/theories/Core/Soundness/UniverseCases.v
index a8f1c86..bdf24b4 100644
--- a/theories/Core/Soundness/UniverseCases.v
+++ b/theories/Core/Soundness/UniverseCases.v
@@ -53,15 +53,16 @@ Proof.
   eapply glu_rel_exp_clean_inversion2 in HM; mauto 3.
 Qed.
 
-#[local]
-  Ltac invert_glu_rel_exp_old H :=
-  invert_glu_rel_exp H.
-
 #[global]
-  Ltac invert_glu_rel_exp H :=
+  Ltac universe_invert_glu_rel_exp H :=
   (unshelve eapply (glu_rel_exp_clean_inversion2' _) in H; shelve_unifiable; [eassumption |];
    simpl in H)
-  + invert_glu_rel_exp_old H.
+  + basic_invert_glu_rel_exp H.
+
+
+#[global]
+  Ltac invert_glu_rel_exp H ::= universe_invert_glu_rel_exp H.
+
 
 Lemma glu_rel_exp_sub_typ : forall {Γ σ Δ i A},
     {{ Γ ⊩s σ : Δ }} ->

From affad6173b99cd23eea3f4afe988c85cef3901a2 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Mon, 23 Dec 2024 19:57:09 -0800
Subject: [PATCH 2/9] partial proof

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

diff --git a/theories/Core/Soundness/EqualityCases.v b/theories/Core/Soundness/EqualityCases.v
index 2322831..58eec3d 100644
--- a/theories/Core/Soundness/EqualityCases.v
+++ b/theories/Core/Soundness/EqualityCases.v
@@ -110,7 +110,7 @@ Qed.
 
 #[global]
   Ltac invert_glu_rel_exp H ::=
-  (unshelve eapply (glu_rel_exp_eq_clean_inversion _) in H; shelve_unifiable; try eassumption;
+  directed (unshelve eapply (glu_rel_exp_eq_clean_inversion _) in H; shelve_unifiable; try eassumption;
    simpl in H)
   + universe_invert_glu_rel_exp H.
 
@@ -123,6 +123,93 @@ 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.
+  }
+  assert {{ ⊩ Γ, A, A[Wk], Eq A[Wk ∘ Wk] #1 #0 }} as [SbΓAAEq] by mauto.
+  saturate_syn_judge.
+
+  unshelve eapply (glu_rel_exp_eq_clean_inversion _) in HN; shelve_unifiable; [eassumption | | eassumption | eassumption| eassumption];
+   simpl in HN.
+
+  invert_sem_judge.
+
+  eexists; split; eauto.
+  exists j; intros.
+  assert {{ Δ ⊢s σ : Γ }} by mauto 4.
+  apply_glu_rel_judge.
+  apply_glu_rel_exp_judge.
+  simpl in *.
+
+  repeat invert_glu_rel1.
+  clear_dups.
+  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.
+
+  (* eassert (exists mr, {{ ⟦ eqrec N as Eq A M1 M2 return B | refl -> BR end ⟧ ρ ↘ ^ mr }} *)
+  (*                /\ {{ Γ0 ⊢ eqrec N as Eq A M1 M2 return B | refl -> BR end[σ] : B[Id,,M1,,M2,,N][σ] ® mr ∈ H53 }}). *)
+  (* { *)
+  (*   destruct_glu_eq. *)
+  (*   - assert {{ Γ0 ⊢w Id : Γ0 }} as HId by mauto. *)
+  (*     pose proof (H78 _ _ HId) as HM''. *)
+
+  (*     match goal with *)
+  (*     | H1 : glu_univ_elem _ _ ?El _, H2 : glu_univ_elem i ?P _ _, H3 : ?P _ _, H4 : ?El _ _ _ _ *)
+  (*       |- _ => *)
+  (*         idtac H1 H2 H3 H4 *)
+  (*     end. *)
+
+  (*     pose proof (glu_univ_elem_exp_conv' H62 H51 HM'' H55). *)
+
+  (*     unify_glu_univ_lvl1 i. *)
+
+  (*     unify_glu_univ_lvl i. *)
+  (*     saturate_glu_info. *)
+  (*     assert {{ Γ0 ⊢ M'' : B1 }} by mauto. *)
+  (*     assert {{ Γ0 ⊢ M'' : B1 ® m' ∈ El2 }} by bulky_rewrite_in HM''. *)
+  (*     eassert {{ Γ0 ⊢ M'' : B1 ® m' ∈ glu_elem_top _ _ }} as [] by mauto. *)
+  (*     match_by_head1 per_top ltac:(fun H => specialize (H (length Γ0)) as [? []]). *)
+
+  (*     assert (SbΓA Γ0 {{{σ ,, M''}}} d{{{ρ ↦ m'}}}). *)
+  (*     { *)
+  (*       match_by_head1 (glu_ctx_env SbΓA) invert_glu_ctx_env. *)
+  (*       apply_equiv_left. *)
+  (*       econstructor; mauto 3. *)
+  (*       destruct_all. *)
+  (*       handle *)
+  (*     } *)
+
+
+  (*     eexists; split. *)
+  (*     + econstructor; mauto 3. *)
+  (*       econstructor. *)
+  (* } *)
+
+  econstructor; mauto.
+
+
 Admitted.
 
 #[export]

From c815b791389e3fd8756827e5f79bd4ae2545b6eb Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Mon, 23 Dec 2024 20:30:52 -0800
Subject: [PATCH 3/9] more tactic setups

---
 theories/Core/Soundness/EqualityCases.v       | 16 +++++++--
 .../Core/Soundness/LogicalRelation/Lemmas.v   |  4 ++-
 theories/Core/Soundness/UniverseCases.v       | 36 +++++++++++++------
 3 files changed, 42 insertions(+), 14 deletions(-)

diff --git a/theories/Core/Soundness/EqualityCases.v b/theories/Core/Soundness/EqualityCases.v
index 58eec3d..52a1d76 100644
--- a/theories/Core/Soundness/EqualityCases.v
+++ b/theories/Core/Soundness/EqualityCases.v
@@ -93,7 +93,6 @@ Qed.
   Hint Resolve glu_rel_eq_refl : mctt.
 
 
-
 Lemma glu_rel_exp_eq_clean_inversion : forall {i Γ Sb M1 M2 A N},
     {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
     {{ Γ ⊩ A : Type@i }} ->
@@ -144,10 +143,21 @@ Proof.
     - rewrite <- @exp_eq_sub_compose_typ with (i := i); mauto 3.
   }
   assert {{ ⊩ Γ, A, A[Wk], Eq A[Wk ∘ Wk] #1 #0 }} as [SbΓAAEq] by mauto.
+  assert {{ Γ, A ⊩s Id,,#0 : Γ, A, A[Wk] }} by
+    (eapply glu_rel_sub_extend; mauto 3; bulky_rewrite).
   saturate_syn_judge.
 
-  unshelve eapply (glu_rel_exp_eq_clean_inversion _) in HN; shelve_unifiable; [eassumption | | eassumption | eassumption| eassumption];
-   simpl in HN.
+  assert {{ Γ, A ⊢ (Eq A[Wk∘Wk] #1 #0)[Id,,#0] ≈ Eq A[Wk] #0 #0 : Type@i }} by admit.
+
+  assert {{ Γ, A ⊩s Id,,#0,,refl A[Wk] #0 : Γ, A, A[Wk], Eq A[Wk∘Wk] #1 #0 }}.
+  {
+    eapply glu_rel_sub_extend; mauto 3.
+    - eapply glu_rel_eq;
+        try rewrite <- @exp_eq_sub_compose_typ with (A:=A); mauto.
+    - bulky_rewrite.
+      mauto 3.
+  }
+  saturate_syn_judge.
 
   invert_sem_judge.
 
diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
index 84ed8ea..06413c8 100644
--- a/theories/Core/Soundness/LogicalRelation/Lemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -1403,15 +1403,17 @@ Qed.
 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
+  | H : {{ ⊩ ^?Γ }} |- _ =>
+      assert {{ ⊢ Γ }} by mauto; fail_if_dup
   end.
 
+
 #[global]
   Ltac saturate_syn_judge :=
   repeat saturate_syn_judge1.
diff --git a/theories/Core/Soundness/UniverseCases.v b/theories/Core/Soundness/UniverseCases.v
index bdf24b4..8af4188 100644
--- a/theories/Core/Soundness/UniverseCases.v
+++ b/theories/Core/Soundness/UniverseCases.v
@@ -53,16 +53,6 @@ Proof.
   eapply glu_rel_exp_clean_inversion2 in HM; mauto 3.
 Qed.
 
-#[global]
-  Ltac universe_invert_glu_rel_exp H :=
-  (unshelve eapply (glu_rel_exp_clean_inversion2' _) in H; shelve_unifiable; [eassumption |];
-   simpl in H)
-  + basic_invert_glu_rel_exp H.
-
-
-#[global]
-  Ltac invert_glu_rel_exp H ::= universe_invert_glu_rel_exp H.
-
 
 Lemma glu_rel_exp_sub_typ : forall {Γ σ Δ i A},
     {{ Γ ⊩s σ : Δ }} ->
@@ -78,3 +68,29 @@ Qed.
 
 #[export]
 Hint Resolve glu_rel_exp_sub_typ : mctt.
+
+
+Lemma glu_rel_exp_typ_sub_clean_inversion : forall {Γ σ Δ Sb M A i},
+    {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
+    {{ Δ ⊩ A : Type@i }} ->
+    {{ Γ ⊩s σ : Δ }} ->
+    {{ Γ ⊩ M : A[σ] }} ->
+    glu_rel_exp_resp_sub_env i Sb M {{{A[σ]}}}.
+Proof.
+  intros * ? ? ? HM.
+  assert {{ Γ ⊩ A[σ] : Type@i }} by mauto.
+  eapply glu_rel_exp_clean_inversion2 in HM; eassumption.
+Qed.
+
+
+#[global]
+  Ltac universe_invert_glu_rel_exp H :=
+  directed (unshelve eapply (glu_rel_exp_typ_sub_clean_inversion _) in H; shelve_unifiable; try eassumption;
+   simpl in H)
+  + (unshelve eapply (glu_rel_exp_clean_inversion2' _) in H; shelve_unifiable; [eassumption |];
+   simpl in H)
+  + basic_invert_glu_rel_exp H.
+
+
+#[global]
+  Ltac invert_glu_rel_exp H ::= universe_invert_glu_rel_exp H.

From af1f4ae744ebf97baeb524cb544d5d0fa3a19919 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Thu, 26 Dec 2024 21:12:50 -0800
Subject: [PATCH 4/9] more automation

---
 .../Core/Soundness/LogicalRelation/Lemmas.v   | 30 +++++++++++++++----
 1 file changed, 25 insertions(+), 5 deletions(-)

diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
index 06413c8..58b9ba0 100644
--- a/theories/Core/Soundness/LogicalRelation/Lemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -1020,8 +1020,22 @@ Proof.
     econstructor; intuition.
 Qed.
 
+
+Lemma glu_ctx_env_cons_clean_inversion' : forall {Γ TSb A Sb i},
+  {{ EG Γ ∈ glu_ctx_env ↘ TSb }} ->
+  {{ EG Γ, A ∈ glu_ctx_env ↘ Sb }} ->
+  {{ Γ ⊩ A : Type@i }} ->
+  (forall Δ σ ρ,
+      {{ Δ ⊢s σ ® ρ ∈ TSb }} ->
+      glu_rel_typ_with_sub i Δ A σ ρ) /\
+    (Sb <∙> cons_glu_sub_pred i Γ A TSb).
+Proof.
+  mauto using glu_ctx_env_cons_clean_inversion'_helper.
+Qed.
+
 Ltac invert_glu_ctx_env H :=
-  (unshelve eapply (glu_ctx_env_cons_clean_inversion _) in H; shelve_unifiable; [eassumption |];
+  directed (unshelve eapply (glu_ctx_env_cons_clean_inversion' _) in H; shelve_unifiable; try eassumption; destruct H)
+  + (unshelve eapply (glu_ctx_env_cons_clean_inversion _) in H; shelve_unifiable; [eassumption |];
    destruct H as [? [? []]])
   + dependent destruction H.
 
@@ -1419,14 +1433,20 @@ Ltac saturate_syn_judge1 :=
   repeat saturate_syn_judge1.
 
 #[global]
-Ltac invert_sem_judge1 :=
+  Ltac invert_sem_judge1 ::=
   match goal with
   | H : {{ ^?Γ ⊩ ^?M : ^?A }} |- _ =>
-      invert_glu_rel_exp H
+      mark H;
+      let H' := fresh "H" in
+      pose proof H as H';
+      invert_glu_rel_exp H'
   | H : {{ ^?Γ ⊩s ^?τ : ^?Γ' }} |- _ =>
-      invert_glu_rel_sub H
+      mark H;
+      let H' := fresh "H" in
+      pose proof H as H';
+      invert_glu_rel_sub H'
   end.
 
 #[global]
   Ltac invert_sem_judge :=
-  repeat invert_sem_judge1.
+  repeat invert_sem_judge1; unmark_all.

From 126d0bef10dec2d0ba73b76dc22e7a8be8183854 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Thu, 26 Dec 2024 21:13:35 -0800
Subject: [PATCH 5/9] missed one lemma

---
 .../Core/Soundness/LogicalRelation/Lemmas.v   | 36 +++++++++++++++++++
 1 file changed, 36 insertions(+)

diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
index 58b9ba0..6483b86 100644
--- a/theories/Core/Soundness/LogicalRelation/Lemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -1021,6 +1021,42 @@ Proof.
 Qed.
 
 
+Lemma glu_ctx_env_cons_clean_inversion'_helper : forall {Γ TSb A Sb i},
+  {{ EG Γ ∈ glu_ctx_env ↘ TSb }} ->
+  {{ EG Γ, A ∈ glu_ctx_env ↘ Sb }} ->
+  {{ Γ ⊩ A : Type@i }} ->
+  {{ Γ ⊢ A : Type@i }} ->
+  (forall Δ σ ρ,
+      {{ Δ ⊢s σ ® ρ ∈ TSb }} ->
+      glu_rel_typ_with_sub i Δ A σ ρ) /\
+    (Sb <∙> cons_glu_sub_pred i Γ A TSb).
+Proof.
+  intros * HΓ HΓA [? [? [j HA]]] ?.
+  handle_functional_glu_ctx_env.
+  assert (forall Δ σ ρ, {{ Δ ⊢s σ ® ρ ∈ TSb }} -> glu_rel_typ_with_sub i Δ A σ ρ) by
+    (intros; apply_equiv_right; mauto).
+  split; trivial.
+
+  match_by_head glu_ctx_env progressive_invert.
+  handle_functional_glu_ctx_env.
+
+  intros Δ σ ρ.
+  split; intros [].
+  - apply_equiv_left.
+    destruct_glu_rel_typ_with_sub.
+    handle_functional_glu_univ_elem.
+    econstructor; intuition.
+    eapply @glu_univ_elem_exp_conv' with (i:=i0) (j:=i); try eassumption.
+    bulky_rewrite.
+  - rewrite <- H5 in *.
+    destruct_glu_rel_typ_with_sub.
+    handle_functional_glu_univ_elem.
+    econstructor; intuition.
+    eapply @glu_univ_elem_exp_conv' with (i:=i) (j:=i0); try eassumption.
+    bulky_rewrite.
+Qed.
+
+
 Lemma glu_ctx_env_cons_clean_inversion' : forall {Γ TSb A Sb i},
   {{ EG Γ ∈ glu_ctx_env ↘ TSb }} ->
   {{ EG Γ, A ∈ glu_ctx_env ↘ Sb }} ->

From 109da68b771555c1b24c8fa611d92a4c9fc413b7 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Thu, 26 Dec 2024 21:19:44 -0800
Subject: [PATCH 6/9] make it compile

---
 .../Core/Soundness/LogicalRelation/Lemmas.v   | 110 ++++++++++--------
 1 file changed, 59 insertions(+), 51 deletions(-)

diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
index 6483b86..56f4bf6 100644
--- a/theories/Core/Soundness/LogicalRelation/Lemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -1021,60 +1021,13 @@ Proof.
 Qed.
 
 
-Lemma glu_ctx_env_cons_clean_inversion'_helper : forall {Γ TSb A Sb i},
-  {{ EG Γ ∈ glu_ctx_env ↘ TSb }} ->
-  {{ EG Γ, A ∈ glu_ctx_env ↘ Sb }} ->
-  {{ Γ ⊩ A : Type@i }} ->
-  {{ Γ ⊢ A : Type@i }} ->
-  (forall Δ σ ρ,
-      {{ Δ ⊢s σ ® ρ ∈ TSb }} ->
-      glu_rel_typ_with_sub i Δ A σ ρ) /\
-    (Sb <∙> cons_glu_sub_pred i Γ A TSb).
-Proof.
-  intros * HΓ HΓA [? [? [j HA]]] ?.
-  handle_functional_glu_ctx_env.
-  assert (forall Δ σ ρ, {{ Δ ⊢s σ ® ρ ∈ TSb }} -> glu_rel_typ_with_sub i Δ A σ ρ) by
-    (intros; apply_equiv_right; mauto).
-  split; trivial.
-
-  match_by_head glu_ctx_env progressive_invert.
-  handle_functional_glu_ctx_env.
-
-  intros Δ σ ρ.
-  split; intros [].
-  - apply_equiv_left.
-    destruct_glu_rel_typ_with_sub.
-    handle_functional_glu_univ_elem.
-    econstructor; intuition.
-    eapply @glu_univ_elem_exp_conv' with (i:=i0) (j:=i); try eassumption.
-    bulky_rewrite.
-  - rewrite <- H5 in *.
-    destruct_glu_rel_typ_with_sub.
-    handle_functional_glu_univ_elem.
-    econstructor; intuition.
-    eapply @glu_univ_elem_exp_conv' with (i:=i) (j:=i0); try eassumption.
-    bulky_rewrite.
-Qed.
-
-
-Lemma glu_ctx_env_cons_clean_inversion' : forall {Γ TSb A Sb i},
-  {{ EG Γ ∈ glu_ctx_env ↘ TSb }} ->
-  {{ EG Γ, A ∈ glu_ctx_env ↘ Sb }} ->
-  {{ Γ ⊩ A : Type@i }} ->
-  (forall Δ σ ρ,
-      {{ Δ ⊢s σ ® ρ ∈ TSb }} ->
-      glu_rel_typ_with_sub i Δ A σ ρ) /\
-    (Sb <∙> cons_glu_sub_pred i Γ A TSb).
-Proof.
-  mauto using glu_ctx_env_cons_clean_inversion'_helper.
-Qed.
-
-Ltac invert_glu_ctx_env H :=
-  directed (unshelve eapply (glu_ctx_env_cons_clean_inversion' _) in H; shelve_unifiable; try eassumption; destruct H)
-  + (unshelve eapply (glu_ctx_env_cons_clean_inversion _) in H; shelve_unifiable; [eassumption |];
+Ltac basic_invert_glu_ctx_env H :=
+  (unshelve eapply (glu_ctx_env_cons_clean_inversion _) in H; shelve_unifiable; [eassumption |];
    destruct H as [? [? []]])
   + dependent destruction H.
 
+Ltac invert_glu_ctx_env H := basic_glu_ctx_env H.
+
 Lemma glu_ctx_env_subtyp_sub_if : forall Γ Γ' Sb Sb' Δ σ ρ,
     {{ ⊢ Γ ⊆ Γ' }} ->
     {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
@@ -1238,6 +1191,61 @@ Ltac destruct_glu_rel_typ_with_sub :=
     end;
   unmark_all.
 
+
+Lemma glu_ctx_env_cons_clean_inversion'_helper : forall {Γ TSb A Sb i},
+  {{ EG Γ ∈ glu_ctx_env ↘ TSb }} ->
+  {{ EG Γ, A ∈ glu_ctx_env ↘ Sb }} ->
+  {{ Γ ⊩ A : Type@i }} ->
+  {{ Γ ⊢ A : Type@i }} ->
+  (forall Δ σ ρ,
+      {{ Δ ⊢s σ ® ρ ∈ TSb }} ->
+      glu_rel_typ_with_sub i Δ A σ ρ) /\
+    (Sb <∙> cons_glu_sub_pred i Γ A TSb).
+Proof.
+  intros * HΓ HΓA [? [? [j HA]]] ?.
+  handle_functional_glu_ctx_env.
+  assert (forall Δ σ ρ, {{ Δ ⊢s σ ® ρ ∈ TSb }} -> glu_rel_typ_with_sub i Δ A σ ρ) by
+    (intros; apply_equiv_right; mauto).
+  split; trivial.
+
+  match_by_head glu_ctx_env progressive_invert.
+  handle_functional_glu_ctx_env.
+
+  intros Δ σ ρ.
+  split; intros [].
+  - apply_equiv_left.
+    destruct_glu_rel_typ_with_sub.
+    handle_functional_glu_univ_elem.
+    econstructor; intuition.
+    eapply @glu_univ_elem_exp_conv' with (i:=i0) (j:=i); try eassumption.
+    bulky_rewrite.
+  - rewrite <- H5 in *.
+    destruct_glu_rel_typ_with_sub.
+    handle_functional_glu_univ_elem.
+    econstructor; intuition.
+    eapply @glu_univ_elem_exp_conv' with (i:=i) (j:=i0); try eassumption.
+    bulky_rewrite.
+Qed.
+
+
+Lemma glu_ctx_env_cons_clean_inversion' : forall {Γ TSb A Sb i},
+  {{ EG Γ ∈ glu_ctx_env ↘ TSb }} ->
+  {{ EG Γ, A ∈ glu_ctx_env ↘ Sb }} ->
+  {{ Γ ⊩ A : Type@i }} ->
+  (forall Δ σ ρ,
+      {{ Δ ⊢s σ ® ρ ∈ TSb }} ->
+      glu_rel_typ_with_sub i Δ A σ ρ) /\
+    (Sb <∙> cons_glu_sub_pred i Γ A TSb).
+Proof.
+  mauto using glu_ctx_env_cons_clean_inversion'_helper.
+Qed.
+
+
+Ltac invert_glu_ctx_env H ::=
+  directed (unshelve eapply (glu_ctx_env_cons_clean_inversion' _) in H; shelve_unifiable; try eassumption; destruct H)
+  + basic_invert_glu_ctx_env H.
+
+
 (** *** Lemmas about [glu_rel_exp] *)
 
 Lemma glu_rel_exp_clean_inversion1 : forall {Γ Sb M A},

From 6050e5fb269b08fbb27720dacce63eb5e5b4c73e Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Thu, 26 Dec 2024 21:22:18 -0800
Subject: [PATCH 7/9] actually compile

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

diff --git a/theories/Core/Soundness/EqualityCases.v b/theories/Core/Soundness/EqualityCases.v
index 52a1d76..3891855 100644
--- a/theories/Core/Soundness/EqualityCases.v
+++ b/theories/Core/Soundness/EqualityCases.v
@@ -169,7 +169,7 @@ Proof.
   simpl in *.
 
   repeat invert_glu_rel1.
-  clear_dups.
+  handle_functional_glu_univ_elem.
   saturate_glu_typ_from_el.
   unify_glu_univ_lvl i.
 
diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
index 56f4bf6..2e225bc 100644
--- a/theories/Core/Soundness/LogicalRelation/Lemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -1026,7 +1026,7 @@ Ltac basic_invert_glu_ctx_env H :=
    destruct H as [? [? []]])
   + dependent destruction H.
 
-Ltac invert_glu_ctx_env H := basic_glu_ctx_env H.
+Ltac invert_glu_ctx_env H := basic_invert_glu_ctx_env H.
 
 Lemma glu_ctx_env_subtyp_sub_if : forall Γ Γ' Sb Sb' Δ σ ρ,
     {{ ⊢ Γ ⊆ Γ' }} ->

From fdc9e7b495151108bb82f1160aae0311cd552cf0 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Thu, 26 Dec 2024 21:26:03 -0800
Subject: [PATCH 8/9] well...

---
 .../Core/Soundness/LogicalRelation/Lemmas.v   | 112 +++++++++---------
 1 file changed, 57 insertions(+), 55 deletions(-)

diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
index 2e225bc..1e350f8 100644
--- a/theories/Core/Soundness/LogicalRelation/Lemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -1192,60 +1192,6 @@ Ltac destruct_glu_rel_typ_with_sub :=
   unmark_all.
 
 
-Lemma glu_ctx_env_cons_clean_inversion'_helper : forall {Γ TSb A Sb i},
-  {{ EG Γ ∈ glu_ctx_env ↘ TSb }} ->
-  {{ EG Γ, A ∈ glu_ctx_env ↘ Sb }} ->
-  {{ Γ ⊩ A : Type@i }} ->
-  {{ Γ ⊢ A : Type@i }} ->
-  (forall Δ σ ρ,
-      {{ Δ ⊢s σ ® ρ ∈ TSb }} ->
-      glu_rel_typ_with_sub i Δ A σ ρ) /\
-    (Sb <∙> cons_glu_sub_pred i Γ A TSb).
-Proof.
-  intros * HΓ HΓA [? [? [j HA]]] ?.
-  handle_functional_glu_ctx_env.
-  assert (forall Δ σ ρ, {{ Δ ⊢s σ ® ρ ∈ TSb }} -> glu_rel_typ_with_sub i Δ A σ ρ) by
-    (intros; apply_equiv_right; mauto).
-  split; trivial.
-
-  match_by_head glu_ctx_env progressive_invert.
-  handle_functional_glu_ctx_env.
-
-  intros Δ σ ρ.
-  split; intros [].
-  - apply_equiv_left.
-    destruct_glu_rel_typ_with_sub.
-    handle_functional_glu_univ_elem.
-    econstructor; intuition.
-    eapply @glu_univ_elem_exp_conv' with (i:=i0) (j:=i); try eassumption.
-    bulky_rewrite.
-  - rewrite <- H5 in *.
-    destruct_glu_rel_typ_with_sub.
-    handle_functional_glu_univ_elem.
-    econstructor; intuition.
-    eapply @glu_univ_elem_exp_conv' with (i:=i) (j:=i0); try eassumption.
-    bulky_rewrite.
-Qed.
-
-
-Lemma glu_ctx_env_cons_clean_inversion' : forall {Γ TSb A Sb i},
-  {{ EG Γ ∈ glu_ctx_env ↘ TSb }} ->
-  {{ EG Γ, A ∈ glu_ctx_env ↘ Sb }} ->
-  {{ Γ ⊩ A : Type@i }} ->
-  (forall Δ σ ρ,
-      {{ Δ ⊢s σ ® ρ ∈ TSb }} ->
-      glu_rel_typ_with_sub i Δ A σ ρ) /\
-    (Sb <∙> cons_glu_sub_pred i Γ A TSb).
-Proof.
-  mauto using glu_ctx_env_cons_clean_inversion'_helper.
-Qed.
-
-
-Ltac invert_glu_ctx_env H ::=
-  directed (unshelve eapply (glu_ctx_env_cons_clean_inversion' _) in H; shelve_unifiable; try eassumption; destruct H)
-  + basic_invert_glu_ctx_env H.
-
-
 (** *** Lemmas about [glu_rel_exp] *)
 
 Lemma glu_rel_exp_clean_inversion1 : forall {Γ Sb M A},
@@ -1317,6 +1263,62 @@ Qed.
 #[export]
 Hint Resolve glu_rel_exp_to_wf_exp : mctt.
 
+
+
+Lemma glu_ctx_env_cons_clean_inversion'_helper : forall {Γ TSb A Sb i},
+  {{ EG Γ ∈ glu_ctx_env ↘ TSb }} ->
+  {{ EG Γ, A ∈ glu_ctx_env ↘ Sb }} ->
+  {{ Γ ⊩ A : Type@i }} ->
+  {{ Γ ⊢ A : Type@i }} ->
+  (forall Δ σ ρ,
+      {{ Δ ⊢s σ ® ρ ∈ TSb }} ->
+      glu_rel_typ_with_sub i Δ A σ ρ) /\
+    (Sb <∙> cons_glu_sub_pred i Γ A TSb).
+Proof.
+  intros * HΓ HΓA [? [? [j HA]]] ?.
+  handle_functional_glu_ctx_env.
+  assert (forall Δ σ ρ, {{ Δ ⊢s σ ® ρ ∈ TSb }} -> glu_rel_typ_with_sub i Δ A σ ρ) by
+    (intros; apply_equiv_right; mauto).
+  split; trivial.
+
+  match_by_head glu_ctx_env progressive_invert.
+  handle_functional_glu_ctx_env.
+
+  intros Δ σ ρ.
+  split; intros [].
+  - apply_equiv_left.
+    destruct_glu_rel_typ_with_sub.
+    handle_functional_glu_univ_elem.
+    econstructor; intuition.
+    eapply @glu_univ_elem_exp_conv' with (i:=i0) (j:=i); try eassumption.
+    bulky_rewrite.
+  - rewrite <- H5 in *.
+    destruct_glu_rel_typ_with_sub.
+    handle_functional_glu_univ_elem.
+    econstructor; intuition.
+    eapply @glu_univ_elem_exp_conv' with (i:=i) (j:=i0); try eassumption.
+    bulky_rewrite.
+Qed.
+
+
+Lemma glu_ctx_env_cons_clean_inversion' : forall {Γ TSb A Sb i},
+  {{ EG Γ ∈ glu_ctx_env ↘ TSb }} ->
+  {{ EG Γ, A ∈ glu_ctx_env ↘ Sb }} ->
+  {{ Γ ⊩ A : Type@i }} ->
+  (forall Δ σ ρ,
+      {{ Δ ⊢s σ ® ρ ∈ TSb }} ->
+      glu_rel_typ_with_sub i Δ A σ ρ) /\
+    (Sb <∙> cons_glu_sub_pred i Γ A TSb).
+Proof.
+  mauto using glu_ctx_env_cons_clean_inversion'_helper.
+Qed.
+
+
+Ltac invert_glu_ctx_env H ::=
+  directed (unshelve eapply (glu_ctx_env_cons_clean_inversion' _) in H; shelve_unifiable; try eassumption; destruct H)
+  + basic_invert_glu_ctx_env H.
+
+
 (** *** Lemmas about [glu_rel_sub] *)
 
 Lemma glu_rel_sub_clean_inversion1 : forall {Γ Sb τ Γ'},
@@ -1477,7 +1479,7 @@ Ltac saturate_syn_judge1 :=
   repeat saturate_syn_judge1.
 
 #[global]
-  Ltac invert_sem_judge1 ::=
+  Ltac invert_sem_judge1 :=
   match goal with
   | H : {{ ^?Γ ⊩ ^?M : ^?A }} |- _ =>
       mark H;

From 7437ab22d9b0e106a072ad159300cc8061800bf5 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Thu, 26 Dec 2024 22:05:05 -0800
Subject: [PATCH 9/9] set up a framework for now

---
 .../Core/Semantic/Evaluation/Definitions.v    |  2 +-
 theories/Core/Soundness/EqualityCases.v       | 77 +++++++++----------
 2 files changed, 38 insertions(+), 41 deletions(-)

diff --git a/theories/Core/Semantic/Evaluation/Definitions.v b/theories/Core/Semantic/Evaluation/Definitions.v
index 47ffb5c..2c04c81 100644
--- a/theories/Core/Semantic/Evaluation/Definitions.v
+++ b/theories/Core/Semantic/Evaluation/Definitions.v
@@ -82,7 +82,7 @@ with eval_eqrec : domain -> exp -> exp -> domain -> domain -> domain -> env -> d
   `( {{ ⟦ BR ⟧ ρ ↦ n ↘ br }} ->
      {{ eqrec refl n as Eq a m1 m2 ⟦return B | refl -> BR end⟧ ρ ↘ br }} )
 | eval_eqrec_neut :
-  `( {{ ⟦ B ⟧ ρ ↦ m1 ↦ m2 ↦ ⇑ (Eq a m1 m2) n ↘ b }} ->
+  `( {{ ⟦ B ⟧ ρ ↦ m1 ↦ m2 ↦ ⇑ c n ↘ b }} ->
      {{ eqrec ⇑ c n as Eq a m1 m2 ⟦return B | refl -> BR end⟧ ρ ↘ ⇑ b (eqrec n under ρ as Eq a m1 m2 return B | refl -> BR end) }} )
 where "'eqrec' n 'as' 'Eq' a m1 m2 '⟦return' B | 'refl' -> BR 'end⟧' ρ '↘' r" := (eval_eqrec a B BR m1 m2 n ρ r) (in custom judg)
 with eval_sub : sub -> env -> env -> Prop :=
diff --git a/theories/Core/Soundness/EqualityCases.v b/theories/Core/Soundness/EqualityCases.v
index 3891855..f3a5b06 100644
--- a/theories/Core/Soundness/EqualityCases.v
+++ b/theories/Core/Soundness/EqualityCases.v
@@ -1,6 +1,5 @@
 From Mctt Require Import LibTactics.
 From Mctt.Core Require Import Base.
-From Mctt.Core.Completeness Require Import FundamentalTheorem.
 From Mctt.Core.Semantic Require Import Realizability.
 From Mctt.Core.Soundness Require Import
   ContextCases
@@ -166,7 +165,6 @@ Proof.
   assert {{ Δ ⊢s σ : Γ }} by mauto 4.
   apply_glu_rel_judge.
   apply_glu_rel_exp_judge.
-  simpl in *.
 
   repeat invert_glu_rel1.
   handle_functional_glu_univ_elem.
@@ -178,44 +176,43 @@ Proof.
   do 2 deepexec (glu_univ_elem_per_elem i) ltac:(fun H => pose proof H; fail_at_if_dup ltac:(4)).
   saturate_glu_info.
 
-  (* eassert (exists mr, {{ ⟦ eqrec N as Eq A M1 M2 return B | refl -> BR end ⟧ ρ ↘ ^ mr }} *)
-  (*                /\ {{ Γ0 ⊢ eqrec N as Eq A M1 M2 return B | refl -> BR end[σ] : B[Id,,M1,,M2,,N][σ] ® mr ∈ H53 }}). *)
-  (* { *)
-  (*   destruct_glu_eq. *)
-  (*   - assert {{ Γ0 ⊢w Id : Γ0 }} as HId by mauto. *)
-  (*     pose proof (H78 _ _ HId) as HM''. *)
-
-  (*     match goal with *)
-  (*     | H1 : glu_univ_elem _ _ ?El _, H2 : glu_univ_elem i ?P _ _, H3 : ?P _ _, H4 : ?El _ _ _ _ *)
-  (*       |- _ => *)
-  (*         idtac H1 H2 H3 H4 *)
-  (*     end. *)
-
-  (*     pose proof (glu_univ_elem_exp_conv' H62 H51 HM'' H55). *)
-
-  (*     unify_glu_univ_lvl1 i. *)
-
-  (*     unify_glu_univ_lvl i. *)
-  (*     saturate_glu_info. *)
-  (*     assert {{ Γ0 ⊢ M'' : B1 }} by mauto. *)
-  (*     assert {{ Γ0 ⊢ M'' : B1 ® m' ∈ El2 }} by bulky_rewrite_in HM''. *)
-  (*     eassert {{ Γ0 ⊢ M'' : B1 ® m' ∈ glu_elem_top _ _ }} as [] by mauto. *)
-  (*     match_by_head1 per_top ltac:(fun H => specialize (H (length Γ0)) as [? []]). *)
-
-  (*     assert (SbΓA Γ0 {{{σ ,, M''}}} d{{{ρ ↦ m'}}}). *)
-  (*     { *)
-  (*       match_by_head1 (glu_ctx_env SbΓA) invert_glu_ctx_env. *)
-  (*       apply_equiv_left. *)
-  (*       econstructor; mauto 3. *)
-  (*       destruct_all. *)
-  (*       handle *)
-  (*     } *)
-
-
-  (*     eexists; split. *)
-  (*     + econstructor; mauto 3. *)
-  (*       econstructor. *)
-  (* } *)
+  eassert (exists mr, {{ ⟦ eqrec N as Eq A M1 M2 return B | refl -> BR end ⟧ ρ ↘ mr }}
+                 /\ {{ Γ0 ⊢ eqrec N as Eq A M1 M2 return B | refl -> BR end[σ] : B[Id,,M1,,M2,,N][σ] ® mr ∈ H77 }}) as [? [? ?]].
+  {
+    destruct_glu_eq.
+    - assert {{ Γ0 ⊢w Id : Γ0 }} as HId by mauto.
+      assert {{ Γ0 ⊢ M'' : B1 }} by (gen_presups; trivial).
+      pose proof (H99 _ _ HId) as HM''.
+      saturate_glu_typ_from_el.
+      assert {{ Γ0 ⊢ B1[Id] ≈ B1 : Type@i }} as HrwB1 by mauto 3.
+      rewrite HrwB1 in *.
+      assert {{ Γ0 ⊢ B1 ≈ A[σ] : Type@i }} as HrwB1' by mauto 4.
+      rewrite HrwB1' in *.
+      saturate_glu_info.
+
+      assert (SbΓA Γ0 {{{σ ,, M''}}} d{{{ρ ↦ m'}}}).
+      {
+        match_by_head1 (glu_ctx_env SbΓA) invert_glu_ctx_env.
+        apply_equiv_left.
+        econstructor; mauto 3; bulky_rewrite.
+        admit.
+      }
+      destruct_glu_rel_exp_with_sub.
+      simplify_evals.
+      simpl in *.
+
+      eexists; split; mauto 3.
+      admit.
+
+    - match_by_head1 per_bot ltac:(fun H => pose proof (H (length Γ0)) as [V [HV _]]).
+      assert {{ Γ0 ⊢w Id : Γ0 }} as HId by mauto.
+      pose proof (H54 _ _ V HId HV).
+      assert {{ Γ0 ⊢ N[σ] ≈ V : (Eq A M1 M2)[σ] }} by admit.
+
+      eexists; split; mauto 3.
+
+      admit.
+  }
 
   econstructor; mauto.