From 66566259df7b21c31ea6e13f36ffa6d48a8974b8 Mon Sep 17 00:00:00 2001
From: Junyoung/Clare Jang <jjc9310@gmail.com>
Date: Thu, 8 Aug 2024 15:05:41 -0400
Subject: [PATCH 1/8] Prove subtyping lemma

---
 theories/Core/Soundness/EquivalenceLemmas.v | 12 +++
 theories/Core/Soundness/SubtypingLemmas.v   | 88 +++++++++++++++++++++
 2 files changed, 100 insertions(+)
 create mode 100644 theories/Core/Soundness/SubtypingLemmas.v

diff --git a/theories/Core/Soundness/EquivalenceLemmas.v b/theories/Core/Soundness/EquivalenceLemmas.v
index b5c3857a..6fa62396 100644
--- a/theories/Core/Soundness/EquivalenceLemmas.v
+++ b/theories/Core/Soundness/EquivalenceLemmas.v
@@ -80,3 +80,15 @@ Proof.
     assert {{ Γ ⊢ A'[Id] ≈ V : Type@i }} as -> by mauto 4.
     mauto 4.
 Qed.
+
+Lemma glu_univ_elem_per_univ_typ_iff : forall {i a a' P P' El El'},
+    {{ Dom a ≈ a' ∈ per_univ i }} ->
+    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    {{ DG a' ∈ glu_univ_elem i ↘ P' ↘ El' }} ->
+    (P <∙> P') /\ (El <∙> El').
+Proof.
+  intros * Hper **.
+  eapply functional_glu_univ_elem;
+    [eassumption | rewrite Hper];
+    eassumption.
+Qed.
diff --git a/theories/Core/Soundness/SubtypingLemmas.v b/theories/Core/Soundness/SubtypingLemmas.v
new file mode 100644
index 00000000..3120215b
--- /dev/null
+++ b/theories/Core/Soundness/SubtypingLemmas.v
@@ -0,0 +1,88 @@
+From Coq Require Import Morphisms Morphisms_Prop Morphisms_Relations Relation_Definitions RelationClasses.
+
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core.Syntactic Require Import Corollaries.
+From Mcltt.Core.Semantic Require Import Realizability.
+From Mcltt.Core.Soundness Require Import Realizability.
+From Mcltt.Core.Soundness Require Export LogicalRelation EquivalenceLemmas.
+Import Domain_Notations.
+
+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 }} ->
+    {{ DG a' ∈ glu_univ_elem i ↘ P' ↘ El' }} ->
+    {{ Γ ⊢ A ® P }} ->
+    {{ Γ ⊢ A' ® P' }} ->
+    {{ Γ ⊢ A ⊆ A' }}.
+Proof.
+  intros * Hsubtyp Hglu Hglu' HA HA'.
+  gen A' A Γ. gen El' El P' P.
+  induction Hsubtyp using per_subtyp_ind; intros; subst;
+    saturate_refl_for per_univ_elem;
+    invert_glu_univ_elem Hglu;
+    handle_functional_glu_univ_elem;
+    handle_per_univ_elem_irrel;
+    destruct_by_head pi_glu_typ_pred;
+    saturate_glu_by_per;
+    invert_glu_univ_elem Hglu';
+    handle_functional_glu_univ_elem;
+    try solve [simpl in *; mauto 4].
+  - match_by_head (per_bot b b') ltac:(fun H => specialize (H (length Γ)) as [V []]).
+    simpl in *.
+    destruct_conjs.
+    assert {{ Γ ⊢ A[Id] ≈ A : Type@i }} as <- by mauto 4.
+    assert {{ Γ ⊢ A'[Id] ≈ A' : Type@i }} as <- by mauto 4.
+    assert {{ Γ ⊢ A'[Id] ≈ V : Type@i }} as -> by mauto 4.
+    econstructor.
+    mauto 4.
+  - bulky_rewrite.
+    mauto 3.
+  - destruct_by_head pi_glu_typ_pred.
+    rename x into IP. rename x0 into IEl. rename x1 into OP. rename x2 into OEl.
+    rename M0 into M'. rename IT0 into IT'. rename OT0 into OT'.
+    rename x3 into OP'. rename x4 into OEl'.
+    assert {{ Γ ⊢ IT ® IP }}.
+    {
+      assert {{ Γ ⊢ IT[Id] ® IP }} by mauto.
+      simpl in *.
+      autorewrite with mcltt in *; mauto.
+    }
+    assert {{ Γ ⊢ IT' ® IP }}.
+    {
+      assert {{ Γ ⊢ IT'[Id] ® IP }} by mauto.
+      simpl in *.
+      autorewrite with mcltt in *; mauto.
+    }
+    do 2 bulky_rewrite1.
+    assert {{ Γ ⊢ IT ≈ IT' : Type@i }} by mauto 4 using glu_univ_elem_per_univ_typ_escape.
+    enough {{ Γ, IT' ⊢ OT ⊆ OT' }} by mauto 3.
+    assert {{ Dom ⇑! a (length Γ) ≈ ⇑! a' (length Γ) ∈ in_rel }} as equiv_len_len' by (eapply per_bot_then_per_elem; mauto).
+    assert {{ Dom ⇑! a (length Γ) ≈ ⇑! a (length Γ) ∈ in_rel }} as equiv_len_len by (eapply per_bot_then_per_elem; mauto).
+    assert {{ Dom ⇑! a' (length Γ) ≈ ⇑! a' (length Γ) ∈ in_rel }} as equiv_len'_len' by (eapply per_bot_then_per_elem; mauto).
+    handle_per_univ_elem_irrel.
+    match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H).
+    apply_relation_equivalence.
+    destruct_rel_mod_eval.
+    handle_per_univ_elem_irrel.
+    rename a1 into b.
+    rename a3 into b'.
+    assert {{ DG b ∈ glu_univ_elem i ↘ OP d{{{ ⇑! a (length Γ) }}} equiv_len_len ↘ OEl d{{{ ⇑! a (length Γ) }}} equiv_len_len }} by mauto.
+    assert {{ DG b' ∈ glu_univ_elem i ↘ OP' d{{{ ⇑! a' (length Γ) }}} equiv_len'_len' ↘ OEl' d{{{ ⇑! a' (length Γ) }}} equiv_len'_len' }} by mauto.
+    assert {{ Γ, IT' ⊢ OT ® OP d{{{ ⇑! a (length Γ) }}} equiv_len_len }}.
+    {
+      assert {{ Γ, IT ⊢ #0 : IT[Wk] ® !(length Γ) ∈ glu_elem_bot i a }} by eauto using var_glu_elem_bot.
+      assert {{ Γ, IT ⊢ #0 : IT[Wk] ® ⇑! a (length Γ) ∈ IEl }} by (eapply realize_glu_elem_bot; mauto).
+      assert {{ ⊢ Γ, IT' ≈ Γ, IT }} as -> by mauto.
+      assert {{ Γ, IT ⊢ OT[Wk,,#0] ≈ OT : Type@i }} as <- by (bulky_rewrite1; mauto 3).
+      mauto.
+    }
+    assert {{ Γ, IT' ⊢ OT' ® OP' d{{{ ⇑! a' (length Γ) }}} equiv_len'_len' }}.
+    {
+      assert {{ Γ, IT' ⊢ #0 : IT'[Wk] ® !(length Γ) ∈ glu_elem_bot i a' }} by eauto using var_glu_elem_bot.
+      assert {{ Γ, IT' ⊢ #0 : IT'[Wk] ® ⇑! a' (length Γ) ∈ IEl }} by (eapply realize_glu_elem_bot; mauto).
+      assert {{ Γ, IT' ⊢ OT'[Wk,,#0] ® OP' d{{{ ⇑! a' (length Γ) }}} equiv_len'_len' }} by mauto.
+      assert {{ Γ, IT' ⊢ OT'[Wk,,#0] ≈ OT' : Type@i }} as <- by (bulky_rewrite1; mauto 3).
+      mauto.
+    }
+    mauto 3.
+Qed.

From 54ed0f2806c49d68ddc7810b782f4a1f05b660bc Mon Sep 17 00:00:00 2001
From: Junyoung/Clare Jang <jjc9310@gmail.com>
Date: Thu, 8 Aug 2024 15:08:10 -0400
Subject: [PATCH 2/8] Stuck

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

diff --git a/theories/Core/Soundness/SubtypingLemmas.v b/theories/Core/Soundness/SubtypingLemmas.v
index 3120215b..107265dd 100644
--- a/theories/Core/Soundness/SubtypingLemmas.v
+++ b/theories/Core/Soundness/SubtypingLemmas.v
@@ -86,3 +86,79 @@ Proof.
     }
     mauto 3.
 Qed.
+
+Lemma glu_univ_elem_per_subtyp_typ_if : forall {i a a' P P' El El' Γ A},
+    {{ Sub a <: a' at i }} ->
+    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    {{ DG a' ∈ glu_univ_elem i ↘ P' ↘ El' }} ->
+    {{ Γ ⊢ A ® P }} ->
+    exists A', {{ Γ ⊢ A' ® P' }}.
+Proof.
+  intros * Hsubtyp Hglu Hglu'.
+  gen A Γ. gen El' El P' P.
+  induction Hsubtyp using per_subtyp_ind; intros; subst;
+    saturate_refl_for per_univ_elem;
+    invert_glu_univ_elem Hglu;
+    handle_functional_glu_univ_elem;
+    handle_per_univ_elem_irrel;
+    destruct_by_head pi_glu_typ_pred;
+    saturate_glu_by_per;
+    invert_glu_univ_elem Hglu';
+    try solve [eexists; handle_functional_glu_univ_elem; simpl in *; mauto 4];
+    handle_functional_glu_univ_elem.
+  - exists A; handle_functional_glu_univ_elem.
+    split; firstorder.
+    match_by_head (per_bot b b') ltac:(fun H => specialize (H (length Δ)) as [V' []]).
+    functional_read_rewrite_clear.
+    mauto.
+  - handle_per_univ_elem_irrel.
+    rename x into IP. rename x0 into IEl. rename x1 into OP. rename x2 into OEl.
+    rename x3 into OP'. rename x4 into OEl'.
+    assert {{ Dom ⇑! a (length Γ) ≈ ⇑! a' (length Γ) ∈ in_rel }} as equiv_len_len' by (eapply per_bot_then_per_elem; mauto).
+    assert {{ Dom ⇑! a (length Γ) ≈ ⇑! a (length Γ) ∈ in_rel }} as equiv_len_len by (eapply per_bot_then_per_elem; mauto).
+    assert {{ Dom ⇑! a' (length Γ) ≈ ⇑! a' (length Γ) ∈ in_rel }} as equiv_len'_len' by (eapply per_bot_then_per_elem; mauto).
+    match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H).
+    apply_relation_equivalence.
+    destruct_rel_mod_eval.
+    handle_per_univ_elem_irrel.
+    rename a1 into b.
+    rename a3 into b'.
+    assert {{ DG b ∈ glu_univ_elem i ↘ OP d{{{ ⇑! a (length Γ) }}} equiv_len_len ↘ OEl d{{{ ⇑! a (length Γ) }}} equiv_len_len }} by mauto.
+    assert {{ DG b' ∈ glu_univ_elem i ↘ OP' d{{{ ⇑! a' (length Γ) }}} equiv_len'_len' ↘ OEl' d{{{ ⇑! a' (length Γ) }}} equiv_len'_len' }} by mauto.
+    assert {{ Γ ⊢ IT ® IP }}.
+    {
+      assert {{ Γ ⊢ IT[Id] ® IP }} by mauto.
+      simpl in *.
+      autorewrite with mcltt in *; mauto.
+    }
+    assert {{ Γ, IT ⊢ OT ® OP d{{{ ⇑! a (length Γ) }}} equiv_len_len }}.
+    {
+      assert {{ Γ, IT ⊢ #0 : IT[Wk] ® !(length Γ) ∈ glu_elem_bot i a }} by mauto using var_glu_elem_bot.
+      assert {{ Γ, IT ⊢ #0 : IT[Wk] ® ⇑! a (length Γ) ∈ IEl }} by (eapply realize_glu_elem_bot; mauto).
+      assert {{ Γ, IT ⊢ OT[Wk,,#0] ≈ OT : Type@i }} as <- by (bulky_rewrite1; mauto 3).
+      mauto.
+    }
+    assert (exists OT', {{ Γ, IT ⊢ OT' ® OP' d{{{ ⇑! a' (length Γ) }}} equiv_len'_len' }}) as [OT'] by mauto.
+    assert {{ Γ, IT ⊢ OT' : Type@i }} by mauto 3 using glu_univ_elem_univ_lvl.
+    exists {{{ Π IT OT' }}}.
+    apply_predicate_equivalence.
+    econstructor; mauto 4.
+    (* stuck.... *)
+    intros.
+    destruct_rel_mod_eval.
+    handle_per_univ_elem_irrel.
+    rename a1 into c.
+    rename equiv_a into equiv_c.
+    rename a2 into b0.
+    rename a7 into b'0.
+    assert (exists OT'', {{ Δ ⊢ OT'' ® OP' c equiv_c }}) as [OT''] by mauto.
+    assert {{ Γ, IT ⊢ OT' ® glu_typ_top i b' }} as [] by mauto 4.
+    assert {{ Δ ⊢ OT'' ® glu_typ_top i b'0 }} as [] by mauto 4.
+    assert {{ DG b'0 ∈ glu_univ_elem i ↘ OP' c equiv_c ↘ OEl' c equiv_c }} by mauto.
+    enough {{ Δ ⊢ OT'[σ,,m] ≈ OT'' : Type@i }} as -> by mauto.
+    (* assert {{ Δ ⊢ OT''[Id] ≈ OT'' : Type@i }} as <- by mauto. *)
+    (* assert {{ Δ ⊢ m : IT[σ] }} by mauto 3 using glu_univ_elem_trm_escape. *)
+    (* assert {{ Δ ⊢s σ : Γ }} by mauto. *)
+    (* assert {{ Δ ⊢s Wk∘(Id,,m) ≈ Id : Δ }} as <- by mauto 3. *)
+    (* assert {{ Γ, IT ⊢ OT[Wk,,#0] ≈ OT : Type@i }} as <- by (bulky_rewrite1; mauto 3). *)
+Abort.

From ca0098321a067b377068687ba689804521a091bf Mon Sep 17 00:00:00 2001
From: Junyoung/Clare Jang <jjc9310@gmail.com>
Date: Thu, 8 Aug 2024 15:16:36 -0400
Subject: [PATCH 3/8] Fix CI

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

diff --git a/theories/_CoqProject b/theories/_CoqProject
index d400f8cd..79f47f52 100644
--- a/theories/_CoqProject
+++ b/theories/_CoqProject
@@ -59,6 +59,7 @@
 ./Core/Soundness/LogicalRelation/Definitions.v
 ./Core/Soundness/LogicalRelation/Lemmas.v
 ./Core/Soundness/Realizability.v
+./Core/Soundness/SubtypingLemmas.v
 ./Core/Soundness/Weakening.v
 ./Core/Soundness/Weakening/Definition.v
 ./Core/Soundness/Weakening/Lemmas.v

From f382bd273e8172c343774a274621f190446bcb75 Mon Sep 17 00:00:00 2001
From: "Junyoung/\"Clare\" Jang" <jjc9310@gmail.com>
Date: Fri, 9 Aug 2024 16:34:36 -0400
Subject: [PATCH 4/8] Some updates

---
 theories/Core/Soundness/SubtypingCases.v  |  60 +++++++
 theories/Core/Soundness/SubtypingLemmas.v | 193 +++++++++++++++-------
 2 files changed, 195 insertions(+), 58 deletions(-)
 create mode 100644 theories/Core/Soundness/SubtypingCases.v

diff --git a/theories/Core/Soundness/SubtypingCases.v b/theories/Core/Soundness/SubtypingCases.v
new file mode 100644
index 00000000..410b36d9
--- /dev/null
+++ b/theories/Core/Soundness/SubtypingCases.v
@@ -0,0 +1,60 @@
+From Coq Require Import Morphisms Morphisms_Prop Morphisms_Relations Relation_Definitions RelationClasses.
+
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core.Completeness Require Import FundamentalTheorem.
+From Mcltt.Core.Semantic Require Import Realizability.
+From Mcltt.Core.Soundness Require Import Realizability.
+From Mcltt.Core.Soundness Require Export LogicalRelation EquivalenceLemmas.
+From Mcltt.Core.Syntactic Require Import Corollaries.
+Import Domain_Notations.
+
+(* TODO: move this to a better place *)
+Lemma destruct_glu_rel_exp : forall {Γ Sb M A},
+  {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
+  {{ Γ ⊩ M : A }} ->
+  exists i,
+  forall Δ σ ρ,
+    {{ Δ ⊢s σ ® ρ ∈ Sb }} ->
+    glu_rel_exp_sub i Δ M A σ ρ.
+Proof.
+  intros * ? [Sb'].
+  destruct_conjs.
+  eexists; intros.
+  (* TODO: handle functional glu_ctx_env here *)
+  assert (Sb <∙> Sb') by admit.
+  apply_predicate_equivalence.
+  mauto.
+Admitted.
+
+Lemma glu_rel_exp_subtyp : forall {Γ M A A' i},
+    {{ Γ ⊩ A : Type@i }} ->
+    {{ Γ ⊩ A' : Type@i }} ->
+    {{ Γ ⊩ M : A }} ->
+    {{ Γ ⊢ A ⊆ A' }} ->
+    {{ Γ ⊩ M : A' }}.
+Proof.
+  intros * HA HA' [Sb [? [i]]] [env_relΓ [? [j]]]%completeness_fundamental_subtyp.
+  destruct_conjs.
+  eapply destruct_glu_rel_exp in HA, HA'; try eassumption.
+  destruct_conjs.
+  econstructor; split; [eassumption |].
+  exists (max i j); intros.
+  (* TODO: extract this as a tactic *)
+  match goal with
+  | H: context[glu_rel_exp_sub _ _ _ _ _ _] |- _ => edestruct H; try eassumption
+  end.
+  (* TODO: introduce a lemma for glu_ctx_env *)
+  assert {{ Dom ρ ≈ ρ ∈ env_relΓ }} by admit.
+  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+  destruct_by_head rel_exp.
+  handle_per_univ_elem_irrel.
+  rename m' into a'.
+  (* assert (exists P' El', {{ DG a' ∈ glu_univ_elem (max i j) ↘ P' ↘ El' }}) as [P' [El']]. *)
+  (* { *)
+  (*   assert (exists R R', {{ DF a ≈ a ∈ per_univ_elem j ↘ R }} /\ {{ DF a' ≈ a' ∈ per_univ_elem j ↘ R' }}) by mauto using per_subtyp_to_univ_elem. *)
+  (*   destruct_conjs. *)
+  (*   assert {{ Dom a' ≈ a' ∈ per_univ (max i j) }} by (eexists; mauto using per_univ_elem_cumu_max_right). *)
+  (*   apply per_univ_glu_univ_elem; mauto. *)
+  (* } *)
+  (* econstructor; try eassumption. *)
+Admitted.
diff --git a/theories/Core/Soundness/SubtypingLemmas.v b/theories/Core/Soundness/SubtypingLemmas.v
index 107265dd..e661fa5d 100644
--- a/theories/Core/Soundness/SubtypingLemmas.v
+++ b/theories/Core/Soundness/SubtypingLemmas.v
@@ -3,7 +3,7 @@ From Coq Require Import Morphisms Morphisms_Prop Morphisms_Relations Relation_De
 From Mcltt Require Import Base LibTactics.
 From Mcltt.Core.Syntactic Require Import Corollaries.
 From Mcltt.Core.Semantic Require Import Realizability.
-From Mcltt.Core.Soundness Require Import Realizability.
+From Mcltt.Core.Soundness Require Import Cumulativity Realizability.
 From Mcltt.Core.Soundness Require Export LogicalRelation EquivalenceLemmas.
 Import Domain_Notations.
 
@@ -87,15 +87,43 @@ Proof.
     mauto 3.
 Qed.
 
-Lemma glu_univ_elem_per_subtyp_typ_if : forall {i a a' P P' El El' Γ A},
+(* Lemma glu_univ_elem_per_subtyp_typ_if : forall {i Γ Sb Δ σ p A A' a a' P P' El El'}, *)
+(*     {{ EG Γ ∈ glu_ctx_env ↘ Sb }} -> *)
+(*     {{ Δ ⊢s σ ® p ∈ Sb }} -> *)
+(*     {{ ⟦ A ⟧ p ↘ a }} -> *)
+(*     {{ ⟦ A' ⟧ p ↘ a' }} -> *)
+(*     {{ Sub a <: a' at i }} -> *)
+(*     {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} -> *)
+(*     {{ DG a' ∈ glu_univ_elem i ↘ P' ↘ El' }} -> *)
+(*     {{ Δ ⊢ A[σ] ® P }} -> *)
+(*     {{ Δ ⊢ A'[σ] ® P' }}. *)
+(* Proof. *)
+(*   intros * HSb Hσ Heval Heval' Hsubtyp Hglu Hglu' HA. *)
+(*   gen El' El P' P. gen A' A p σ. gen Δ Sb Γ. *)
+(*   induction Hsubtyp using per_subtyp_ind; intros; subst; *)
+(*     saturate_refl_for per_univ_elem; *)
+(*     invert_glu_univ_elem Hglu; *)
+(*     handle_functional_glu_univ_elem; *)
+(*     handle_per_univ_elem_irrel; *)
+(*     destruct_by_head pi_glu_typ_pred; *)
+(*     saturate_glu_by_per; *)
+(*     invert_glu_univ_elem Hglu'; *)
+(*     handle_functional_glu_univ_elem; *)
+(*     try solve [simpl in *; mauto 4]. *)
+(*   - inversion_by_head neut_glu_typ_pred. *)
+(*     econstructor; mauto. *)
+
+Lemma glu_univ_elem_per_subtyp_trm_if : forall {i a a' P P' El El' Γ A A' M m},
     {{ Sub a <: a' at i }} ->
     {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
     {{ DG a' ∈ glu_univ_elem i ↘ P' ↘ El' }} ->
     {{ Γ ⊢ A ® P }} ->
-    exists A', {{ Γ ⊢ A' ® P' }}.
+    {{ Γ ⊢ A' ® P' }} ->
+    {{ Γ ⊢ M : A ® m ∈ El }} ->
+    {{ Γ ⊢ M : A' ® m ∈ El' }}.
 Proof.
   intros * Hsubtyp Hglu Hglu'.
-  gen A Γ. gen El' El P' P.
+  gen m M A Γ. gen El' El P' P.
   induction Hsubtyp using per_subtyp_ind; intros; subst;
     saturate_refl_for per_univ_elem;
     invert_glu_univ_elem Hglu;
@@ -104,61 +132,110 @@ Proof.
     destruct_by_head pi_glu_typ_pred;
     saturate_glu_by_per;
     invert_glu_univ_elem Hglu';
-    try solve [eexists; handle_functional_glu_univ_elem; simpl in *; mauto 4];
-    handle_functional_glu_univ_elem.
-  - exists A; handle_functional_glu_univ_elem.
-    split; firstorder.
-    match_by_head (per_bot b b') ltac:(fun H => specialize (H (length Δ)) as [V' []]).
-    functional_read_rewrite_clear.
-    mauto.
-  - handle_per_univ_elem_irrel.
-    rename x into IP. rename x0 into IEl. rename x1 into OP. rename x2 into OEl.
-    rename x3 into OP'. rename x4 into OEl'.
-    assert {{ Dom ⇑! a (length Γ) ≈ ⇑! a' (length Γ) ∈ in_rel }} as equiv_len_len' by (eapply per_bot_then_per_elem; mauto).
-    assert {{ Dom ⇑! a (length Γ) ≈ ⇑! a (length Γ) ∈ in_rel }} as equiv_len_len by (eapply per_bot_then_per_elem; mauto).
-    assert {{ Dom ⇑! a' (length Γ) ≈ ⇑! a' (length Γ) ∈ in_rel }} as equiv_len'_len' by (eapply per_bot_then_per_elem; mauto).
-    match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H).
-    apply_relation_equivalence.
-    destruct_rel_mod_eval.
-    handle_per_univ_elem_irrel.
-    rename a1 into b.
-    rename a3 into b'.
-    assert {{ DG b ∈ glu_univ_elem i ↘ OP d{{{ ⇑! a (length Γ) }}} equiv_len_len ↘ OEl d{{{ ⇑! a (length Γ) }}} equiv_len_len }} by mauto.
-    assert {{ DG b' ∈ glu_univ_elem i ↘ OP' d{{{ ⇑! a' (length Γ) }}} equiv_len'_len' ↘ OEl' d{{{ ⇑! a' (length Γ) }}} equiv_len'_len' }} by mauto.
-    assert {{ Γ ⊢ IT ® IP }}.
+    handle_functional_glu_univ_elem;
+    try solve [simpl in *; intuition].
+  - destruct_by_head neut_glu_exp_pred.
+    destruct_by_head neut_glu_typ_pred.
+    rename A into a''.
+    rename M into A.
+    rename m into M.
+    clear_dups.
+    match_by_head1 (per_bot b b') ltac:(fun H => destruct (H (length Γ)) as [V []]).
+    assert {{ Γ ⊢ A ≈ A' : Type@i }}.
     {
-      assert {{ Γ ⊢ IT[Id] ® IP }} by mauto.
-      simpl in *.
-      autorewrite with mcltt in *; mauto.
+      assert {{ Γ ⊢ A'[Id] ≈ V : Type@i }} by mauto 4.
+      assert {{ Γ ⊢ A[Id] ≈ V : Type@i }} by mauto 4.
+      autorewrite with mcltt in *.
+      mauto.
     }
-    assert {{ Γ, IT ⊢ OT ® OP d{{{ ⇑! a (length Γ) }}} equiv_len_len }}.
-    {
-      assert {{ Γ, IT ⊢ #0 : IT[Wk] ® !(length Γ) ∈ glu_elem_bot i a }} by mauto using var_glu_elem_bot.
-      assert {{ Γ, IT ⊢ #0 : IT[Wk] ® ⇑! a (length Γ) ∈ IEl }} by (eapply realize_glu_elem_bot; mauto).
-      assert {{ Γ, IT ⊢ OT[Wk,,#0] ≈ OT : Type@i }} as <- by (bulky_rewrite1; mauto 3).
+    econstructor; mauto 3.
+    + econstructor; mauto 3.
+    + intros.
+      match_by_head1 (per_bot b b') ltac:(fun H => destruct (H (length Δ)) as [? []]).
+      functional_read_rewrite_clear.
+      assert {{ Δ ⊢ A[σ] ≈ A'[σ] : Type@i }} by mauto.
+      assert {{ Δ ⊢ M[σ] ≈ v : A[σ] }} by mauto.
       mauto.
+  - simpl in *.
+    assert {{ Γ ⊢ A ⊆ A' }}
+      by (transitivity {{{ Type@i }}}; mauto 3; transitivity {{{ Type@j }}}; mauto 3).
+    destruct_conjs.
+    intuition mauto 3.
+    assert (exists P El, {{ DG m ∈ glu_univ_elem j ↘ P ↘ El }}) as [? [?]].
+    {
+      assert {{ Dom m ≈ m ∈ per_univ i }} as [] by mauto using glu_univ_elem_per_univ.
+      mauto using per_univ_glu_univ_elem.
     }
-    assert (exists OT', {{ Γ, IT ⊢ OT' ® OP' d{{{ ⇑! a' (length Γ) }}} equiv_len'_len' }}) as [OT'] by mauto.
-    assert {{ Γ, IT ⊢ OT' : Type@i }} by mauto 3 using glu_univ_elem_univ_lvl.
-    exists {{{ Π IT OT' }}}.
-    apply_predicate_equivalence.
-    econstructor; mauto 4.
-    (* stuck.... *)
-    intros.
-    destruct_rel_mod_eval.
-    handle_per_univ_elem_irrel.
-    rename a1 into c.
-    rename equiv_a into equiv_c.
-    rename a2 into b0.
-    rename a7 into b'0.
-    assert (exists OT'', {{ Δ ⊢ OT'' ® OP' c equiv_c }}) as [OT''] by mauto.
-    assert {{ Γ, IT ⊢ OT' ® glu_typ_top i b' }} as [] by mauto 4.
-    assert {{ Δ ⊢ OT'' ® glu_typ_top i b'0 }} as [] by mauto 4.
-    assert {{ DG b'0 ∈ glu_univ_elem i ↘ OP' c equiv_c ↘ OEl' c equiv_c }} by mauto.
-    enough {{ Δ ⊢ OT'[σ,,m] ≈ OT'' : Type@i }} as -> by mauto.
-    (* assert {{ Δ ⊢ OT''[Id] ≈ OT'' : Type@i }} as <- by mauto. *)
-    (* assert {{ Δ ⊢ m : IT[σ] }} by mauto 3 using glu_univ_elem_trm_escape. *)
-    (* assert {{ Δ ⊢s σ : Γ }} by mauto. *)
-    (* assert {{ Δ ⊢s Wk∘(Id,,m) ≈ Id : Δ }} as <- by mauto 3. *)
-    (* assert {{ Γ, IT ⊢ OT[Wk,,#0] ≈ OT : Type@i }} as <- by (bulky_rewrite1; mauto 3). *)
-Abort.
+    do 2 eexists; split; mauto.
+    eapply glu_univ_elem_typ_cumu_ge; revgoals; mautosolve.
+  - eexists; handle_functional_glu_univ_elem.
+
+(* Proof. *)
+(*   intros * Hsubtyp Hglu Hglu'. *)
+(*   gen A Γ. gen El' El P' P. *)
+(*   induction Hsubtyp using per_subtyp_ind; intros; subst; *)
+(*     saturate_refl_for per_univ_elem; *)
+(*     invert_glu_univ_elem Hglu; *)
+(*     handle_functional_glu_univ_elem; *)
+(*     handle_per_univ_elem_irrel; *)
+(*     destruct_by_head pi_glu_typ_pred; *)
+(*     saturate_glu_by_per; *)
+(*     invert_glu_univ_elem Hglu'; *)
+(*     try solve [eexists; handle_functional_glu_univ_elem; simpl in *; mauto 4]; *)
+(*     handle_functional_glu_univ_elem. *)
+(*   - exists A; handle_functional_glu_univ_elem. *)
+(*     split; firstorder. *)
+(*     match_by_head (per_bot b b') ltac:(fun H => specialize (H (length Δ)) as [V' []]). *)
+(*     functional_read_rewrite_clear. *)
+(*     mauto. *)
+(*   - handle_per_univ_elem_irrel. *)
+(*     rename x into IP. rename x0 into IEl. rename x1 into OP. rename x2 into OEl. *)
+(*     rename x3 into OP'. rename x4 into OEl'. *)
+(*     assert {{ Dom ⇑! a (length Γ) ≈ ⇑! a' (length Γ) ∈ in_rel }} as equiv_len_len' by (eapply per_bot_then_per_elem; mauto). *)
+(*     assert {{ Dom ⇑! a (length Γ) ≈ ⇑! a (length Γ) ∈ in_rel }} as equiv_len_len by (eapply per_bot_then_per_elem; mauto). *)
+(*     assert {{ Dom ⇑! a' (length Γ) ≈ ⇑! a' (length Γ) ∈ in_rel }} as equiv_len'_len' by (eapply per_bot_then_per_elem; mauto). *)
+(*     match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H). *)
+(*     apply_relation_equivalence. *)
+(*     destruct_rel_mod_eval. *)
+(*     handle_per_univ_elem_irrel. *)
+(*     rename a1 into b. *)
+(*     rename a3 into b'. *)
+(*     assert {{ DG b ∈ glu_univ_elem i ↘ OP d{{{ ⇑! a (length Γ) }}} equiv_len_len ↘ OEl d{{{ ⇑! a (length Γ) }}} equiv_len_len }} by mauto. *)
+(*     assert {{ DG b' ∈ glu_univ_elem i ↘ OP' d{{{ ⇑! a' (length Γ) }}} equiv_len'_len' ↘ OEl' d{{{ ⇑! a' (length Γ) }}} equiv_len'_len' }} by mauto. *)
+(*     assert {{ Γ ⊢ IT ® IP }}. *)
+(*     { *)
+(*       assert {{ Γ ⊢ IT[Id] ® IP }} by mauto. *)
+(*       simpl in *. *)
+(*       autorewrite with mcltt in *; mauto. *)
+(*     } *)
+(*     assert {{ Γ, IT ⊢ OT ® OP d{{{ ⇑! a (length Γ) }}} equiv_len_len }}. *)
+(*     { *)
+(*       assert {{ Γ, IT ⊢ #0 : IT[Wk] ® !(length Γ) ∈ glu_elem_bot i a }} by mauto using var_glu_elem_bot. *)
+(*       assert {{ Γ, IT ⊢ #0 : IT[Wk] ® ⇑! a (length Γ) ∈ IEl }} by (eapply realize_glu_elem_bot; mauto). *)
+(*       assert {{ Γ, IT ⊢ OT[Wk,,#0] ≈ OT : Type@i }} as <- by (bulky_rewrite1; mauto 3). *)
+(*       mauto. *)
+(*     } *)
+(*     assert (exists OT', {{ Γ, IT ⊢ OT' ® OP' d{{{ ⇑! a' (length Γ) }}} equiv_len'_len' }}) as [OT'] by mauto. *)
+(*     assert {{ Γ, IT ⊢ OT' : Type@i }} by mauto 3 using glu_univ_elem_univ_lvl. *)
+(*     exists {{{ Π IT OT' }}}. *)
+(*     apply_predicate_equivalence. *)
+(*     econstructor; mauto 4. *)
+(*     (* stuck.... *) *)
+(*     intros. *)
+(*     destruct_rel_mod_eval. *)
+(*     handle_per_univ_elem_irrel. *)
+(*     rename a1 into c. *)
+(*     rename equiv_a into equiv_c. *)
+(*     rename a2 into b0. *)
+(*     rename a7 into b'0. *)
+(*     assert (exists OT'', {{ Δ ⊢ OT'' ® OP' c equiv_c }}) as [OT''] by mauto. *)
+(*     assert {{ Γ, IT ⊢ OT' ® glu_typ_top i b' }} as [] by mauto 4. *)
+(*     assert {{ Δ ⊢ OT'' ® glu_typ_top i b'0 }} as [] by mauto 4. *)
+(*     assert {{ DG b'0 ∈ glu_univ_elem i ↘ OP' c equiv_c ↘ OEl' c equiv_c }} by mauto. *)
+(*     enough {{ Δ ⊢ OT'[σ,,m] ≈ OT'' : Type@i }} as -> by mauto. *)
+(*     (* assert {{ Δ ⊢ OT''[Id] ≈ OT'' : Type@i }} as <- by mauto. *) *)
+(*     (* assert {{ Δ ⊢ m : IT[σ] }} by mauto 3 using glu_univ_elem_trm_escape. *) *)
+(*     (* assert {{ Δ ⊢s σ : Γ }} by mauto. *) *)
+(*     (* assert {{ Δ ⊢s Wk∘(Id,,m) ≈ Id : Δ }} as <- by mauto 3. *) *)
+(*     (* assert {{ Γ, IT ⊢ OT[Wk,,#0] ≈ OT : Type@i }} as <- by (bulky_rewrite1; mauto 3). *) *)
+(* Abort. *)

From e3730872e1132cb46a60e0161e71f638cc534049 Mon Sep 17 00:00:00 2001
From: Junyoung/Clare Jang <jjc9310@gmail.com>
Date: Sun, 11 Aug 2024 00:19:24 -0400
Subject: [PATCH 5/8] Prove subtyping case with some admitted asserts

---
 theories/Core/Soundness/EquivalenceLemmas.v |  20 ++-
 theories/Core/Soundness/SubtypingCases.v    |  40 +++--
 theories/Core/Soundness/SubtypingLemmas.v   | 155 ++++++--------------
 3 files changed, 83 insertions(+), 132 deletions(-)

diff --git a/theories/Core/Soundness/EquivalenceLemmas.v b/theories/Core/Soundness/EquivalenceLemmas.v
index 6fa62396..879bc3d6 100644
--- a/theories/Core/Soundness/EquivalenceLemmas.v
+++ b/theories/Core/Soundness/EquivalenceLemmas.v
@@ -7,16 +7,16 @@ From Mcltt.Core.Soundness Require Import Realizability.
 From Mcltt.Core.Soundness Require Export LogicalRelation.
 Import Domain_Notations.
 
-Lemma glu_univ_elem_per_univ_typ_escape : forall {i a a' P P' El El' Γ A A'},
-    {{ Dom a ≈ a' ∈ per_univ i }} ->
+Lemma glu_univ_elem_per_univ_elem_typ_escape : forall {i a a' elem_rel P P' El El' Γ A A'},
+    {{ DF a ≈ a' ∈ per_univ_elem i ↘ elem_rel }} ->
     {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
     {{ DG a' ∈ glu_univ_elem i ↘ P' ↘ El' }} ->
     {{ Γ ⊢ A ® P }} ->
     {{ Γ ⊢ A' ® P' }} ->
     {{ Γ ⊢ A ≈ A' : Type@i }}.
 Proof.
-  intros * [? Hper] Hglu Hglu' HA HA'.
-  gen A' A Γ. gen El' El P' P.
+  intros * Hper Hglu Hglu' HA HA'.
+  gen A' A Γ. gen El' El P' P. simpl in Hper.
   induction Hper using per_univ_elem_ind; intros; subst;
     saturate_refl_for per_univ_elem;
     invert_glu_univ_elem Hglu;
@@ -81,6 +81,18 @@ Proof.
     mauto 4.
 Qed.
 
+Lemma glu_univ_elem_per_univ_typ_escape : forall {i a a' P P' El El' Γ A A'},
+    {{ Dom a ≈ a' ∈ per_univ i }} ->
+    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    {{ DG a' ∈ glu_univ_elem i ↘ P' ↘ El' }} ->
+    {{ Γ ⊢ A ® P }} ->
+    {{ Γ ⊢ A' ® P' }} ->
+    {{ Γ ⊢ A ≈ A' : Type@i }}.
+Proof.
+  intros * [] **.
+  mauto using glu_univ_elem_per_univ_elem_typ_escape.
+Qed.
+
 Lemma glu_univ_elem_per_univ_typ_iff : forall {i a a' P P' El El'},
     {{ Dom a ≈ a' ∈ per_univ i }} ->
     {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
diff --git a/theories/Core/Soundness/SubtypingCases.v b/theories/Core/Soundness/SubtypingCases.v
index 410b36d9..7994a4b6 100644
--- a/theories/Core/Soundness/SubtypingCases.v
+++ b/theories/Core/Soundness/SubtypingCases.v
@@ -3,8 +3,7 @@ From Coq Require Import Morphisms Morphisms_Prop Morphisms_Relations Relation_De
 From Mcltt Require Import Base LibTactics.
 From Mcltt.Core.Completeness Require Import FundamentalTheorem.
 From Mcltt.Core.Semantic Require Import Realizability.
-From Mcltt.Core.Soundness Require Import Realizability.
-From Mcltt.Core.Soundness Require Export LogicalRelation EquivalenceLemmas.
+From Mcltt.Core.Soundness Require Import Cumulativity EquivalenceLemmas LogicalRelation Realizability SubtypingLemmas.
 From Mcltt.Core.Syntactic Require Import Corollaries.
 Import Domain_Notations.
 
@@ -37,24 +36,35 @@ Proof.
   destruct_conjs.
   eapply destruct_glu_rel_exp in HA, HA'; try eassumption.
   destruct_conjs.
+  rename i0 into k.
   econstructor; split; [eassumption |].
-  exists (max i j); intros.
+  exists (max i (max j k)); intros.
   (* TODO: extract this as a tactic *)
-  match goal with
-  | H: context[glu_rel_exp_sub _ _ _ _ _ _] |- _ => edestruct H; try eassumption
-  end.
+  repeat match goal with
+         | H: context[glu_rel_exp_sub _ _ _ _ _ _] |- _ =>
+             match type of H with
+             | __mark__ _ _ => fail 1
+             | _ => edestruct H; try eassumption; mark H
+             end
+         end; unmark_all.
+  simplify_evals.
+  match_by_head glu_univ_elem ltac:(fun H => directed invert_glu_univ_elem H).
+  handle_functional_glu_univ_elem.
+  simpl in *.
   (* TODO: introduce a lemma for glu_ctx_env *)
   assert {{ Dom ρ ≈ ρ ∈ env_relΓ }} by admit.
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).
   destruct_by_head rel_exp.
   handle_per_univ_elem_irrel.
-  rename m' into a'.
-  (* assert (exists P' El', {{ DG a' ∈ glu_univ_elem (max i j) ↘ P' ↘ El' }}) as [P' [El']]. *)
-  (* { *)
-  (*   assert (exists R R', {{ DF a ≈ a ∈ per_univ_elem j ↘ R }} /\ {{ DF a' ≈ a' ∈ per_univ_elem j ↘ R' }}) by mauto using per_subtyp_to_univ_elem. *)
-  (*   destruct_conjs. *)
-  (*   assert {{ Dom a' ≈ a' ∈ per_univ (max i j) }} by (eexists; mauto using per_univ_elem_cumu_max_right). *)
-  (*   apply per_univ_glu_univ_elem; mauto. *)
-  (* } *)
-  (* econstructor; try eassumption. *)
+  assert (exists P El, glu_univ_elem (max i (max j k)) P El m0) as [? []] by admit. (* simple by cumulativity *)
+  econstructor; try eassumption.
+  assert {{ Sub m <: m0 at max i (max j k) }} by mauto using per_subtyp_cumu_left, per_subtyp_cumu_right.
+  assert (exists P El, glu_univ_elem (max i (max j k)) P El m) as [? []] by admit. (* simple by cumulativity *)
+  eapply glu_univ_elem_per_subtyp_trm_if; mauto.
+  - assert (k <= max i (max j k)) by lia.
+    eapply glu_univ_elem_typ_cumu_ge; mauto.
+  - assert (k <= max i (max j k)) by lia.
+    eapply glu_univ_elem_typ_cumu_ge; revgoals; mauto.
+  - assert (i <= max i (max j k)) by lia.
+    eapply glu_univ_elem_exp_cumu_ge; mauto.
 Admitted.
diff --git a/theories/Core/Soundness/SubtypingLemmas.v b/theories/Core/Soundness/SubtypingLemmas.v
index e661fa5d..a3f93753 100644
--- a/theories/Core/Soundness/SubtypingLemmas.v
+++ b/theories/Core/Soundness/SubtypingLemmas.v
@@ -87,32 +87,6 @@ Proof.
     mauto 3.
 Qed.
 
-(* Lemma glu_univ_elem_per_subtyp_typ_if : forall {i Γ Sb Δ σ p A A' a a' P P' El El'}, *)
-(*     {{ EG Γ ∈ glu_ctx_env ↘ Sb }} -> *)
-(*     {{ Δ ⊢s σ ® p ∈ Sb }} -> *)
-(*     {{ ⟦ A ⟧ p ↘ a }} -> *)
-(*     {{ ⟦ A' ⟧ p ↘ a' }} -> *)
-(*     {{ Sub a <: a' at i }} -> *)
-(*     {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} -> *)
-(*     {{ DG a' ∈ glu_univ_elem i ↘ P' ↘ El' }} -> *)
-(*     {{ Δ ⊢ A[σ] ® P }} -> *)
-(*     {{ Δ ⊢ A'[σ] ® P' }}. *)
-(* Proof. *)
-(*   intros * HSb Hσ Heval Heval' Hsubtyp Hglu Hglu' HA. *)
-(*   gen El' El P' P. gen A' A p σ. gen Δ Sb Γ. *)
-(*   induction Hsubtyp using per_subtyp_ind; intros; subst; *)
-(*     saturate_refl_for per_univ_elem; *)
-(*     invert_glu_univ_elem Hglu; *)
-(*     handle_functional_glu_univ_elem; *)
-(*     handle_per_univ_elem_irrel; *)
-(*     destruct_by_head pi_glu_typ_pred; *)
-(*     saturate_glu_by_per; *)
-(*     invert_glu_univ_elem Hglu'; *)
-(*     handle_functional_glu_univ_elem; *)
-(*     try solve [simpl in *; mauto 4]. *)
-(*   - inversion_by_head neut_glu_typ_pred. *)
-(*     econstructor; mauto. *)
-
 Lemma glu_univ_elem_per_subtyp_trm_if : forall {i a a' P P' El El' Γ A A' M m},
     {{ Sub a <: a' at i }} ->
     {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
@@ -122,43 +96,34 @@ Lemma glu_univ_elem_per_subtyp_trm_if : forall {i a a' P P' El El' Γ A A' M m},
     {{ Γ ⊢ M : A ® m ∈ El }} ->
     {{ Γ ⊢ M : A' ® m ∈ El' }}.
 Proof.
-  intros * Hsubtyp Hglu Hglu'.
-  gen m M A Γ. gen El' El P' P.
+  intros * Hsubtyp Hglu Hglu' HA HA'.
+  assert {{ Γ ⊢ A ⊆ A' }} by mauto 3 using glu_univ_elem_per_subtyp_typ_escape.
+  gen m M A' A. gen Γ. gen El' El P' P.
   induction Hsubtyp using per_subtyp_ind; intros; subst;
     saturate_refl_for per_univ_elem;
     invert_glu_univ_elem Hglu;
     handle_functional_glu_univ_elem;
     handle_per_univ_elem_irrel;
-    destruct_by_head pi_glu_typ_pred;
+    repeat invert_glu_rel1;
     saturate_glu_by_per;
     invert_glu_univ_elem Hglu';
     handle_functional_glu_univ_elem;
+    repeat invert_glu_rel1;
     try solve [simpl in *; intuition].
-  - destruct_by_head neut_glu_exp_pred.
-    destruct_by_head neut_glu_typ_pred.
-    rename A into a''.
+  - rename A into a''.
     rename M into A.
     rename m into M.
     clear_dups.
     match_by_head1 (per_bot b b') ltac:(fun H => destruct (H (length Γ)) as [V []]).
-    assert {{ Γ ⊢ A ≈ A' : Type@i }}.
-    {
-      assert {{ Γ ⊢ A'[Id] ≈ V : Type@i }} by mauto 4.
-      assert {{ Γ ⊢ A[Id] ≈ V : Type@i }} by mauto 4.
-      autorewrite with mcltt in *.
-      mauto.
-    }
     econstructor; mauto 3.
     + econstructor; mauto 3.
     + intros.
       match_by_head1 (per_bot b b') ltac:(fun H => destruct (H (length Δ)) as [? []]).
       functional_read_rewrite_clear.
-      assert {{ Δ ⊢ A[σ] ≈ A'[σ] : Type@i }} by mauto.
+      assert {{ Δ ⊢ A[σ] ⊆ A'[σ] }} by mauto 3.
       assert {{ Δ ⊢ M[σ] ≈ v : A[σ] }} by mauto.
       mauto.
   - simpl in *.
-    assert {{ Γ ⊢ A ⊆ A' }}
-      by (transitivity {{{ Type@i }}}; mauto 3; transitivity {{{ Type@j }}}; mauto 3).
     destruct_conjs.
     intuition mauto 3.
     assert (exists P El, {{ DG m ∈ glu_univ_elem j ↘ P ↘ El }}) as [? [?]].
@@ -168,74 +133,38 @@ Proof.
     }
     do 2 eexists; split; mauto.
     eapply glu_univ_elem_typ_cumu_ge; revgoals; mautosolve.
-  - eexists; handle_functional_glu_univ_elem.
-
-(* Proof. *)
-(*   intros * Hsubtyp Hglu Hglu'. *)
-(*   gen A Γ. gen El' El P' P. *)
-(*   induction Hsubtyp using per_subtyp_ind; intros; subst; *)
-(*     saturate_refl_for per_univ_elem; *)
-(*     invert_glu_univ_elem Hglu; *)
-(*     handle_functional_glu_univ_elem; *)
-(*     handle_per_univ_elem_irrel; *)
-(*     destruct_by_head pi_glu_typ_pred; *)
-(*     saturate_glu_by_per; *)
-(*     invert_glu_univ_elem Hglu'; *)
-(*     try solve [eexists; handle_functional_glu_univ_elem; simpl in *; mauto 4]; *)
-(*     handle_functional_glu_univ_elem. *)
-(*   - exists A; handle_functional_glu_univ_elem. *)
-(*     split; firstorder. *)
-(*     match_by_head (per_bot b b') ltac:(fun H => specialize (H (length Δ)) as [V' []]). *)
-(*     functional_read_rewrite_clear. *)
-(*     mauto. *)
-(*   - handle_per_univ_elem_irrel. *)
-(*     rename x into IP. rename x0 into IEl. rename x1 into OP. rename x2 into OEl. *)
-(*     rename x3 into OP'. rename x4 into OEl'. *)
-(*     assert {{ Dom ⇑! a (length Γ) ≈ ⇑! a' (length Γ) ∈ in_rel }} as equiv_len_len' by (eapply per_bot_then_per_elem; mauto). *)
-(*     assert {{ Dom ⇑! a (length Γ) ≈ ⇑! a (length Γ) ∈ in_rel }} as equiv_len_len by (eapply per_bot_then_per_elem; mauto). *)
-(*     assert {{ Dom ⇑! a' (length Γ) ≈ ⇑! a' (length Γ) ∈ in_rel }} as equiv_len'_len' by (eapply per_bot_then_per_elem; mauto). *)
-(*     match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H). *)
-(*     apply_relation_equivalence. *)
-(*     destruct_rel_mod_eval. *)
-(*     handle_per_univ_elem_irrel. *)
-(*     rename a1 into b. *)
-(*     rename a3 into b'. *)
-(*     assert {{ DG b ∈ glu_univ_elem i ↘ OP d{{{ ⇑! a (length Γ) }}} equiv_len_len ↘ OEl d{{{ ⇑! a (length Γ) }}} equiv_len_len }} by mauto. *)
-(*     assert {{ DG b' ∈ glu_univ_elem i ↘ OP' d{{{ ⇑! a' (length Γ) }}} equiv_len'_len' ↘ OEl' d{{{ ⇑! a' (length Γ) }}} equiv_len'_len' }} by mauto. *)
-(*     assert {{ Γ ⊢ IT ® IP }}. *)
-(*     { *)
-(*       assert {{ Γ ⊢ IT[Id] ® IP }} by mauto. *)
-(*       simpl in *. *)
-(*       autorewrite with mcltt in *; mauto. *)
-(*     } *)
-(*     assert {{ Γ, IT ⊢ OT ® OP d{{{ ⇑! a (length Γ) }}} equiv_len_len }}. *)
-(*     { *)
-(*       assert {{ Γ, IT ⊢ #0 : IT[Wk] ® !(length Γ) ∈ glu_elem_bot i a }} by mauto using var_glu_elem_bot. *)
-(*       assert {{ Γ, IT ⊢ #0 : IT[Wk] ® ⇑! a (length Γ) ∈ IEl }} by (eapply realize_glu_elem_bot; mauto). *)
-(*       assert {{ Γ, IT ⊢ OT[Wk,,#0] ≈ OT : Type@i }} as <- by (bulky_rewrite1; mauto 3). *)
-(*       mauto. *)
-(*     } *)
-(*     assert (exists OT', {{ Γ, IT ⊢ OT' ® OP' d{{{ ⇑! a' (length Γ) }}} equiv_len'_len' }}) as [OT'] by mauto. *)
-(*     assert {{ Γ, IT ⊢ OT' : Type@i }} by mauto 3 using glu_univ_elem_univ_lvl. *)
-(*     exists {{{ Π IT OT' }}}. *)
-(*     apply_predicate_equivalence. *)
-(*     econstructor; mauto 4. *)
-(*     (* stuck.... *) *)
-(*     intros. *)
-(*     destruct_rel_mod_eval. *)
-(*     handle_per_univ_elem_irrel. *)
-(*     rename a1 into c. *)
-(*     rename equiv_a into equiv_c. *)
-(*     rename a2 into b0. *)
-(*     rename a7 into b'0. *)
-(*     assert (exists OT'', {{ Δ ⊢ OT'' ® OP' c equiv_c }}) as [OT''] by mauto. *)
-(*     assert {{ Γ, IT ⊢ OT' ® glu_typ_top i b' }} as [] by mauto 4. *)
-(*     assert {{ Δ ⊢ OT'' ® glu_typ_top i b'0 }} as [] by mauto 4. *)
-(*     assert {{ DG b'0 ∈ glu_univ_elem i ↘ OP' c equiv_c ↘ OEl' c equiv_c }} by mauto. *)
-(*     enough {{ Δ ⊢ OT'[σ,,m] ≈ OT'' : Type@i }} as -> by mauto. *)
-(*     (* assert {{ Δ ⊢ OT''[Id] ≈ OT'' : Type@i }} as <- by mauto. *) *)
-(*     (* assert {{ Δ ⊢ m : IT[σ] }} by mauto 3 using glu_univ_elem_trm_escape. *) *)
-(*     (* assert {{ Δ ⊢s σ : Γ }} by mauto. *) *)
-(*     (* assert {{ Δ ⊢s Wk∘(Id,,m) ≈ Id : Δ }} as <- by mauto 3. *) *)
-(*     (* assert {{ Γ, IT ⊢ OT[Wk,,#0] ≈ OT : Type@i }} as <- by (bulky_rewrite1; mauto 3). *) *)
-(* Abort. *)
+  - rename M into A.
+    rename M0 into A'.
+    rename m into M.
+    rename IT1 into IT'. rename OT1 into OT'.
+    rename x into IP. rename x0 into IEl.
+    rename x1 into OP. rename x2 into OEl.
+    handle_per_univ_elem_irrel.
+    econstructor; mauto 4.
+    + admit.
+    + intros.
+      assert {{ Γ ⊢w Id : Γ }} by mauto.
+      assert {{ Γ ⊢ IT0 ® IP }}.
+      {
+        assert {{ Γ ⊢ IT0[Id] ® IP }} by mauto.
+        simpl in *.
+        autorewrite with mcltt in *; mauto.
+      }
+      assert {{ Γ ⊢ IT' ® IP }}.
+      {
+        assert {{ Γ ⊢ IT'[Id] ® IP }} by mauto.
+        simpl in *.
+        autorewrite with mcltt in *; mauto.
+      }
+      assert {{ Δ ⊢ IT0[σ] ≈ IT'[σ] : Type@i }} by mauto 4 using glu_univ_elem_per_univ_elem_typ_escape.
+      assert {{ Δ ⊢ m' : IT0[σ] ® b ∈ IEl }} by (simpl; bulky_rewrite1; eassumption).
+      assert (exists ab : domain, {{ $| a0 & b |↘ ab }} /\ OEl b equiv_b Δ (a_sub OT0 {{{ σ,, m' }}}) {{{ ~ (a_sub M σ) m' }}} ab) by mauto.
+      destruct_conjs.
+      eexists; split; mauto.
+      match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H).
+      destruct_rel_mod_eval.
+      handle_per_univ_elem_irrel.
+      eapply H1 with (M := {{{ M[σ] m' }}}) (m := H35); mauto 3.
+      * admit. (* almost obvious *)
+      * admit. (* by a separate lemma *)
+Admitted.

From 9093c9541a43247b5398fb84a2c7beaa91565464 Mon Sep 17 00:00:00 2001
From: Junyoung/Clare Jang <jjc9310@gmail.com>
Date: Sun, 11 Aug 2024 00:25:10 -0400
Subject: [PATCH 6/8] Fix CI error

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

diff --git a/theories/_CoqProject b/theories/_CoqProject
index 79f47f52..782eec3c 100644
--- a/theories/_CoqProject
+++ b/theories/_CoqProject
@@ -59,6 +59,7 @@
 ./Core/Soundness/LogicalRelation/Definitions.v
 ./Core/Soundness/LogicalRelation/Lemmas.v
 ./Core/Soundness/Realizability.v
+./Core/Soundness/SubtypingCases.v
 ./Core/Soundness/SubtypingLemmas.v
 ./Core/Soundness/Weakening.v
 ./Core/Soundness/Weakening/Definition.v

From 28e13a24b694344dae3d78fcc788be0da7075d8a Mon Sep 17 00:00:00 2001
From: Junyoung/Clare Jang <jjc9310@gmail.com>
Date: Mon, 12 Aug 2024 14:04:29 -0400
Subject: [PATCH 7/8] Remove most of admitted subgoals

---
 theories/Core/Soundness/Cumulativity.v        | 32 +++++++++++++++
 .../Core/Soundness/LogicalRelation/Lemmas.v   | 19 ++++++++-
 theories/Core/Soundness/SubtypingCases.v      | 10 +++--
 theories/Core/Soundness/SubtypingLemmas.v     | 40 ++++++++++---------
 4 files changed, 78 insertions(+), 23 deletions(-)

diff --git a/theories/Core/Soundness/Cumulativity.v b/theories/Core/Soundness/Cumulativity.v
index 67125235..4fea3a68 100644
--- a/theories/Core/Soundness/Cumulativity.v
+++ b/theories/Core/Soundness/Cumulativity.v
@@ -7,6 +7,38 @@ From Mcltt.Core.Soundness Require Import Realizability.
 From Mcltt.Core.Soundness Require Export LogicalRelation.
 Import Domain_Notations.
 
+Corollary glu_univ_elem_cumu_ge : forall {i j a P El},
+    i <= j ->
+    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    exists P' El', {{ DG a ∈ glu_univ_elem j ↘ P' ↘ El' }}.
+Proof.
+  intros.
+  assert {{ Dom a ≈ a ∈ per_univ i }} as [R] by mauto.
+  assert {{ DF a ≈ a ∈ per_univ_elem j ↘ R }} by mauto using per_univ_elem_cumu_ge.
+  mauto.
+Qed.
+
+#[export]
+Hint Resolve glu_univ_elem_cumu_ge : mcltt.
+
+Corollary glu_univ_elem_cumu_max_left : forall {i j a P El},
+    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    exists P' El', {{ DG a ∈ glu_univ_elem (max i j) ↘ P' ↘ El' }}.
+Proof.
+  intros.
+  assert (i <= max i j) by lia.
+  mauto.
+Qed.
+
+Corollary glu_univ_elem_cumu_max_right : forall {i j a P El},
+    {{ DG a ∈ glu_univ_elem j ↘ P ↘ El }} ->
+    exists P' El', {{ DG a ∈ glu_univ_elem (max i j) ↘ P' ↘ El' }}.
+Proof.
+  intros.
+  assert (j <= max i j) by lia.
+  mauto.
+Qed.
+
 Section glu_univ_elem_cumulativity.
   #[local]
   Lemma glu_univ_elem_cumulativity_ge : forall {i j a P P' El El'},
diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
index c0e95de2..8e4b83b2 100644
--- a/theories/Core/Soundness/LogicalRelation/Lemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -260,6 +260,9 @@ Proof.
     mauto.
 Qed.
 
+#[export]
+Hint Resolve glu_univ_elem_per_univ : mcltt.
+
 Lemma glu_univ_elem_per_elem : forall i P El A,
     {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} ->
     forall Γ t T a R,
@@ -272,7 +275,7 @@ Proof.
     try do 2 match_by_head1 per_univ_elem invert_per_univ_elem;
     simpl_glu_rel;
     try fold (per_univ j a a);
-    mauto 4 using glu_univ_elem_per_univ.
+    mauto 4.
 
   intros.
   destruct_rel_mod_app.
@@ -728,6 +731,20 @@ Proof.
     glu_univ_elem_econstructor; try reflexivity; mauto.
 Qed.
 
+#[export]
+Hint Resolve per_univ_glu_univ_elem : mcltt.
+
+Corollary per_univ_elem_glu_univ_elem : forall i a R,
+    {{ DF a ≈ a ∈ per_univ_elem i ↘ R }} ->
+    exists P El, {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }}.
+Proof.
+  intros.
+  apply per_univ_glu_univ_elem; mauto.
+Qed.
+
+#[export]
+Hint Resolve per_univ_elem_glu_univ_elem : mcltt.
+
 Ltac saturate_glu_info1 :=
   match goal with
   | H : glu_univ_elem _ ?P _ _,
diff --git a/theories/Core/Soundness/SubtypingCases.v b/theories/Core/Soundness/SubtypingCases.v
index 7994a4b6..7fb1c205 100644
--- a/theories/Core/Soundness/SubtypingCases.v
+++ b/theories/Core/Soundness/SubtypingCases.v
@@ -56,13 +56,15 @@ Proof.
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).
   destruct_by_head rel_exp.
   handle_per_univ_elem_irrel.
-  assert (exists P El, glu_univ_elem (max i (max j k)) P El m0) as [? []] by admit. (* simple by cumulativity *)
+  assert (exists P El, glu_univ_elem (max i (max j k)) P El m0) as [? []].
+  {
+    assert (exists P El, glu_univ_elem (max j k) P El m0) as [? []];
+      mauto using glu_univ_elem_cumu_max_right.
+  }
   econstructor; try eassumption.
   assert {{ Sub m <: m0 at max i (max j k) }} by mauto using per_subtyp_cumu_left, per_subtyp_cumu_right.
-  assert (exists P El, glu_univ_elem (max i (max j k)) P El m) as [? []] by admit. (* simple by cumulativity *)
+  assert (exists P El, glu_univ_elem (max i (max j k)) P El m) as [? []] by mauto using glu_univ_elem_cumu_max_left.
   eapply glu_univ_elem_per_subtyp_trm_if; mauto.
-  - assert (k <= max i (max j k)) by lia.
-    eapply glu_univ_elem_typ_cumu_ge; mauto.
   - assert (k <= max i (max j k)) by lia.
     eapply glu_univ_elem_typ_cumu_ge; revgoals; mauto.
   - assert (i <= max i (max j k)) by lia.
diff --git a/theories/Core/Soundness/SubtypingLemmas.v b/theories/Core/Soundness/SubtypingLemmas.v
index a3f93753..e5165235 100644
--- a/theories/Core/Soundness/SubtypingLemmas.v
+++ b/theories/Core/Soundness/SubtypingLemmas.v
@@ -91,13 +91,12 @@ Lemma glu_univ_elem_per_subtyp_trm_if : forall {i a a' P P' El El' Γ A A' M m},
     {{ Sub a <: a' at i }} ->
     {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
     {{ DG a' ∈ glu_univ_elem i ↘ P' ↘ El' }} ->
-    {{ Γ ⊢ A ® P }} ->
     {{ Γ ⊢ A' ® P' }} ->
     {{ Γ ⊢ M : A ® m ∈ El }} ->
     {{ Γ ⊢ M : A' ® m ∈ El' }}.
 Proof.
   intros * Hsubtyp Hglu Hglu' HA HA'.
-  assert {{ Γ ⊢ A ⊆ A' }} by mauto 3 using glu_univ_elem_per_subtyp_typ_escape.
+  assert {{ Γ ⊢ A ⊆ A' }} by (eapply glu_univ_elem_per_subtyp_typ_escape; only 4: eapply glu_univ_elem_trm_typ; mauto).
   gen m M A' A. gen Γ. gen El' El P' P.
   induction Hsubtyp using per_subtyp_ind; intros; subst;
     saturate_refl_for per_univ_elem;
@@ -126,27 +125,27 @@ Proof.
   - simpl in *.
     destruct_conjs.
     intuition mauto 3.
-    assert (exists P El, {{ DG m ∈ glu_univ_elem j ↘ P ↘ El }}) as [? [?]].
-    {
-      assert {{ Dom m ≈ m ∈ per_univ i }} as [] by mauto using glu_univ_elem_per_univ.
-      mauto using per_univ_glu_univ_elem.
-    }
+    assert (exists P El, {{ DG m ∈ glu_univ_elem j ↘ P ↘ El }}) as [? [?]] by mauto.
     do 2 eexists; split; mauto.
     eapply glu_univ_elem_typ_cumu_ge; revgoals; mautosolve.
   - rename M into A.
     rename M0 into A'.
     rename m into M.
-    rename IT1 into IT'. rename OT1 into OT'.
+    rename IT0 into IT'. rename OT0 into OT'.
     rename x into IP. rename x0 into IEl.
     rename x1 into OP. rename x2 into OEl.
+    rename x3 into OP'. rename x4 into OEl'.
     handle_per_univ_elem_irrel.
     econstructor; mauto 4.
-    + admit.
+    + enough {{ Sub Π a p B <: Π a' p' B' at i }} by (eapply per_elem_subtyping; try eassumption).
+      econstructor; mauto.
     + intros.
+      rename b into c.
+      rename equiv_b into equiv_c.
       assert {{ Γ ⊢w Id : Γ }} by mauto.
-      assert {{ Γ ⊢ IT0 ® IP }}.
+      assert {{ Γ ⊢ IT ® IP }}.
       {
-        assert {{ Γ ⊢ IT0[Id] ® IP }} by mauto.
+        assert {{ Γ ⊢ IT[Id] ® IP }} by mauto.
         simpl in *.
         autorewrite with mcltt in *; mauto.
       }
@@ -156,15 +155,20 @@ Proof.
         simpl in *.
         autorewrite with mcltt in *; mauto.
       }
-      assert {{ Δ ⊢ IT0[σ] ≈ IT'[σ] : Type@i }} by mauto 4 using glu_univ_elem_per_univ_elem_typ_escape.
-      assert {{ Δ ⊢ m' : IT0[σ] ® b ∈ IEl }} by (simpl; bulky_rewrite1; eassumption).
-      assert (exists ab : domain, {{ $| a0 & b |↘ ab }} /\ OEl b equiv_b Δ (a_sub OT0 {{{ σ,, m' }}}) {{{ ~ (a_sub M σ) m' }}} ab) by mauto.
+      assert {{ Δ ⊢ IT[σ] ≈ IT'[σ] : Type@i }} by mauto 4 using glu_univ_elem_per_univ_elem_typ_escape.
+      assert {{ Δ ⊢ m' : IT[σ] ® c ∈ IEl }} by (simpl; bulky_rewrite1; eassumption).
+      assert (exists ac : domain, {{ $| a0 & c |↘ ac }} /\ OEl c equiv_c Δ (a_sub OT {{{ σ,, m' }}}) {{{ ~ (a_sub M σ) m' }}} ac) by mauto.
       destruct_conjs.
       eexists; split; mauto.
       match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H).
       destruct_rel_mod_eval.
       handle_per_univ_elem_irrel.
-      eapply H1 with (M := {{{ M[σ] m' }}}) (m := H35); mauto 3.
-      * admit. (* almost obvious *)
-      * admit. (* by a separate lemma *)
-Admitted.
+      rename a1 into b.
+      rename a2 into b'.
+      eapply H1 with (M := {{{ M[σ] m' }}}) (m := H30); mauto 3.
+      assert {{ Δ ⊢ OT[σ,,m'] ® OP c equiv_c }} by (eapply glu_univ_elem_trm_typ; mauto).
+      assert {{ DG b ∈ glu_univ_elem i ↘ OP c equiv_c ↘ OEl c equiv_c }} by mauto.
+      assert {{ DG b' ∈ glu_univ_elem i ↘ OP' c equiv_c ↘ OEl' c equiv_c }} by mauto.
+      enough {{ Sub b <: b' at i }} by mauto 3 using glu_univ_elem_per_subtyp_typ_escape.
+      mauto.
+Qed.

From 925106d385edea57495945e8dee978d94cd8ae04 Mon Sep 17 00:00:00 2001
From: Junyoung/Clare Jang <jjc9310@gmail.com>
Date: Thu, 15 Aug 2024 12:45:33 -0400
Subject: [PATCH 8/8] Refactor proofs a bit

---
 theories/Core/Soundness/Cumulativity.v        |  52 ++------
 theories/Core/Soundness/EquivalenceLemmas.v   | 125 +++++++++---------
 .../Core/Soundness/LogicalRelation/Lemmas.v   |   2 +
 theories/Core/Soundness/SubtypingLemmas.v     |  13 +-
 4 files changed, 83 insertions(+), 109 deletions(-)

diff --git a/theories/Core/Soundness/Cumulativity.v b/theories/Core/Soundness/Cumulativity.v
index 4fea3a68..2158151a 100644
--- a/theories/Core/Soundness/Cumulativity.v
+++ b/theories/Core/Soundness/Cumulativity.v
@@ -3,7 +3,7 @@ From Coq Require Import Morphisms Morphisms_Prop Morphisms_Relations Relation_De
 From Mcltt Require Import Base LibTactics.
 From Mcltt.Core.Syntactic Require Import Corollaries.
 From Mcltt.Core.Semantic Require Import Realizability.
-From Mcltt.Core.Soundness Require Import Realizability.
+From Mcltt.Core.Soundness Require Import EquivalenceLemmas Realizability.
 From Mcltt.Core.Soundness Require Export LogicalRelation.
 Import Domain_Notations.
 
@@ -14,7 +14,7 @@ Corollary glu_univ_elem_cumu_ge : forall {i j a P El},
 Proof.
   intros.
   assert {{ Dom a ≈ a ∈ per_univ i }} as [R] by mauto.
-  assert {{ DF a ≈ a ∈ per_univ_elem j ↘ R }} by mauto using per_univ_elem_cumu_ge.
+  assert {{ DF a ≈ a ∈ per_univ_elem j ↘ R }} by mauto.
   mauto.
 Qed.
 
@@ -48,7 +48,7 @@ Section glu_univ_elem_cumulativity.
       (forall Γ A, {{ Γ ⊢ A ® P }} -> {{ Γ ⊢ A ® P' }}) /\
         (forall Γ A M m, {{ Γ ⊢ M : A ® m ∈ El }} -> {{ Γ ⊢ M : A ® m ∈ El' }}) /\
         (forall Γ A M m, {{ Γ ⊢ A ® P }} -> {{ Γ ⊢ M : A ® m ∈ El' }} -> {{ Γ ⊢ M : A ® m ∈ El }}).
-  Proof.
+  Proof with mautosolve 4.
     simpl.
     intros * Hge Hglu Hglu'. gen El' P' j.
     induction Hglu using glu_univ_elem_ind; repeat split; intros;
@@ -65,8 +65,8 @@ Section glu_univ_elem_cumulativity.
       destruct_by_head pi_glu_typ_pred.
       econstructor; intros; mauto 4.
       + assert {{ Δ ⊢ IT[σ] ® IP }} by mauto.
-        assert (forall Γ A, {{ Γ ⊢ A ® IP }} -> {{ Γ ⊢ A ® IP' }}) by (eapply proj1; mauto).
-        mauto.
+        enough (forall Γ A, {{ Γ ⊢ A ® IP }} -> {{ Γ ⊢ A ® IP' }}) by mauto 4.
+        eapply proj1...
       + rename a0 into c.
         rename equiv_a into equiv_c.
         match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H).
@@ -76,7 +76,7 @@ Section glu_univ_elem_cumulativity.
         assert (forall Γ A, {{ Γ ⊢ A ® OP c equiv_c }} -> {{ Γ ⊢ A ® OP' c equiv_c }}) by (eapply proj1; mauto).
         enough {{ Δ ⊢ OT[σ,,m] ® OP c equiv_c }} by mauto.
         enough {{ Δ ⊢ m : IT[σ] ® c ∈ IEl }} by mauto.
-        eapply IHHglu; mauto.
+        eapply IHHglu...
     - rename x into IP'.
       rename x0 into IEl'.
       rename x1 into OP'.
@@ -84,8 +84,8 @@ Section glu_univ_elem_cumulativity.
       destruct_by_head pi_glu_exp_pred.
       handle_per_univ_elem_irrel.
       econstructor; intros; mauto 4.
-      + assert (forall Γ A, {{ Γ ⊢ A ® IP }} -> {{ Γ ⊢ A ® IP' }}) by (eapply proj1; mauto).
-        mauto.
+      + enough (forall Γ A, {{ Γ ⊢ A ® IP }} -> {{ Γ ⊢ A ® IP' }}) by mauto 4.
+        eapply proj1...
       + rename b into c.
         rename equiv_b into equiv_c.
         match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H).
@@ -99,8 +99,7 @@ Section glu_univ_elem_cumulativity.
         assert {{ Δ ⊢ m' : IT[σ] ® c ∈ IEl }} by (eapply IHHglu; mauto).
         assert (exists ac, {{ $| a0 & c |↘ ac }} /\ {{ Δ ⊢ m[σ] m' : OT[σ,,m'] ® ac ∈ OEl c equiv_c }}) by mauto.
         destruct_conjs.
-        functional_eval_rewrite_clear.
-        mauto.
+        functional_eval_rewrite_clear...
     - rename x into IP'.
       rename x0 into IEl'.
       rename x1 into OP'.
@@ -118,47 +117,24 @@ Section glu_univ_elem_cumulativity.
       handle_per_univ_elem_irrel.
       rename a1 into b.
       eexists; split; mauto.
-      assert (forall Γ A M m, {{ Γ ⊢ A ® OP c equiv_c }} -> {{ Γ ⊢ M : A ® m ∈ OEl' c equiv_c }} -> {{ Γ ⊢ M : A ® m ∈ OEl c equiv_c }}) by (eapply proj2, proj2; eauto 3).
+      assert (forall Γ A M m, {{ Γ ⊢ A ® OP c equiv_c }} -> {{ Γ ⊢ M : A ® m ∈ OEl' c equiv_c }} -> {{ Γ ⊢ M : A ® m ∈ OEl c equiv_c }}) by (eapply proj2, proj2; eauto).
       assert {{ Δ ⊢ OT[σ,,m'] ® OP c equiv_c }} by mauto.
       enough {{ Δ ⊢ m[σ] m' : OT[σ,,m'] ® fa ∈ OEl' c equiv_c }} by mauto.
       assert {{ Δ ⊢ m' : IT[σ] ® c ∈ IEl' }} by (eapply IHHglu; mauto).
-      assert {{ Δ ⊢ IT[σ] ≈ IT0[σ] : Type@j }} as HITeq.
-      {
-        assert {{ Δ ⊢ IT[σ] ® glu_typ_top i a }} as [] by mauto 3.
-        assert {{ Δ ⊢ IT0[σ] ® glu_typ_top j a }} as [] by mauto 3.
-        match_by_head per_top_typ ltac:(fun H => destruct (H (length Δ)) as [? []]).
-        clear_dups.
-        functional_read_rewrite_clear.
-        assert {{ Δ ⊢ IT[σ][Id] ≈ x1 : Type@i }} by mauto 4.
-        assert {{ Δ ⊢ IT[σ] ≈ x1 : Type@i }} by mauto 4.
-        assert {{ Δ ⊢ IT[σ] ≈ x1 : Type@j }} by mauto 4.
-        assert {{ Δ ⊢ IT0[σ][Id] ≈ x1 : Type@j }} by mauto 4.
-        enough {{ Δ ⊢ IT0[σ] ≈ x1 : Type@j }}; mautosolve 4.
-      }
+      assert {{ Δ ⊢ IT[σ] ≈ IT0[σ] : Type@j }} as HITeq by mauto 4.
       assert {{ Δ ⊢ m' : IT0[σ] ® c ∈ IEl' }} by (rewrite <- HITeq; mauto).
       assert (exists ac, {{ $| a0 & c |↘ ac }} /\ {{ Δ ⊢ m[σ] m' : OT0[σ,,m'] ® ac ∈ OEl' c equiv_c }}) by mauto.
       destruct_conjs.
       functional_eval_rewrite_clear.
       assert {{ DG b ∈ glu_univ_elem j ↘ OP' c equiv_c ↘ OEl' c equiv_c }} by mauto.
-      enough {{ Δ ⊢ OT[σ,,m'] ≈ OT0[σ,,m'] : Type@j }} as -> by mauto.
-      assert {{ DG b ∈ glu_univ_elem i ↘ OP c equiv_c ↘ OEl c equiv_c }} by mauto.
       assert {{ Δ ⊢ OT0[σ,,m'] ® OP' c equiv_c }} by (eapply glu_univ_elem_trm_typ; mauto).
-      assert {{ Δ ⊢ OT[σ,,m'] ® glu_typ_top i b }} as [] by mauto 3.
-      assert {{ Δ ⊢ OT0[σ,,m'] ® glu_typ_top j b }} as [] by mauto 3.
-      match_by_head per_top_typ ltac:(fun H => destruct (H (length Δ)) as [? []]).
-      clear_dups.
-      functional_read_rewrite_clear.
-      assert {{ Δ ⊢ OT[σ,,m'][Id] ≈ x1 : Type@i }} by mauto 4.
-      assert {{ Δ ⊢ OT[σ,,m'] ≈ x1 : Type@i }} by mauto 4.
-      assert {{ Δ ⊢ OT[σ,,m'] ≈ x1 : Type@j }} by mauto 4.
-      assert {{ Δ ⊢ OT0[σ,,m'][Id] ≈ x1 : Type@j }} by mauto 4.
-      enough {{ Δ ⊢ OT0[σ,,m'] ≈ x1 : Type@j }}; mautosolve 4.
+      enough {{ Δ ⊢ OT[σ,,m'] ≈ OT0[σ,,m'] : Type@j }} as ->...
     - destruct_by_head neut_glu_exp_pred.
       econstructor; mauto.
       destruct_by_head neut_glu_typ_pred.
-      econstructor; mauto.
+      econstructor...
     - destruct_by_head neut_glu_exp_pred.
-      econstructor; mauto.
+      econstructor...
   Qed.
 End glu_univ_elem_cumulativity.
 
diff --git a/theories/Core/Soundness/EquivalenceLemmas.v b/theories/Core/Soundness/EquivalenceLemmas.v
index 879bc3d6..861c7d61 100644
--- a/theories/Core/Soundness/EquivalenceLemmas.v
+++ b/theories/Core/Soundness/EquivalenceLemmas.v
@@ -7,6 +7,56 @@ From Mcltt.Core.Soundness Require Import Realizability.
 From Mcltt.Core.Soundness Require Export LogicalRelation.
 Import Domain_Notations.
 
+Lemma glu_univ_elem_typ_escape : forall {i j a P P' El El' Γ A A'},
+    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    {{ DG a ∈ glu_univ_elem j ↘ P' ↘ El' }} ->
+    {{ Γ ⊢ A ® P }} ->
+    {{ Γ ⊢ A' ® P' }} ->
+    {{ Γ ⊢ A ≈ A' : Type@(max i j) }}.
+Proof with mautosolve 4.
+  intros.
+  assert {{ Γ ⊢ A ® glu_typ_top i a }} as [] by mauto 3.
+  assert {{ Γ ⊢ A' ® glu_typ_top j a }} as [] by mauto 3.
+  match_by_head per_top_typ ltac:(fun H => destruct (H (length Γ)) as [V []]).
+  clear_dups.
+  functional_read_rewrite_clear.
+  assert {{ Γ ⊢ A : Type@(max i j) }} by mauto 4 using lift_exp_max_left.
+  assert {{ Γ ⊢ A' : Type@(max i j) }} by mauto 4 using lift_exp_max_right.
+  assert {{ Γ ⊢ A[Id] ≈ V : Type@i }} by mauto 4.
+  assert {{ Γ ⊢ A[Id] ≈ V : Type@(max i j) }} by mauto 4 using lift_exp_eq_max_left.
+  assert {{ Γ ⊢ A'[Id] ≈ V : Type@j }} by mauto 4.
+  assert {{ Γ ⊢ A'[Id] ≈ V : Type@(max i j) }} by mauto 4 using lift_exp_eq_max_right.
+  autorewrite with mcltt in *...
+Qed.
+
+#[export]
+Hint Resolve glu_univ_elem_typ_escape : mcltt.
+
+Lemma glu_univ_elem_typ_escape_ge : forall {i j a P P' El El' Γ A A'},
+    i <= j ->
+    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    {{ DG a ∈ glu_univ_elem j ↘ P' ↘ El' }} ->
+    {{ Γ ⊢ A ® P }} ->
+    {{ Γ ⊢ A' ® P' }} ->
+    {{ Γ ⊢ A ≈ A' : Type@j }}.
+Proof with mautosolve 4.
+  intros.
+  replace j with (max i j) by lia...
+Qed.
+
+#[export]
+Hint Resolve glu_univ_elem_typ_escape_ge : mcltt.
+
+Lemma glu_univ_elem_typ_escape' : forall {i a P El Γ A A'},
+    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    {{ Γ ⊢ A ® P }} ->
+    {{ Γ ⊢ A' ® P }} ->
+    {{ Γ ⊢ A ≈ A' : Type@i }}.
+Proof. mautosolve 4. Qed.
+
+#[export]
+Hint Resolve glu_univ_elem_typ_escape' : mcltt.
+
 Lemma glu_univ_elem_per_univ_elem_typ_escape : forall {i a a' elem_rel P P' El El' Γ A A'},
     {{ DF a ≈ a' ∈ per_univ_elem i ↘ elem_rel }} ->
     {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
@@ -14,73 +64,16 @@ Lemma glu_univ_elem_per_univ_elem_typ_escape : forall {i a a' elem_rel P P' El E
     {{ Γ ⊢ A ® P }} ->
     {{ Γ ⊢ A' ® P' }} ->
     {{ Γ ⊢ A ≈ A' : Type@i }}.
-Proof.
+Proof with mautosolve 4.
+  simpl in *.
   intros * Hper Hglu Hglu' HA HA'.
-  gen A' A Γ. gen El' El P' P. simpl in Hper.
-  induction Hper using per_univ_elem_ind; intros; subst;
-    saturate_refl_for per_univ_elem;
-    invert_glu_univ_elem Hglu;
-    handle_functional_glu_univ_elem;
-    handle_per_univ_elem_irrel;
-    destruct_by_head pi_glu_typ_pred;
-    saturate_glu_by_per;
-    invert_glu_univ_elem Hglu';
-    handle_functional_glu_univ_elem;
-    try solve [simpl in *; mauto 4].
-  - destruct_by_head pi_glu_typ_pred.
-    rename x into IP. rename x0 into IEl. rename x1 into OP. rename x2 into OEl.
-    rename M0 into M'. rename IT0 into IT'. rename OT0 into OT'.
-    rename x4 into OP'. rename x5 into OEl'.
-    assert {{ Γ ⊢ IT ® IP }}.
-    {
-      assert {{ Γ ⊢ IT[Id] ® IP }} by mauto.
-      simpl in *.
-      autorewrite with mcltt in *; mauto.
-    }
-    assert {{ Γ ⊢ IT' ® IP }}.
-    {
-      assert {{ Γ ⊢ IT'[Id] ® IP }} by mauto.
-      simpl in *.
-      autorewrite with mcltt in *; mauto.
-    }
-    do 2 bulky_rewrite1.
-    assert {{ Γ ⊢ IT ≈ IT' : Type@i }} by mauto.
-    enough {{ Γ, IT ⊢ OT ≈ OT' : Type@i }} by mauto 3.
-    assert {{ Dom ⇑! A (length Γ) ≈ ⇑! A' (length Γ) ∈ in_rel }} as equiv_len_len' by (eapply per_bot_then_per_elem; mauto).
-    assert {{ Dom ⇑! A (length Γ) ≈ ⇑! A (length Γ) ∈ in_rel }} as equiv_len_len by (eapply per_bot_then_per_elem; mauto).
-    assert {{ Dom ⇑! A' (length Γ) ≈ ⇑! A' (length Γ) ∈ in_rel }} as equiv_len'_len' by (eapply per_bot_then_per_elem; mauto).
-    destruct_rel_mod_eval.
-    handle_per_univ_elem_irrel.
-    rename a0 into b.
-    rename a' into b'.
-    assert {{ DG b ∈ glu_univ_elem i ↘ OP d{{{ ⇑! A (length Γ) }}} equiv_len_len ↘ OEl d{{{ ⇑! A (length Γ) }}} equiv_len_len }} by mauto.
-    assert {{ DG b' ∈ glu_univ_elem i ↘ OP' d{{{ ⇑! A' (length Γ) }}} equiv_len'_len' ↘ OEl' d{{{ ⇑! A' (length Γ) }}} equiv_len'_len' }} by mauto.
-    assert {{ Γ, IT ⊢ OT ® OP d{{{ ⇑! A (length Γ) }}} equiv_len_len }}.
-    {
-      assert {{ Γ, IT ⊢ #0 : IT[Wk] ® !(length Γ) ∈ glu_elem_bot i A }} by eauto using var_glu_elem_bot.
-      assert {{ Γ, IT ⊢ #0 : IT[Wk] ® ⇑! A (length Γ) ∈ IEl }} by (eapply realize_glu_elem_bot; mauto).
-      assert {{ Γ, IT ⊢ OT[Wk,,#0] ≈ OT : Type@i }} as <- by (bulky_rewrite1; mauto 3).
-      mauto.
-    }
-    assert {{ Γ, IT ⊢ OT' ® OP' d{{{ ⇑! A' (length Γ) }}} equiv_len'_len' }}.
-    {
-      assert {{ Γ, IT' ⊢ #0 : IT'[Wk] ® !(length Γ) ∈ glu_elem_bot i A' }} by eauto using var_glu_elem_bot.
-      assert {{ Γ, IT' ⊢ #0 : IT'[Wk] ® ⇑! A' (length Γ) ∈ IEl }} by (eapply realize_glu_elem_bot; mauto).
-      assert {{ Γ, IT' ⊢ OT'[Wk,,#0] ® OP' d{{{ ⇑! A' (length Γ) }}} equiv_len'_len' }} by mauto.
-      assert {{ ⊢ Γ, IT' ≈ Γ, IT }} as <- by mauto.
-      assert {{ Γ, IT' ⊢ OT'[Wk,,#0] ≈ OT' : Type@i }} as <- by (bulky_rewrite1; mauto 3).
-      mauto.
-    }
-    mauto 3.
-  - match_by_head (per_bot b b') ltac:(fun H => specialize (H (length Γ)) as [V []]).
-    simpl in *.
-    destruct_conjs.
-    assert {{ Γ ⊢ A[Id] ≈ A : Type@i }} as <- by mauto 4.
-    assert {{ Γ ⊢ A'[Id] ≈ A' : Type@i }} as <- by mauto 4.
-    assert {{ Γ ⊢ A'[Id] ≈ V : Type@i }} as -> by mauto 4.
-    mauto 4.
+  assert {{ DG a ∈ glu_univ_elem i ↘ P' ↘ El' }} by (setoid_rewrite Hper; eassumption).
+  handle_functional_glu_univ_elem...
 Qed.
 
+#[export]
+Hint Resolve glu_univ_elem_per_univ_elem_typ_escape : mcltt.
+
 Lemma glu_univ_elem_per_univ_typ_escape : forall {i a a' P P' El El' Γ A A'},
     {{ Dom a ≈ a' ∈ per_univ i }} ->
     {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
@@ -89,8 +82,8 @@ Lemma glu_univ_elem_per_univ_typ_escape : forall {i a a' P P' El El' Γ A A'},
     {{ Γ ⊢ A' ® P' }} ->
     {{ Γ ⊢ A ≈ A' : Type@i }}.
 Proof.
-  intros * [] **.
-  mauto using glu_univ_elem_per_univ_elem_typ_escape.
+  intros * [] **...
+  mauto 4.
 Qed.
 
 Lemma glu_univ_elem_per_univ_typ_iff : forall {i a a' P P' El El'},
diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
index 8e4b83b2..549824a3 100644
--- a/theories/Core/Soundness/LogicalRelation/Lemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -524,6 +524,8 @@ Ltac apply_functional_glu_univ_elem :=
 
 Ltac handle_functional_glu_univ_elem :=
   functional_eval_rewrite_clear;
+  fold glu_typ_pred in *;
+  fold glu_exp_pred in *;
   apply_functional_glu_univ_elem;
   apply_predicate_equivalence;
   clear_dups.
diff --git a/theories/Core/Soundness/SubtypingLemmas.v b/theories/Core/Soundness/SubtypingLemmas.v
index e5165235..ffbed94b 100644
--- a/theories/Core/Soundness/SubtypingLemmas.v
+++ b/theories/Core/Soundness/SubtypingLemmas.v
@@ -54,7 +54,7 @@ Proof.
       autorewrite with mcltt in *; mauto.
     }
     do 2 bulky_rewrite1.
-    assert {{ Γ ⊢ IT ≈ IT' : Type@i }} by mauto 4 using glu_univ_elem_per_univ_typ_escape.
+    assert {{ Γ ⊢ IT ≈ IT' : Type@i }} by mauto 4.
     enough {{ Γ, IT' ⊢ OT ⊆ OT' }} by mauto 3.
     assert {{ Dom ⇑! a (length Γ) ≈ ⇑! a' (length Γ) ∈ in_rel }} as equiv_len_len' by (eapply per_bot_then_per_elem; mauto).
     assert {{ Dom ⇑! a (length Γ) ≈ ⇑! a (length Γ) ∈ in_rel }} as equiv_len_len by (eapply per_bot_then_per_elem; mauto).
@@ -87,6 +87,9 @@ Proof.
     mauto 3.
 Qed.
 
+#[export]
+Hint Resolve glu_univ_elem_per_subtyp_typ_escape : mcltt.
+
 Lemma glu_univ_elem_per_subtyp_trm_if : forall {i a a' P P' El El' Γ A A' M m},
     {{ Sub a <: a' at i }} ->
     {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
@@ -165,10 +168,10 @@ Proof.
       handle_per_univ_elem_irrel.
       rename a1 into b.
       rename a2 into b'.
-      eapply H1 with (M := {{{ M[σ] m' }}}) (m := H30); mauto 3.
-      assert {{ Δ ⊢ OT[σ,,m'] ® OP c equiv_c }} by (eapply glu_univ_elem_trm_typ; mauto).
       assert {{ DG b ∈ glu_univ_elem i ↘ OP c equiv_c ↘ OEl c equiv_c }} by mauto.
       assert {{ DG b' ∈ glu_univ_elem i ↘ OP' c equiv_c ↘ OEl' c equiv_c }} by mauto.
-      enough {{ Sub b <: b' at i }} by mauto 3 using glu_univ_elem_per_subtyp_typ_escape.
-      mauto.
+      assert {{ Δ ⊢ OT[σ,,m'] ® OP c equiv_c }} by (eapply glu_univ_elem_trm_typ; mauto).
+      assert {{ Sub b <: b' at i }} by mauto 3.
+      assert {{ Δ ⊢ OT[σ,,m'] ⊆ OT'[σ,,m'] }} by mauto 3.
+      eapply H1; mauto 2.
 Qed.