diff --git a/theories/Core/Soundness/Cumulativity.v b/theories/Core/Soundness/Cumulativity.v
deleted file mode 100644
index 2158151a..00000000
--- a/theories/Core/Soundness/Cumulativity.v
+++ /dev/null
@@ -1,173 +0,0 @@
-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 EquivalenceLemmas 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.
-  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'},
-      i <= j ->
-      {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
-      {{ DG a ∈ glu_univ_elem j ↘ P' ↘ El' }} ->
-      (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 with mautosolve 4.
-    simpl.
-    intros * Hge Hglu Hglu'. gen El' P' j.
-    induction Hglu using glu_univ_elem_ind; repeat split; intros;
-      try assert {{ DF a ≈ a ∈ per_univ_elem j ↘ in_rel }} by mauto;
-      invert_glu_univ_elem Hglu';
-      handle_functional_glu_univ_elem;
-      simpl in *;
-      try solve [repeat split; intros; destruct_conjs; mauto 3 | intuition; mauto 4].
-
-    - rename x into IP'.
-      rename x0 into IEl'.
-      rename x1 into OP'.
-      rename x2 into OEl'.
-      destruct_by_head pi_glu_typ_pred.
-      econstructor; intros; mauto 4.
-      + assert {{ Δ ⊢ IT[σ] ® IP }} by 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).
-        apply_relation_equivalence.
-        destruct_rel_mod_eval.
-        handle_per_univ_elem_irrel.
-        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...
-    - rename x into IP'.
-      rename x0 into IEl'.
-      rename x1 into OP'.
-      rename x2 into OEl'.
-      destruct_by_head pi_glu_exp_pred.
-      handle_per_univ_elem_irrel.
-      econstructor; intros; mauto 4.
-      + 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).
-        handle_per_univ_elem_irrel.
-        destruct_rel_mod_eval.
-        destruct_rel_mod_app.
-        handle_per_univ_elem_irrel.
-        eexists; split; mauto.
-        assert (forall Γ A M m, {{ Γ ⊢ M : A ® m ∈ OEl c equiv_c }} -> {{ Γ ⊢ M : A ® m ∈ OEl' c equiv_c }}) by (eapply proj1, proj2; mauto).
-        enough {{ Δ ⊢ m[σ] m' : OT[σ,,m'] ® fa ∈ OEl c equiv_c }} by mauto.
-        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...
-    - rename x into IP'.
-      rename x0 into IEl'.
-      rename x1 into OP'.
-      rename x2 into OEl'.
-      destruct_by_head pi_glu_typ_pred.
-      destruct_by_head pi_glu_exp_pred.
-      handle_per_univ_elem_irrel.
-      econstructor; intros; mauto.
-      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).
-      handle_per_univ_elem_irrel.
-      destruct_rel_mod_eval.
-      destruct_rel_mod_app.
-      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).
-      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 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.
-      assert {{ Δ ⊢ OT0[σ,,m'] ® OP' c equiv_c }} by (eapply glu_univ_elem_trm_typ; mauto).
-      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...
-    - destruct_by_head neut_glu_exp_pred.
-      econstructor...
-  Qed.
-End glu_univ_elem_cumulativity.
-
-Corollary glu_univ_elem_typ_cumu_ge :  forall {i j a P P' El El' Γ A},
-    i <= j ->
-    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
-    {{ DG a ∈ glu_univ_elem j ↘ P' ↘ El' }} ->
-    {{ Γ ⊢ A ® P }} ->
-    {{ Γ ⊢ A ® P' }}.
-Proof.
-  intros.
-  eapply glu_univ_elem_cumulativity_ge; mauto.
-Qed.
-
-Corollary glu_univ_elem_exp_cumu_ge :  forall {i j a P P' El El' Γ A M m},
-    i <= j ->
-    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
-    {{ DG a ∈ glu_univ_elem j ↘ P' ↘ El' }} ->
-    {{ Γ ⊢ M : A ® m ∈ El }} ->
-    {{ Γ ⊢ M : A ® m ∈ El' }}.
-Proof.
-  intros * ? ? ?. gen m M A Γ.
-  eapply glu_univ_elem_cumulativity_ge; mauto.
-Qed.
-
-Corollary glu_univ_elem_exp_lower :  forall {i j a P P' El El' Γ A M m},
-    i <= j ->
-    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
-    {{ DG a ∈ glu_univ_elem j ↘ P' ↘ El' }} ->
-    {{ Γ ⊢ A ® P }} ->
-    {{ Γ ⊢ M : A ® m ∈ El' }} ->
-    {{ Γ ⊢ M : A ® m ∈ El }}.
-Proof.
-  intros * ? ? ?. gen m M A Γ.
-  eapply glu_univ_elem_cumulativity_ge; mauto.
-Qed.
diff --git a/theories/Core/Soundness/EquivalenceLemmas.v b/theories/Core/Soundness/EquivalenceLemmas.v
deleted file mode 100644
index 861c7d61..00000000
--- a/theories/Core/Soundness/EquivalenceLemmas.v
+++ /dev/null
@@ -1,99 +0,0 @@
-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.
-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 }} ->
-    {{ DG a' ∈ glu_univ_elem i ↘ P' ↘ El' }} ->
-    {{ Γ ⊢ A ® P }} ->
-    {{ Γ ⊢ A' ® P' }} ->
-    {{ Γ ⊢ A ≈ A' : Type@i }}.
-Proof with mautosolve 4.
-  simpl in *.
-  intros * Hper Hglu Hglu' HA HA'.
-  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 }} ->
-    {{ DG a' ∈ glu_univ_elem i ↘ P' ↘ El' }} ->
-    {{ Γ ⊢ A ® P }} ->
-    {{ Γ ⊢ A' ® P' }} ->
-    {{ Γ ⊢ A ≈ A' : Type@i }}.
-Proof.
-  intros * [] **...
-  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/LogicalRelation.v b/theories/Core/Soundness/LogicalRelation.v
index c583a933..ffffd117 100644
--- a/theories/Core/Soundness/LogicalRelation.v
+++ b/theories/Core/Soundness/LogicalRelation.v
@@ -1 +1 @@
-From Mcltt.Core.Soundness Require Export LogicalRelation.Definitions LogicalRelation.Lemmas.
+From Mcltt.Core.Soundness Require Export LogicalRelation.Core LogicalRelation.Lemmas.
diff --git a/theories/Core/Soundness/LogicalRelation/Core.v b/theories/Core/Soundness/LogicalRelation/Core.v
new file mode 100644
index 00000000..96b8b8b5
--- /dev/null
+++ b/theories/Core/Soundness/LogicalRelation/Core.v
@@ -0,0 +1 @@
+From Mcltt.Core.Soundness Require Export LogicalRelation.Definitions LogicalRelation.CoreLemmas.
diff --git a/theories/Core/Soundness/LogicalRelation/CoreLemmas.v b/theories/Core/Soundness/LogicalRelation/CoreLemmas.v
new file mode 100644
index 00000000..336f4b80
--- /dev/null
+++ b/theories/Core/Soundness/LogicalRelation/CoreLemmas.v
@@ -0,0 +1,861 @@
+From Coq Require Import Equivalence Morphisms Morphisms_Prop Morphisms_Relations Relation_Definitions RelationClasses.
+
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core Require Import PER Syntactic.Corollaries.
+From Mcltt.Core.Soundness Require Import LogicalRelation.Definitions LogicalRelation.CoreTactics.
+From Mcltt.Core.Soundness Require Export Weakening.Lemmas.
+Import Domain_Notations.
+
+Lemma glu_nat_per_nat : forall Γ m a,
+    glu_nat Γ m a ->
+    {{ Dom a ≈ a ∈ per_nat }}.
+Proof.
+  induction 1; mauto.
+Qed.
+
+#[local]
+Hint Resolve glu_nat_per_nat : mcltt.
+
+Lemma glu_nat_escape : forall Γ m a,
+    glu_nat Γ m a ->
+    {{ ⊢ Γ }} ->
+    {{ Γ ⊢ m : ℕ }}.
+Proof.
+  induction 1; intros;
+    try match goal with
+    | H : _ |- _ => solve [gen_presup H; mauto]
+    end.
+  assert {{ Γ ⊢w Id : Γ }} by mauto.
+  match_by_head (per_bot c c) ltac:(fun H => specialize (H (length Γ)) as [L []]).
+  clear_dups.
+  assert {{ Γ ⊢ m[Id] ≈ L : ℕ }} by mauto.
+  gen_presups.
+  mauto.
+Qed.
+
+#[export]
+Hint Resolve glu_nat_escape : mcltt.
+
+Lemma glu_nat_resp_exp_eq : forall Γ m a,
+    glu_nat Γ m a ->
+    forall m',
+    {{ Γ ⊢ m ≈ m' : ℕ }} ->
+    glu_nat Γ m' a.
+Proof.
+  induction 1; intros; mauto.
+  econstructor; trivial.
+  intros.
+  transitivity {{{ m[σ] }}}; mauto.
+Qed.
+
+#[local]
+Hint Resolve glu_nat_resp_exp_eq : mcltt.
+
+Lemma glu_nat_resp_ctx_eq : forall Γ m a Δ,
+    glu_nat Γ m a ->
+    {{ ⊢ Γ ≈ Δ }} ->
+    glu_nat Δ m a.
+Proof.
+  induction 1; intros; mauto.
+Qed.
+
+#[local]
+Hint Resolve glu_nat_resp_ctx_eq : mcltt.
+
+Lemma glu_nat_readback : forall Γ m a,
+    glu_nat Γ m a ->
+    forall Δ σ b,
+      {{ Δ ⊢w σ : Γ }} ->
+      {{ Rnf ⇓ ℕ a in length Δ ↘ b }} ->
+      {{ Δ ⊢ m [ σ ] ≈ b : ℕ }}.
+Proof.
+  induction 1; intros; progressive_inversion; gen_presups.
+  - transitivity {{{ zero[σ] }}}; mauto.
+  - assert {{ Δ ⊢ m'[σ] ≈ M : ℕ }} by mauto.
+    transitivity {{{ (succ m')[σ] }}}; mauto 3.
+    transitivity {{{ succ m'[σ] }}}; mauto 4.
+  - mauto.
+Qed.
+
+#[global]
+Ltac simpl_glu_rel :=
+  apply_equiv_left;
+  repeat invert_glu_rel1;
+  apply_equiv_left;
+  destruct_all;
+  gen_presups.
+
+Lemma glu_univ_elem_univ_lvl : forall i P El A,
+    {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    forall Γ T,
+      {{ Γ ⊢ T ® P }} ->
+      {{ Γ ⊢ T : Type@i }}.
+Proof.
+  simpl.
+  induction 1 using glu_univ_elem_ind; intros;
+    simpl_glu_rel; trivial.
+Qed.
+
+Lemma glu_univ_elem_typ_resp_exp_eq : forall i P El A,
+    {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    forall Γ T T',
+      {{ Γ ⊢ T ® P }} ->
+      {{ Γ ⊢ T ≈ T' : Type@i }} ->
+      {{ Γ ⊢ T' ® P }}.
+Proof.
+  simpl.
+  induction 1 using glu_univ_elem_ind; intros;
+    simpl_glu_rel; mauto 4.
+
+  split; [trivial |].
+  intros.
+  assert {{ Δ ⊢ T[σ] ≈ V : Type@i }}; mauto.
+Qed.
+
+
+Add Parametric Morphism i P El A (H : glu_univ_elem i P El A) Γ : (P Γ)
+    with signature wf_exp_eq Γ {{{Type@i}}} ==> iff as glu_univ_elem_typ_morphism_iff1.
+Proof.
+  intros. split; intros;
+    eapply glu_univ_elem_typ_resp_exp_eq;
+    mauto 2.
+Qed.
+
+
+Lemma glu_univ_elem_trm_resp_typ_exp_eq : forall i P El A,
+    {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    forall Γ t T a T',
+      {{ Γ ⊢ t : T ® a ∈ El }} ->
+      {{ Γ ⊢ T ≈ T' : Type@i }} ->
+      {{ Γ ⊢ t : T' ® a ∈ El }}.
+Proof.
+  simpl.
+  induction 1 using glu_univ_elem_ind; intros;
+    simpl_glu_rel; repeat split; mauto.
+
+  intros.
+  assert {{ Δ ⊢ M[σ] ≈ V : Type@i }}; mauto.
+Qed.
+
+Add Parametric Morphism i P El A (H : glu_univ_elem i P El A) Γ : (El Γ)
+    with signature wf_exp_eq Γ {{{Type@i}}} ==> eq ==> eq ==> iff as glu_univ_elem_trm_morphism_iff1.
+Proof.
+  split; intros;
+    eapply glu_univ_elem_trm_resp_typ_exp_eq;
+    mauto 2.
+Qed.
+
+Lemma glu_univ_elem_typ_resp_ctx_eq : forall i P El A,
+    {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    forall Γ T Δ,
+      {{ Γ ⊢ T ® P }} ->
+      {{ ⊢ Γ ≈ Δ }} ->
+      {{ Δ ⊢ T ® P }}.
+Proof.
+  simpl.
+  induction 1 using glu_univ_elem_ind; intros;
+    simpl_glu_rel; mauto 2;
+    econstructor; mauto.
+Qed.
+
+Add Parametric Morphism i P El A (H : glu_univ_elem i P El A) : P
+    with signature wf_ctx_eq ==> eq ==> iff as glu_univ_elem_typ_morphism_iff2.
+Proof.
+  intros. split; intros;
+    eapply glu_univ_elem_typ_resp_ctx_eq;
+    mauto 2.
+Qed.
+
+Lemma glu_univ_elem_trm_resp_ctx_eq : forall i P El A,
+    {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    forall Γ T M m Δ,
+      {{ Γ ⊢ M : T ® m ∈ El }} ->
+      {{ ⊢ Γ ≈ Δ }} ->
+      {{ Δ ⊢ M : T ® m ∈ El }}.
+Proof.
+  simpl.
+  induction 1 using glu_univ_elem_ind; intros;
+    simpl_glu_rel; mauto 2;
+    econstructor; mauto using glu_nat_resp_ctx_eq.
+
+  - split; mauto.
+    do 2 eexists.
+    split; mauto.
+    eapply glu_univ_elem_typ_resp_ctx_eq; mauto.
+  - split; mauto.
+Qed.
+
+Add Parametric Morphism i P El A (H : glu_univ_elem i P El A) : El
+    with signature wf_ctx_eq ==> eq ==> eq ==> eq ==> iff as glu_univ_elem_trm_morphism_iff2.
+Proof.
+  intros. split; intros;
+    eapply glu_univ_elem_trm_resp_ctx_eq;
+    mauto 2.
+Qed.
+
+Lemma glu_nat_resp_wk' : forall Γ m a,
+    glu_nat Γ m a ->
+    forall Δ σ,
+      {{ Γ ⊢ m : ℕ }} ->
+      {{ Δ ⊢w σ : Γ }} ->
+      glu_nat Δ {{{ m[σ] }}} a.
+Proof.
+  induction 1; intros; gen_presups.
+  - econstructor.
+    transitivity {{{ zero[σ] }}}; mauto.
+  - econstructor; [ |mauto].
+    transitivity {{{ (succ m')[σ] }}}; mauto 4.
+  - econstructor; trivial.
+    intros. gen_presups.
+    assert {{ Δ0 ⊢w σ ∘ σ0 : Γ }} by mauto.
+    assert {{ Δ0 ⊢ m[σ ∘ σ0] ≈ v : ℕ }} by mauto 4.
+    transitivity {{{ m[σ ∘ σ0] }}}; mauto 4.
+Qed.
+
+Lemma glu_nat_resp_wk : forall Γ m a,
+    glu_nat Γ m a ->
+    forall Δ σ,
+      {{ Δ ⊢w σ : Γ }} ->
+      glu_nat Δ {{{ m[σ] }}} a.
+Proof.
+  mauto using glu_nat_resp_wk'.
+Qed.
+
+#[export]
+Hint Resolve glu_nat_resp_wk : mcltt.
+
+Lemma glu_univ_elem_trm_escape : forall i P El A,
+    {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    forall Γ t T a,
+      {{ Γ ⊢ t : T ® a ∈ El }} ->
+      {{ Γ ⊢ t : T }}.
+Proof.
+  simpl.
+  induction 1 using glu_univ_elem_ind; intros;
+    simpl_glu_rel; mauto 4.
+Qed.
+
+Lemma glu_univ_elem_per_univ : forall i P El A,
+    {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    {{ Dom A ≈ A ∈ per_univ i }}.
+Proof.
+  simpl.
+  induction 1 using glu_univ_elem_ind; intros; eexists;
+    try solve [per_univ_elem_econstructor; try reflexivity; trivial].
+
+  - subst. eapply per_univ_elem_core_univ'; trivial.
+    reflexivity.
+  - match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H).
+    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,
+      {{ Γ ⊢ t : T ® a ∈ El }} ->
+      {{ DF A ≈ A ∈ per_univ_elem i ↘ R }} ->
+      {{ Dom a ≈ a ∈ R }}.
+Proof.
+  simpl.
+  induction 1 using glu_univ_elem_ind; intros;
+    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.
+
+  intros.
+  destruct_rel_mod_app.
+  destruct_rel_mod_eval.
+  functional_eval_rewrite_clear.
+  do_per_univ_elem_irrel_assert.
+
+  econstructor; firstorder eauto.
+Qed.
+
+Lemma glu_univ_elem_trm_typ : forall i P El A,
+    {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    forall Γ t T a,
+      {{ Γ ⊢ t : T ® a ∈ El }} ->
+      {{ Γ ⊢ T ® P }}.
+Proof.
+  simpl.
+  induction 1 using glu_univ_elem_ind; intros;
+    simpl_glu_rel;
+    mauto 4.
+
+  econstructor; eauto.
+  match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H).
+  intros.
+  destruct_rel_mod_eval.
+  edestruct H12 as [? []]; eauto.
+Qed.
+
+Lemma glu_univ_elem_trm_univ_lvl : forall i P El A,
+    {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    forall Γ t T a,
+      {{ Γ ⊢ t : T ® a ∈ El }} ->
+      {{ Γ ⊢ T : Type@i }}.
+Proof.
+  intros. eapply glu_univ_elem_univ_lvl; [| eapply glu_univ_elem_trm_typ]; eassumption.
+Qed.
+
+Lemma glu_univ_elem_trm_resp_exp_eq : forall i P El A,
+    {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    forall Γ t T a t',
+      {{ Γ ⊢ t : T ® a ∈ El }} ->
+      {{ Γ ⊢ t ≈ t' : T }} ->
+      {{ Γ ⊢ t' : T ® a ∈ El }}.
+Proof.
+  simpl.
+  induction 1 using glu_univ_elem_ind; intros;
+    simpl_glu_rel;
+    repeat split; mauto 3.
+
+  - repeat eexists; try split; eauto.
+    eapply glu_univ_elem_typ_resp_exp_eq; mauto.
+
+  - econstructor; eauto.
+    invert_per_univ_elem H3.
+    intros.
+    destruct_rel_mod_eval.
+    assert {{ Δ ⊢ m' : IT [σ]}} by eauto using glu_univ_elem_trm_escape.
+    edestruct H13 as [? []]; eauto.
+    eexists; split; eauto.
+    enough {{ Δ ⊢ m[σ] m' ≈ t'[σ] m' : OT[σ,,m'] }} by eauto.
+    assert {{ Γ ⊢ m ≈ t' : Π IT OT }} as Hty by mauto.
+    eassert {{ Δ ⊢ IT[σ] : Type@_ }} by mauto 3.
+    eapply wf_exp_eq_sub_cong with (Γ := Δ) in Hty; [| eapply sub_eq_refl; mauto 3].
+    autorewrite with mcltt in Hty.
+    eapply wf_exp_eq_app_cong with (N := m') (N' := m') in Hty; try pi_univ_level_tac; [|mauto 2].
+    autorewrite with mcltt in Hty.
+    eassumption.
+  - intros.
+    assert {{ Δ ⊢ m[σ] ≈ t'[σ] : M[σ] }} by mauto 4.
+    mauto 4.
+Qed.
+
+Add Parametric Morphism i P El A (H : glu_univ_elem i P El A) Γ T : (El Γ T)
+    with signature wf_exp_eq Γ T ==> eq ==> iff as glu_univ_elem_trm_morphism_iff3.
+Proof.
+  split; intros;
+    eapply glu_univ_elem_trm_resp_exp_eq;
+    mauto 2.
+Qed.
+
+Lemma glu_univ_elem_core_univ' : forall j i typ_rel el_rel,
+    j < i ->
+    (typ_rel <∙> univ_glu_typ_pred j i) ->
+    (el_rel <∙> univ_glu_exp_pred j i) ->
+    {{ DG 𝕌@j ∈ glu_univ_elem i ↘ typ_rel ↘ el_rel }}.
+Proof.
+  intros.
+  unshelve basic_glu_univ_elem_econstructor; mautosolve.
+Qed.
+
+#[export]
+Hint Resolve glu_univ_elem_core_univ' : mcltt.
+
+Ltac glu_univ_elem_econstructor :=
+  eapply glu_univ_elem_core_univ' + basic_glu_univ_elem_econstructor.
+
+Ltac rewrite_predicate_equivalence_left :=
+  repeat match goal with
+    | H : ?R1 <∙> ?R2 |- _ =>
+        try setoid_rewrite H;
+        (on_all_hyp: fun H' => assert_fails (unify H H'); unmark H; setoid_rewrite H in H');
+        let T := type of H in
+        fold (id T) in H
+    end; unfold id in *.
+
+Ltac rewrite_predicate_equivalence_right :=
+  repeat match goal with
+    | H : ?R1 <∙> ?R2 |- _ =>
+        try setoid_rewrite <- H;
+        (on_all_hyp: fun H' => assert_fails (unify H H'); unmark H; setoid_rewrite <- H in H');
+        let T := type of H in
+        fold (id T) in H
+    end; unfold id in *.
+
+Ltac clear_predicate_equivalence :=
+  repeat match goal with
+    | H : ?R1 <∙> ?R2 |- _ =>
+        (unify R1 R2; clear H) + (is_var R1; clear R1 H) + (is_var R2; clear R2 H)
+    end.
+
+Ltac apply_predicate_equivalence :=
+  clear_predicate_equivalence;
+  rewrite_predicate_equivalence_right;
+  clear_predicate_equivalence;
+  rewrite_predicate_equivalence_left;
+  clear_predicate_equivalence.
+
+(* Simple Morphism instance for "glu_univ_elem" *)
+Add Parametric Morphism i : (glu_univ_elem i)
+    with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> eq ==> iff as simple_glu_univ_elem_morphism_iff.
+Proof with mautosolve.
+  intros P P' HPP' El El' HElEl' a.
+  split; intro Horig; [gen El' P' | gen El P];
+    induction Horig using glu_univ_elem_ind; unshelve glu_univ_elem_econstructor;
+    try (etransitivity; [symmetry + idtac|]; eassumption); eauto.
+Qed.
+
+(* Morphism instances for "neut_glu_*_pred"s *)
+Add Parametric Morphism i : (neut_glu_typ_pred i)
+    with signature per_bot ==> eq ==> eq ==> iff as neut_glu_typ_pred_morphism_iff.
+Proof with mautosolve.
+  split; intros []; econstructor; intuition;
+    match_by_head per_bot ltac:(fun H => specialize (H (length Δ)) as [? []]);
+    functional_read_rewrite_clear; intuition.
+Qed.
+
+Add Parametric Morphism i : (neut_glu_typ_pred i)
+    with signature per_bot ==> glu_typ_pred_equivalence as neut_glu_typ_pred_morphism_glu_typ_pred_equivalence.
+Proof with mautosolve.
+  split; apply neut_glu_typ_pred_morphism_iff; mauto.
+Qed.
+
+Add Parametric Morphism i : (neut_glu_exp_pred i)
+    with signature per_bot ==> eq ==> eq ==> eq ==> eq ==> iff as neut_glu_exp_pred_morphism_iff.
+Proof with mautosolve.
+  split; intros []; econstructor; intuition;
+    match_by_head per_bot ltac:(fun H => specialize (H (length Δ)) as [? []]);
+    functional_read_rewrite_clear; intuition;
+    match_by_head per_bot ltac:(fun H => rewrite H in *); eassumption.
+Qed.
+
+Add Parametric Morphism i : (neut_glu_exp_pred i)
+    with signature per_bot ==> glu_exp_pred_equivalence as neut_glu_exp_pred_morphism_glu_exp_pred_equivalence.
+Proof with mautosolve.
+  split; apply neut_glu_exp_pred_morphism_iff; mauto.
+Qed.
+
+(* Morphism instances for "pi_glu_*_pred"s *)
+Add Parametric Morphism i IR : (pi_glu_typ_pred i IR)
+    with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> eq ==> eq ==> eq ==> iff as pi_glu_typ_pred_morphism_iff.
+Proof with mautosolve.
+  split; intros []; econstructor; intuition.
+Qed.
+
+Add Parametric Morphism i IR : (pi_glu_typ_pred i IR)
+    with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> eq ==> glu_typ_pred_equivalence as pi_glu_typ_pred_morphism_glu_typ_pred_equivalence.
+Proof with mautosolve.
+  split; intros []; econstructor; intuition.
+Qed.
+
+Add Parametric Morphism i IR : (pi_glu_exp_pred i IR)
+    with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> relation_equivalence ==> eq ==> eq ==> eq ==> eq ==> eq ==> iff as pi_glu_exp_pred_morphism_iff.
+Proof with mautosolve.
+  split; intros []; econstructor; intuition.
+Qed.
+
+Add Parametric Morphism i IR : (pi_glu_exp_pred i IR)
+    with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> relation_equivalence ==> eq ==> glu_exp_pred_equivalence as pi_glu_exp_pred_morphism_glu_exp_pred_equivalence.
+Proof with mautosolve.
+  split; intros []; econstructor; intuition.
+Qed.
+
+Lemma functional_glu_univ_elem : forall i a P P' El El',
+    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    {{ DG a ∈ glu_univ_elem i ↘ P' ↘ El' }} ->
+    (P <∙> P') /\ (El <∙> El').
+Proof.
+  simpl.
+  intros * Ha Ha'. gen P' El'.
+  induction Ha using glu_univ_elem_ind; intros; basic_invert_glu_univ_elem Ha';
+    apply_predicate_equivalence; try solve [split; reflexivity].
+  assert ((IP <∙> IP0) /\ (IEl <∙> IEl0)) as [] by mauto.
+  apply_predicate_equivalence.
+  handle_per_univ_elem_irrel.
+  (on_all_hyp: fun H => directed invert_per_univ_elem H).
+  handle_per_univ_elem_irrel.
+  split; [intros Γ C | intros Γ M C m].
+  - split; intros []; econstructor; intuition;
+      rename a0 into c;
+      [rename equiv_a into equiv_c; assert (equiv_c' : in_rel c c) by intuition
+      | rename equiv_a into equiv_c'; assert (equiv_c : in_rel0 c c) by intuition];
+      destruct_rel_mod_eval;
+      rename a0 into b;
+      assert ((OP c equiv_c' <∙> OP0 c equiv_c) /\ (OEl c equiv_c' <∙> OEl0 c equiv_c)) as [] by mauto 3;
+      intuition.
+  - split; intros []; econstructor; intuition;
+      clear m;
+      rename b into m;
+      [rename equiv_b into equiv_m; assert (equiv_m' : in_rel m m) by intuition
+      | rename equiv_b into equiv_m'; assert (equiv_m : in_rel0 m m) by intuition];
+      destruct_rel_mod_eval;
+      [assert (exists am : domain, {{ $| a0 & m |↘ am }} /\ {{ Δ ⊢ m0[σ] m' : OT[σ,,m'] ® am ∈ OEl m equiv_m' }}) by intuition
+      | assert (exists am : domain, {{ $| a0 & m |↘ am }} /\ {{ Δ ⊢ m0[σ] m' : OT[σ,,m'] ® am ∈ OEl0 m equiv_m }}) by intuition];
+      destruct_conjs;
+      assert ((OP m equiv_m' <∙> OP0 m equiv_m) /\ (OEl m equiv_m' <∙> OEl0 m equiv_m)) as [] by mauto 3;
+      eexists; split; intuition.
+Qed.
+
+Ltac apply_functional_glu_univ_elem1 :=
+  let tactic_error o1 o2 := fail 2 "functional_glu_univ_elem biconditional between" o1 "and" o2 "cannot be solved" in
+  match goal with
+  | H1 : {{ DG ~?A ∈ glu_univ_elem ?i ↘ ?P1 ↘ ?El1 }},
+      H2 : {{ DG ~?A ∈ glu_univ_elem ?i' ↘ ?P2 ↘ ?El2 }} |- _ =>
+      assert_fails (unify P1 P2; unify El1 El2);
+      match goal with
+      | H : P1 <∙> P2, H0 : El1 <∙> El2 |- _ => fail 1
+      | H : P1 <∙> P2, H0 : El2 <∙> El1 |- _ => fail 1
+      | H : P2 <∙> P1, H0 : El1 <∙> El2 |- _ => fail 1
+      | H : P2 <∙> P1, H0 : El2 <∙> El1 |- _ => fail 1
+      | _ => assert ((P1 <∙> P2) /\ (El1 <∙> El2)) as [] by (eapply functional_glu_univ_elem; [apply H1 | apply H2]) || tactic_error P1 P2
+      end
+  end.
+
+Ltac apply_functional_glu_univ_elem :=
+  repeat apply_functional_glu_univ_elem1.
+
+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.
+
+Lemma glu_univ_elem_pi_clean_inversion1 : forall {i a p B in_rel typ_rel el_rel},
+  {{ DF a ≈ a ∈ per_univ_elem i ↘ in_rel }} ->
+  {{ DG Π a p B ∈ glu_univ_elem i ↘ typ_rel ↘ el_rel }} ->
+  exists IP IEl (OP : forall c (equiv_c_c : {{ Dom c ≈ c ∈ in_rel }}), glu_typ_pred)
+     (OEl : forall c (equiv_c_c : {{ Dom c ≈ c ∈ in_rel }}), glu_exp_pred) elem_rel,
+      {{ DG a ∈ glu_univ_elem i ↘ IP ↘ IEl }} /\
+        (forall c (equiv_c : {{ Dom c ≈ c ∈ in_rel }}) b,
+            {{ ⟦ B ⟧ p ↦ c ↘ b }} ->
+            {{ DG b ∈ glu_univ_elem i ↘ OP _ equiv_c ↘ OEl _ equiv_c }}) /\
+        {{ DF Π a p B ≈ Π a p B ∈ per_univ_elem i ↘ elem_rel }} /\
+        (typ_rel <∙> pi_glu_typ_pred i in_rel IP IEl OP) /\
+        (el_rel <∙> pi_glu_exp_pred i in_rel IP IEl elem_rel OEl).
+Proof.
+  intros *.
+  simpl.
+  intros Hinper Hglu.
+  basic_invert_glu_univ_elem Hglu.
+  handle_functional_glu_univ_elem.
+  handle_per_univ_elem_irrel.
+  do 5 eexists.
+  repeat split.
+  1,3: eassumption.
+  1: instantiate (1 := fun c equiv_c Γ A M m => forall (b : domain) Pb Elb,
+                          {{ ⟦ B ⟧ p ↦ c ↘ b }} ->
+                          {{ DG b ∈ glu_univ_elem i ↘ Pb ↘ Elb }} ->
+                          {{ Γ ⊢ M : A ® m ∈ Elb }}).
+  1: instantiate (1 := fun c equiv_c Γ A => forall (b : domain) Pb Elb,
+                          {{ ⟦ B ⟧ p ↦ c ↘ b }} ->
+                          {{ DG b ∈ glu_univ_elem i ↘ Pb ↘ Elb }} ->
+                          {{ Γ ⊢ A ® Pb }}).
+  2-5: intros []; econstructor; mauto.
+  all: intros.
+  - assert {{ Dom c ≈ c ∈ in_rel0 }} as equiv0_c by intuition.
+    assert {{ DG b ∈ glu_univ_elem i ↘ OP c equiv0_c ↘ OEl c equiv0_c }} by mauto 3.
+    apply -> simple_glu_univ_elem_morphism_iff; [| reflexivity | |]; [eauto | |].
+    + intros ? ? ? ?.
+      split; intros; handle_functional_glu_univ_elem; intuition.
+    + intros ? ?.
+      split; [intros; handle_functional_glu_univ_elem |]; intuition.
+  - rename a0 into c.
+    rename equiv_a into equiv_c.
+    assert {{ Dom c ≈ c ∈ in_rel0 }} as equiv0_c by intuition.
+    assert {{ DG b ∈ glu_univ_elem i ↘ OP c equiv0_c ↘ OEl c equiv0_c }} by mauto 3.
+    handle_functional_glu_univ_elem.
+    intuition.
+  - match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H).
+    destruct_rel_mod_eval.
+    intuition.
+  - rename b into c.
+    rename equiv_b into equiv_c.
+    assert {{ Dom c ≈ c ∈ in_rel0 }} as equiv0_c by intuition.
+    assert (exists ac : domain, {{ $| a0 & c |↘ ac }} /\ {{ Δ ⊢ m[σ] m' : OT[σ,,m'] ® ac ∈ OEl c equiv0_c }}) by mauto 3.
+    destruct_conjs.
+    eexists.
+    intuition.
+    assert {{ DG b ∈ glu_univ_elem i ↘ OP c equiv0_c ↘ OEl c equiv0_c }} by mauto 3.
+    handle_functional_glu_univ_elem.
+    intuition.
+  - assert (exists ab : domain,
+               {{ $| a0 & b |↘ ab }} /\
+                 (forall (b0 : domain) (Pb : glu_typ_pred) (Elb : glu_exp_pred),
+                     {{ ⟦ B ⟧ p ↦ b ↘ b0 }} ->
+                     {{ DG b0 ∈ glu_univ_elem i ↘ Pb ↘ Elb }} ->
+                     {{ Δ ⊢ m[σ] m' : OT[σ,,m'] ® ab ∈ Elb }})) by intuition.
+    destruct_conjs.
+    match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H).
+    handle_per_univ_elem_irrel.
+    destruct_rel_mod_eval.
+    destruct_rel_mod_app.
+    functional_eval_rewrite_clear.
+    eexists.
+    intuition.
+Qed.
+
+Lemma glu_univ_elem_pi_clean_inversion2 : forall {i a p B in_rel IP IEl typ_rel el_rel},
+  {{ DF a ≈ a ∈ per_univ_elem i ↘ in_rel }} ->
+  {{ DG a ∈ glu_univ_elem i ↘ IP ↘ IEl }} ->
+  {{ DG Π a p B ∈ glu_univ_elem i ↘ typ_rel ↘ el_rel }} ->
+  exists (OP : forall c (equiv_c_c : {{ Dom c ≈ c ∈ in_rel }}), glu_typ_pred)
+     (OEl : forall c (equiv_c_c : {{ Dom c ≈ c ∈ in_rel }}), glu_exp_pred) elem_rel,
+    (forall c (equiv_c : {{ Dom c ≈ c ∈ in_rel }}) b,
+        {{ ⟦ B ⟧ p ↦ c ↘ b }} ->
+        {{ DG b ∈ glu_univ_elem i ↘ OP _ equiv_c ↘ OEl _ equiv_c }}) /\
+      {{ DF Π a p B ≈ Π a p B ∈ per_univ_elem i ↘ elem_rel }} /\
+      (typ_rel <∙> pi_glu_typ_pred i in_rel IP IEl OP) /\
+      (el_rel <∙> pi_glu_exp_pred i in_rel IP IEl elem_rel OEl).
+Proof.
+  intros *.
+  simpl.
+  intros Hinper Hinglu Hglu.
+  unshelve eapply (glu_univ_elem_pi_clean_inversion1 _) in Hglu; shelve_unifiable; [eassumption |];
+    destruct Hglu as [? [? [? [? [? [? [? [? []]]]]]]]].
+  handle_functional_glu_univ_elem.
+  do 3 eexists.
+  repeat split; try eassumption;
+    intros []; econstructor; mauto.
+Qed.
+
+Ltac invert_glu_univ_elem H :=
+  (unshelve eapply (glu_univ_elem_pi_clean_inversion2 _ _) in H; shelve_unifiable; [eassumption | eassumption |];
+   destruct H as [? [? [? [? [? []]]]]])
+  + (unshelve eapply (glu_univ_elem_pi_clean_inversion1 _) in H; shelve_unifiable; [eassumption |];
+   destruct H as [? [? [? [? [? [? [? [? []]]]]]]]])
+  + basic_invert_glu_univ_elem H.
+
+Lemma glu_univ_elem_morphism_helper : forall i a a' P El,
+    {{ Dom a ≈ a' ∈ per_univ i }} ->
+    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    {{ DG a' ∈ glu_univ_elem i ↘ P ↘ El }}.
+Proof.
+  simpl.
+  intros * [elem_rel Hper] Horig.
+  pose proof Hper.
+  gen P El.
+  induction Hper using per_univ_elem_ind; intros; subst;
+    saturate_refl_for per_univ_elem;
+    invert_glu_univ_elem Horig; glu_univ_elem_econstructor; try eassumption; mauto;
+    handle_per_univ_elem_irrel;
+    handle_functional_glu_univ_elem.
+  - intros.
+    match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H).
+    destruct_rel_mod_eval.
+    handle_per_univ_elem_irrel.
+    intuition.
+  - reflexivity.
+  - apply neut_glu_typ_pred_morphism_glu_typ_pred_equivalence.
+    eassumption.
+  - apply neut_glu_exp_pred_morphism_glu_exp_pred_equivalence.
+    eassumption.
+Qed.
+
+(* Morphism instances for "glu_univ_elem" *)
+Add Parametric Morphism i : (glu_univ_elem i)
+    with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> per_univ i ==> iff as glu_univ_elem_morphism_iff.
+Proof with mautosolve.
+  intros P P' HPP' El El' HElEl' a a' Haa'.
+  rewrite HPP', HElEl'.
+  split; intros; eapply glu_univ_elem_morphism_helper; mauto.
+  symmetry; eassumption.
+Qed.
+
+Add Parametric Morphism i R : (glu_univ_elem i)
+    with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> per_univ_elem i R ==> iff as glu_univ_elem_morphism_iff'.
+Proof with mautosolve.
+  intros P P' HPP' El El' HElEl' a a' Haa'.
+  rewrite HPP', HElEl'.
+  split; intros; eapply glu_univ_elem_morphism_helper; mauto.
+  symmetry; mauto.
+Qed.
+
+Ltac saturate_glu_by_per1 :=
+  match goal with
+  | H : glu_univ_elem ?i ?P ?El ?a,
+      H1 : per_univ_elem ?i _ ?a ?a' |- _ =>
+      assert (glu_univ_elem i P El a') by (rewrite <- H1; eassumption);
+      fail_if_dup
+  | H : glu_univ_elem ?i ?P ?El ?a',
+      H1 : per_univ_elem ?i _ ?a ?a' |- _ =>
+      assert (glu_univ_elem i P El a) by (rewrite H1; eassumption);
+      fail_if_dup
+  end.
+
+Ltac saturate_glu_by_per :=
+  clear_dups;
+  repeat saturate_glu_by_per1.
+
+Lemma per_univ_glu_univ_elem : forall i a,
+    {{ Dom a ≈ a ∈ per_univ i }} ->
+    exists P El, {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }}.
+Proof.
+  simpl.
+  intros * [? Hper].
+  induction Hper using per_univ_elem_ind; intros;
+    try solve [do 2 eexists; unshelve (glu_univ_elem_econstructor; try reflexivity; subst; trivial)].
+
+  - destruct_conjs.
+    do 2 eexists.
+    glu_univ_elem_econstructor; try (eassumption + reflexivity).
+    + saturate_refl; eassumption.
+    + instantiate (1 := fun (c : domain) (equiv_c : in_rel c c) Γ A M m =>
+                          forall b P El,
+                            {{ ⟦ B' ⟧ p' ↦ c ↘ b }} ->
+                            glu_univ_elem i P El b ->
+                            {{ Γ ⊢ M : A ® m ∈ El }}).
+      instantiate (1 := fun (c : domain) (equiv_c : in_rel c c) Γ A =>
+                          forall b P El,
+                            {{ ⟦ B' ⟧ p' ↦ c ↘ b }} ->
+                            glu_univ_elem i P El b ->
+                            {{ Γ ⊢ A ® P }}).
+      intros.
+      (on_all_hyp: destruct_rel_by_assumption in_rel).
+      handle_per_univ_elem_irrel.
+      rewrite simple_glu_univ_elem_morphism_iff; try (eassumption + reflexivity);
+        split; intros; handle_functional_glu_univ_elem; intuition.
+    + enough {{ DF Π A p B ≈ Π A' p' B' ∈ per_univ_elem i ↘ elem_rel }} by (etransitivity; [symmetry |]; eassumption).
+      per_univ_elem_econstructor; mauto.
+      intros.
+      (on_all_hyp: destruct_rel_by_assumption in_rel).
+      econstructor; mauto.
+  - do 2 eexists.
+    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 _ _,
+      H1 : ?P _ _ |- _ =>
+      pose proof (glu_univ_elem_univ_lvl _ _ _ _ H _ _ H1);
+      fail_if_dup
+  | H : glu_univ_elem _ _ ?El _,
+      H1 : ?El _ _ _ _ |- _ =>
+      pose proof (glu_univ_elem_trm_escape _ _ _ _ H _ _ _ _ H1);
+      fail_if_dup
+  end.
+
+Ltac saturate_glu_info :=
+  clear_dups;
+  repeat saturate_glu_info1.
+
+#[local]
+Hint Rewrite -> sub_decompose_q using solve [mauto 4] : mcltt.
+
+Lemma glu_univ_elem_typ_monotone : forall i a P El,
+    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    forall Δ σ Γ A,
+      {{ Γ ⊢ A ® P }} ->
+      {{ Δ ⊢w σ : Γ }} ->
+      {{ Δ ⊢ A[σ] ® P }}.
+Proof.
+  simpl. induction 1 using glu_univ_elem_ind; intros;
+    saturate_weakening_escape;
+    handle_functional_glu_univ_elem;
+    simpl in *;
+    try solve [bulky_rewrite].
+  - simpl_glu_rel. econstructor; eauto; try solve [bulky_rewrite]; mauto 3.
+    intros.
+    saturate_weakening_escape.
+    saturate_glu_info.
+    invert_per_univ_elem H3.
+    destruct_rel_mod_eval.
+    simplify_evals.
+    deepexec H1 ltac:(fun H => pose proof H).
+    autorewrite with mcltt in *.
+    mauto 3.
+
+  - destruct_conjs.
+    split; [mauto 3 |].
+    intros.
+    saturate_weakening_escape.
+    autorewrite with mcltt.
+    mauto 3.
+Qed.
+
+
+Lemma glu_univ_elem_exp_monotone : forall i a P El,
+    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    forall Δ σ Γ M A m,
+      {{ Γ ⊢ M : A ® m ∈ El }} ->
+      {{ Δ ⊢w σ : Γ }} ->
+      {{ Δ ⊢ M[σ] : A[σ] ® m ∈ El }}.
+Proof.
+  simpl. induction 1 using glu_univ_elem_ind; intros;
+    saturate_weakening_escape;
+    handle_functional_glu_univ_elem;
+    simpl in *;
+    destruct_all.
+  - repeat eexists; mauto 2; bulky_rewrite.
+    eapply glu_univ_elem_typ_monotone; eauto.
+  - repeat eexists; mauto 2; bulky_rewrite.
+
+  - simpl_glu_rel.
+    econstructor; mauto 4;
+      intros;
+      saturate_weakening_escape.
+    + eapply glu_univ_elem_typ_monotone; eauto.
+    + saturate_glu_info.
+      invert_per_univ_elem H3.
+      apply_equiv_left.
+      destruct_rel_mod_eval.
+      destruct_rel_mod_app.
+      simplify_evals.
+      deepexec H1 ltac:(fun H => pose proof H).
+      autorewrite with mcltt in *.
+      repeat eexists; eauto.
+      assert {{ Δ0 ⊢s σ0,, m' : Δ, ~ (a_sub IT σ) }}. {
+        econstructor; mauto 2.
+        bulky_rewrite.
+      }
+      assert {{Δ0 ⊢ (m [σ][σ0]) m' ≈ (m [σ ∘ σ0]) m' : OT [σ ∘ σ0,, m']}}. {
+        rewrite <- sub_eq_q_sigma_id_extend; mauto 4.
+        rewrite <- exp_eq_sub_compose_typ; mauto 3;
+          [eapply wf_exp_eq_app_cong' |];
+          mauto 4.
+        symmetry.
+        bulky_rewrite_in H4.
+        eapply wf_exp_eq_conv; mauto 3.
+      }
+
+      bulky_rewrite.
+      edestruct H10 with (b := b) as [? []];
+        simplify_evals; [| | eassumption];
+      mauto.
+
+  - simpl_glu_rel.
+    econstructor; repeat split; mauto 3;
+      intros;
+      saturate_weakening_escape.
+    + autorewrite with mcltt.
+      mauto 3.
+    + autorewrite with mcltt.
+      etransitivity.
+      * symmetry.
+        eapply wf_exp_eq_sub_compose;
+          mauto 3.
+      * mauto 3.
+Qed.
+
+(* Simple Morphism instance for "glu_ctx_env" *)
+Add Parametric Morphism : glu_ctx_env
+    with signature glu_sub_pred_equivalence ==> eq ==> iff as simple_glu_ctx_env_morphism_iff.
+Proof with mautosolve.
+  intros Sb Sb' HSbSb' a.
+  split; intro Horig; [gen Sb' | gen Sb];
+    induction Horig; econstructor;
+    try (etransitivity; [symmetry + idtac|]; eassumption); eauto.
+Qed.
diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
index 549824a3..62aca209 100644
--- a/theories/Core/Soundness/LogicalRelation/Lemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -2,871 +2,585 @@ From Coq Require Import Equivalence Morphisms Morphisms_Prop Morphisms_Relations
 
 From Mcltt Require Import Base LibTactics.
 From Mcltt.Core Require Import PER Syntactic.Corollaries.
-From Mcltt.Core.Soundness Require Import LogicalRelation.Definitions LogicalRelation.CoreTactics.
-From Mcltt.Core.Soundness Require Export Weakening.Lemmas.
+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 Import LogicalRelation.Core.
+From Mcltt.Core.Syntactic Require Import Corollaries.
 Import Domain_Notations.
 
-Lemma pi_glu_exp_pred_pi_glu_typ_pred : forall i IR IP IEl (OP : forall c (equiv_c : {{ Dom c ≈ c ∈ IR }}), glu_typ_pred) elem_rel OEl Γ m M a,
-    {{ Γ ⊢ m : M ® a ∈ pi_glu_exp_pred i IR IP IEl elem_rel OEl }} ->
-    (forall Δ m' M' b c (equiv_c : {{ Dom c ≈ c ∈ IR }}),
-        {{ Δ ⊢ m' : M' ® b ∈ OEl _ equiv_c }} ->
-        {{ Δ ⊢ M' ® OP _ equiv_c }}) ->
-    {{ Γ ⊢ M ® pi_glu_typ_pred i IR IP IEl OP }}.
-Proof.
-  inversion_clear 1; econstructor; eauto.
+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.
-  edestruct H6 as [? []]; eauto.
-Qed.
-
-Lemma glu_nat_per_nat : forall Γ m a,
-    glu_nat Γ m a ->
-    {{ Dom a ≈ a ∈ per_nat }}.
-Proof.
-  induction 1; mauto.
-Qed.
-
-#[local]
-Hint Resolve glu_nat_per_nat : mcltt.
-
-Lemma glu_nat_escape : forall Γ m a,
-    glu_nat Γ m a ->
-    {{ ⊢ Γ }} ->
-    {{ Γ ⊢ m : ℕ }}.
-Proof.
-  induction 1; intros;
-    try match goal with
-    | H : _ |- _ => solve [gen_presup H; mauto]
-    end.
-  assert {{ Γ ⊢w Id : Γ }} by mauto.
-  match_by_head (per_bot c c) ltac:(fun H => specialize (H (length Γ)) as [L []]).
+  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.
-  assert {{ Γ ⊢ m[Id] ≈ L : ℕ }} by mauto.
-  gen_presups.
-  mauto.
+  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_nat_escape : mcltt.
+Hint Resolve glu_univ_elem_typ_escape : mcltt.
 
-Lemma glu_nat_resp_exp_eq : forall Γ m a,
-    glu_nat Γ m a ->
-    forall m',
-    {{ Γ ⊢ m ≈ m' : ℕ }} ->
-    glu_nat Γ m' a.
-Proof.
-  induction 1; intros; mauto.
-  econstructor; trivial.
+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.
-  transitivity {{{ m[σ] }}}; mauto.
+  replace j with (max i j) by lia...
 Qed.
 
-#[local]
-Hint Resolve glu_nat_resp_exp_eq : mcltt.
+#[export]
+Hint Resolve glu_univ_elem_typ_escape_ge : mcltt.
 
-Lemma glu_nat_resp_ctx_eq : forall Γ m a Δ,
-    glu_nat Γ m a ->
-    {{ ⊢ Γ ≈ Δ }} ->
-    glu_nat Δ m a.
-Proof.
-  induction 1; intros; mauto.
-Qed.
+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.
 
-#[local]
-Hint Resolve glu_nat_resp_ctx_eq : mcltt.
+#[export]
+Hint Resolve glu_univ_elem_typ_escape' : mcltt.
 
-Lemma glu_nat_readback : forall Γ m a,
-    glu_nat Γ m a ->
-    forall Δ σ b,
-      {{ Δ ⊢w σ : Γ }} ->
-      {{ Rnf ⇓ ℕ a in length Δ ↘ b }} ->
-      {{ Δ ⊢ m [ σ ] ≈ b : ℕ }}.
-Proof.
-  induction 1; intros; progressive_inversion; gen_presups.
-  - transitivity {{{ zero[σ] }}}; mauto.
-  - assert {{ Δ ⊢ m'[σ] ≈ M : ℕ }} by mauto.
-    transitivity {{{ (succ m')[σ] }}}; mauto 3.
-    transitivity {{{ succ m'[σ] }}}; mauto 4.
-  - mauto.
+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 with mautosolve 4.
+  simpl in *.
+  intros * Hper Hglu Hglu' HA HA'.
+  assert {{ DG a ∈ glu_univ_elem i ↘ P' ↘ El' }} by (setoid_rewrite Hper; eassumption).
+  handle_functional_glu_univ_elem...
 Qed.
 
-#[global]
-Ltac simpl_glu_rel :=
-  apply_equiv_left;
-  repeat invert_glu_rel1;
-  apply_equiv_left;
-  destruct_all;
-  gen_presups.
-
-Lemma glu_univ_elem_univ_lvl : forall i P El A,
-    {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} ->
-    forall Γ T,
-      {{ Γ ⊢ T ® P }} ->
-      {{ Γ ⊢ T : Type@i }}.
-Proof.
-  simpl.
-  induction 1 using glu_univ_elem_ind; intros;
-    simpl_glu_rel; trivial.
-Qed.
+#[export]
+Hint Resolve glu_univ_elem_per_univ_elem_typ_escape : mcltt.
 
-Lemma glu_univ_elem_typ_resp_exp_eq : forall i P El A,
-    {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} ->
-    forall Γ T T',
-      {{ Γ ⊢ T ® P }} ->
-      {{ Γ ⊢ T ≈ T' : Type@i }} ->
-      {{ Γ ⊢ T' ® P }}.
+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.
-  simpl.
-  induction 1 using glu_univ_elem_ind; intros;
-    simpl_glu_rel; mauto 4.
-
-  split; [trivial |].
-  intros.
-  assert {{ Δ ⊢ T[σ] ≈ V : Type@i }}; mauto.
+  intros * [] **...
+  mauto 4.
 Qed.
 
-
-Add Parametric Morphism i P El A (H : glu_univ_elem i P El A) Γ : (P Γ)
-    with signature wf_exp_eq Γ {{{Type@i}}} ==> iff as glu_univ_elem_typ_morphism_iff1.
+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. split; intros;
-    eapply glu_univ_elem_typ_resp_exp_eq;
-    mauto 2.
+  intros * Hper **.
+  eapply functional_glu_univ_elem;
+    [eassumption | rewrite Hper];
+    eassumption.
 Qed.
 
-
-Lemma glu_univ_elem_trm_resp_typ_exp_eq : forall i P El A,
-    {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} ->
-    forall Γ t T a T',
-      {{ Γ ⊢ t : T ® a ∈ El }} ->
-      {{ Γ ⊢ T ≈ T' : Type@i }} ->
-      {{ Γ ⊢ t : T' ® a ∈ El }}.
+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.
-  simpl.
-  induction 1 using glu_univ_elem_ind; intros;
-    simpl_glu_rel; repeat split; mauto.
-
   intros.
-  assert {{ Δ ⊢ M[σ] ≈ V : Type@i }}; mauto.
-Qed.
-
-Add Parametric Morphism i P El A (H : glu_univ_elem i P El A) Γ : (El Γ)
-    with signature wf_exp_eq Γ {{{Type@i}}} ==> eq ==> eq ==> iff as glu_univ_elem_trm_morphism_iff1.
-Proof.
-  split; intros;
-    eapply glu_univ_elem_trm_resp_typ_exp_eq;
-    mauto 2.
-Qed.
-
-Lemma glu_univ_elem_typ_resp_ctx_eq : forall i P El A,
-    {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} ->
-    forall Γ T Δ,
-      {{ Γ ⊢ T ® P }} ->
-      {{ ⊢ Γ ≈ Δ }} ->
-      {{ Δ ⊢ T ® P }}.
-Proof.
-  simpl.
-  induction 1 using glu_univ_elem_ind; intros;
-    simpl_glu_rel; mauto 2;
-    econstructor; mauto.
-Qed.
-
-Add Parametric Morphism i P El A (H : glu_univ_elem i P El A) : P
-    with signature wf_ctx_eq ==> eq ==> iff as glu_univ_elem_typ_morphism_iff2.
-Proof.
-  intros. split; intros;
-    eapply glu_univ_elem_typ_resp_ctx_eq;
-    mauto 2.
-Qed.
-
-Lemma glu_univ_elem_trm_resp_ctx_eq : forall i P El A,
-    {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} ->
-    forall Γ T M m Δ,
-      {{ Γ ⊢ M : T ® m ∈ El }} ->
-      {{ ⊢ Γ ≈ Δ }} ->
-      {{ Δ ⊢ M : T ® m ∈ El }}.
-Proof.
-  simpl.
-  induction 1 using glu_univ_elem_ind; intros;
-    simpl_glu_rel; mauto 2;
-    econstructor; mauto using glu_nat_resp_ctx_eq.
-
-  - split; mauto.
-    do 2 eexists.
-    split; mauto.
-    eapply glu_univ_elem_typ_resp_ctx_eq; mauto.
-  - split; mauto.
-Qed.
-
-Add Parametric Morphism i P El A (H : glu_univ_elem i P El A) : El
-    with signature wf_ctx_eq ==> eq ==> eq ==> eq ==> iff as glu_univ_elem_trm_morphism_iff2.
-Proof.
-  intros. split; intros;
-    eapply glu_univ_elem_trm_resp_ctx_eq;
-    mauto 2.
-Qed.
-
-Lemma glu_nat_resp_wk' : forall Γ m a,
-    glu_nat Γ m a ->
-    forall Δ σ,
-      {{ Γ ⊢ m : ℕ }} ->
-      {{ Δ ⊢w σ : Γ }} ->
-      glu_nat Δ {{{ m[σ] }}} a.
-Proof.
-  induction 1; intros; gen_presups.
-  - econstructor.
-    transitivity {{{ zero[σ] }}}; mauto.
-  - econstructor; [ |mauto].
-    transitivity {{{ (succ m')[σ] }}}; mauto 4.
-  - econstructor; trivial.
-    intros. gen_presups.
-    assert {{ Δ0 ⊢w σ ∘ σ0 : Γ }} by mauto.
-    assert {{ Δ0 ⊢ m[σ ∘ σ0] ≈ v : ℕ }} by mauto 4.
-    transitivity {{{ m[σ ∘ σ0] }}}; mauto 4.
+  assert {{ Dom a ≈ a ∈ per_univ i }} as [R] by mauto.
+  assert {{ DF a ≈ a ∈ per_univ_elem j ↘ R }} by mauto.
+  mauto.
 Qed.
 
-Lemma glu_nat_resp_wk : forall Γ m a,
-    glu_nat Γ m a ->
-    forall Δ σ,
-      {{ Δ ⊢w σ : Γ }} ->
-      glu_nat Δ {{{ m[σ] }}} a.
-Proof.
-  mauto using glu_nat_resp_wk'.
-Qed.
 #[export]
- Hint Resolve glu_nat_resp_wk : mcltt.
-
-Lemma glu_univ_elem_trm_escape : forall i P El A,
-    {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} ->
-    forall Γ t T a,
-      {{ Γ ⊢ t : T ® a ∈ El }} ->
-      {{ Γ ⊢ t : T }}.
-Proof.
-  simpl.
-  induction 1 using glu_univ_elem_ind; intros;
-    simpl_glu_rel; mauto 4.
-Qed.
-
-Lemma glu_univ_elem_per_univ : forall i P El A,
-    {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} ->
-    {{ Dom A ≈ A ∈ per_univ i }}.
-Proof.
-  simpl.
-  induction 1 using glu_univ_elem_ind; intros; eexists;
-    try solve [per_univ_elem_econstructor; try reflexivity; trivial].
+Hint Resolve glu_univ_elem_cumu_ge : mcltt.
 
-  - subst. eapply per_univ_elem_core_univ'; trivial.
-    reflexivity.
-  - match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H).
-    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,
-      {{ Γ ⊢ t : T ® a ∈ El }} ->
-      {{ DF A ≈ A ∈ per_univ_elem i ↘ R }} ->
-      {{ Dom a ≈ a ∈ R }}.
+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.
-  simpl.
-  induction 1 using glu_univ_elem_ind; intros;
-    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.
-
   intros.
-  destruct_rel_mod_app.
-  destruct_rel_mod_eval.
-  functional_eval_rewrite_clear.
-  do_per_univ_elem_irrel_assert.
-
-  econstructor; firstorder eauto.
+  assert (i <= max i j) by lia.
+  mauto.
 Qed.
 
-Lemma glu_univ_elem_trm_typ : forall i P El A,
-    {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} ->
-    forall Γ t T a,
-      {{ Γ ⊢ t : T ® a ∈ El }} ->
-      {{ Γ ⊢ T ® P }}.
+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.
-  simpl.
-  induction 1 using glu_univ_elem_ind; intros;
-    simpl_glu_rel;
-    mauto 4.
-
-  econstructor; eauto.
-  match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H).
   intros.
-  destruct_rel_mod_eval.
-  edestruct H12 as [? []]; eauto.
-Qed.
-
-Lemma glu_univ_elem_trm_univ_lvl : forall i P El A,
-    {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} ->
-    forall Γ t T a,
-      {{ Γ ⊢ t : T ® a ∈ El }} ->
-      {{ Γ ⊢ T : Type@i }}.
-Proof.
-  intros. eapply glu_univ_elem_univ_lvl; [| eapply glu_univ_elem_trm_typ]; eassumption.
-Qed.
-
-Lemma glu_univ_elem_trm_resp_exp_eq : forall i P El A,
-    {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} ->
-    forall Γ t T a t',
-      {{ Γ ⊢ t : T ® a ∈ El }} ->
-      {{ Γ ⊢ t ≈ t' : T }} ->
-      {{ Γ ⊢ t' : T ® a ∈ El }}.
-Proof.
-  simpl.
-  induction 1 using glu_univ_elem_ind; intros;
-    simpl_glu_rel;
-    repeat split; mauto 3.
-
-  - repeat eexists; try split; eauto.
-    eapply glu_univ_elem_typ_resp_exp_eq; mauto.
-
-  - econstructor; eauto.
-    invert_per_univ_elem H3.
-    intros.
-    destruct_rel_mod_eval.
-    assert {{ Δ ⊢ m' : IT [σ]}} by eauto using glu_univ_elem_trm_escape.
-    edestruct H13 as [? []]; eauto.
-    eexists; split; eauto.
-    enough {{ Δ ⊢ m[σ] m' ≈ t'[σ] m' : OT[σ,,m'] }} by eauto.
-    assert {{ Γ ⊢ m ≈ t' : Π IT OT }} as Hty by mauto.
-    eassert {{ Δ ⊢ IT[σ] : Type@_ }} by mauto 3.
-    eapply wf_exp_eq_sub_cong with (Γ := Δ) in Hty; [| eapply sub_eq_refl; mauto 3].
-    autorewrite with mcltt in Hty.
-    eapply wf_exp_eq_app_cong with (N := m') (N' := m') in Hty; try pi_univ_level_tac; [|mauto 2].
-    autorewrite with mcltt in Hty.
-    eassumption.
-  - intros.
-    assert {{ Δ ⊢ m[σ] ≈ t'[σ] : M[σ] }} by mauto 4.
-    mauto 4.
-Qed.
-
-Add Parametric Morphism i P El A (H : glu_univ_elem i P El A) Γ T : (El Γ T)
-    with signature wf_exp_eq Γ T ==> eq ==> iff as glu_univ_elem_trm_morphism_iff3.
-Proof.
-  split; intros;
-    eapply glu_univ_elem_trm_resp_exp_eq;
-    mauto 2.
+  assert (j <= max i j) by lia.
+  mauto.
 Qed.
 
-Lemma glu_univ_elem_core_univ' : forall j i typ_rel el_rel,
-    j < i ->
-    (typ_rel <∙> univ_glu_typ_pred j i) ->
-    (el_rel <∙> univ_glu_exp_pred j i) ->
-    {{ DG 𝕌@j ∈ glu_univ_elem i ↘ typ_rel ↘ el_rel }}.
+Section glu_univ_elem_cumulativity.
+  #[local]
+  Lemma glu_univ_elem_cumulativity_ge : forall {i j a P P' El El'},
+      i <= j ->
+      {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+      {{ DG a ∈ glu_univ_elem j ↘ P' ↘ El' }} ->
+      (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 with mautosolve 4.
+    simpl.
+    intros * Hge Hglu Hglu'. gen El' P' j.
+    induction Hglu using glu_univ_elem_ind; repeat split; intros;
+      try assert {{ DF a ≈ a ∈ per_univ_elem j ↘ in_rel }} by mauto;
+      invert_glu_univ_elem Hglu';
+      handle_functional_glu_univ_elem;
+      simpl in *;
+      try solve [repeat split; intros; destruct_conjs; mauto 3 | intuition; mauto 4].
+
+    - rename x into IP'.
+      rename x0 into IEl'.
+      rename x1 into OP'.
+      rename x2 into OEl'.
+      destruct_by_head pi_glu_typ_pred.
+      econstructor; intros; mauto 4.
+      + assert {{ Δ ⊢ IT[σ] ® IP }} by 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).
+        apply_relation_equivalence.
+        destruct_rel_mod_eval.
+        handle_per_univ_elem_irrel.
+        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...
+    - rename x into IP'.
+      rename x0 into IEl'.
+      rename x1 into OP'.
+      rename x2 into OEl'.
+      destruct_by_head pi_glu_exp_pred.
+      handle_per_univ_elem_irrel.
+      econstructor; intros; mauto 4.
+      + 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).
+        handle_per_univ_elem_irrel.
+        destruct_rel_mod_eval.
+        destruct_rel_mod_app.
+        handle_per_univ_elem_irrel.
+        eexists; split; mauto.
+        assert (forall Γ A M m, {{ Γ ⊢ M : A ® m ∈ OEl c equiv_c }} -> {{ Γ ⊢ M : A ® m ∈ OEl' c equiv_c }}) by (eapply proj1, proj2; mauto).
+        enough {{ Δ ⊢ m[σ] m' : OT[σ,,m'] ® fa ∈ OEl c equiv_c }} by mauto.
+        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...
+    - rename x into IP'.
+      rename x0 into IEl'.
+      rename x1 into OP'.
+      rename x2 into OEl'.
+      destruct_by_head pi_glu_typ_pred.
+      destruct_by_head pi_glu_exp_pred.
+      handle_per_univ_elem_irrel.
+      econstructor; intros; mauto.
+      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).
+      handle_per_univ_elem_irrel.
+      destruct_rel_mod_eval.
+      destruct_rel_mod_app.
+      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).
+      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 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.
+      assert {{ Δ ⊢ OT0[σ,,m'] ® OP' c equiv_c }} by (eapply glu_univ_elem_trm_typ; mauto).
+      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...
+    - destruct_by_head neut_glu_exp_pred.
+      econstructor...
+  Qed.
+End glu_univ_elem_cumulativity.
+
+Corollary glu_univ_elem_typ_cumu_ge :  forall {i j a P P' El El' Γ A},
+    i <= j ->
+    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    {{ DG a ∈ glu_univ_elem j ↘ P' ↘ El' }} ->
+    {{ Γ ⊢ A ® P }} ->
+    {{ Γ ⊢ A ® P' }}.
 Proof.
   intros.
-  unshelve basic_glu_univ_elem_econstructor; mautosolve.
-Qed.
-
-#[export]
-Hint Resolve glu_univ_elem_core_univ' : mcltt.
-
-Ltac glu_univ_elem_econstructor :=
-  eapply glu_univ_elem_core_univ' + basic_glu_univ_elem_econstructor.
-
-Ltac rewrite_predicate_equivalence_left :=
-  repeat match goal with
-    | H : ?R1 <∙> ?R2 |- _ =>
-        try setoid_rewrite H;
-        (on_all_hyp: fun H' => assert_fails (unify H H'); unmark H; setoid_rewrite H in H');
-        let T := type of H in
-        fold (id T) in H
-    end; unfold id in *.
-
-Ltac rewrite_predicate_equivalence_right :=
-  repeat match goal with
-    | H : ?R1 <∙> ?R2 |- _ =>
-        try setoid_rewrite <- H;
-        (on_all_hyp: fun H' => assert_fails (unify H H'); unmark H; setoid_rewrite <- H in H');
-        let T := type of H in
-        fold (id T) in H
-    end; unfold id in *.
-
-Ltac clear_predicate_equivalence :=
-  repeat match goal with
-    | H : ?R1 <∙> ?R2 |- _ =>
-        (unify R1 R2; clear H) + (is_var R1; clear R1 H) + (is_var R2; clear R2 H)
-    end.
-
-Ltac apply_predicate_equivalence :=
-  clear_predicate_equivalence;
-  rewrite_predicate_equivalence_right;
-  clear_predicate_equivalence;
-  rewrite_predicate_equivalence_left;
-  clear_predicate_equivalence.
-
-(* Simple Morphism instance for "glu_univ_elem" *)
-Add Parametric Morphism i : (glu_univ_elem i)
-    with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> eq ==> iff as simple_glu_univ_elem_morphism_iff.
-Proof with mautosolve.
-  intros P P' HPP' El El' HElEl' a.
-  split; intro Horig; [gen El' P' | gen El P];
-    induction Horig using glu_univ_elem_ind; unshelve glu_univ_elem_econstructor;
-    try (etransitivity; [symmetry + idtac|]; eassumption); eauto.
-Qed.
-
-(* Morphism instances for "neut_glu_*_pred"s *)
-Add Parametric Morphism i : (neut_glu_typ_pred i)
-    with signature per_bot ==> eq ==> eq ==> iff as neut_glu_typ_pred_morphism_iff.
-Proof with mautosolve.
-  split; intros []; econstructor; intuition;
-    match_by_head per_bot ltac:(fun H => specialize (H (length Δ)) as [? []]);
-    functional_read_rewrite_clear; intuition.
-Qed.
-
-Add Parametric Morphism i : (neut_glu_typ_pred i)
-    with signature per_bot ==> glu_typ_pred_equivalence as neut_glu_typ_pred_morphism_glu_typ_pred_equivalence.
-Proof with mautosolve.
-  split; apply neut_glu_typ_pred_morphism_iff; mauto.
-Qed.
-
-Add Parametric Morphism i : (neut_glu_exp_pred i)
-    with signature per_bot ==> eq ==> eq ==> eq ==> eq ==> iff as neut_glu_exp_pred_morphism_iff.
-Proof with mautosolve.
-  split; intros []; econstructor; intuition;
-    match_by_head per_bot ltac:(fun H => specialize (H (length Δ)) as [? []]);
-    functional_read_rewrite_clear; intuition;
-    match_by_head per_bot ltac:(fun H => rewrite H in *); eassumption.
-Qed.
-
-Add Parametric Morphism i : (neut_glu_exp_pred i)
-    with signature per_bot ==> glu_exp_pred_equivalence as neut_glu_exp_pred_morphism_glu_exp_pred_equivalence.
-Proof with mautosolve.
-  split; apply neut_glu_exp_pred_morphism_iff; mauto.
-Qed.
-
-(* Morphism instances for "pi_glu_*_pred"s *)
-Add Parametric Morphism i IR : (pi_glu_typ_pred i IR)
-    with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> eq ==> eq ==> eq ==> iff as pi_glu_typ_pred_morphism_iff.
-Proof with mautosolve.
-  split; intros []; econstructor; intuition.
+  eapply glu_univ_elem_cumulativity_ge; mauto.
 Qed.
 
-Add Parametric Morphism i IR : (pi_glu_typ_pred i IR)
-    with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> eq ==> glu_typ_pred_equivalence as pi_glu_typ_pred_morphism_glu_typ_pred_equivalence.
-Proof with mautosolve.
-  split; intros []; econstructor; intuition.
-Qed.
-
-Add Parametric Morphism i IR : (pi_glu_exp_pred i IR)
-    with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> relation_equivalence ==> eq ==> eq ==> eq ==> eq ==> eq ==> iff as pi_glu_exp_pred_morphism_iff.
-Proof with mautosolve.
-  split; intros []; econstructor; intuition.
-Qed.
-
-Add Parametric Morphism i IR : (pi_glu_exp_pred i IR)
-    with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> relation_equivalence ==> eq ==> glu_exp_pred_equivalence as pi_glu_exp_pred_morphism_glu_exp_pred_equivalence.
-Proof with mautosolve.
-  split; intros []; econstructor; intuition.
+Corollary glu_univ_elem_exp_cumu_ge :  forall {i j a P P' El El' Γ A M m},
+    i <= j ->
+    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    {{ DG a ∈ glu_univ_elem j ↘ P' ↘ El' }} ->
+    {{ Γ ⊢ M : A ® m ∈ El }} ->
+    {{ Γ ⊢ M : A ® m ∈ El' }}.
+Proof.
+  intros * ? ? ?. gen m M A Γ.
+  eapply glu_univ_elem_cumulativity_ge; mauto.
 Qed.
 
-Lemma functional_glu_univ_elem : forall i a P P' El El',
+Corollary glu_univ_elem_exp_lower :  forall {i j a P P' El El' Γ A M m},
+    i <= j ->
     {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
-    {{ DG a ∈ glu_univ_elem i ↘ P' ↘ El' }} ->
-    (P <∙> P') /\ (El <∙> El').
+    {{ DG a ∈ glu_univ_elem j ↘ P' ↘ El' }} ->
+    {{ Γ ⊢ A ® P }} ->
+    {{ Γ ⊢ M : A ® m ∈ El' }} ->
+    {{ Γ ⊢ M : A ® m ∈ El }}.
 Proof.
-  simpl.
-  intros * Ha Ha'. gen P' El'.
-  induction Ha using glu_univ_elem_ind; intros; basic_invert_glu_univ_elem Ha';
-    apply_predicate_equivalence; try solve [split; reflexivity].
-  assert ((IP <∙> IP0) /\ (IEl <∙> IEl0)) as [] by mauto.
-  apply_predicate_equivalence.
-  handle_per_univ_elem_irrel.
-  (on_all_hyp: fun H => directed invert_per_univ_elem H).
-  handle_per_univ_elem_irrel.
-  split; [intros Γ C | intros Γ M C m].
-  - split; intros []; econstructor; intuition;
-      rename a0 into c;
-      [rename equiv_a into equiv_c; assert (equiv_c' : in_rel c c) by intuition
-      | rename equiv_a into equiv_c'; assert (equiv_c : in_rel0 c c) by intuition];
-      destruct_rel_mod_eval;
-      rename a0 into b;
-      assert ((OP c equiv_c' <∙> OP0 c equiv_c) /\ (OEl c equiv_c' <∙> OEl0 c equiv_c)) as [] by mauto 3;
-      intuition.
-  - split; intros []; econstructor; intuition;
-      clear m;
-      rename b into m;
-      [rename equiv_b into equiv_m; assert (equiv_m' : in_rel m m) by intuition
-      | rename equiv_b into equiv_m'; assert (equiv_m : in_rel0 m m) by intuition];
-      destruct_rel_mod_eval;
-      [assert (exists am : domain, {{ $| a0 & m |↘ am }} /\ {{ Δ ⊢ m0[σ] m' : OT[σ,,m'] ® am ∈ OEl m equiv_m' }}) by intuition
-      | assert (exists am : domain, {{ $| a0 & m |↘ am }} /\ {{ Δ ⊢ m0[σ] m' : OT[σ,,m'] ® am ∈ OEl0 m equiv_m }}) by intuition];
-      destruct_conjs;
-      assert ((OP m equiv_m' <∙> OP0 m equiv_m) /\ (OEl m equiv_m' <∙> OEl0 m equiv_m)) as [] by mauto 3;
-      eexists; split; intuition.
+  intros * ? ? ?. gen m M A Γ.
+  eapply glu_univ_elem_cumulativity_ge; mauto.
 Qed.
 
-Ltac apply_functional_glu_univ_elem1 :=
-  let tactic_error o1 o2 := fail 2 "functional_glu_univ_elem biconditional between" o1 "and" o2 "cannot be solved" in
-  match goal with
-  | H1 : {{ DG ~?A ∈ glu_univ_elem ?i ↘ ?P1 ↘ ?El1 }},
-      H2 : {{ DG ~?A ∈ glu_univ_elem ?i' ↘ ?P2 ↘ ?El2 }} |- _ =>
-      assert_fails (unify P1 P2; unify El1 El2);
-      match goal with
-      | H : P1 <∙> P2, H0 : El1 <∙> El2 |- _ => fail 1
-      | H : P1 <∙> P2, H0 : El2 <∙> El1 |- _ => fail 1
-      | H : P2 <∙> P1, H0 : El1 <∙> El2 |- _ => fail 1
-      | H : P2 <∙> P1, H0 : El2 <∙> El1 |- _ => fail 1
-      | _ => assert ((P1 <∙> P2) /\ (El1 <∙> El2)) as [] by (eapply functional_glu_univ_elem; [apply H1 | apply H2]) || tactic_error P1 P2
-      end
-  end.
-
-Ltac apply_functional_glu_univ_elem :=
-  repeat apply_functional_glu_univ_elem1.
-
-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.
-
-Lemma glu_univ_elem_pi_clean_inversion1 : forall {i a p B in_rel typ_rel el_rel},
-  {{ DF a ≈ a ∈ per_univ_elem i ↘ in_rel }} ->
-  {{ DG Π a p B ∈ glu_univ_elem i ↘ typ_rel ↘ el_rel }} ->
-  exists IP IEl (OP : forall c (equiv_c_c : {{ Dom c ≈ c ∈ in_rel }}), glu_typ_pred)
-     (OEl : forall c (equiv_c_c : {{ Dom c ≈ c ∈ in_rel }}), glu_exp_pred) elem_rel,
-      {{ DG a ∈ glu_univ_elem i ↘ IP ↘ IEl }} /\
-        (forall c (equiv_c : {{ Dom c ≈ c ∈ in_rel }}) b,
-            {{ ⟦ B ⟧ p ↦ c ↘ b }} ->
-            {{ DG b ∈ glu_univ_elem i ↘ OP _ equiv_c ↘ OEl _ equiv_c }}) /\
-        {{ DF Π a p B ≈ Π a p B ∈ per_univ_elem i ↘ elem_rel }} /\
-        (typ_rel <∙> pi_glu_typ_pred i in_rel IP IEl OP) /\
-        (el_rel <∙> pi_glu_exp_pred i in_rel IP IEl elem_rel OEl).
-Proof.
-  intros *.
-  simpl.
-  intros Hinper Hglu.
-  basic_invert_glu_univ_elem Hglu.
-  handle_functional_glu_univ_elem.
-  handle_per_univ_elem_irrel.
-  do 5 eexists.
-  repeat split.
-  1,3: eassumption.
-  1: instantiate (1 := fun c equiv_c Γ A M m => forall (b : domain) Pb Elb,
-                          {{ ⟦ B ⟧ p ↦ c ↘ b }} ->
-                          {{ DG b ∈ glu_univ_elem i ↘ Pb ↘ Elb }} ->
-                          {{ Γ ⊢ M : A ® m ∈ Elb }}).
-  1: instantiate (1 := fun c equiv_c Γ A => forall (b : domain) Pb Elb,
-                          {{ ⟦ B ⟧ p ↦ c ↘ b }} ->
-                          {{ DG b ∈ glu_univ_elem i ↘ Pb ↘ Elb }} ->
-                          {{ Γ ⊢ A ® Pb }}).
-  2-5: intros []; econstructor; mauto.
-  all: intros.
-  - assert {{ Dom c ≈ c ∈ in_rel0 }} as equiv0_c by intuition.
-    assert {{ DG b ∈ glu_univ_elem i ↘ OP c equiv0_c ↘ OEl c equiv0_c }} by mauto 3.
-    apply -> simple_glu_univ_elem_morphism_iff; [| reflexivity | |]; [eauto | |].
-    + intros ? ? ? ?.
-      split; intros; handle_functional_glu_univ_elem; intuition.
-    + intros ? ?.
-      split; [intros; handle_functional_glu_univ_elem |]; intuition.
-  - rename a0 into c.
-    rename equiv_a into equiv_c.
-    assert {{ Dom c ≈ c ∈ in_rel0 }} as equiv0_c by intuition.
-    assert {{ DG b ∈ glu_univ_elem i ↘ OP c equiv0_c ↘ OEl c equiv0_c }} by mauto 3.
-    handle_functional_glu_univ_elem.
-    intuition.
-  - match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H).
-    destruct_rel_mod_eval.
-    intuition.
-  - rename b into c.
-    rename equiv_b into equiv_c.
-    assert {{ Dom c ≈ c ∈ in_rel0 }} as equiv0_c by intuition.
-    assert (exists ac : domain, {{ $| a0 & c |↘ ac }} /\ {{ Δ ⊢ m[σ] m' : OT[σ,,m'] ® ac ∈ OEl c equiv0_c }}) by mauto 3.
-    destruct_conjs.
-    eexists.
-    intuition.
-    assert {{ DG b ∈ glu_univ_elem i ↘ OP c equiv0_c ↘ OEl c equiv0_c }} by mauto 3.
-    handle_functional_glu_univ_elem.
-    intuition.
-  - assert (exists ab : domain,
-               {{ $| a0 & b |↘ ab }} /\
-                 (forall (b0 : domain) (Pb : glu_typ_pred) (Elb : glu_exp_pred),
-                     {{ ⟦ B ⟧ p ↦ b ↘ b0 }} ->
-                     {{ DG b0 ∈ glu_univ_elem i ↘ Pb ↘ Elb }} ->
-                     {{ Δ ⊢ m[σ] m' : OT[σ,,m'] ® ab ∈ Elb }})) by intuition.
+Lemma glu_univ_elem_exp_conv : forall {i j k a a' P P' El El' Γ A M m},
+    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    {{ DG a' ∈ glu_univ_elem j ↘ P' ↘ El' }} ->
+    {{ Dom a ≈ a' ∈ per_univ k }} ->
+    {{ Γ ⊢ M : A ® m ∈ El }} ->
+    {{ Γ ⊢ A ® P' }} ->
+    {{ Γ ⊢ M : A ® m ∈ El' }}.
+Proof.
+  intros * ? ? [] ? ?.
+  assert {{ Dom a ≈ a' ∈ per_univ (max i k) }} by (eexists; mauto using per_univ_elem_cumu_max_right).
+  assert (exists P El, {{ DG a ∈ glu_univ_elem (max i k) ↘ P ↘ El }}) as [Pik [Elik]] by mauto using glu_univ_elem_cumu_max_left.
+  assert {{ DG a' ∈ glu_univ_elem (max i k) ↘ Pik ↘ Elik }} by (erewrite <- glu_univ_elem_morphism_iff; try reflexivity; mauto).
+  assert (i <= max i k) by lia.
+  assert {{ Γ ⊢ M : A ® m ∈ Elik }} by (eapply glu_univ_elem_exp_cumu_ge; mauto).
+  assert (exists P El, {{ DG a' ∈ glu_univ_elem (max j (max i k)) ↘ P ↘ El }}) as [Ptop [Eltop]] by mauto using glu_univ_elem_cumu_max_right.
+  assert (max i k <= max j (max i k)) by lia.
+  assert {{ Γ ⊢ M : A ® m ∈ Eltop }} by (eapply glu_univ_elem_exp_cumu_ge; mauto).
+  assert (j <= max j (max i k)) by lia.
+  eapply glu_univ_elem_exp_lower; mauto.
+Qed.
+
+Lemma glu_univ_elem_per_subtyp_typ_escape : forall {i a a' P P' El El' Γ A A'},
+    {{ Sub a <: a' at i }} ->
+    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    {{ 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.
-    match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H).
+    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.
+    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.
-    destruct_rel_mod_app.
-    functional_eval_rewrite_clear.
-    eexists.
-    intuition.
-Qed.
-
-Lemma glu_univ_elem_pi_clean_inversion2 : forall {i a p B in_rel IP IEl typ_rel el_rel},
-  {{ DF a ≈ a ∈ per_univ_elem i ↘ in_rel }} ->
-  {{ DG a ∈ glu_univ_elem i ↘ IP ↘ IEl }} ->
-  {{ DG Π a p B ∈ glu_univ_elem i ↘ typ_rel ↘ el_rel }} ->
-  exists (OP : forall c (equiv_c_c : {{ Dom c ≈ c ∈ in_rel }}), glu_typ_pred)
-     (OEl : forall c (equiv_c_c : {{ Dom c ≈ c ∈ in_rel }}), glu_exp_pred) elem_rel,
-    (forall c (equiv_c : {{ Dom c ≈ c ∈ in_rel }}) b,
-        {{ ⟦ B ⟧ p ↦ c ↘ b }} ->
-        {{ DG b ∈ glu_univ_elem i ↘ OP _ equiv_c ↘ OEl _ equiv_c }}) /\
-      {{ DF Π a p B ≈ Π a p B ∈ per_univ_elem i ↘ elem_rel }} /\
-      (typ_rel <∙> pi_glu_typ_pred i in_rel IP IEl OP) /\
-      (el_rel <∙> pi_glu_exp_pred i in_rel IP IEl elem_rel OEl).
-Proof.
-  intros *.
-  simpl.
-  intros Hinper Hinglu Hglu.
-  unshelve eapply (glu_univ_elem_pi_clean_inversion1 _) in Hglu; shelve_unifiable; [eassumption |];
-    destruct Hglu as [? [? [? [? [? [? [? [? []]]]]]]]].
-  handle_functional_glu_univ_elem.
-  do 3 eexists.
-  repeat split; try eassumption;
-    intros []; econstructor; mauto.
+    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.
 
-Ltac invert_glu_univ_elem H :=
-  (unshelve eapply (glu_univ_elem_pi_clean_inversion2 _ _) in H; shelve_unifiable; [eassumption | eassumption |];
-   destruct H as [? [? [? [? [? []]]]]])
-  + (unshelve eapply (glu_univ_elem_pi_clean_inversion1 _) in H; shelve_unifiable; [eassumption |];
-   destruct H as [? [? [? [? [? [? [? [? []]]]]]]]])
-  + basic_invert_glu_univ_elem H.
+#[export]
+Hint Resolve glu_univ_elem_per_subtyp_typ_escape : mcltt.
 
-Lemma glu_univ_elem_morphism_helper : forall i a a' P El,
-    {{ Dom a ≈ a' ∈ per_univ i }} ->
+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 }}.
-Proof.
-  simpl.
-  intros * [elem_rel Hper] Horig.
-  pose proof Hper.
-  gen P El.
-  induction Hper using per_univ_elem_ind; intros; subst;
+    {{ DG a' ∈ glu_univ_elem i ↘ P' ↘ El' }} ->
+    {{ Γ ⊢ A' ® P' }} ->
+    {{ Γ ⊢ M : A ® m ∈ El }} ->
+    {{ Γ ⊢ M : A' ® m ∈ El' }}.
+Proof.
+  intros * Hsubtyp Hglu Hglu' HA HA'.
+  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;
-    invert_glu_univ_elem Horig; glu_univ_elem_econstructor; try eassumption; mauto;
+    invert_glu_univ_elem Hglu;
+    handle_functional_glu_univ_elem;
     handle_per_univ_elem_irrel;
-    handle_functional_glu_univ_elem.
-  - intros.
-    match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H).
-    destruct_rel_mod_eval.
+    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].
+  - 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 []]).
+    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'[σ] }} by mauto 3.
+      assert {{ Δ ⊢ M[σ] ≈ v : A[σ] }} by mauto.
+      mauto.
+  - simpl in *.
+    destruct_conjs.
+    intuition mauto 3.
+    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 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.
-    intuition.
-  - reflexivity.
-  - apply neut_glu_typ_pred_morphism_glu_typ_pred_equivalence.
-    eassumption.
-  - apply neut_glu_exp_pred_morphism_glu_exp_pred_equivalence.
-    eassumption.
-Qed.
-
-(* Morphism instances for "glu_univ_elem" *)
-Add Parametric Morphism i : (glu_univ_elem i)
-    with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> per_univ i ==> iff as glu_univ_elem_morphism_iff.
-Proof with mautosolve.
-  intros P P' HPP' El El' HElEl' a a' Haa'.
-  rewrite HPP', HElEl'.
-  split; intros; eapply glu_univ_elem_morphism_helper; mauto.
-  symmetry; eassumption.
-Qed.
+    econstructor; mauto 4.
+    + 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 {{ Γ ⊢ 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.
+      }
+      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.
+      rename a1 into b.
+      rename a2 into b'.
+      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.
+      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.
+
+Lemma glu_ctx_env_per_env : forall {Γ Sb env_rel Δ σ p},
+    {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
+    {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ env_rel }} ->
+    {{ Δ ⊢s σ ® p ∈ Sb }} ->
+    {{ Dom p ≈ p ∈ env_rel }}.
+Proof.
+  intros * Hglu Hper.
+  gen p σ Δ env_rel.
+  induction Hglu; intros;
+    invert_per_ctx_env Hper;
+    apply_predicate_equivalence;
+    handle_per_ctx_env_irrel;
+    mauto.
 
-Add Parametric Morphism i R : (glu_univ_elem i)
-    with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> per_univ_elem i R ==> iff as glu_univ_elem_morphism_iff'.
-Proof with mautosolve.
-  intros P P' HPP' El El' HElEl' a a' Haa'.
-  rewrite HPP', HElEl'.
-  split; intros; eapply glu_univ_elem_morphism_helper; mauto.
-  symmetry; mauto.
+  rename i0 into j.
+  inversion_clear_by_head cons_glu_sub_pred.
+  assert {{ Dom p ↯ ≈ p ↯ ∈ tail_rel }} by (eapply IHHglu; mauto).
+  destruct_rel_typ.
+  handle_per_univ_elem_irrel.
+  assert (exists P' El', {{ DG a ∈ glu_univ_elem (max i j) ↘ P' ↘ El' }}) as [? []] by mauto using glu_univ_elem_cumu_max_left.
+  eexists; eapply glu_univ_elem_per_elem; mauto using per_univ_elem_cumu_max_right.
+  assert (i <= max i j) by lia.
+  eapply glu_univ_elem_exp_cumu_ge; mauto.
 Qed.
 
-Ltac saturate_glu_by_per1 :=
-  match goal with
-  | H : glu_univ_elem ?i ?P ?El ?a,
-      H1 : per_univ_elem ?i _ ?a ?a' |- _ =>
-      assert (glu_univ_elem i P El a') by (rewrite <- H1; eassumption);
-      fail_if_dup
-  | H : glu_univ_elem ?i ?P ?El ?a',
-      H1 : per_univ_elem ?i _ ?a ?a' |- _ =>
-      assert (glu_univ_elem i P El a) by (rewrite H1; eassumption);
-      fail_if_dup
-  end.
-
-Ltac saturate_glu_by_per :=
-  clear_dups;
-  repeat saturate_glu_by_per1.
-
-Lemma per_univ_glu_univ_elem : forall i a,
-    {{ Dom a ≈ a ∈ per_univ i }} ->
-    exists P El, {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }}.
+Lemma glu_ctx_env_wf_ctx : forall {Γ Sb},
+    {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
+    {{ ⊢ Γ }}.
 Proof.
-  simpl.
-  intros * [? Hper].
-  induction Hper using per_univ_elem_ind; intros;
-    try solve [do 2 eexists; unshelve (glu_univ_elem_econstructor; try reflexivity; subst; trivial)].
-
-  - destruct_conjs.
-    do 2 eexists.
-    glu_univ_elem_econstructor; try (eassumption + reflexivity).
-    + saturate_refl; eassumption.
-    + instantiate (1 := fun (c : domain) (equiv_c : in_rel c c) Γ A M m =>
-                          forall b P El,
-                            {{ ⟦ B' ⟧ p' ↦ c ↘ b }} ->
-                            glu_univ_elem i P El b ->
-                            {{ Γ ⊢ M : A ® m ∈ El }}).
-      instantiate (1 := fun (c : domain) (equiv_c : in_rel c c) Γ A =>
-                          forall b P El,
-                            {{ ⟦ B' ⟧ p' ↦ c ↘ b }} ->
-                            glu_univ_elem i P El b ->
-                            {{ Γ ⊢ A ® P }}).
-      intros.
-      (on_all_hyp: destruct_rel_by_assumption in_rel).
-      handle_per_univ_elem_irrel.
-      rewrite simple_glu_univ_elem_morphism_iff; try (eassumption + reflexivity);
-        split; intros; handle_functional_glu_univ_elem; intuition.
-    + enough {{ DF Π A p B ≈ Π A' p' B' ∈ per_univ_elem i ↘ elem_rel }} by (etransitivity; [symmetry |]; eassumption).
-      per_univ_elem_econstructor; mauto.
-      intros.
-      (on_all_hyp: destruct_rel_by_assumption in_rel).
-      econstructor; mauto.
-  - do 2 eexists.
-    glu_univ_elem_econstructor; try reflexivity; mauto.
+  induction 1; intros; 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 }}.
+Lemma glu_ctx_env_resp_per_ctx_helper : forall {Γ Γ' Sb Sb'},
+    {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
+    {{ EG Γ' ∈ glu_ctx_env ↘ Sb' }} ->
+    {{ ⊢ Γ ≈ Γ' }} ->
+    (Sb -∙> Sb').
+Proof.
+  intros * Hglu Hglu' HΓΓ'.
+  gen Sb' Γ'.
+  induction Hglu; intros;
+    destruct (completeness_fundamental_ctx_eq _ _ HΓΓ') as [env_relΓ Hper];
+    apply_predicate_equivalence;
+    handle_per_univ_elem_irrel;
+    dependent destruction Hglu';
+    apply_predicate_equivalence;
+    invert_per_ctx_env Hper;
+    handle_per_ctx_env_irrel;
+    gintuition.
+
+  rename i0 into j.
+  rename Γ0 into Γ'.
+  rename A0 into A'.
+  rename TSb0 into TSb'.
+  rename i1 into k.
+  inversion HΓΓ' as [|? ? l]; subst.
+  assert (TSb -∙> TSb') by (eapply IHHglu; mauto).
+  intros Δ σ p [].
+  saturate_refl_for per_ctx_env.
+  assert {{ Dom ρ ↯ ≈ ρ ↯ ∈ tail_rel }}
+    by (eapply glu_ctx_env_per_env; only 3: eassumption; eassumption).
+  assert {{ Δ0 ⊢s Wk∘σ0 ® ρ ↯ ∈ TSb' }} by intuition.
+  assert (glu_rel_typ_sub j Δ0 A' {{{ Wk∘σ0 }}} d{{{ ρ ↯ }}}) as [] by mauto.
+  destruct_rel_typ.
+  handle_functional_glu_univ_elem.
+  rename a0 into a'.
+  rename El0 into El'.
+  rename P0 into P'.
+  econstructor; mauto 4.
+  assert (exists Pmax Elmax, {{ DG a ∈ glu_univ_elem (max i l) ↘ Pmax ↘ Elmax }}) as [Pmax [Elmax]]
+      by mauto using glu_univ_elem_cumu_max_left.
+  assert (i <= max i l) by lia.
+  assert {{ Δ0 ⊢ #0[σ0] : A'[Wk∘σ0] ® ~(ρ 0) ∈ Elmax }}.
+  {
+    assert {{ Δ0 ⊢s Wk∘σ0 : Γ }} by mauto 4.
+    assert {{ Δ0 ⊢ A'[Wk∘σ0] ≈ A[Wk∘σ0] : Type@(max i l) }} as -> by mauto 4 using lift_exp_eq_max_right.
+    eapply glu_univ_elem_exp_cumu_ge; mauto.
+  }
+  eapply glu_univ_elem_exp_conv; intuition.
+  eexists; mauto.
+Qed.
+
+Corollary functional_glu_ctx_env : forall {Γ Sb Sb'},
+    {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
+    {{ EG Γ ∈ glu_ctx_env ↘ Sb' }} ->
+    (Sb <∙> Sb').
 Proof.
   intros.
-  apply per_univ_glu_univ_elem; mauto.
+  assert {{ ⊢ Γ ≈ Γ }} by mauto using glu_ctx_env_wf_ctx.
+  split; eapply glu_ctx_env_resp_per_ctx_helper; eassumption.
 Qed.
 
-#[export]
-Hint Resolve per_univ_elem_glu_univ_elem : mcltt.
-
-Ltac saturate_glu_info1 :=
+Ltac apply_functional_glu_ctx_env1 :=
+  let tactic_error o1 o2 := fail 2 "functional_glu_ctx_env biconditional between" o1 "and" o2 "cannot be solved" in
   match goal with
-  | H : glu_univ_elem _ ?P _ _,
-      H1 : ?P _ _ |- _ =>
-      pose proof (glu_univ_elem_univ_lvl _ _ _ _ H _ _ H1);
-      fail_if_dup
-  | H : glu_univ_elem _ _ ?El _,
-      H1 : ?El _ _ _ _ |- _ =>
-      pose proof (glu_univ_elem_trm_escape _ _ _ _ H _ _ _ _ H1);
-      fail_if_dup
+  | H1 : {{ EG ~?Γ ∈ glu_ctx_env ↘ ?Sb1 }},
+      H2 : {{ EG ~?Γ ∈ glu_ctx_env ↘ ?Sb2 }} |- _ =>
+      assert_fails (unify Sb1 Sb2);
+      match goal with
+      | H : Sb1 <∙> Sb2 |- _ => fail 1
+      | _ => assert (Sb1 <∙> Sb2) by (eapply functional_glu_ctx_env; [apply H1 | apply H2]) || tactic_error Sb1 Sb2
+      end
   end.
 
-Ltac saturate_glu_info :=
-  clear_dups;
-  repeat saturate_glu_info1.
-
-#[local]
-Hint Rewrite -> sub_decompose_q using solve [mauto 4] : mcltt.
+Ltac apply_functional_glu_ctx_env :=
+  repeat apply_functional_glu_ctx_env1.
 
-Lemma glu_univ_elem_typ_monotone : forall i a P El,
-    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
-    forall Δ σ Γ A,
-      {{ Γ ⊢ A ® P }} ->
-      {{ Δ ⊢w σ : Γ }} ->
-      {{ Δ ⊢ A[σ] ® P }}.
-Proof.
-  simpl. induction 1 using glu_univ_elem_ind; intros;
-    saturate_weakening_escape;
-    handle_functional_glu_univ_elem;
-    simpl in *;
-    try solve [bulky_rewrite].
-  - simpl_glu_rel. econstructor; eauto; try solve [bulky_rewrite]; mauto 3.
-    intros.
-    saturate_weakening_escape.
-    saturate_glu_info.
-    invert_per_univ_elem H3.
-    destruct_rel_mod_eval.
-    simplify_evals.
-    deepexec H1 ltac:(fun H => pose proof H).
-    autorewrite with mcltt in *.
-    mauto 3.
-
-  - destruct_conjs.
-    split; [mauto 3 |].
-    intros.
-    saturate_weakening_escape.
-    autorewrite with mcltt.
-    mauto 3.
-Qed.
-
-
-Lemma glu_univ_elem_exp_monotone : forall i a P El,
-    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
-    forall Δ σ Γ M A m,
-      {{ Γ ⊢ M : A ® m ∈ El }} ->
-      {{ Δ ⊢w σ : Γ }} ->
-      {{ Δ ⊢ M[σ] : A[σ] ® m ∈ El }}.
-Proof.
-  simpl. induction 1 using glu_univ_elem_ind; intros;
-    saturate_weakening_escape;
-    handle_functional_glu_univ_elem;
-    simpl in *;
-    destruct_all.
-  - repeat eexists; mauto 2; bulky_rewrite.
-    eapply glu_univ_elem_typ_monotone; eauto.
-  - repeat eexists; mauto 2; bulky_rewrite.
-
-  - simpl_glu_rel.
-    econstructor; mauto 4;
-      intros;
-      saturate_weakening_escape.
-    + eapply glu_univ_elem_typ_monotone; eauto.
-    + saturate_glu_info.
-      invert_per_univ_elem H3.
-      apply_equiv_left.
-      destruct_rel_mod_eval.
-      destruct_rel_mod_app.
-      simplify_evals.
-      deepexec H1 ltac:(fun H => pose proof H).
-      autorewrite with mcltt in *.
-      repeat eexists; eauto.
-      assert {{ Δ0 ⊢s σ0,, m' : Δ, ~ (a_sub IT σ) }}. {
-        econstructor; mauto 2.
-        bulky_rewrite.
-      }
-      assert {{Δ0 ⊢ (m [σ][σ0]) m' ≈ (m [σ ∘ σ0]) m' : OT [σ ∘ σ0,, m']}}. {
-        rewrite <- sub_eq_q_sigma_id_extend; mauto 4.
-        rewrite <- exp_eq_sub_compose_typ; mauto 3;
-          [eapply wf_exp_eq_app_cong' |];
-          mauto 4.
-        symmetry.
-        bulky_rewrite_in H4.
-        eapply wf_exp_eq_conv; mauto 3.
-      }
-
-      bulky_rewrite.
-      edestruct H10 with (b := b) as [? []];
-        simplify_evals; [| | eassumption];
-      mauto.
-
-  - simpl_glu_rel.
-    econstructor; repeat split; mauto 3;
-      intros;
-      saturate_weakening_escape.
-    + autorewrite with mcltt.
-      mauto 3.
-    + autorewrite with mcltt.
-      etransitivity.
-      * symmetry.
-        eapply wf_exp_eq_sub_compose;
-          mauto 3.
-      * mauto 3.
-Qed.
+Ltac handle_functional_glu_ctx_env :=
+  functional_eval_rewrite_clear;
+  fold glu_typ_pred in *;
+  fold glu_exp_pred in *;
+  apply_functional_glu_ctx_env;
+  apply_predicate_equivalence;
+  clear_dups.
 
-(* Simple Morphism instance for "glu_ctx_env" *)
-Add Parametric Morphism : glu_ctx_env
-    with signature glu_sub_pred_equivalence ==> eq ==> iff as simple_glu_ctx_env_morphism_iff.
-Proof with mautosolve.
-  intros Sb Sb' HSbSb' a.
-  split; intro Horig; [gen Sb' | gen Sb];
-    induction Horig; econstructor;
-    try (etransitivity; [symmetry + idtac|]; eassumption); eauto.
+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.
+  handle_functional_glu_ctx_env.
+  mauto.
 Qed.
diff --git a/theories/Core/Soundness/Realizability.v b/theories/Core/Soundness/Realizability.v
index 2e8d30e7..943b9a9a 100644
--- a/theories/Core/Soundness/Realizability.v
+++ b/theories/Core/Soundness/Realizability.v
@@ -3,7 +3,7 @@ From Coq Require Import Nat.
 From Mcltt Require Import Base LibTactics.
 From Mcltt.Core.Syntactic Require Import CtxSub Corollaries.
 From Mcltt.Core.Semantic Require Import Realizability.
-From Mcltt.Core.Soundness Require Export LogicalRelation Weakening.
+From Mcltt.Core.Soundness Require Export LogicalRelation.Core Weakening.
 Import Domain_Notations.
 
 Open Scope list_scope.
diff --git a/theories/Core/Soundness/SubtypingCases.v b/theories/Core/Soundness/SubtypingCases.v
index 7fb1c205..826f6e5e 100644
--- a/theories/Core/Soundness/SubtypingCases.v
+++ b/theories/Core/Soundness/SubtypingCases.v
@@ -3,28 +3,10 @@ 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 Cumulativity EquivalenceLemmas LogicalRelation Realizability SubtypingLemmas.
+From Mcltt.Core.Soundness Require Import LogicalRelation Realizability.
 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 }} ->
@@ -51,8 +33,7 @@ Proof.
   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.
+  assert {{ Dom ρ ≈ ρ ∈ env_relΓ }} by (eapply glu_ctx_env_per_env; mauto).
   (on_all_hyp: destruct_rel_by_assumption env_relΓ).
   destruct_by_head rel_exp.
   handle_per_univ_elem_irrel.
@@ -69,4 +50,4 @@ Proof.
     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.
+Qed.
diff --git a/theories/Core/Soundness/SubtypingLemmas.v b/theories/Core/Soundness/SubtypingLemmas.v
deleted file mode 100644
index ffbed94b..00000000
--- a/theories/Core/Soundness/SubtypingLemmas.v
+++ /dev/null
@@ -1,177 +0,0 @@
-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 Cumulativity 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.
-    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.
-
-#[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 }} ->
-    {{ DG a' ∈ glu_univ_elem i ↘ P' ↘ El' }} ->
-    {{ Γ ⊢ A' ® P' }} ->
-    {{ Γ ⊢ M : A ® m ∈ El }} ->
-    {{ Γ ⊢ M : A' ® m ∈ El' }}.
-Proof.
-  intros * Hsubtyp Hglu Hglu' HA HA'.
-  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;
-    invert_glu_univ_elem Hglu;
-    handle_functional_glu_univ_elem;
-    handle_per_univ_elem_irrel;
-    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].
-  - 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 []]).
-    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'[σ] }} by mauto 3.
-      assert {{ Δ ⊢ M[σ] ≈ v : A[σ] }} by mauto.
-      mauto.
-  - simpl in *.
-    destruct_conjs.
-    intuition mauto 3.
-    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 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.
-    + 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 {{ Γ ⊢ 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.
-      }
-      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.
-      rename a1 into b.
-      rename a2 into b'.
-      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.
-      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.
diff --git a/theories/Core/Soundness/Weakening.v b/theories/Core/Soundness/Weakening.v
index e06ce979..3b62cca9 100644
--- a/theories/Core/Soundness/Weakening.v
+++ b/theories/Core/Soundness/Weakening.v
@@ -1 +1 @@
-From Mcltt.Core.Soundness Require Export Weakening.Definition.
+From Mcltt.Core.Soundness Require Export Weakening.Definition Weakening.Lemmas.
diff --git a/theories/LibTactics.v b/theories/LibTactics.v
index 1075ddc0..206857fe 100644
--- a/theories/LibTactics.v
+++ b/theories/LibTactics.v
@@ -240,10 +240,12 @@ Ltac predicate_resolve :=
       simple apply @Equivalence_Symmetric
   | |- @Transitive _ (@predicate_equivalence _) =>
       simple apply @Equivalence_Transitive
+  | |- @Transitive _ (@predicate_implication _) =>
+      simple apply @PreOrder_Transitive
   end.
 
 #[export]
- Hint Extern 1 => predicate_resolve : typeclass_instances.
+Hint Extern 1 => predicate_resolve : typeclass_instances.
 
 
 (* intuition tactic default setting *)
@@ -422,6 +424,34 @@ Hint Extern 1 (subrelation iff (Basics.flip Basics.impl)) => exact iff_flip_impl
 #[export]
 Hint Extern 1 (subrelation (@relation_equivalence ?A) _) => (let H := fresh "H" in intros ? ? H; exact H) : typeclass_instances.
 
+#[export]
+Hint Extern 1 (subrelation (@predicate_implication ?Ts) _) => (let H := fresh "H" in intros ? ? H; exact H) : typeclass_instances.
+
+#[export]
+Hint Extern 1 (subrelation (@subrelation ?A) _) => (let H := fresh "H" in intros ? ? H; exact H) : typeclass_instances.
+
+#[export]
+Instance predicate_implication_equivalence Ts : subrelation (@predicate_equivalence Ts) (@predicate_implication Ts).
+Proof.
+  induction Ts; gintuition.
+
+  intros ? ? H v.
+  apply IHTs.
+  exact (H v).
+Qed.
+
+Add Parametric Morphism Ts : (@predicate_implication Ts)
+    with signature (@predicate_equivalence Ts) ==> (@predicate_equivalence Ts) ==> iff as predicate_implication_morphism.
+Proof.
+  induction Ts; split; intros; gintuition.
+  - rewrite <- H.
+    transitivity x0; try eassumption.
+    rewrite H0; reflexivity.
+  - rewrite H.
+    transitivity y0; try eassumption.
+    rewrite <- H0; reflexivity.
+Qed.
+
 Add Parametric Morphism A : PER
     with signature (@relation_equivalence A) ==> iff as PER_morphism.
 Proof.
diff --git a/theories/_CoqProject b/theories/_CoqProject
index 782eec3c..31532a9c 100644
--- a/theories/_CoqProject
+++ b/theories/_CoqProject
@@ -52,15 +52,14 @@
 ./Core/Syntactic/System/Tactics.v
 ./Core/Syntactic/SystemOpt.v
 ./Core/Soundness.v
-./Core/Soundness/Cumulativity.v
-./Core/Soundness/EquivalenceLemmas.v
 ./Core/Soundness/LogicalRelation.v
+./Core/Soundness/LogicalRelation/Core.v
+./Core/Soundness/LogicalRelation/CoreLemmas.v
 ./Core/Soundness/LogicalRelation/CoreTactics.v
 ./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
 ./Core/Soundness/Weakening/Lemmas.v