From 6f4fb0d35eb96fc3e6df92c97392d68744d93783 Mon Sep 17 00:00:00 2001
From: "Junyoung/\"Clare\" Jang" <jjc9310@gmail.com>
Date: Tue, 4 Jun 2024 10:21:20 -0400
Subject: [PATCH] Refactoring and optimizing proofs (#98)

* Some refactoring

* Bit more refactoring

* Optimize proofs

* Update minor

* Update Lemmas.v a bit
---
 theories/Core/Semantic/PER/Lemmas.v           |  7 --
 .../Soundness/LogicalRelation/Definitions.v   |  2 +
 .../Core/Soundness/LogicalRelation/Lemmas.v   | 60 +++++-----------
 theories/Core/Soundness/Weakening/Lemmas.v    | 39 ++++------
 theories/Core/Syntactic/Corollaries.v         | 37 ++++++++++
 theories/Core/Syntactic/CtxEq.v               | 14 ++--
 theories/Core/Syntactic/Presup.v              | 71 +++++++++++++------
 theories/Core/Syntactic/System/Lemmas.v       | 64 +++++++++++------
 theories/LibTactics.v                         |  4 +-
 theories/_CoqProject                          |  1 +
 10 files changed, 174 insertions(+), 125 deletions(-)
 create mode 100644 theories/Core/Syntactic/Corollaries.v

diff --git a/theories/Core/Semantic/PER/Lemmas.v b/theories/Core/Semantic/PER/Lemmas.v
index 9f7bbefb..ba11ac85 100644
--- a/theories/Core/Semantic/PER/Lemmas.v
+++ b/theories/Core/Semantic/PER/Lemmas.v
@@ -4,13 +4,6 @@ From Mcltt Require Import Base LibTactics.
 From Mcltt.Core Require Import Evaluation PER.Definitions PER.CoreTactics Readback.
 Import Domain_Notations.
 
-Add Parametric Morphism A : (@all A)
-    with signature forall_relation (fun (x : A) => iff) ==> iff as all_iff_moprhism'.
-Proof.
-  unfold forall_relation.
-  split; intros ** ?; intuition.
-Qed.
-
 Add Parametric Morphism A : PER
     with signature (@relation_equivalence A) ==> iff as PER_morphism.
 Proof.
diff --git a/theories/Core/Soundness/LogicalRelation/Definitions.v b/theories/Core/Soundness/LogicalRelation/Definitions.v
index d136f7ec..d5ece808 100644
--- a/theories/Core/Soundness/LogicalRelation/Definitions.v
+++ b/theories/Core/Soundness/LogicalRelation/Definitions.v
@@ -12,7 +12,9 @@ Global Open Scope predicate_scope.
 Generalizable All Variables.
 
 Notation "'typ_pred'" := (predicate (Tcons ctx (Tcons typ Tnil))).
+Notation "'typ_pred_equivalence'" := (@predicate_equivalence (Tcons ctx (Tcons typ Tnil))).
 Notation "'glu_pred'" := (predicate (Tcons ctx (Tcons exp (Tcons typ (Tcons domain Tnil))))).
+Notation "'glu_pred_equivalence'" := (@predicate_equivalence (Tcons ctx (Tcons exp (Tcons typ (Tcons domain Tnil))))).
 
 Definition univ_typ_pred j i : typ_pred := fun Γ T => {{ Γ ⊢ T ≈ Type@j :  Type@i }}.
 Arguments univ_typ_pred j i Γ T/.
diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
index 3284504d..5c50fb04 100644
--- a/theories/Core/Soundness/LogicalRelation/Lemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -1,11 +1,11 @@
+From Coq Require Import Morphisms Morphisms_Relations.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import System.Definitions Presup CtxEq Evaluation Readback PER.
+From Mcltt.Core Require Import Evaluation PER Presup Readback Syntactic.Corollaries.
 
 From Mcltt.Core.Soundness Require Import LogicalRelation.Definitions.
 From Mcltt.Core.Soundness Require Export Weakening.Lemmas.
 Import Domain_Notations.
 
-
 Lemma glu_nat_per_nat : forall Γ m a,
     glu_nat Γ m a ->
     per_nat a a.
@@ -13,31 +13,6 @@ Proof.
   induction 1; mauto.
 Qed.
 
-Lemma sub_id_typ : forall Γ M A,
-    {{ Γ ⊢ M : A }} ->
-    {{ Γ ⊢ M : A [ Id ] }}.
-Proof.
-  intros. gen_presups. mauto 6.
-Qed.
-
-#[export]
- Hint Resolve invert_id sub_id_typ : mcltt.
-
-Lemma invert_sub_id : forall Γ M A,
-    {{ Γ ⊢ M [ Id ] : A }} ->
-    {{ Γ ⊢ M : A }}.
-Proof.
-  intros. remember {{{ M [ Id ]}}} as M'.
-  gen M.
-  induction H; intros; try congruence;
-    gen_presups;
-    progressive_inversion;
-    mauto.
-Qed.
-
-#[export]
- Hint Resolve invert_sub_id : mcltt.
-
 Lemma glu_nat_escape : forall Γ m a,
     glu_nat Γ m a ->
     {{ ⊢ Γ }} ->
@@ -49,14 +24,14 @@ Proof.
     end.
   assert {{ Γ ⊢w Id : Γ }} by mauto.
   specialize (H (length Γ)).
-  destruct_all.
+  destruct_conjs.
   specialize (H0 _ _ _ H2 H3).
   gen_presups.
   mauto.
 Qed.
 
 #[export]
- Hint Resolve glu_nat_escape : mcltt.
+Hint Resolve glu_nat_escape : mcltt.
 
 Lemma glu_nat_resp_equiv : forall Γ m a,
     glu_nat Γ m a ->
@@ -67,21 +42,19 @@ Proof.
   induction 1; intros; mauto.
   econstructor; trivial.
   intros.
-  specialize (H0 _ _ _ H2 H3).
-  mauto.
+  transitivity {{{ m[σ] }}}; mauto.
 Qed.
 
-
 Lemma glu_nat_per_top : forall Γ m a,
     glu_nat Γ m a ->
     per_top d{{{ ⇓ ℕ a }}} d{{{ ⇓ ℕ a }}}.
 Proof.
-  induction 1; unfold per_top in *; intros; mauto.
+  induction 1; intros s; mauto.
   - specialize (IHglu_nat s).
-    destruct_all.
+    destruct_conjs.
     mauto.
   - specialize (H s).
-    destruct_all.
+    destruct_conjs.
     mauto.
 Qed.
 
@@ -95,21 +68,24 @@ Proof.
   induction 1; intros; progressive_inversion; gen_presups.
   - transitivity {{{ zero [ σ ] }}}; mauto.
   - specialize (IHglu_nat _ _ _ H1 H5).
-    transitivity {{{ (succ m') [ σ ]}}}; [mauto |].
-    transitivity {{{ succ m' [ σ ] }}}; mauto 6.
+    transitivity {{{ (succ m') [ σ ]}}}; mauto.
+    transitivity {{{ succ m' [ σ ] }}}; mauto.
   - mauto.
 Qed.
 
-
 Lemma glu_univ_elem_univ_lvl : forall i P El A B,
     glu_univ_elem i P El A B ->
     forall Γ T,
       P Γ T ->
       {{ Γ ⊢ T : Type@i }}.
 Proof with (simpl in *; destruct_all; gen_presups; trivial).
+  pose proof iff_impl_subrelation.
+  assert (Proper (typ_pred_equivalence ==> pointwise_relation ctx (pointwise_relation typ iff)) id)
+    by apply predicate_equivalence_pointwise.
   induction 1 using glu_univ_elem_ind; intros.
-  - apply H1 in H3...
-  - apply H in H1...
-  - apply H4 in H6. progressive_invert H6...
-  - apply H0 in H2...
+  (* Use [apply_relation_equivalence]-like tactic later *)
+  - rewrite H3 in H5...
+  - rewrite H1 in H3...
+  - rewrite H6 in H8. dir_inversion_by_head pi_typ_pred...
+  - rewrite H2 in H4...
 Qed.
diff --git a/theories/Core/Soundness/Weakening/Lemmas.v b/theories/Core/Soundness/Weakening/Lemmas.v
index 921eb6ef..9c0c9aec 100644
--- a/theories/Core/Soundness/Weakening/Lemmas.v
+++ b/theories/Core/Soundness/Weakening/Lemmas.v
@@ -1,9 +1,9 @@
-Require Import Coq.Program.Equality.
+From Coq Require Import Program.Equality.
 
-From Mcltt Require Import Base System.Definitions System.Lemmas Weakening.Definition Presup CtxEq LibTactics.
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core Require Import CtxEq Presup Syntactic.Corollaries System Weakening.Definition.
 Import Syntax_Notations.
 
-
 Lemma weakening_escape : forall Γ σ Δ,
     {{ Γ ⊢w σ : Δ }} ->
     {{ Γ ⊢s σ : Δ }}.
@@ -16,8 +16,7 @@ Proof.
 Qed.
 
 #[export]
-  Hint Resolve weakening_escape : mcltt.
-
+Hint Resolve weakening_escape : mcltt.
 
 Lemma weakening_resp_equiv : forall Γ σ σ' Δ,
     {{ Γ ⊢w σ : Δ }} ->
@@ -27,7 +26,6 @@ Proof.
   induction 1; mauto.
 Qed.
 
-
 Lemma ctxeq_weakening : forall Γ σ Δ,
     {{ Γ ⊢w σ : Δ }} ->
     forall Γ',
@@ -37,7 +35,6 @@ Proof.
   induction 1; mauto.
 Qed.
 
-
 Lemma weakening_conv : forall Γ σ Δ,
     {{ Γ ⊢w σ : Δ }} ->
     forall Δ',
@@ -55,33 +52,24 @@ Proof.
 Qed.
 
 #[export]
- Hint Resolve weakening_conv : mcltt.
-
-Lemma invert_id : forall Γ Δ,
-    {{ Γ ⊢s Id : Δ }} ->
-    {{ ⊢ Γ ≈ Δ }}.
-Proof.
-  intros. dependent induction H; intros; try congruence; mauto.
-Qed.
-
+Hint Resolve weakening_conv : mcltt.
 
 Lemma weakening_compose : forall Γ' σ' Γ'',
     {{ Γ' ⊢w σ' : Γ'' }} ->
     forall Γ σ,
       {{ Γ ⊢w σ : Γ' }} ->
       {{ Γ ⊢w σ' ∘ σ : Γ'' }}.
-Proof.
+Proof with mautosolve.
   induction 1; intros.
   - gen_presup H.
-    apply invert_id in Hτ.
-    eapply weakening_resp_equiv; [ mauto | ].
-    transitivity {{{ Id ∘ σ0 }}}; mauto.
+    assert {{ ⊢ Γ ≈ Δ }} by mauto.
+    eapply weakening_resp_equiv; [mauto 2 |].
+    transitivity {{{ Id ∘ σ0 }}}...
   - eapply wk_p; [eauto |].
-    apply weakening_escape in H.
-    transitivity {{{ Wk ∘ τ ∘ σ0 }}}; mauto.
+    transitivity {{{ Wk ∘ τ ∘ σ0 }}}; mauto 4.
+    eapply wf_sub_eq_compose_assoc; revgoals...
 Qed.
 
-
 Lemma weakening_id : forall Γ,
     {{ ⊢ Γ }} ->
     {{ Γ ⊢w Id : Γ }}.
@@ -93,8 +81,9 @@ Lemma weakening_wk : forall Γ T,
     {{ ⊢ Γ , T }} ->
     {{ Γ , T ⊢w Wk : Γ }}.
 Proof.
-  intros. eapply wk_p; mauto.
+  intros.
+  econstructor; mautosolve.
 Qed.
 
 #[export]
- Hint Resolve weakening_id weakening_wk : mcltt.
+Hint Resolve weakening_id weakening_wk : mcltt.
diff --git a/theories/Core/Syntactic/Corollaries.v b/theories/Core/Syntactic/Corollaries.v
new file mode 100644
index 00000000..e34f70f2
--- /dev/null
+++ b/theories/Core/Syntactic/Corollaries.v
@@ -0,0 +1,37 @@
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core Require Import CtxEq Presup.
+Import Syntax_Notations.
+
+Corollary invert_id : forall Γ Δ,
+    {{ Γ ⊢s Id : Δ }} ->
+    {{ ⊢ Γ ≈ Δ }}.
+Proof.
+  intros * H.
+  dependent induction H; mauto.
+Qed.
+
+#[export]
+Hint Resolve invert_id : mcltt.
+
+Corollary sub_id_typ : forall Γ M A,
+    {{ Γ ⊢ M : A }} ->
+    {{ Γ ⊢ M : A [ Id ] }}.
+Proof.
+  intros.
+  gen_presups.
+  mauto 6.
+Qed.
+
+#[export]
+Hint Resolve sub_id_typ : mcltt.
+
+Corollary invert_sub_id : forall Γ M A,
+    {{ Γ ⊢ M [ Id ] : A }} ->
+    {{ Γ ⊢ M : A }}.
+Proof.
+  intros * H.
+  dependent induction H; mauto.
+Qed.
+
+#[export]
+Hint Resolve invert_sub_id : mcltt.
diff --git a/theories/Core/Syntactic/CtxEq.v b/theories/Core/Syntactic/CtxEq.v
index 9d3e1ac7..eb83a815 100644
--- a/theories/Core/Syntactic/CtxEq.v
+++ b/theories/Core/Syntactic/CtxEq.v
@@ -40,24 +40,26 @@ Module ctxeq_judg.
     all: inversion_clear 1;
       (on_all_hyp: gen_ctxeq_helper_IH ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper);
       clear ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper;
-      intros * HΓΔ; destruct (presup_ctx_eq HΓΔ); mauto;
+      intros * HΓΔ; destruct (presup_ctx_eq HΓΔ); mauto 4;
       try (rename B into C); try (rename B' into C'); try (rename A0 into B); try (rename A' into B').
     (* ctxeq_exp_helper & ctxeq_exp_eq_helper recursion cases *)
     1,6-8: assert {{ ⊢ Γ, ℕ ≈ Δ, ℕ }} by (econstructor; mautosolve);
       assert {{ Δ, ℕ ⊢ B : Type@i }} by eauto; econstructor...
     (* ctxeq_exp_helper & ctxeq_exp_eq_helper function cases *)
     1-3,5-9: assert {{ Δ ⊢ B : Type@i }} by eauto; assert {{ ⊢ Γ, B ≈ Δ, B }} by mauto;
-      try econstructor; mautosolve.
+      try econstructor...
     (* ctxeq_exp_helper & ctxeq_exp_eq_helper variable cases *)
-    1-2: assert (exists B i, {{ #x : B ∈ Δ }} /\ {{ Γ ⊢ A ≈ B : Type@i }} /\ {{ Δ ⊢ A ≈ B : Type@i }}); destruct_conjs...
+    1-2: assert (exists B i, {{ #x : B ∈ Δ }} /\ {{ Γ ⊢ A ≈ B : Type@i }} /\ {{ Δ ⊢ A ≈ B : Type@i }}); destruct_conjs; mautosolve 4.
     (* ctxeq_sub_helper & ctxeq_sub_eq_helper weakening cases *)
-    2-3: inversion_clear HΓΔ; econstructor...
+    2-3: inversion_clear HΓΔ; econstructor; mautosolve 4.
 
     (* ctxeq_exp_eq_helper variable case *)
     inversion_clear HΓΔ as [|? Δ0 ? ? C'].
     assert (exists D i', {{ #x : D ∈ Δ0 }} /\ {{ Γ0 ⊢ B ≈ D : Type@i' }} /\ {{ Δ0 ⊢ B ≈ D : Type@i' }}) as [D [i0 ?]] by mauto.
     destruct_conjs.
-    assert {{ Δ0, C' ⊢ B[Wk] ≈ D[Wk] : Type @ i0 }}...
+    assert {{ ⊢ Δ0, C' }} by mauto.
+    assert {{ Δ0 ⊢ D ≈ B : Type@i0 }} by mauto.
+    assert {{ Δ0, C' ⊢ D[Wk] ≈ B[Wk] : Type@i0 }}...
   Qed.
 
   Corollary ctxeq_exp : forall {Γ Δ M A}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢ M : A }} -> {{ Δ ⊢ M : A }}.
@@ -98,6 +100,8 @@ Proof with mautosolve.
   assert {{ Γ2 ⊢ T2 : Type@i }} by mauto using lift_exp_max_right.
   assert {{ Γ0 ⊢ T0 ≈ T1 : Type@i }} by mauto using lift_exp_eq_max_left.
   assert {{ Γ2 ⊢ T1 ≈ T2 : Type@i }} by mauto using lift_exp_eq_max_right.
+  assert {{ ⊢ Γ0 ≈ Γ2 }} by mauto.
+  assert {{ Γ0 ⊢ T0 ≈ T2 : Type@i }} by mauto.
   econstructor...
 Qed.
 
diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index 2dd03303..38dc29d8 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -42,7 +42,7 @@ Ltac gen_presup_IH presup_exp presup_exp_eq presup_sub_eq H :=
 Lemma presup_exp : forall {Γ M A}, {{ Γ ⊢ M : A }} -> {{ ⊢ Γ }} /\ exists i, {{ Γ ⊢ A : Type@i }}
 with presup_exp_eq : forall {Γ M M' A}, {{ Γ ⊢ M ≈ M' : A }} -> {{ ⊢ Γ }} /\ {{ Γ ⊢ M : A }} /\ {{ Γ ⊢ M' : A }} /\ exists i, {{ Γ ⊢ A : Type@i }}
 with presup_sub_eq : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Γ }} /\ {{ Γ ⊢s σ : Δ }} /\ {{ Γ ⊢s σ' : Δ }} /\ {{ ⊢ Δ }}.
-Proof with solve [mauto 4].
+Proof with mautosolve 4.
   2: set (WkWksucc := {{{ Wk∘Wk ,, succ #1 }}}).
   all: inversion_clear 1; (on_all_hyp: gen_presup_IH presup_exp presup_exp_eq presup_sub_eq);
       clear presup_exp presup_exp_eq presup_sub_eq;
@@ -68,12 +68,15 @@ Proof with solve [mauto 4].
     enough {{ Γ ⊢ rec N' return B' | zero -> NZ' | succ -> NS' end : B'[Id ,, N'] }}...
 
   - assert {{ Γ ⊢ B[(Id,,N)][σ] ≈ B[(Id,,N)∘σ] : Type@i }} by mauto 4.
-    assert {{ Γ ⊢ B[(Id,,N)∘σ] ≈ B[σ,,N[σ]] : Type@i }} by mauto.
+    assert {{ Γ ⊢s (Id,,N)∘σ ≈ σ,,N[σ] : Δ, ℕ }} by mauto.
+    assert {{ Γ ⊢ B[(Id,,N)∘σ] ≈ B[σ,,N[σ]] : Type@i }} by mauto 4.
     enough {{ Γ ⊢ B[(Id,,N)][σ] ≈ B[σ,,N[σ]] : Type@i }}...
 
   - assert {{ Γ ⊢s Id,,N[σ] : Γ, ℕ }} by mauto.
     assert {{ Γ, ℕ ⊢s q σ : Δ, ℕ }} by mauto.
+    assert {{ Γ, ℕ ⊢ B[q σ] : Type@i }} by mauto.
     assert {{ Γ ⊢ B[q σ][(Id,,N[σ])] ≈ B[q σ∘(Id,,N[σ])] : Type@i }} by mauto.
+    assert {{ Γ ⊢s q σ∘(Id,,N[σ]) ≈ σ,,N[σ] : Δ, ℕ }} by mauto.
     assert {{ Γ ⊢ B[q σ∘(Id,,N[σ])] ≈ B[σ,,N[σ]] : Type@i }} by mauto.
     assert {{ Γ ⊢ B[q σ][Id,,N[σ]] ≈ B[σ,,N[σ]] : Type@i }} by mauto.
     assert {{ Γ ⊢ NZ[σ] : B[Id ,, zero][σ] }} by mauto.
@@ -88,10 +91,12 @@ Proof with solve [mauto 4].
     set (Γ' := {{{ Γ, ℕ, B[q σ] }}}).
     assert {{ Γ' ⊢s q (q σ) : Δ, ℕ, B }} by mauto.
     assert {{ Γ' ⊢s q σ∘WkWksucc ≈ WkWksucc∘q (q σ) : Δ, ℕ }} by mauto.
+    assert {{ Γ' ⊢s WkWksucc : Γ, ℕ }} by mauto.
     assert {{ Γ' ⊢ B[q σ][WkWksucc] ≈ B[WkWksucc][q (q σ)] : Type@i }} by mauto.
-    enough {{ Γ' ⊢ NS[q (q σ)] : B[q σ][WkWksucc] }}; mauto.
+    assert {{ Γ' ⊢ NS[q (q σ)] : B[q σ][WkWksucc] }}...
+
+  - eexists...
 
-  - mauto.
   - set (recN := {{{ rec N return B | zero -> NZ | succ -> NS end }}}).
     set (IdNrecN := {{{ Id ,, N ,, recN }}}).
     assert {{ Γ ⊢ recN : B[Id ,, N] }} by mauto.
@@ -110,9 +115,12 @@ Proof with solve [mauto 4].
     assert {{ Γ ⊢ B[WkWksucc∘IdNrecN] ≈ B[Id ,, succ N] : Type@i }} by mauto 4.
     enough {{ Γ ⊢ B[WkWksucc][IdNrecN] ≈ B[Id ,, succ N] : Type@i }}...
 
+  - eexists...
+
   - mauto.
+
   - mauto.
-  - mauto.
+
   - assert {{ Γ ⊢ B : Type@(max i i0) }} by mauto using lift_exp_max_left.
     assert {{ Γ ⊢ B ≈ B' : Type@(max i i0) }} by mauto using lift_exp_eq_max_left.
     assert {{ Γ, B ⊢ C : Type@(max i i0) }} by mauto using lift_exp_max_right.
@@ -123,8 +131,12 @@ Proof with solve [mauto 4].
 
   - assert {{ Δ ⊢ B : Type@(max i i0) }} by mauto using lift_exp_max_left.
     assert {{ Δ, B ⊢ C : Type@(max i i0) }} by mauto using lift_exp_max_right.
+    assert {{ Γ ⊢ B[σ] : Type@(max i i0) }} by mauto.
+    assert {{ Γ, B[σ] ⊢ C[q σ] : Type@(max i i0) }} by mauto 4.
+    assert {{ Γ ⊢ Π B[σ] C[q σ] : Type@(max i i0) }} by mauto.
     assert {{ Γ ⊢ Π B[σ] C[q σ] ≈ Π B[σ] C[q σ] : Type@(max i i0) }} by mauto.
-    enough {{ Γ ⊢ λ B[σ] N[q σ] : Π B[σ] C[q σ] }}; mauto.
+    assert {{ Γ, B[σ] ⊢ N[q σ] : C[q σ] }} by mauto 4.
+    enough {{ Γ ⊢ λ B[σ] N[q σ] : Π B[σ] C[q σ] }}...
 
   - assert {{ Δ ⊢ B : Type@(max i i0) }} by mauto using lift_exp_max_left.
     assert {{ Δ, B ⊢ C : Type@(max i i0) }} by mauto using lift_exp_max_right...
@@ -139,14 +151,17 @@ Proof with solve [mauto 4].
     assert {{ Γ ⊢ C[(Id ,, L)∘σ] ≈ C[σ ,, L[σ]] : Type@i }} by mauto.
     enough {{ Γ ⊢ C[Id ,, L][σ] ≈ C[σ ,, L[σ]] : Type@i }}...
 
-  - assert {{ Γ ⊢ N[σ] : Π B[σ] C[q σ] }} by mauto.
+  - assert {{ Γ ⊢ B[σ] : Type@i }} by mauto.
+    assert {{ Γ, B[σ] ⊢ C[q σ] : Type@i }} by mauto 4.
+    assert {{ Γ ⊢ N[σ] : Π B[σ] C[q σ] }} by mauto 4.
     assert {{ Γ ⊢ L[σ] : B[σ] }} by mauto.
     assert {{ Γ, B[σ] ⊢s q σ : Δ, B }} by mauto.
     assert {{ Γ ⊢s q σ∘(Id ,, L[σ]) ≈ σ ,, L[σ] : Δ, B }} by mauto.
-    assert {{ Γ ⊢ C[q σ∘(Id ,, L[σ])] ≈ C[σ ,, L[σ]] : Type@i }} by mauto.
-    enough {{ Γ ⊢ C[q σ][(Id ,, L[σ])] ≈ C[σ ,, L[σ]] : Type@i }}; mauto.
+    assert {{ Γ ⊢ C[q σ∘(Id ,, L[σ])] ≈ C[σ ,, L[σ]] : Type@i }} by mauto 4.
+    enough {{ Γ ⊢ C[q σ][(Id ,, L[σ])] ≈ C[σ ,, L[σ]] : Type@i }}...
+
+  - eexists...
 
-  - mauto.
   - set (Id0 := {{{ Id ,, #0 }}}).
     assert {{ Γ, B ⊢ B[Wk] : Type@i }} by mauto.
     assert {{ Γ, B, B[Wk] ⊢ C[q Wk] : Type@i }} by mauto.
@@ -159,10 +174,14 @@ Proof with solve [mauto 4].
     assert {{ Γ, B ⊢ #0 : B[Wk][Id] }} by mauto 4.
     assert {{ Γ, B ⊢s Id0 : Γ, B, B[Wk] }} by mauto.
     assert {{ Γ, B ⊢s Wk : Γ }} by mauto.
-    assert {{ Γ, B ⊢s Wk∘Id0 ≈ Id : Γ, B }} by mauto.
+    assert {{ Γ, B ⊢s Wk∘Id : Γ }} by mauto.
+    assert {{ Γ, B ⊢s (Wk∘Wk)∘Id0 : Γ }} by mauto.
+    assert {{ Γ, B, B[Wk] ⊢s Wk : Γ, B }} by mauto.
+    assert {{ Γ, B ⊢s Id ≈ Wk∘Id0 : Γ, B }} by mauto.
+    assert {{ Γ, B ⊢s Wk∘Id ≈ Wk∘(Wk∘Id0) : Γ }} by mauto.
     assert {{ Γ, B ⊢s Wk∘Id ≈ (Wk∘Wk)∘Id0 : Γ }} by mauto.
-    assert {{ Γ, B, B[Wk] ⊢ #0 : B[Wk][Wk] }} by mauto.
-    assert {{ Γ, B, B[Wk] ⊢ #0 : B[Wk∘Wk] }} by mauto.
+    assert {{ Γ, B, B[Wk] ⊢ #0 : B[Wk][Wk] }} by mauto 4.
+    assert {{ Γ, B, B[Wk] ⊢ #0 : B[Wk∘Wk] }} by mauto 3.
     assert {{ Γ, B ⊢s q Wk ∘ Id0 ≈ (Wk∘Wk)∘Id0 ,, #0[Id0] : Γ, B }} by mauto.
     assert {{ Γ, B ⊢s (Wk∘Wk)∘Id0 ≈ Wk∘(Wk∘Id0) : Γ }} by mauto.
     assert {{ Γ, B ⊢s (Wk∘Wk)∘Id0 ≈ Wk∘Id : Γ }} by mauto.
@@ -170,25 +189,27 @@ Proof with solve [mauto 4].
     assert {{ Γ, B ⊢ #0 ≈ #0[Id] : B[Wk][Id] }} by mauto.
     assert {{ Γ, B ⊢ #0[Id0] ≈ #0[Id] : B[Wk][Id] }} by mauto.
     assert {{ Γ, B ⊢ #0[Id0] ≈ #0[Id] : B[Wk∘Id] }} by mauto 4.
+    assert {{ Γ, B ⊢ B[Wk∘Id] ≈ B[(Wk∘Wk)∘Id0] : Type@i }} by mauto.
     assert {{ Γ, B ⊢ #0[Id0] ≈ #0[Id] : B[(Wk∘Wk)∘Id0] }} by mauto.
     assert {{ Γ, B ⊢s (Wk∘Wk)∘Id0 ,, #0[Id0] ≈ Wk∘Id ,, #0[Id] : Γ, B }} by mauto.
     assert {{ Γ, B ⊢s Wk∘Id ,, #0[Id] ≈ Id : Γ, B }} by mauto.
     assert {{ Γ, B ⊢s q Wk ∘ Id0 ≈ Id : Γ, B }} by mauto.
-    assert {{ Γ, B ⊢ M[Wk] #0 : C[Id] }} by mauto.
+    assert {{ Γ, B ⊢ C[q Wk ∘ Id0] ≈ C[Id] : Type@i }} by mauto 4.
     enough {{ Γ, B ⊢ M[Wk] #0 : C }}...
 
   - assert {{ Γ ⊢s Wk∘(σ ,, N') ≈ σ : Δ }} by mauto.
     assert {{ Γ ⊢ B[Wk∘(σ ,, N')] ≈ B[σ] : Type@i }} by mauto.
+    assert {{ ⊢ Δ, B }} by mauto.
     assert {{ Δ, B ⊢s Wk : Δ }} by mauto.
     assert {{ Γ ⊢ B[Wk][σ ,, N'] ≈ B[σ] : Type@i }} by mauto 4.
-    enough {{ Γ ⊢ #0[σ ,, N'] : B[Wk][σ ,, N'] }}; mauto.
+    enough {{ Γ ⊢ #0[σ ,, N'] : B[Wk][σ ,, N'] }}...
 
-  - assert (exists i, {{ Δ ⊢ C : Type@i }}) as [i'] by mauto.
+  - assert (exists i, {{ Δ ⊢ C : Type@i }}) as [i'] by mauto 4.
     assert {{ Γ ⊢s Wk∘(σ ,, N) ≈ σ : Δ }} by mauto.
     assert {{ Γ ⊢ C[Wk∘(σ ,, N)] ≈ C[σ] : Type@i' }} by mauto.
     assert {{ Δ, B ⊢s Wk : Δ }} by mauto.
-    assert {{ Γ ⊢ C[Wk][σ ,, N] ≈ C[σ] : Type@i' }} by mauto.
-    assert {{ Δ, B ⊢ #(S x) : C[Wk] }} by mauto.
+    assert {{ Γ ⊢ C[Wk][σ ,, N] ≈ C[σ] : Type@i' }} by mauto 4.
+    assert {{ Δ, B ⊢ #(S x) : C[Wk] }} by mauto 4.
     enough {{ Γ ⊢ #(S x)[σ ,, N] : C[Wk][σ ,, N] }}...
 
   - assert (exists i, {{ Δ ⊢ C : Type@i }}) as []...
@@ -196,11 +217,15 @@ Proof with solve [mauto 4].
   (* presup_sub_eq cases *)
   - econstructor...
 
-  - mauto.
-  - mauto.
-  - mauto.
-  - econstructor; mauto 4.
-  - mauto.
+  - assert {{ Γ ⊢ B[σ] ≈ B[σ'] : Type@i }}...
+
+  - assert {{ Γ ⊢ N'[Id] : A[Id] }}...
+
+  - assert {{ Γ ⊢ N[σ][τ] : B[σ][τ] }}...
+
+  - econstructor...
+
+  - assert {{ ⊢ Δ, A }}...
 
   - assert (exists i, {{ Γ0 ⊢ A : Type@i }}) as [] by mauto.
     assert {{ Γ ⊢ #0[σ] : A[Wk][σ] }} by mauto.
diff --git a/theories/Core/Syntactic/System/Lemmas.v b/theories/Core/Syntactic/System/Lemmas.v
index a0ff08fc..1abaa453 100644
--- a/theories/Core/Syntactic/System/Lemmas.v
+++ b/theories/Core/Syntactic/System/Lemmas.v
@@ -125,7 +125,7 @@ Qed.
 Hint Resolve presup_sub_eq_ctx presup_sub_eq_ctx_left presup_sub_eq_ctx_right : mcltt.
 
 Lemma presup_exp_eq_ctx : forall {Γ M M' A}, {{ Γ ⊢ M ≈ M' : A }} -> {{ ⊢ Γ }}.
-Proof with mautosolve.
+Proof with (mautosolve 2).
   induction 1...
 Qed.
 
@@ -188,10 +188,10 @@ Proof with mautosolve.
 Qed.
 
 Lemma vlookup_1_typ : forall {Γ i A j}, {{ ⊢ Γ }} -> {{ Γ, Type@i ⊢ A : Type@j }} -> {{ Γ, Type@i, A ⊢ # 1 : Type@i }}.
-Proof with mautosolve.
+Proof with mautosolve 4.
   intros.
-  assert {{ ⊢ Γ, Type@i }} by mauto.
-  assert {{ ⊢ Γ, Type@i, A }} by mautosolve.
+  assert {{ ⊢ Γ, Type@i }} by mauto 4.
+  assert {{ ⊢ Γ, Type@i, A }} by mauto 4.
   eapply wf_conv...
 Qed.
 
@@ -199,15 +199,15 @@ Qed.
 Hint Resolve vlookup_0_typ vlookup_1_typ : mcltt.
 
 Lemma exp_eq_var_0_sub_typ : forall {Γ σ Δ M i}, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ M : Type@i }} -> {{ Γ ⊢ #0[σ ,, M] ≈ M : Type@i }}.
-Proof with mautosolve.
+Proof with mautosolve 4.
   intros.
-  assert {{ ⊢ Δ }} by mautosolve.
-  assert {{ Γ ⊢ M : Type@i[σ] }} by mautosolve.
+  assert {{ ⊢ Δ }} by mauto 4.
+  assert {{ Γ ⊢ M : Type@i[σ] }} by mauto 4.
   eapply wf_exp_eq_conv...
 Qed.
 
 Lemma exp_eq_var_1_sub_typ : forall {Γ σ Δ A i M j}, {{ Γ ⊢s σ : Δ }} -> {{ Δ ⊢ A : Type@i }} -> {{ Γ ⊢ M : A[σ] }} -> {{ #0 : Type@j[Wk] ∈ Δ }} -> {{ Γ ⊢ #1[σ ,, M] ≈ #0[σ] : Type@j }}.
-Proof with mautosolve.
+Proof with mautosolve 4.
   inversion 4 as [? Δ'|]; subst.
   assert {{ ⊢ Δ' }} by mauto.
   eapply wf_exp_eq_conv...
@@ -316,17 +316,19 @@ Qed.
 Hint Resolve exp_eq_nat_sub_sub_to_nat_sub : mcltt.
 
 Lemma vlookup_0_nat : forall {Γ}, {{ ⊢ Γ }} -> {{ Γ, ℕ ⊢ # 0 : ℕ }}.
-Proof with mautosolve.
+Proof with mautosolve 4.
   intros.
+  assert {{ ⊢ Γ, ℕ }} by mautosolve 3.
   assert {{ Γ, ℕ ⊢ # 0 : ℕ[Wk] }}...
 Qed.
 
 Lemma vlookup_1_nat : forall {Γ A i}, {{ ⊢ Γ }} -> {{ Γ, ℕ ⊢ A : Type@i }} -> {{ Γ, ℕ, A ⊢ # 1 : ℕ }}.
-Proof with mautosolve.
+Proof with mautosolve 4.
   intros.
   assert {{ ⊢ Γ, ℕ }} by mautosolve.
   assert {{ ⊢ Γ, ℕ, A }} by mautosolve.
-  assert {{ Γ, ℕ, A ⊢ #1 : ℕ[Wk][Wk] }}...
+  assert {{ Γ, ℕ, A ⊢ #1 : ℕ[Wk][Wk] }} by mauto.
+  assert {{ Γ, ℕ, A ⊢ ℕ[Wk][Wk] ≈ ℕ : Type@0 }}...
 Qed.
 
 #[export]
@@ -337,14 +339,16 @@ Proof with mautosolve.
   intros.
   assert {{ ⊢ Δ }} by mauto.
   assert {{ Γ ⊢ M : ℕ[σ] }} by mautosolve.
-  assert {{ Γ ⊢ #0[σ,, M] ≈ M : ℕ[σ] }}...
+  assert {{ Γ ⊢ #0[σ,, M] ≈ M : ℕ[σ] }} by mautosolve.
+  assert {{ Γ ⊢ ℕ[σ] ≈ ℕ : Type@0 }}...
 Qed.
 
 Lemma exp_eq_var_1_sub_nat : forall {Γ σ Δ A i M}, {{ Γ ⊢s σ : Δ }} -> {{ Δ ⊢ A : Type@i }} -> {{ Γ ⊢ M : A[σ] }} -> {{ #0 : ℕ[Wk] ∈ Δ }} -> {{ Γ ⊢ #1[σ ,, M] ≈ #0[σ] : ℕ }}.
 Proof with mautosolve.
   inversion 4 as [? Δ'|]; subst.
   assert {{ ⊢ Δ' }} by mauto.
-  assert {{ Γ ⊢ #1[σ,, M] ≈ #0[σ] : ℕ[Wk][σ] }}...
+  assert {{ Γ ⊢ #1[σ,, M] ≈ #0[σ] : ℕ[Wk][σ] }} by mauto.
+  assert {{ Γ ⊢ ℕ[Wk][σ] ≈ ℕ : Type@0 }}...
 Qed.
 
 #[export]
@@ -355,7 +359,8 @@ Proof with mautosolve.
   inversion 1; subst.
   inversion 1 as [? Γ'|]; subst.
   assert {{ ⊢ Γ' }} by mauto.
-  assert {{ Γ', ℕ, A ⊢ #0[Wk] ≈ # 1 : ℕ[Wk][Wk] }}...
+  assert {{ Γ', ℕ, A ⊢ #0[Wk] ≈ # 1 : ℕ[Wk][Wk] }} by mauto.
+  assert {{ Γ', ℕ, A ⊢ ℕ[Wk][Wk] ≈ ℕ : Type@0 }}...
 Qed.
 
 #[export]
@@ -388,7 +393,7 @@ Lemma sub_eq_p_extend_nat : forall {Γ σ Γ' M}, {{ Γ' ⊢s σ : Γ }} -> {{ 
 Proof with mautosolve.
   intros.
   assert {{ ⊢ Γ }} by mauto.
-  econstructor; only 3: mautosolve...
+  econstructor; revgoals...
 Qed.
 
 #[export]
@@ -420,7 +425,9 @@ Hint Resolve exp_eq_sub_sub_compose_cong : mcltt.
 Lemma ctx_lookup_wf : forall {Γ A x}, {{ ⊢ Γ }} -> {{ #x : A ∈ Γ }} -> exists i, {{ Γ ⊢ A : Type@i }}.
 Proof with mautosolve.
   intros * HΓ.
-  induction 1; inversion_clear HΓ; [|assert (exists i, {{ Γ ⊢ A : Type@i }}) as [] by eauto]...
+  induction 1; inversion_clear HΓ;
+    [assert {{ Γ, A ⊢ Type@i[Wk] ≈ Type@i : Type@(S i) }} by mauto 4
+    | assert (exists i, {{ Γ ⊢ A : Type@i }}) as [] by eauto]; econstructor...
 Qed.
 
 #[export]
@@ -457,8 +464,10 @@ Hint Resolve sub_eq_p_id_extend : mcltt.
 Lemma sub_q : forall {Γ A i σ Δ}, {{ Δ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ , A[σ] ⊢s q σ : Δ , A }}.
 Proof with mautosolve.
   intros.
-  assert {{ Γ, A[σ] ⊢ # 0 : A[σ][Wk] }} by mauto.
-  econstructor...
+  assert {{ Γ ⊢ A[σ] : Type@i }} by mauto.
+  assert {{ ⊢ Γ, A[σ] }} by mauto 3.
+  assert {{ Γ, A[σ] ⊢s Wk : Γ }} by mauto.
+  assert {{ Γ, A[σ] ⊢ # 0 : A[σ][Wk] }} by mauto...
 Qed.
 
 Lemma sub_q_typ : forall {Γ σ Δ i}, {{ Γ ⊢s σ : Δ }} -> {{ Γ , Type@i ⊢s q σ : Δ , Type@i }}.
@@ -491,6 +500,8 @@ Proof with mautosolve.
   assert {{ ⊢ Γ, ℕ }} by mauto.
   assert {{ Γ, ℕ ⊢s q σ : Δ, ℕ }} by mauto.
   assert {{ ⊢ Γ, ℕ, A[q σ] }} by mauto.
+  assert {{ Γ, ℕ, A[q σ] ⊢ #0 : A[q σ][Wk] }} by mauto.
+  assert {{ Γ, ℕ, A[q σ] ⊢ #0 : A[q σ∘Wk] }} by mauto 4.
   assert {{ Γ, ℕ, A[q σ] ⊢ #1[q (q σ)] ≈ #0[q σ∘Wk] : ℕ }} by (eapply exp_eq_var_1_sub_nat; mauto).
   assert {{ Γ, ℕ, A[q σ] ⊢ #0[q σ∘Wk] ≈ #0[q σ][Wk] : ℕ }} by mauto.
   assert {{ Γ, ℕ ⊢ #0[q σ] ≈ #0 : ℕ }} by mauto.
@@ -549,8 +560,9 @@ Lemma sub_eq_q_sigma_id_extend : forall {Γ M A i σ Δ}, {{ Δ ⊢ A : Type@i }
 Proof with mautosolve.
   intros.
   assert {{ Γ ⊢s Id ,, M : Γ, A[σ] }} by mauto.
+  assert {{ Γ, A[σ] ⊢s Wk : Γ }} by mauto.
   assert {{ Γ, A[σ] ⊢ #0 : A[σ][Wk] }} by mauto.
-  assert {{ Γ, A[σ] ⊢ #0 : A[σ∘Wk] }} by mauto.
+  assert {{ Γ, A[σ] ⊢ #0 : A[σ∘Wk] }} by mauto 3.
   assert {{ Γ ⊢s q σ∘(Id ,, M) ≈ (σ∘Wk)∘(Id ,, M) ,, #0[Id ,, M] : Δ, A }} by mauto.
   assert {{ Γ ⊢s (σ∘Wk)∘(Id ,, M) ≈ σ : Δ }} by mauto.
   assert {{ Γ ⊢ M : A[σ][Id] }} by mauto.
@@ -563,9 +575,10 @@ Qed.
 Hint Resolve sub_eq_q_sigma_id_extend : mcltt.
 
 Lemma sub_eq_p_q_sigma : forall {Γ A i σ Δ}, {{ Δ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ, A[σ] ⊢s Wk∘q σ ≈ σ∘Wk : Δ }}.
-Proof with mautosolve.
+Proof with mautosolve 3.
   intros.
   assert {{ ⊢ Γ }} by mauto.
+  assert {{ Γ, A[σ] ⊢s Wk : Γ }} by mauto.
   assert {{ Γ, A[σ] ⊢ #0 : A[σ][Wk] }} by mauto.
   assert {{ Γ, A[σ] ⊢ #0 : A[σ∘Wk] }}...
 Qed.
@@ -608,8 +621,11 @@ Proof with mautosolve.
   set (WkWksucc := {{{ Wk∘Wk ,, succ #1 }}}).
   assert {{ Γ' ⊢s Wk ∘ Wk : Γ }} by mauto.
   assert {{ Γ' ⊢s WkWksucc : Γ, ℕ }} by mauto.
+  assert {{ Γ, ℕ ⊢ #0 : ℕ }} by mauto.
   assert {{ Γ' ⊢s q σ∘WkWksucc ≈ (σ∘Wk)∘WkWksucc ,, #0[WkWksucc] : Δ, ℕ }} by mautosolve.
-  assert {{ Γ' ⊢ #1 : ℕ }} by mauto.
+  assert {{ Γ' ⊢ #1 : ℕ[Wk][Wk] }} by mauto.
+  assert {{ Γ' ⊢ ℕ[Wk][Wk] ≈ ℕ : Type@0 }} by mauto.
+  assert {{ Γ' ⊢ #1 : ℕ }} by mauto 3.
   assert {{ Γ' ⊢ succ #1 : ℕ }} by mauto.
   assert {{ Γ' ⊢s Wk∘WkWksucc ≈ Wk∘Wk : Γ }} by mauto.
   assert {{ Γ' ⊢s (σ∘Wk)∘WkWksucc ≈ σ∘(Wk∘Wk) : Δ }} by mauto.
@@ -625,7 +641,11 @@ Proof with mautosolve.
   assert {{ Γ' ⊢ #0[WkWksucc] ≈ (succ #1)[q (q σ)] : ℕ }} by mauto.
   assert {{ Γ' ⊢s (σ∘Wk)∘WkWksucc ,, #0[WkWksucc] ≈ (Wk∘Wk)∘q (q σ) ,, (succ #1)[q (q σ)] : Δ, ℕ }} by mauto.
   assert {{ Δ, ℕ, A ⊢s Wk∘Wk : Δ }} by mauto.
-  assert {{ Δ, ℕ, A ⊢ #1 : ℕ }} by mauto.
+  assert {{ Δ, ℕ, A ⊢ #1 : ℕ[Wk][Wk] }} by mauto 4.
+  assert {{ ⊢ Δ, ℕ }} by mauto 2.
+  assert {{ ⊢ Δ, ℕ, A }} by mauto 2.
+  assert {{ Δ, ℕ, A ⊢ ℕ[Wk][Wk] ≈ ℕ : Type@0 }} by mauto 3.
+  assert {{ Δ, ℕ, A ⊢ #1 : ℕ }} by mauto 3.
   assert {{ Δ, ℕ, A ⊢ succ #1 : ℕ }} by mauto.
   assert {{ Γ' ⊢s (Wk∘Wk)∘q (q σ) ,, (succ #1)[q (q σ)] ≈ WkWksucc∘q (q σ) : Δ, ℕ }}...
 Qed.
diff --git a/theories/LibTactics.v b/theories/LibTactics.v
index e0801c70..66de8cea 100644
--- a/theories/LibTactics.v
+++ b/theories/LibTactics.v
@@ -200,8 +200,10 @@ Tactic Notation "mauto" int_or_var(pow) "using" uconstr(use1) "," uconstr(use2)
 Tactic Notation "mauto" int_or_var(pow) "using" uconstr(use1) "," uconstr(use2) "," uconstr(use3) "," uconstr(use4) :=
   eauto pow using use1, use2, use3, use4 with mcltt core.
 
-Ltac mautosolve := unshelve solve [mauto]; solve [constructor].
+Ltac mautosolve_impl pow := unshelve solve [mauto pow]; solve [constructor].
 
+Tactic Notation "mautosolve" := mautosolve_impl integer:(5).
+Tactic Notation "mautosolve" int_or_var(pow) := mautosolve_impl pow.
 
 (* Improve type class resolution *)
 
diff --git a/theories/_CoqProject b/theories/_CoqProject
index fbb45948..f698e76b 100644
--- a/theories/_CoqProject
+++ b/theories/_CoqProject
@@ -30,6 +30,7 @@
 ./Core/Semantic/Readback/Lemmas.v
 ./Core/Semantic/Realizability.v
 ./Core/Semantic/NbE.v
+./Core/Syntactic/Corollaries.v
 ./Core/Syntactic/CtxEq.v
 ./Core/Syntactic/Presup.v
 ./Core/Syntactic/Syntax.v