From 736ec6ea185bd61726ee04330773ed65d138af9e Mon Sep 17 00:00:00 2001
From: Junyoung/Clare Jang <jjc9310@gmail.com>
Date: Thu, 13 Jun 2024 03:23:58 -0400
Subject: [PATCH 1/4] Rename a constructor

---
 theories/Core/Syntactic/System/Definitions.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Core/Syntactic/System/Definitions.v b/theories/Core/Syntactic/System/Definitions.v
index eaa961ba..dc6384f3 100644
--- a/theories/Core/Syntactic/System/Definitions.v
+++ b/theories/Core/Syntactic/System/Definitions.v
@@ -39,7 +39,7 @@ with wf_ctx_eq : ctx -> ctx -> Prop :=
 where "⊢ Γ ≈ Γ'" := (wf_ctx_eq Γ Γ') (in custom judg) : type_scope
 
 with wf_exp : ctx -> exp -> typ -> Prop :=
-| wf_univ :
+| wf_typ :
   `( {{ ⊢ Γ }} ->
      {{ Γ ⊢ Type@i : Type@(S i) }} )
 | wf_nat :

From 735ef591d2fe8555be321f546238b08982e3de51 Mon Sep 17 00:00:00 2001
From: Junyoung/Clare Jang <jjc9310@gmail.com>
Date: Thu, 13 Jun 2024 03:28:45 -0400
Subject: [PATCH 2/4] Remove duplicated inversion theorems

---
 theories/Core/Syntactic/CoreInversions.v     | 37 +------------------
 theories/Core/Syntactic/CoreTypeInversions.v | 39 ++++++++++++++++++++
 theories/Core/Syntactic/System/Lemmas.v      |  8 ----
 theories/Core/Syntactic/SystemOpt.v          |  2 +-
 theories/_CoqProject                         |  1 +
 5 files changed, 42 insertions(+), 45 deletions(-)
 create mode 100644 theories/Core/Syntactic/CoreTypeInversions.v

diff --git a/theories/Core/Syntactic/CoreInversions.v b/theories/Core/Syntactic/CoreInversions.v
index 0966da67..dca35677 100644
--- a/theories/Core/Syntactic/CoreInversions.v
+++ b/theories/Core/Syntactic/CoreInversions.v
@@ -3,29 +3,6 @@ From Mcltt Require Import Base LibTactics.
 From Mcltt.Core Require Export SystemOpt.
 Import Syntax_Notations.
 
-Lemma wf_univ_inversion : forall {Γ i A},
-    {{ Γ ⊢ Type@i : A }} ->
-    {{ Γ ⊢ Type@(S i) ⊆ A }}.
-Proof.
-  intros * H.
-  dependent induction H; mautosolve.
-Qed.
-
-#[export]
-Hint Resolve wf_univ_inversion : mcltt.
-
-Lemma wf_nat_inversion : forall Γ A,
-    {{ Γ ⊢ ℕ : A }} ->
-    {{ Γ ⊢ Type@0 ⊆ A }}.
-Proof.
-  intros * H.
-  assert (forall i, 0 <= i) by lia.
-  dependent induction H; mautosolve 4.
-Qed.
-
-#[export]
-Hint Resolve wf_nat_inversion : mcltt.
-
 Lemma wf_natrec_inversion : forall Γ A M A' MZ MS,
     {{ Γ ⊢ rec M return A' | zero -> MZ | succ -> MS end : A }} ->
     {{ Γ ⊢ M : ℕ }} /\ {{ Γ ⊢ MZ : A'[Id,,zero] }} /\ {{ Γ, ℕ, A' ⊢ MS : A'[Wk∘Wk,,succ(#1)] }} /\ {{ Γ ⊢ A'[Id,,M] ⊆ A }}.
@@ -41,18 +18,6 @@ Qed.
 #[export]
 Hint Resolve wf_natrec_inversion : mcltt.
 
-Lemma wf_pi_inversion : forall {Γ A B C},
-    {{ Γ ⊢ Π A B : C }} ->
-    exists i, {{ Γ ⊢ A : Type@i }} /\ {{ Γ, A ⊢ B : Type@i }} /\ {{ Γ ⊢ Type@i ⊆ C }}.
-Proof.
-  intros * H.
-  dependent induction H; assert {{ ⊢ Γ }} by mauto 3; try solve [eexists; mauto 4];
-    specialize (IHwf_exp _ _ eq_refl); destruct_conjs; eexists; repeat split; mauto 3.
-Qed.
-
-#[export]
-Hint Resolve wf_pi_inversion : mcltt.
-
 Lemma wf_app_inversion : forall {Γ M N C},
     {{ Γ ⊢ M N : C }} ->
     exists A B, {{ Γ ⊢ M : Π A B }} /\ {{ Γ ⊢ N : A }} /\ {{ Γ ⊢ B[Id,,N] ⊆ C }}.
@@ -132,7 +97,7 @@ Proof with mautosolve 4.
   specialize (IHwf_sub _ _ eq_refl).
   destruct_conjs.
   eexists.
-  repeat split; mauto.
+  repeat split...
 Qed.
 
 #[export]
diff --git a/theories/Core/Syntactic/CoreTypeInversions.v b/theories/Core/Syntactic/CoreTypeInversions.v
new file mode 100644
index 00000000..e7c2e294
--- /dev/null
+++ b/theories/Core/Syntactic/CoreTypeInversions.v
@@ -0,0 +1,39 @@
+From Coq Require Import Setoid.
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core Require Export System.
+Import Syntax_Notations.
+
+Lemma wf_univ_inversion : forall {Γ i A},
+    {{ Γ ⊢ Type@i : A }} ->
+    {{ Γ ⊢ Type@(S i) ⊆ A }}.
+Proof.
+  intros * H.
+  dependent induction H; mautosolve.
+Qed.
+
+#[export]
+Hint Resolve wf_univ_inversion : mcltt.
+
+Lemma wf_nat_inversion : forall Γ A,
+    {{ Γ ⊢ ℕ : A }} ->
+    {{ Γ ⊢ Type@0 ⊆ A }}.
+Proof.
+  intros * H.
+  assert (forall i, 0 <= i) by lia.
+  dependent induction H; mautosolve 4.
+Qed.
+
+#[export]
+Hint Resolve wf_nat_inversion : mcltt.
+
+Lemma wf_pi_inversion : forall {Γ A B C},
+    {{ Γ ⊢ Π A B : C }} ->
+    exists i, {{ Γ ⊢ A : Type@i }} /\ {{ Γ, A ⊢ B : Type@i }} /\ {{ Γ ⊢ Type@i ⊆ C }}.
+Proof.
+  intros * H.
+  dependent induction H; assert {{ ⊢ Γ }} by mauto 3; try solve [eexists; mauto 4];
+    specialize (IHwf_exp _ _ eq_refl); destruct_conjs; eexists; repeat split; mauto 3.
+Qed.
+
+#[export]
+Hint Resolve wf_pi_inversion : mcltt.
diff --git a/theories/Core/Syntactic/System/Lemmas.v b/theories/Core/Syntactic/System/Lemmas.v
index da40661e..4b1eeae4 100644
--- a/theories/Core/Syntactic/System/Lemmas.v
+++ b/theories/Core/Syntactic/System/Lemmas.v
@@ -145,14 +145,6 @@ Qed.
 #[export]
 Hint Resolve presup_exp_eq_ctx : mcltt.
 
-Lemma wf_pi_syntactic_inversion : forall {Γ A B C},
-    {{ Γ ⊢ Π A B : C }} ->
-    exists i, {{ Γ ⊢ A : Type@i }} /\ {{ Γ, A ⊢ B : Type@i }}.
-Proof.
-  intros * H.
-  dependent induction H; mauto 4.
-Qed.
-
 Lemma exp_eq_refl : forall {Γ M A}, {{ Γ ⊢ M : A }} -> {{ Γ ⊢ M ≈ M : A }}.
 Proof.
   mauto.
diff --git a/theories/Core/Syntactic/SystemOpt.v b/theories/Core/Syntactic/SystemOpt.v
index 976483fc..0458b232 100644
--- a/theories/Core/Syntactic/SystemOpt.v
+++ b/theories/Core/Syntactic/SystemOpt.v
@@ -1,6 +1,6 @@
 From Coq Require Import Setoid.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Export CtxEq Presup System.
+From Mcltt.Core Require Export CtxEq Presup System CoreTypeInversions.
 Import Syntax_Notations.
 
 #[local]
diff --git a/theories/_CoqProject b/theories/_CoqProject
index b890e0fe..27bfdded 100644
--- a/theories/_CoqProject
+++ b/theories/_CoqProject
@@ -33,6 +33,7 @@
 ./Core/Semantic/Realizability.v
 ./Core/Semantic/NbE.v
 ./Core/Syntactic/CoreInversions.v
+./Core/Syntactic/CoreTypeInversions.v
 ./Core/Syntactic/Corollaries.v
 ./Core/Syntactic/CtxEq.v
 ./Core/Syntactic/Presup.v

From c6b54b2493d97d50fc2eba1563990a625cd59cc6 Mon Sep 17 00:00:00 2001
From: Junyoung/Clare Jang <jjc9310@gmail.com>
Date: Thu, 13 Jun 2024 03:30:54 -0400
Subject: [PATCH 3/4] Add an inversion theorem unexpectedly syntactic

---
 theories/Core/Syntactic/CoreTypeInversions.v | 15 +++++++++++++++
 theories/Core/Syntactic/System/Lemmas.v      | 16 ++++++++++++++++
 theories/Core/Syntactic/SystemOpt.v          |  8 ++++----
 3 files changed, 35 insertions(+), 4 deletions(-)

diff --git a/theories/Core/Syntactic/CoreTypeInversions.v b/theories/Core/Syntactic/CoreTypeInversions.v
index e7c2e294..97204661 100644
--- a/theories/Core/Syntactic/CoreTypeInversions.v
+++ b/theories/Core/Syntactic/CoreTypeInversions.v
@@ -37,3 +37,18 @@ Qed.
 
 #[export]
 Hint Resolve wf_pi_inversion : mcltt.
+
+Corollary wf_pi_inversion' : forall {Γ A B i},
+    {{ Γ ⊢ Π A B : Type@i }} ->
+    {{ Γ ⊢ A : Type@i }} /\ {{ Γ, A ⊢ B : Type@i }}.
+Proof with mautosolve 4.
+  intros * [j [? []]]%wf_pi_inversion.
+  assert {{ Γ, A ⊢s Wk : Γ }} by mauto 4.
+  assert {{ Γ, A ⊢ Type@j ⊆ Type@j[Wk] }} by mauto 4.
+  assert {{ Γ, A ⊢ Type@j[Wk] ⊆ Type@i[Wk] }} by mauto 4.
+  assert {{ Γ, A ⊢ Type@i[Wk] ⊆ Type@i }} by mauto 4.
+  assert {{ Γ, A ⊢ Type@j ⊆ Type@i }}...
+Qed.
+
+#[export]
+Hint Resolve wf_pi_inversion' : mcltt.
diff --git a/theories/Core/Syntactic/System/Lemmas.v b/theories/Core/Syntactic/System/Lemmas.v
index 4b1eeae4..689f8c74 100644
--- a/theories/Core/Syntactic/System/Lemmas.v
+++ b/theories/Core/Syntactic/System/Lemmas.v
@@ -724,6 +724,22 @@ Qed.
 #[export]
 Hint Resolve typ_subsumption_ge : mcltt.
 
+Lemma typ_subsumption_sub : forall {Γ σ Δ A A'},
+    {{ Γ ⊢s σ : Δ }} ->
+    {{ Δ ⊢ A ⊆ A' }} ->
+    {{ Γ ⊢ A[σ] ⊆ A'[σ] }}.
+Proof.
+  intros * Hsub H.
+  dependent induction H.
+  - etransitivity; [do 2 econstructor; eassumption |].
+    etransitivity; mauto.
+  - mauto.
+  - mauto.
+Qed.
+
+#[export]
+Hint Resolve typ_subsumption_sub : mcltt.
+
 Lemma wf_exp_respects_typ_subsumption : forall {Γ M A A'},
     {{ Γ ⊢ M : A }} ->
     {{ Γ ⊢ A ⊆ A' }} ->
diff --git a/theories/Core/Syntactic/SystemOpt.v b/theories/Core/Syntactic/SystemOpt.v
index 0458b232..35c91f1d 100644
--- a/theories/Core/Syntactic/SystemOpt.v
+++ b/theories/Core/Syntactic/SystemOpt.v
@@ -55,7 +55,7 @@ Corollary wf_app' : forall {Γ M N A B},
 Proof.
   intros.
   gen_presups.
-  assert (exists i, {{ Γ ⊢ A : Type@i }} /\ {{ Γ, A ⊢ B : Type@i }}) as [? []] by eauto using wf_pi_syntactic_inversion.
+  exvar nat ltac:(fun i => assert ({{ Γ ⊢ A : Type@i }} /\ {{ Γ, A ⊢ B : Type@i }}) as [] by eauto using wf_pi_inversion').
   mautosolve 3.
 Qed.
 
@@ -167,7 +167,7 @@ Corollary wf_exp_eq_app_cong' : forall {Γ A B M M' N N'},
 Proof.
   intros.
   gen_presups.
-  assert (exists i, {{ Γ ⊢ A : Type@i }} /\ {{ Γ, A ⊢ B : Type@i }}) as [? []] by eauto using wf_pi_syntactic_inversion.
+  exvar nat ltac:(fun i => assert ({{ Γ ⊢ A : Type@i }} /\ {{ Γ, A ⊢ B : Type@i }}) as [] by eauto using wf_pi_inversion').
   mautosolve 3.
 Qed.
 
@@ -184,7 +184,7 @@ Corollary wf_exp_eq_app_sub' : forall {Γ σ Δ A B M N},
 Proof.
   intros.
   gen_presups.
-  assert (exists i, {{ Δ ⊢ A : Type@i }} /\ {{ Δ, A ⊢ B : Type@i }}) as [? []] by eauto using wf_pi_syntactic_inversion.
+  exvar nat ltac:(fun i => assert ({{ Δ ⊢ A : Type@i }} /\ {{ Δ, A ⊢ B : Type@i }}) as [] by eauto using wf_pi_inversion').
   mautosolve 3.
 Qed.
 
@@ -216,7 +216,7 @@ Corollary wf_exp_eq_pi_eta' : forall {Γ A B M},
 Proof.
   intros.
   gen_presups.
-  assert (exists i, {{ Γ ⊢ A : Type@i }} /\ {{ Γ, A ⊢ B : Type@i }}) as [? []] by eauto using wf_pi_syntactic_inversion.
+  exvar nat ltac:(fun i => assert ({{ Γ ⊢ A : Type@i }} /\ {{ Γ, A ⊢ B : Type@i }}) as [] by eauto using wf_pi_inversion').
   mautosolve 3.
 Qed.
 

From 1271e1918cb883e94d222e2cd9be6f3a1ce8fff5 Mon Sep 17 00:00:00 2001
From: Junyoung/Clare Jang <jjc9310@gmail.com>
Date: Thu, 13 Jun 2024 03:37:13 -0400
Subject: [PATCH 4/4] Rearrange completeness consequences in a clearer
 structure

---
 .../Completeness/Consequences/Inversions.v    |  50 +-------
 .../Core/Completeness/Consequences/Types.v    | 116 ++++++++++++++++++
 theories/Core/Syntactic/System/Lemmas.v       |  24 ++++
 theories/_CoqProject                          |   1 +
 4 files changed, 144 insertions(+), 47 deletions(-)
 create mode 100644 theories/Core/Completeness/Consequences/Types.v

diff --git a/theories/Core/Completeness/Consequences/Inversions.v b/theories/Core/Completeness/Consequences/Inversions.v
index b1fe4ddf..8474be1d 100644
--- a/theories/Core/Completeness/Consequences/Inversions.v
+++ b/theories/Core/Completeness/Consequences/Inversions.v
@@ -1,30 +1,9 @@
 From Coq Require Import RelationClasses.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Completeness Completeness.FundamentalTheorem Completeness.LogicalRelation Semantic.Realizability.
+From Mcltt.Core Require Import Completeness Semantic.Realizability Completeness.Consequences.Types.
 From Mcltt.Core Require Export SystemOpt CoreInversions.
 Import Domain_Notations.
 
-Theorem not_exp_eq_typ_nat : forall Γ i j,
-    ~ {{ Γ ⊢ ℕ ≈ Type@i : Type@j }}.
-Proof.
-  intros ** ?.
-  assert {{ Γ ⊨ ℕ ≈ Type@i : Type@j }} as [env_relΓ] by mauto using completeness_fundamental_exp_eq.
-  destruct_conjs.
-  assert (exists p p', initial_env Γ p /\ initial_env Γ p' /\ {{ Dom p ≈ p' ∈ env_relΓ }}) by mauto using per_ctx_then_per_env_initial_env.
-  destruct_conjs.
-  functional_initial_env_rewrite_clear.
-  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
-  destruct_by_head rel_typ.
-  invert_rel_typ_body.
-  destruct_by_head rel_exp.
-  invert_rel_typ_body.
-  destruct_conjs.
-  match_by_head1 per_univ_elem invert_per_univ_elem.
-Qed.
-
-#[export]
-Hint Resolve not_exp_eq_typ_nat : mcltt.
-
 Corollary wf_zero_inversion : forall Γ A,
     {{ Γ ⊢ zero : A }} ->
     exists i, {{ Γ ⊢ ℕ ≈ A : Type@i }}.
@@ -32,8 +11,7 @@ Proof with mautosolve 4.
   intros * H.
   dependent induction H; try mautosolve.
   - (* wf_conv *)
-    assert (exists i : nat, {{ Γ ⊢ ℕ ≈ A : Type@i }}) as [j] by eauto.
-    mauto using lift_exp_eq_max_left, lift_exp_eq_max_right.
+    assert (exists i : nat, {{ Γ ⊢ ℕ ≈ A : Type@i }}) as [j] by eauto...
   - (* wf_cumu *)
     assert (exists j : nat, {{ Γ ⊢ ℕ ≈ Type@i : Type@j }}) as [j contra] by eauto.
     contradict contra...
@@ -47,34 +25,12 @@ Proof with mautosolve.
   dependent induction H; try (split; mautosolve).
   - (* wf_conv *)
     assert ({{ Γ ⊢ M : ℕ }} /\ exists i : nat, {{ Γ ⊢ ℕ ≈ A : Type@i }}) as [] by eauto.
-    destruct_conjs.
-    mauto 6 using lift_exp_eq_max_left, lift_exp_eq_max_right.
+    destruct_conjs...
   - (* wf_cumu *)
     assert ({{ Γ ⊢ M : ℕ }} /\ exists j : nat, {{ Γ ⊢ ℕ ≈ Type@i : Type@j }}) as [? [? contra]] by eauto.
     contradict contra...
 Qed.
 
-Theorem not_exp_eq_typ_pi : forall Γ i A B j,
-    ~ {{ Γ ⊢ Π A B ≈ Type@i : Type@j }}.
-Proof.
-  intros ** ?.
-  assert {{ Γ ⊨ Π A B ≈ Type@i : Type@j }} as [env_relΓ] by mauto using completeness_fundamental_exp_eq.
-  destruct_conjs.
-  assert (exists p p', initial_env Γ p /\ initial_env Γ p' /\ {{ Dom p ≈ p' ∈ env_relΓ }}) by mauto using per_ctx_then_per_env_initial_env.
-  destruct_conjs.
-  functional_initial_env_rewrite_clear.
-  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
-  destruct_by_head rel_typ.
-  invert_rel_typ_body.
-  destruct_by_head rel_exp.
-  invert_rel_typ_body.
-  destruct_conjs.
-  match_by_head1 per_univ_elem invert_per_univ_elem.
-Qed.
-
-#[export]
-Hint Resolve not_exp_eq_typ_pi : mcltt.
-
 Corollary wf_fn_inversion : forall {Γ A M C},
     {{ Γ ⊢ λ A M : C }} ->
     exists i B, {{ Γ ⊢ A : Type@i }} /\ {{ Γ, A ⊢ B : Type@i }} /\ {{ Γ ⊢ Π A B ≈ C : Type@i }}.
diff --git a/theories/Core/Completeness/Consequences/Types.v b/theories/Core/Completeness/Consequences/Types.v
new file mode 100644
index 00000000..6d1cb9ef
--- /dev/null
+++ b/theories/Core/Completeness/Consequences/Types.v
@@ -0,0 +1,116 @@
+From Coq Require Import RelationClasses.
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core Require Import Completeness Completeness.FundamentalTheorem Completeness.LogicalRelation Semantic.Realizability.
+From Mcltt.Core Require Export SystemOpt.
+Import Domain_Notations.
+
+Lemma exp_eq_typ_implies_eq_level : forall {Γ i j k},
+    {{ Γ ⊢ Type@i ≈ Type@j : Type@k }} ->
+    i = j.
+Proof with mautosolve.
+  intros * H.
+  assert {{ Γ ⊨ Type@i ≈ Type@j : Type@k }} as [env_relΓ] by eauto using completeness_fundamental_exp_eq.
+  destruct_conjs.
+  assert (exists p p', initial_env Γ p /\ initial_env Γ p' /\ {{ Dom p ≈ p' ∈ env_relΓ }}) as [p [? [? []]]] by eauto using per_ctx_then_per_env_initial_env.
+  functional_initial_env_rewrite_clear.
+  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+  destruct_by_head rel_typ.
+  invert_rel_typ_body.
+  destruct_by_head rel_exp.
+  invert_rel_typ_body.
+  destruct_conjs.
+  match_by_head1 per_univ_elem invert_per_univ_elem.
+  reflexivity.
+Qed.
+
+#[export]
+Hint Resolve exp_eq_typ_implies_eq_level : mcltt.
+
+Theorem not_exp_eq_typ_nat : forall Γ i j,
+    ~ {{ Γ ⊢ ℕ ≈ Type@i : Type@j }}.
+Proof.
+  intros ** ?.
+  assert {{ Γ ⊨ ℕ ≈ Type@i : Type@j }} as [env_relΓ] by mauto using completeness_fundamental_exp_eq.
+  destruct_conjs.
+  assert (exists p p', initial_env Γ p /\ initial_env Γ p' /\ {{ Dom p ≈ p' ∈ env_relΓ }}) by mauto using per_ctx_then_per_env_initial_env.
+  destruct_conjs.
+  functional_initial_env_rewrite_clear.
+  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+  destruct_by_head rel_typ.
+  invert_rel_typ_body.
+  destruct_by_head rel_exp.
+  invert_rel_typ_body.
+  destruct_conjs.
+  match_by_head1 per_univ_elem invert_per_univ_elem.
+Qed.
+
+#[export]
+Hint Resolve not_exp_eq_typ_nat : mcltt.
+
+Theorem not_exp_eq_typ_pi : forall Γ i A B j,
+    ~ {{ Γ ⊢ Π A B ≈ Type@i : Type@j }}.
+Proof.
+  intros ** ?.
+  assert {{ Γ ⊨ Π A B ≈ Type@i : Type@j }} as [env_relΓ] by mauto using completeness_fundamental_exp_eq.
+  destruct_conjs.
+  assert (exists p p', initial_env Γ p /\ initial_env Γ p' /\ {{ Dom p ≈ p' ∈ env_relΓ }}) by mauto using per_ctx_then_per_env_initial_env.
+  destruct_conjs.
+  functional_initial_env_rewrite_clear.
+  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+  destruct_by_head rel_typ.
+  invert_rel_typ_body.
+  destruct_by_head rel_exp.
+  invert_rel_typ_body.
+  destruct_conjs.
+  match_by_head1 per_univ_elem invert_per_univ_elem.
+Qed.
+
+#[export]
+Hint Resolve not_exp_eq_typ_pi : mcltt.
+
+Lemma typ_subsumption_spec : forall {Γ A A'},
+    {{ Γ ⊢ A ⊆ A' }} ->
+    {{ ⊢ Γ }} /\ exists j, {{ Γ ⊢ A ≈ A' : Type@j }} \/ exists i i', i < i' /\ {{ Γ ⊢ Type@i ≈ A : Type@j }} /\ {{ Γ ⊢ A' ≈ Type@i' : Type@j }}.
+Proof.
+  intros * H.
+  dependent induction H; split; mauto 3.
+  - (* typ_subsumption_typ *)
+    eexists.
+    right.
+    do 2 eexists.
+    repeat split; revgoals; mauto.
+  - (* typ_subsumption_trans *)
+    destruct IHtyp_subsumption1 as [? [? [| [i1 [i1']]]]]; destruct IHtyp_subsumption2 as [? [? [| [i2 [i2']]]]];
+      destruct_conjs;
+      only 1: mautosolve 4;
+      eexists; right; do 2 eexists.
+    + (* left & right *)
+      split; [eassumption |].
+      solve [mauto using lift_exp_eq_max_left].
+    + (* right & left *)
+      split; [eassumption |].
+      solve [mauto using lift_exp_eq_max_right].
+    + exvar nat ltac:(fun j => assert {{ Γ ⊢ Type@i2 ≈ Type@i1' : Type@j }} by mauto).
+      replace i2 with i1' in * by mauto.
+      split; [etransitivity; revgoals; eassumption |].
+      mauto 4 using lift_exp_eq_max_left, lift_exp_eq_max_right.
+Qed.
+
+#[export]
+Hint Resolve typ_subsumption_spec : mcltt.
+
+Lemma typ_subsumption_typ_spec : forall {Γ i i'},
+    {{ Γ ⊢ Type@i ⊆ Type@i' }} ->
+    {{ ⊢ Γ }} /\ i <= i'.
+Proof with mautosolve.
+  intros * [? [j [| [i0 [i0']]]]]%typ_subsumption_spec.
+  - (* when lhs is equivalent to rhs *)
+    replace i with i' in *...
+  - (* when lhs is (strictly) subsumed by rhs *)
+    destruct_conjs.
+    (on_all_hyp: fun H => apply exp_eq_typ_implies_eq_level in H); subst.
+    split; [| lia]...
+Qed.
+
+#[export]
+Hint Resolve typ_subsumption_typ_spec : mcltt.
diff --git a/theories/Core/Syntactic/System/Lemmas.v b/theories/Core/Syntactic/System/Lemmas.v
index 689f8c74..f374aeec 100644
--- a/theories/Core/Syntactic/System/Lemmas.v
+++ b/theories/Core/Syntactic/System/Lemmas.v
@@ -161,6 +161,19 @@ Qed.
 #[export]
 Hint Resolve sub_eq_refl : mcltt.
 
+Lemma exp_eq_trans_typ_max : forall {Γ i i' A A' A''},
+    {{ Γ ⊢ A ≈ A' : Type@i }} ->
+    {{ Γ ⊢ A' ≈ A'' : Type@i' }} ->
+    {{ Γ ⊢ A ≈ A'' : Type@(max i i') }}.
+Proof with mautosolve 4.
+  intros.
+  assert {{ Γ ⊢ A ≈ A' : Type@(max i i') }} by eauto using lift_exp_eq_max_left.
+  assert {{ Γ ⊢ A' ≈ A'' : Type@(max i i') }} by eauto using lift_exp_eq_max_right...
+Qed.
+
+#[export]
+Hint Resolve exp_eq_trans_typ_max : mcltt.
+
 Lemma exp_sub_typ : forall {Δ Γ A σ i}, {{ Δ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ A[σ] : Type@i }}.
 Proof.
   mauto.
@@ -703,6 +716,17 @@ Qed.
 #[export]
 Hint Resolve sub_eq_q_sigma_compose_weak_weak_extend_succ_var_1 : mcltt.
 
+Lemma typ_subsumption_wf_ctx : forall {Γ A A'},
+    {{ Γ ⊢ A ⊆ A' }} ->
+    {{ ⊢ Γ }}.
+Proof.
+  intros * H.
+  dependent induction H; mauto.
+Qed.
+
+#[export]
+Hint Resolve typ_subsumption_wf_ctx : mcltt.
+
 Fact typ_subsumption_refl : forall {Γ A i},
     {{ Γ ⊢ A : Type@i }} ->
     {{ Γ ⊢ A ⊆ A }}.
diff --git a/theories/_CoqProject b/theories/_CoqProject
index 27bfdded..a8279ce2 100644
--- a/theories/_CoqProject
+++ b/theories/_CoqProject
@@ -4,6 +4,7 @@
 
 ./Core/Axioms.v
 ./Core/Base.v
+./Core/Completeness/Consequences/Types.v
 ./Core/Completeness/Consequences/Inversions.v
 ./Core/Completeness/ContextCases.v
 ./Core/Completeness/FunctionCases.v