From 0bf07450f212db668e388987d98207c382085af7 Mon Sep 17 00:00:00 2001
From: "Junyoung/\"Clare\" Jang" <jjc9310@gmail.com>
Date: Tue, 8 Oct 2024 16:41:24 -0400
Subject: [PATCH] Clean up some modules (#248)

* Remove an unused module

* Reorder some modules
---
 theories/Algorithmic/Typing/Lemmas.v          |  3 +-
 theories/CoqMakefile.mk.local-late            |  3 +-
 .../Core/Completeness/Consequences/Types.v    |  2 +-
 .../Soundness/LogicalRelation/CoreLemmas.v    |  2 +-
 theories/Core/Soundness/Realizability.v       |  2 +-
 theories/Core/Soundness/Weakening.v           |  1 -
 theories/Core/Syntactic/CoreInversions.v      | 82 +++++++++++++++----
 theories/Core/Syntactic/CoreTypeInversions.v  | 58 -------------
 theories/Core/Syntactic/Corollaries.v         | 44 +++++-----
 theories/Core/Syntactic/Presup.v              | 35 ++------
 theories/Core/Syntactic/System/Tactics.v      | 59 ++++++++++++-
 theories/Core/Syntactic/SystemOpt.v           | 43 +++++-----
 theories/_CoqProject                          |  2 -
 13 files changed, 173 insertions(+), 163 deletions(-)
 delete mode 100644 theories/Core/Soundness/Weakening.v
 delete mode 100644 theories/Core/Syntactic/CoreTypeInversions.v

diff --git a/theories/Algorithmic/Typing/Lemmas.v b/theories/Algorithmic/Typing/Lemmas.v
index 39b19a9..ebe95ab 100644
--- a/theories/Algorithmic/Typing/Lemmas.v
+++ b/theories/Algorithmic/Typing/Lemmas.v
@@ -268,8 +268,7 @@ Proof.
     assert {{ Γ ⊢ B'[Id,,N] ⊆ B[Id,,N] }} by mauto 3.
     assert {{ Γ ⊢ W ⊆ B[Id,,N] }} by (transitivity {{{ B'[Id,,N] }}}; mauto 3).
     econstructor; mauto 4 using alg_subtyping_complete.
-  - assert (exists i, {{ Γ ⊢ A : Type@i }}) as [i] by mauto 3.
-    assert (exists W, nbe_ty Γ A W /\ {{ Γ ⊢ A ≈ W : Type@i }}) as [W []] by (eapply soundness_ty; mauto 3).
+  - assert (exists W, nbe_ty Γ A W /\ {{ Γ ⊢ A ≈ W : Type@i }}) as [W []] by (eapply soundness_ty; mauto 3).
     econstructor; mauto 4 using alg_subtyping_complete.
 Qed.
 
diff --git a/theories/CoqMakefile.mk.local-late b/theories/CoqMakefile.mk.local-late
index 2d8af51..bca61b6 100644
--- a/theories/CoqMakefile.mk.local-late
+++ b/theories/CoqMakefile.mk.local-late
@@ -63,4 +63,5 @@ $(DEPGRAPHDOC): $(DEPGRAPHDOT) $(DEPPOSTPROCESSSCRIPT)
 depgraphdoc: $(DEPGRAPHDOC)
 
 clean::
-	@rm $(DEPGRAPHDOT) $(DEPGRAPHDOC)
+	@echo "CLEAN $(DEPGRAPHDOT) $(DEPGRAPHDOC)"
+	@rm -f $(DEPGRAPHDOT) $(DEPGRAPHDOC)
diff --git a/theories/Core/Completeness/Consequences/Types.v b/theories/Core/Completeness/Consequences/Types.v
index 48f3887..f426b64 100644
--- a/theories/Core/Completeness/Consequences/Types.v
+++ b/theories/Core/Completeness/Consequences/Types.v
@@ -3,7 +3,7 @@ From Mcltt Require Import LibTactics.
 From Mcltt.Core Require Import Base.
 From Mcltt.Core Require Export Completeness.
 From Mcltt.Core.Semantic Require Import Realizability.
-From Mcltt.Core.Syntactic Require Export CoreInversions.
+From Mcltt.Core.Syntactic Require Export SystemOpt.
 Import Domain_Notations.
 
 Lemma exp_eq_typ_implies_eq_level : forall {Γ i j k},
diff --git a/theories/Core/Soundness/LogicalRelation/CoreLemmas.v b/theories/Core/Soundness/LogicalRelation/CoreLemmas.v
index 2f7e176..a744fd7 100644
--- a/theories/Core/Soundness/LogicalRelation/CoreLemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/CoreLemmas.v
@@ -841,7 +841,7 @@ Proof.
           mauto 4.
         symmetry.
         bulky_rewrite_in H4.
-        assert {{ Δ0 ⊢ Π IT[σ∘σ0] (OT[q (σ∘σ0)]) ≈ (Π IT OT)[σ∘σ0] : Type@(S (max i4 i)) }} by mauto.
+        assert {{ Δ0 ⊢ Π IT[σ∘σ0] (OT[q (σ∘σ0)]) ≈ (Π IT OT)[σ∘σ0] : Type@_ }} by mauto.
         eapply wf_exp_eq_conv'; mauto 4.
       }
 
diff --git a/theories/Core/Soundness/Realizability.v b/theories/Core/Soundness/Realizability.v
index 494cabe..a928e21 100644
--- a/theories/Core/Soundness/Realizability.v
+++ b/theories/Core/Soundness/Realizability.v
@@ -42,7 +42,7 @@ Lemma var_weaken_gen : forall Δ σ Γ,
       {{ Δ ⊢ #(length Γ1)[σ] ≈ #(length Δ - length Γ2 - 1) : ^(iter (S (length Γ1)) (fun A => {{{ A[Wk] }}}) A0)[σ] }}.
 Proof.
   induction 1; intros; subst; gen_presups.
-  - pose proof (app_ctx_vlookup _ _ _ _ HΔ eq_refl) as Hvar.
+  - pose proof (app_ctx_vlookup _ _ _ _ ltac:(eassumption) eq_refl) as Hvar.
     gen_presup Hvar.
     clear_dups.
     apply wf_sub_id_inversion in Hτ.
diff --git a/theories/Core/Soundness/Weakening.v b/theories/Core/Soundness/Weakening.v
deleted file mode 100644
index 6d758c9..0000000
--- a/theories/Core/Soundness/Weakening.v
+++ /dev/null
@@ -1 +0,0 @@
-From Mcltt.Core.Soundness.Weakening Require Export Definitions Lemmas.
diff --git a/theories/Core/Syntactic/CoreInversions.v b/theories/Core/Syntactic/CoreInversions.v
index e56f113..19da398 100644
--- a/theories/Core/Syntactic/CoreInversions.v
+++ b/theories/Core/Syntactic/CoreInversions.v
@@ -1,9 +1,32 @@
 From Coq Require Import Setoid.
 From Mcltt Require Import LibTactics.
 From Mcltt.Core Require Import Base.
-From Mcltt.Core.Syntactic Require Export SystemOpt.
+From Mcltt.Core.Syntactic Require Export CtxEq.
 Import Syntax_Notations.
 
+Lemma wf_typ_inversion : forall {Γ i A},
+    {{ Γ ⊢ Type@i : A }} ->
+    {{ Γ ⊢ Type@(S i) ⊆ A }}.
+Proof with mautosolve.
+  intros * H.
+  dependent induction H...
+Qed.
+
+#[export]
+Hint Resolve wf_typ_inversion : mcltt.
+
+Lemma wf_nat_inversion : forall Γ A,
+    {{ Γ ⊢ ℕ : A }} ->
+    {{ Γ ⊢ Type@0 ⊆ A }}.
+Proof with mautosolve 4.
+  intros * H.
+  assert (forall i, 0 <= i) by lia.
+  dependent induction H...
+Qed.
+
+#[export]
+Hint Resolve wf_nat_inversion : mcltt.
+
 Corollary wf_zero_inversion : forall Γ A,
     {{ Γ ⊢ zero : A }} ->
     {{ Γ ⊢ ℕ ⊆ A }}.
@@ -37,23 +60,48 @@ Proof with mautosolve.
   pose (A0 := A).
   dependent induction H;
     try (specialize (IHwf_exp1 _ _ _ _ eq_refl));
-    destruct_conjs;
-    assert {{ Γ ⊢s Id : Γ }} by mauto 3;
-    repeat split...
+    destruct_conjs; gen_core_presups; repeat split...
 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 with mautosolve 4.
+  intros * H.
+  dependent induction H;
+    try specialize (IHwf_exp1 _ _ eq_refl);
+    destruct_conjs; gen_core_presups; eexists...
+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 (econstructor; mauto 4).
+  assert {{ Γ, A ⊢ Type@j[Wk] ⊆ Type@i[Wk] }} by mauto 4.
+  assert {{ Γ, A ⊢ Type@i[Wk] ⊆ Type@i }} by (econstructor; mauto 4).
+  enough {{ Γ, A ⊢ Type@j ⊆ Type@i }}...
+Qed.
+
+#[export]
+Hint Resolve wf_pi_inversion' : mcltt.
+
 Corollary wf_fn_inversion : forall {Γ A M C},
     {{ Γ ⊢ λ A M : C }} ->
     exists B, {{ Γ, A ⊢ M : B }} /\ {{ Γ ⊢ Π A B ⊆ C }}.
-Proof with mautosolve 4.
+Proof with solve [mauto using lift_exp_max_left, lift_exp_max_right].
   intros * H.
   dependent induction H;
     try specialize (IHwf_exp1 _ _ eq_refl);
-    destruct_conjs;
-    gen_presups;
+    destruct_conjs; gen_core_presups;
     eexists; split...
 Qed.
 
@@ -63,7 +111,7 @@ Hint Resolve wf_fn_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 }}.
-Proof with mautosolve.
+Proof with mautosolve 4.
   intros * H.
   dependent induction H;
     try specialize (IHwf_exp1 _ _ eq_refl);
@@ -80,10 +128,8 @@ Lemma wf_vlookup_inversion : forall {Γ x A},
 Proof with mautosolve 4.
   intros * H.
   dependent induction H;
-    [assert (exists i, {{ Γ ⊢ A : Type@i }}) as [] by mauto 4 |];
     try (specialize (IHwf_exp1 _ eq_refl));
-    destruct_conjs;
-    eexists; split...
+    destruct_conjs; gen_core_presups; eexists; split...
 Qed.
 
 #[export]
@@ -92,13 +138,13 @@ Hint Resolve wf_vlookup_inversion : mcltt.
 Lemma wf_exp_sub_inversion : forall {Γ M σ A},
     {{ Γ ⊢ M[σ] : A }} ->
     exists Δ A', {{ Γ ⊢s σ : Δ }} /\ {{ Δ ⊢ M : A' }} /\ {{ Γ ⊢ A'[σ] ⊆ A }}.
-Proof with mautosolve.
+Proof with mautosolve 3.
   intros * H.
   dependent induction H;
     try (specialize (IHwf_exp1 _ _ eq_refl));
     destruct_conjs;
-    gen_presups;
-    do 2 eexists; split...
+    do 2 eexists; repeat split; mauto 3.
+  assert (exists j, {{ Δ ⊢ A : Type@j }}) as [] by mauto 2 using presup_exp_typ...
 Qed.
 
 #[export]
@@ -111,7 +157,7 @@ Lemma wf_sub_id_inversion : forall Γ Δ,
     {{ ⊢ Γ ⊆ Δ }}.
 Proof.
   intros * H.
-  dependent induction H; mautosolve.
+  dependent induction H; mautosolve 3.
 Qed.
 
 #[export]
@@ -125,7 +171,7 @@ Proof.
   dependent induction H;
     firstorder;
     progressive_inversion;
-    repeat eexists; mauto.
+    repeat eexists; mautosolve 3.
 Qed.
 
 #[export]
@@ -134,9 +180,9 @@ Hint Resolve wf_sub_weaken_inversion : mcltt.
 Lemma wf_sub_compose_inversion : forall {Γ1 σ1 σ2 Γ3},
     {{ Γ1 ⊢s σ1 ∘ σ2 : Γ3 }} ->
     exists Γ2, {{ Γ1 ⊢s σ2 : Γ2 }} /\ {{ Γ2 ⊢s σ1 : Γ3 }}.
-Proof with mautosolve 4.
+Proof with mautosolve 3.
   intros * H.
-  dependent induction H; mauto.
+  dependent induction H; mauto 3.
   specialize (IHwf_sub _ _ eq_refl).
   destruct_conjs.
   eexists.
diff --git a/theories/Core/Syntactic/CoreTypeInversions.v b/theories/Core/Syntactic/CoreTypeInversions.v
deleted file mode 100644
index bfccffe..0000000
--- a/theories/Core/Syntactic/CoreTypeInversions.v
+++ /dev/null
@@ -1,58 +0,0 @@
-From Coq Require Import Setoid.
-From Mcltt Require Import LibTactics.
-From Mcltt.Core Require Import Base.
-From Mcltt.Core.Syntactic Require Export System.
-Import Syntax_Notations.
-
-Lemma wf_typ_inversion : forall {Γ i A},
-    {{ Γ ⊢ Type@i : A }} ->
-    {{ Γ ⊢ Type@(S i) ⊆ A }}.
-Proof with mautosolve.
-  intros * H.
-  dependent induction H...
-Qed.
-
-#[export]
-Hint Resolve wf_typ_inversion : mcltt.
-
-Lemma wf_nat_inversion : forall Γ A,
-    {{ Γ ⊢ ℕ : A }} ->
-    {{ Γ ⊢ Type@0 ⊆ A }}.
-Proof with mautosolve 4.
-  intros * H.
-  assert (forall i, 0 <= i) by lia.
-  dependent induction H...
-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 with mautosolve 4.
-  intros * H.
-  dependent induction H;
-    try specialize (IHwf_exp1 _ _ eq_refl);
-    destruct_conjs;
-    assert {{ ⊢ Γ }} by mauto 3;
-    eexists; split...
-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 (econstructor; mauto 4).
-  assert {{ Γ, A ⊢ Type@j[Wk] ⊆ Type@i[Wk] }} by mauto 4.
-  assert {{ Γ, A ⊢ Type@i[Wk] ⊆ Type@i }} by (econstructor; mauto 4).
-  enough {{ Γ, A ⊢ Type@j ⊆ Type@i }}...
-Qed.
-
-#[export]
-Hint Resolve wf_pi_inversion' : mcltt.
diff --git a/theories/Core/Syntactic/Corollaries.v b/theories/Core/Syntactic/Corollaries.v
index a0fd7e8..111da3a 100644
--- a/theories/Core/Syntactic/Corollaries.v
+++ b/theories/Core/Syntactic/Corollaries.v
@@ -1,23 +1,23 @@
 From Coq Require Import Setoid Nat.
 From Mcltt Require Import LibTactics.
 From Mcltt.Core Require Import Base.
-From Mcltt.Core.Syntactic Require Export CoreInversions.
+From Mcltt.Core.Syntactic Require Export SystemOpt.
 Import Syntax_Notations.
 
 Corollary sub_id_typ : forall Γ M A,
     {{ Γ ⊢ M : A }} ->
-    {{ Γ ⊢ M : A [ Id ] }}.
+    {{ Γ ⊢ M : A[Id] }}.
 Proof.
   intros.
   gen_presups.
-  econstructor; mauto 4.
+  mauto 4.
 Qed.
 
 #[export]
 Hint Resolve sub_id_typ : mcltt.
 
 Corollary invert_sub_id : forall Γ M A,
-    {{ Γ ⊢ M [ Id ] : A }} ->
+    {{ Γ ⊢ M[Id] : A }} ->
     {{ Γ ⊢ M : A }}.
 Proof.
   intros * [? [? [?%wf_sub_id_inversion []]]]%wf_exp_sub_inversion.
@@ -41,7 +41,7 @@ Qed.
 Hint Resolve invert_sub_id_typ : mcltt.
 
 Lemma invert_compose_id : forall {Γ σ Δ},
-    {{ Γ ⊢s σ ∘ Id : Δ }} ->
+    {{ Γ ⊢s σ∘Id : Δ }} ->
     {{ Γ ⊢s σ : Δ }}.
 Proof.
   intros * [? []]%wf_sub_compose_inversion.
@@ -72,7 +72,7 @@ Open Scope list_scope.
 
 Lemma app_ctx_lookup : forall Δ T Γ n,
     length Δ = n ->
-    {{ #n : ^(iter (S n) (fun T => {{{T [ Wk ]}}}) T) ∈ ^(Δ ++ T :: Γ) }}.
+    {{ #n : ^(iter (S n) (fun T => {{{ T[Wk] }}}) T) ∈ ^(Δ ++ T :: Γ) }}.
 Proof.
   induction Δ; intros; simpl in *; subst; mauto.
 Qed.
@@ -90,15 +90,15 @@ Qed.
 Lemma app_ctx_vlookup : forall Δ T Γ n,
     {{ ⊢ ^(Δ ++ T :: Γ) }} ->
     length Δ = n ->
-    {{ ^(Δ ++ T :: Γ) ⊢ #n : ^(iter (S n) (fun T => {{{T [ Wk ]}}}) T) }}.
+    {{ ^(Δ ++ T :: Γ) ⊢ #n : ^(iter (S n) (fun T => {{{ T[Wk] }}}) T) }}.
 Proof.
   intros. econstructor; auto using app_ctx_lookup.
 Qed.
 
 Lemma sub_q_eq : forall Δ A i Γ σ σ',
-                   {{ Δ ⊢ A : Type@i }} ->
-                   {{ Γ ⊢s σ ≈ σ' : Δ }} ->
-                   {{ Γ, A[σ] ⊢s q σ ≈ q σ' : Δ, A }}.
+    {{ Δ ⊢ A : Type@i }} ->
+    {{ Γ ⊢s σ ≈ σ' : Δ }} ->
+    {{ Γ, A[σ] ⊢s q σ ≈ q σ' : Δ, A }}.
 Proof.
   intros. gen_presup H0.
   econstructor; mauto 3.
@@ -112,7 +112,7 @@ Lemma wf_subtyp_subst_eq : forall Δ A B,
     {{ Δ ⊢ A ⊆ B }} ->
     forall Γ σ σ',
       {{ Γ ⊢s σ ≈ σ' : Δ }} ->
-      {{ Γ ⊢ A [σ] ⊆ B[σ'] }}.
+      {{ Γ ⊢ A[σ] ⊆ B[σ'] }}.
 Proof.
   induction 1; intros * Hσσ'; gen_presup Hσσ'.
   - eapply wf_subtyp_refl'.
@@ -128,7 +128,7 @@ Lemma wf_subtyp_subst : forall Δ A B,
     {{ Δ ⊢ A ⊆ B }} ->
     forall Γ σ,
       {{ Γ ⊢s σ : Δ }} ->
-      {{ Γ ⊢ A [σ] ⊆ B[σ] }}.
+      {{ Γ ⊢ A[σ] ⊆ B[σ] }}.
 Proof.
   intros; mauto 2 using wf_subtyp_subst_eq.
 Qed.
@@ -183,11 +183,11 @@ Qed.
 Hint Resolve exp_succ_sub_rhs : mcltt.
 
 Lemma sub_decompose_q : forall Γ S i σ Δ Δ' τ t,
-  {{Γ ⊢ S : Type@i}} ->
-  {{Δ ⊢s σ : Γ}} ->
-  {{Δ' ⊢s τ : Δ}} ->
-  {{Δ' ⊢ t : S [ σ ] [ τ ]}} ->
-  {{Δ' ⊢s q σ ∘ (τ ,, t) ≈ σ ∘ τ ,, t : Γ, S}}.
+  {{ Γ ⊢ S : Type@i }} ->
+  {{ Δ ⊢s σ : Γ }} ->
+  {{ Δ' ⊢s τ : Δ }} ->
+  {{ Δ' ⊢ t : S[σ][τ] }} ->
+  {{ Δ' ⊢s q σ ∘ (τ ,, t) ≈ σ ∘ τ ,, t : Γ, S }}.
 Proof.
   intros. gen_presups.
   simpl. autorewrite with mcltt.
@@ -205,11 +205,11 @@ Qed.
 Hint Rewrite -> @sub_decompose_q using mauto 4 : mcltt.
 
 Lemma sub_decompose_q_typ : forall Γ S T i σ Δ Δ' τ t,
-  {{Γ, S ⊢ T : Type@i}} ->
-  {{Δ ⊢s σ : Γ}} ->
-  {{Δ' ⊢s τ : Δ}} ->
-  {{Δ' ⊢ t : S [ σ ] [ τ ]}} ->
-  {{Δ' ⊢ T [ σ ∘ τ ,, t ] ≈ T [ q σ ] [ τ ,, t ] : Type@i}}.
+  {{ Γ, S ⊢ T : Type@i }} ->
+  {{ Δ ⊢s σ : Γ }} ->
+  {{ Δ' ⊢s τ : Δ }} ->
+  {{ Δ' ⊢ t : S[σ][τ] }} ->
+  {{ Δ' ⊢ T[σ∘τ,,t] ≈ T[q σ][τ,,t] : Type@i}}.
 Proof.
   intros. gen_presups.
   autorewrite with mcltt.
diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index e7803d9..5deedff 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -3,19 +3,6 @@ From Mcltt.Core Require Import Base.
 From Mcltt.Core.Syntactic Require Export CtxEq.
 Import Syntax_Notations.
 
-#[local]
-Ltac gen_presup_ctx H :=
-  match type of H with
-  | {{ ⊢ ^?Γ ≈ ^?Δ }} =>
-      let HΓ := fresh "HΓ" in
-      let HΔ := fresh "HΔ" in
-      pose proof presup_ctx_eq H as [HΓ HΔ]
-  | {{ ⊢ ^?Γ ⊆ ^?Δ }} =>
-      let HΓ := fresh "HΓ" in
-      let HΔ := fresh "HΔ" in
-      pose proof presup_ctx_sub H as [HΓ HΔ]
-  end.
-
 #[local]
 Ltac gen_presup_IH presup_exp_eq presup_sub_eq presup_subtyp H :=
   match type of H with
@@ -38,16 +25,6 @@ Ltac gen_presup_IH presup_exp_eq presup_sub_eq presup_subtyp H :=
       let HM := fresh "HM" in
       let HN := fresh "HN" in
       pose proof presup_subtyp _ _ _ H as [HΓ [i [HM HN]]]
-  | {{ ^?Γ ⊢ ^?M : ^?A }} =>
-      let HΓ := fresh "HΓ" in
-      let i := fresh "i" in
-      let HAi := fresh "HAi" in
-      pose proof presup_exp H as [HΓ [i HAi]]
-  | {{ ^?Γ ⊢s ^?σ : ^?Δ }} =>
-      let HΓ := fresh "HΓ" in
-      let HΔ := fresh "HΔ" in
-      pose proof presup_sub H as [HΓ HΔ]
-  | _ => gen_presup_ctx H
   end.
 
 Lemma presup_exp_eq : forall {Γ M M' A}, {{ Γ ⊢ M ≈ M' : A }} -> {{ ⊢ Γ }} /\ {{ Γ ⊢ M : A }} /\ {{ Γ ⊢ M' : A }} /\ exists i, {{ Γ ⊢ A : Type@i }}
@@ -55,7 +32,9 @@ with presup_sub_eq : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{
 with presup_subtyp : forall {Γ M M'}, {{ Γ ⊢ M ⊆ M' }} -> {{ ⊢ Γ }} /\ exists i, {{ Γ ⊢ M : Type@i }} /\ {{ Γ ⊢ M' : Type@i }}.
 Proof with mautosolve 4.
   1: set (WkWksucc := {{{ Wk∘Wk ,, succ #1 }}}).
-  all: inversion_clear 1; (on_all_hyp: gen_presup_IH presup_exp_eq presup_sub_eq presup_subtyp);
+  all: inversion_clear 1;
+    (on_all_hyp: gen_presup_IH presup_exp_eq presup_sub_eq presup_subtyp);
+    gen_core_presups;
     clear presup_exp_eq presup_sub_eq presup_subtyp;
     repeat split; mauto 4;
     try (rename B into C); try (rename B' into C'); try (rename A0 into B); try (rename A' into B');
@@ -248,11 +227,7 @@ Proof with mautosolve 4.
     assert {{ Δ, B ⊢ #(S x) : C[Wk] }} by mauto 4.
     enough {{ Γ ⊢ #(S x)[σ ,, N] : C[Wk][σ ,, N] }}...
 
-  - assert (exists i, {{ Δ ⊢ C : Type@i }}) as []...
-
   (** presup_sub_eq cases *)
-  - econstructor...
-
   - assert {{ Γ ⊢ B[σ] ≈ B[σ'] : Type@i }} by mauto 2.
     eapply wf_conv...
 
@@ -279,6 +254,6 @@ Proof with mautosolve 4.
   - mauto.
 Qed.
 
-Ltac gen_presup H := gen_presup_IH @presup_exp_eq @presup_sub_eq @presup_subtyp H.
+Ltac gen_presup H := gen_presup_IH @presup_exp_eq @presup_sub_eq @presup_subtyp H + gen_core_presup H.
 
-Ltac gen_presups := (on_all_hyp: fun H => gen_presup H); invert_wf_ctx; clear_dups.
+Ltac gen_presups := (on_all_hyp: fun H => gen_presup H); invert_wf_ctx; (on_all_hyp: fun H => gen_lookup_presup H); clear_dups.
diff --git a/theories/Core/Syntactic/System/Tactics.v b/theories/Core/Syntactic/System/Tactics.v
index 8ffdb31..fa18175 100644
--- a/theories/Core/Syntactic/System/Tactics.v
+++ b/theories/Core/Syntactic/System/Tactics.v
@@ -19,12 +19,63 @@ Hint Rewrite -> wf_exp_eq_pi_sub using pi_univ_level_tac : mcltt.
 #[local]
 Ltac invert_wf_ctx1 H :=
   match type of H with
-  | {{ ⊢ ^_ , ^_ }} =>
-      let H' := fresh "H" in
-      pose proof H as H';
-      progressive_invert H'
+  | {{ ⊢ ^?Γ, ^?A }} =>
+      let HΓ := fresh "HΓ" in
+      let HAi := fresh "HAi" in
+      pose proof ctx_decomp H as [HΓ HAi];
+      match goal with
+      | _: {{ Γ ⊢ A : Type@_ }} |- _ => clear HAi
+      | _: __mark__ _ {{ Γ ⊢ A : Type@_ }} |- _ => clear HAi
+      | _ =>
+          let i := fresh "i" in
+          let HA := fresh "HA" in
+          destruct HAi as [i HA]
+      end
   end.
 
 Ltac invert_wf_ctx :=
   (on_all_hyp: fun H => invert_wf_ctx1 H);
   clear_dups.
+
+Ltac gen_core_presup H :=
+  match type of H with
+  | {{ ⊢ ^?Γ ≈ ^?Δ }} =>
+      let HΓ := fresh "HΓ" in
+      let HΔ := fresh "HΔ" in
+      pose proof presup_ctx_eq H as [HΓ HΔ]
+  | {{ ⊢ ^?Γ ⊆ ^?Δ }} =>
+      let HΓ := fresh "HΓ" in
+      let HΔ := fresh "HΔ" in
+      pose proof presup_ctx_sub H as [HΓ HΔ]
+  | {{ ^?Γ ⊢ ^?M : ^?A }} =>
+      let HΓ := fresh "HΓ" in
+      let HAi := fresh "HAi" in
+      pose proof presup_exp H as [HΓ HAi];
+      match goal with
+      | _: {{ Γ ⊢ A : Type@_ }} |- _ => clear HAi
+      | _: __mark__ _ {{ Γ ⊢ A : Type@_ }} |- _ => clear HAi
+      | _ =>
+          let i := fresh "i" in
+          let HA := fresh "HA" in
+          destruct HAi as [i HA]
+      end
+  | {{ ^?Γ ⊢s ^?σ : ^?Δ }} =>
+      let HΓ := fresh "HΓ" in
+      let HΔ := fresh "HΔ" in
+      pose proof presup_sub H as [HΓ HΔ]
+  end.
+
+Ltac gen_lookup_presup H :=
+  match type of H with
+  | {{ #?x : ^?A ∈ ^?Γ }} =>
+      match goal with
+      | _: {{ Γ ⊢ A : Type@_ }} |- _ => fail
+      | _: __mark__ _ {{ Γ ⊢ A : Type@_ }} |- _ => fail
+      | _ =>
+          let i := fresh "i" in
+          let HA := fresh "HA" in
+          pose proof presup_ctx_lookup_typ ltac:(eassumption) H as [i HA]
+      end
+  end.
+
+Ltac gen_core_presups := (on_all_hyp: fun H => gen_core_presup H); invert_wf_ctx; (on_all_hyp: fun H => gen_lookup_presup H); clear_dups.
diff --git a/theories/Core/Syntactic/SystemOpt.v b/theories/Core/Syntactic/SystemOpt.v
index 4bda60c..7966abd 100644
--- a/theories/Core/Syntactic/SystemOpt.v
+++ b/theories/Core/Syntactic/SystemOpt.v
@@ -1,7 +1,7 @@
 From Coq Require Import Setoid.
 From Mcltt Require Import LibTactics.
 From Mcltt.Core Require Import Base.
-From Mcltt.Core.Syntactic Require Export CoreTypeInversions Presup.
+From Mcltt.Core.Syntactic Require Export CoreInversions Presup.
 Import Syntax_Notations.
 
 Add Parametric Morphism i Γ : (wf_exp Γ)
@@ -17,14 +17,14 @@ Proof with mautosolve.
 Qed.
 
 Add Parametric Morphism Γ i : (wf_subtyp Γ)
-    with signature (wf_exp_eq Γ {{{Type@i}}}) ==> eq ==> iff as wf_subtyp_morphism_iff1.
+    with signature (wf_exp_eq Γ {{{ Type@i }}}) ==> eq ==> iff as wf_subtyp_morphism_iff1.
 Proof.
   split; intros; gen_presups;
     etransitivity; mauto 4.
 Qed.
 
 Add Parametric Morphism Γ j : (wf_subtyp Γ)
-    with signature eq ==> (wf_exp_eq Γ {{{Type@j}}}) ==> iff as wf_subtyp_morphism_iff2.
+    with signature eq ==> (wf_exp_eq Γ {{{ Type@j }}}) ==> iff as wf_subtyp_morphism_iff2.
 Proof.
   split; intros; gen_presups;
     etransitivity; mauto 3.
@@ -77,7 +77,7 @@ Remove Hints wf_exp_eq_conv : mcltt.
 Corollary wf_ctx_eq_extend' : forall {Γ Δ A A' i},
     {{ ⊢ Γ ≈ Δ }} ->
     {{ Γ ⊢ A ≈ A' : Type@i }} ->
-    {{ ⊢ Γ , A ≈ Δ , A' }}.
+    {{ ⊢ Γ, A ≈ Δ, A' }}.
 Proof.
   intros.
   assert {{ Δ ⊢ A ≈ A' : Type@i }} by mauto.
@@ -106,7 +106,7 @@ Remove Hints wf_nat : mcltt.
 
 Corollary wf_natrec' : forall {Γ A MZ MS M},
     {{ Γ ⊢ MZ : A[Id,,zero] }} ->
-    {{ Γ , ℕ , A ⊢ MS : A[Wk∘Wk,,succ(#1)] }} ->
+    {{ Γ, ℕ, A ⊢ MS : A[Wk∘Wk,,succ #1] }} ->
     {{ Γ ⊢ M : ℕ }} ->
     {{ Γ ⊢ rec M return A | zero -> MZ | succ -> MS end : A[Id,,M] }}.
 Proof.
@@ -120,7 +120,7 @@ Remove Hints wf_natrec : mcltt.
 
 Corollary wf_pi_max : forall {Γ A i B j},
     {{ Γ ⊢ A : Type@i }} ->
-    {{ Γ , A ⊢ B : Type@j }} ->
+    {{ Γ, A ⊢ B : Type@j }} ->
     {{ Γ ⊢ Π A B : Type@(max i j) }}.
 Proof.
   intros.
@@ -133,7 +133,7 @@ Qed.
 Hint Resolve wf_pi_max : mcltt.
 
 Corollary wf_fn' : forall {Γ A M B},
-    {{ Γ , A ⊢ M : B }} ->
+    {{ Γ, A ⊢ M : B }} ->
     {{ Γ ⊢ λ A M : Π A B }}.
 Proof.
   impl_opt_constructor.
@@ -190,9 +190,9 @@ Remove Hints wf_exp_eq_nat_sub : mcltt.
 Hint Rewrite -> wf_exp_eq_nat_sub' using mautosolve 3 : mcltt.
 
 Corollary wf_exp_eq_natrec_cong' : forall {Γ A A' i MZ MZ' MS MS' M M'},
-    {{ Γ , ℕ ⊢ A ≈ A' : Type@i }} ->
+    {{ Γ, ℕ ⊢ A ≈ A' : Type@i }} ->
     {{ Γ ⊢ MZ ≈ MZ' : A[Id,,zero] }} ->
-    {{ Γ , ℕ , A ⊢ MS ≈ MS' : A[Wk∘Wk,,succ(#1)] }} ->
+    {{ Γ, ℕ, A ⊢ MS ≈ MS' : A[Wk∘Wk,,succ #1] }} ->
     {{ Γ ⊢ M ≈ M' : ℕ }} ->
     {{ Γ ⊢ rec M return A | zero -> MZ | succ -> MS end ≈ rec M' return A' | zero -> MZ' | succ -> MS' end : A[Id,,M] }}.
 Proof.
@@ -207,7 +207,7 @@ Remove Hints wf_exp_eq_natrec_cong : mcltt.
 Corollary wf_exp_eq_natrec_sub' : forall {Γ σ Δ A MZ MS M},
     {{ Γ ⊢s σ : Δ }} ->
     {{ Δ ⊢ MZ : A[Id,,zero] }} ->
-    {{ Δ , ℕ , A ⊢ MS : A[Wk∘Wk,,succ(#1)] }} ->
+    {{ Δ, ℕ, A ⊢ MS : A[Wk∘Wk,,succ #1] }} ->
     {{ Δ ⊢ M : ℕ }} ->
     {{ Γ ⊢ rec M return A | zero -> MZ | succ -> MS end[σ] ≈ rec M[σ] return A[q σ] | zero -> MZ[σ] | succ -> MS[q (q σ)] end : A[σ,,M[σ]] }}.
 Proof.
@@ -221,7 +221,7 @@ Remove Hints wf_exp_eq_natrec_sub : mcltt.
 
 Corollary wf_exp_eq_nat_beta_zero' : forall {Γ A MZ MS},
     {{ Γ ⊢ MZ : A[Id,,zero] }} ->
-    {{ Γ , ℕ , A ⊢ MS : A[Wk∘Wk,,succ(#1)] }} ->
+    {{ Γ, ℕ, A ⊢ MS : A[Wk∘Wk,,succ #1] }} ->
     {{ Γ ⊢ rec zero return A | zero -> MZ | succ -> MS end ≈ MZ : A[Id,,zero] }}.
 Proof.
   impl_opt_constructor.
@@ -234,7 +234,7 @@ Remove Hints wf_exp_eq_nat_beta_zero : mcltt.
 
 Corollary wf_exp_eq_nat_beta_succ' : forall {Γ A MZ MS M},
     {{ Γ ⊢ MZ : A[Id,,zero] }} ->
-    {{ Γ , ℕ , A ⊢ MS : A[Wk∘Wk,,succ(#1)] }} ->
+    {{ Γ, ℕ, A ⊢ MS : A[Wk∘Wk,,succ #1] }} ->
     {{ Γ ⊢ M : ℕ }} ->
     {{ Γ ⊢ rec (succ M) return A | zero -> MZ | succ -> MS end ≈ MS[Id,,M,,rec M return A | zero -> MZ | succ -> MS end] : A[Id,,succ M] }}.
 Proof.
@@ -249,12 +249,12 @@ Remove Hints wf_exp_eq_nat_beta_succ : mcltt.
 Corollary wf_exp_eq_pi_sub_max : forall {Γ σ Δ A i B j},
     {{ Γ ⊢s σ : Δ }} ->
     {{ Δ ⊢ A : Type@i }} ->
-    {{ Δ , A ⊢ B : Type@j }} ->
+    {{ Δ, A ⊢ B : Type@j }} ->
     {{ Γ ⊢ (Π A B)[σ] ≈ Π (A[σ]) (B[q σ]) : Type@(max i j) }}.
 Proof.
   intros.
   assert {{ Δ ⊢ A : Type@(max i j) }} by mauto using lift_exp_max_left.
-  assert {{ Δ , A ⊢ B : Type@(max i j) }} by mauto using lift_exp_max_right.
+  assert {{ Δ, A ⊢ B : Type@(max i j) }} by mauto using lift_exp_max_right.
   mauto.
 Qed.
 
@@ -263,7 +263,7 @@ Hint Resolve wf_exp_eq_pi_sub_max : mcltt.
 
 Corollary wf_exp_eq_pi_cong' : forall {Γ A A' B B' i},
     {{ Γ ⊢ A ≈ A' : Type@i }} ->
-    {{ Γ , A ⊢ B ≈ B' : Type@i }} ->
+    {{ Γ, A ⊢ B ≈ B' : Type@i }} ->
     {{ Γ ⊢ Π A B ≈ Π A' B' : Type@i }}.
 Proof.
   impl_opt_constructor.
@@ -276,12 +276,12 @@ Remove Hints wf_exp_eq_pi_cong : mcltt.
 
 Corollary wf_exp_eq_pi_cong_max : forall {Γ A A' i B B' j},
     {{ Γ ⊢ A ≈ A' : Type@i }} ->
-    {{ Γ , A ⊢ B ≈ B' : Type@j }} ->
+    {{ Γ, A ⊢ B ≈ B' : Type@j }} ->
     {{ Γ ⊢ Π A B ≈ Π A' B' : Type@(max i j) }}.
 Proof.
   intros.
   assert {{ Γ ⊢ A ≈ A' : Type@(max i j) }} by eauto using lift_exp_eq_max_left.
-  assert {{ Γ , A ⊢ B ≈ B' : Type@(max i j) }} by eauto using lift_exp_eq_max_right.
+  assert {{ Γ, A ⊢ B ≈ B' : Type@(max i j) }} by eauto using lift_exp_eq_max_right.
   mauto.
 Qed.
 
@@ -290,7 +290,7 @@ Hint Resolve wf_exp_eq_pi_cong_max : mcltt.
 
 Corollary wf_exp_eq_fn_cong' : forall {Γ A A' i B M M'},
     {{ Γ ⊢ A ≈ A' : Type@i }} ->
-    {{ Γ , A ⊢ M ≈ M' : B }} ->
+    {{ Γ, A ⊢ M ≈ M' : B }} ->
     {{ Γ ⊢ λ A M ≈ λ A' M' : Π A B }}.
 Proof.
   impl_opt_constructor.
@@ -303,7 +303,7 @@ Remove Hints wf_exp_eq_fn_cong : mcltt.
 
 Corollary wf_exp_eq_fn_sub' : forall {Γ σ Δ A M B},
     {{ Γ ⊢s σ : Δ }} ->
-    {{ Δ , A ⊢ M : B }} ->
+    {{ Δ, A ⊢ M : B }} ->
     {{ Γ ⊢ (λ A M)[σ] ≈ λ A[σ] M[q σ] : (Π A B)[σ] }}.
 Proof.
   impl_opt_constructor.
@@ -348,7 +348,7 @@ Hint Resolve wf_exp_eq_app_sub' : mcltt.
 Remove Hints wf_exp_eq_app_sub : mcltt.
 
 Corollary wf_exp_eq_pi_beta' : forall {Γ A B M N},
-    {{ Γ , A ⊢ M : B }} ->
+    {{ Γ, A ⊢ M : B }} ->
     {{ Γ ⊢ N : A }} ->
     {{ Γ ⊢ (λ A M) N ≈ M[Id,,N] : B[Id,,N] }}.
 Proof.
@@ -379,10 +379,9 @@ Hint Resolve wf_exp_eq_pi_eta' : mcltt.
 #[export]
 Remove Hints wf_exp_eq_pi_eta : mcltt.
 
-
 Lemma wf_subtyp_pi' : forall Γ A A' B B' i,
     {{ Γ ⊢ A ≈ A' : Type@i }} ->
-    {{ Γ , A' ⊢ B ⊆ B' }} ->
+    {{ Γ, A' ⊢ B ⊆ B' }} ->
     {{ Γ ⊢ Π A B ⊆ Π A' B' }}.
 Proof.
   intros. gen_presups.
diff --git a/theories/_CoqProject b/theories/_CoqProject
index 28bad81..e7e73ad 100644
--- a/theories/_CoqProject
+++ b/theories/_CoqProject
@@ -56,11 +56,9 @@
 ./Core/Soundness/SubtypingCases.v
 ./Core/Soundness/TermStructureCases.v
 ./Core/Soundness/UniverseCases.v
-./Core/Soundness/Weakening.v
 ./Core/Soundness/Weakening/Definitions.v
 ./Core/Soundness/Weakening/Lemmas.v
 ./Core/Syntactic/CoreInversions.v
-./Core/Syntactic/CoreTypeInversions.v
 ./Core/Syntactic/Corollaries.v
 ./Core/Syntactic/CtxEq.v
 ./Core/Syntactic/CtxSub.v