From eef8e4890014dfb76171f0f7306048b599c16fc3 Mon Sep 17 00:00:00 2001
From: "Junyoung/\"Clare\" Jang" <jjc9310@gmail.com>
Date: Fri, 10 May 2024 16:31:44 -0400
Subject: [PATCH] Update some proofs (#77)

---
 theories/Core/Semantic/Evaluation/Lemmas.v |   8 +-
 theories/Core/Semantic/PER/Lemmas.v        |  77 +++--
 theories/Core/Semantic/Realizability.v     |  33 +--
 theories/Core/Syntactic/CtxEq.v            |  99 +++----
 theories/Core/Syntactic/Presup.v           | 312 ++++++++++-----------
 theories/Core/Syntactic/System/Lemmas.v    | 254 +++++++----------
 theories/LibTactics.v                      |   2 +
 7 files changed, 339 insertions(+), 446 deletions(-)

diff --git a/theories/Core/Semantic/Evaluation/Lemmas.v b/theories/Core/Semantic/Evaluation/Lemmas.v
index ca603fcc..6aaca52f 100644
--- a/theories/Core/Semantic/Evaluation/Lemmas.v
+++ b/theories/Core/Semantic/Evaluation/Lemmas.v
@@ -14,7 +14,7 @@ Section functional_eval.
     clear functional_eval_exp_prop functional_eval_natrec_prop functional_eval_app_prop functional_eval_sub_prop.
 
   Lemma functional_eval_exp : forall M p m1 (Heval1 : {{ ⟦ M ⟧ p ↘ m1 }}), functional_eval_exp_prop M p m1 Heval1.
-  Proof with ((on_all_hyp: fun H => erewrite H in *; eauto); eauto) using.
+  Proof with ((on_all_hyp: fun H => erewrite H in *; eauto); solve [eauto]) using.
     induction Heval1
       using eval_exp_mut_ind
       with (P0 := functional_eval_natrec_prop)
@@ -25,7 +25,7 @@ Section functional_eval.
   Qed.
 
   Lemma functional_eval_natrec : forall A MZ MS m p r1 (Heval1 : {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r1 }}), functional_eval_natrec_prop A MZ MS m p r1 Heval1.
-  Proof with ((on_all_hyp: fun H => erewrite H in *; eauto); eauto) using.
+  Proof with ((on_all_hyp: fun H => erewrite H in *; eauto); solve [eauto]) using.
     induction Heval1
       using eval_natrec_mut_ind
       with (P := functional_eval_exp_prop)
@@ -36,7 +36,7 @@ Section functional_eval.
   Qed.
 
   Lemma functional_eval_app : forall m n r1 (Heval1 : {{ $| m & n |↘ r1 }}), functional_eval_app_prop m n r1 Heval1.
-  Proof with ((on_all_hyp: fun H => erewrite H in *; eauto); eauto) using.
+  Proof with ((on_all_hyp: fun H => erewrite H in *; eauto); solve [eauto]) using.
     induction Heval1
       using eval_app_mut_ind
       with (P := functional_eval_exp_prop)
@@ -47,7 +47,7 @@ Section functional_eval.
   Qed.
 
   Lemma functional_eval_sub : forall σ p p1 (Heval1 : {{ ⟦ σ ⟧s p ↘ p1 }}), functional_eval_sub_prop σ p p1 Heval1.
-  Proof with ((on_all_hyp: fun H => erewrite H in *; eauto); eauto) using.
+  Proof with ((on_all_hyp: fun H => erewrite H in *; eauto); solve [eauto]) using.
     induction Heval1
       using eval_sub_mut_ind
       with (P := functional_eval_exp_prop)
diff --git a/theories/Core/Semantic/PER/Lemmas.v b/theories/Core/Semantic/PER/Lemmas.v
index aa9a4997..9be5418a 100644
--- a/theories/Core/Semantic/PER/Lemmas.v
+++ b/theories/Core/Semantic/PER/Lemmas.v
@@ -68,7 +68,8 @@ Lemma per_bot_then_per_top : forall m m' a a' b b' c c',
     {{ Dom ⇓ (⇑ a b) ⇑ c m ≈ ⇓ (⇑ a' b') ⇑ c' m' ∈ per_top }}.
 Proof.
   intros * H s.
-  specialize (H s) as [? []].
+  pose proof H s.
+  destruct_conjs.
   eexists; split; constructor; eassumption.
 Qed.
 
@@ -104,7 +105,7 @@ Hint Resolve per_top_typ_trans : mcltt.
 Lemma per_nat_sym : forall m n,
     {{ Dom m ≈ n ∈ per_nat }} ->
     {{ Dom n ≈ m ∈ per_nat }}.
-Proof with solve [eauto using per_bot_sym].
+Proof with mautosolve.
   induction 1; econstructor...
 Qed.
 
@@ -115,7 +116,7 @@ Lemma per_nat_trans : forall m n l,
     {{ Dom m ≈ n ∈ per_nat }} ->
     {{ Dom n ≈ l ∈ per_nat }} ->
     {{ Dom m ≈ l ∈ per_nat }}.
-Proof with solve [eauto using per_bot_trans].
+Proof with mautosolve.
   intros * H. gen l.
   induction H; inversion_clear 1; econstructor...
 Qed.
@@ -126,7 +127,7 @@ Hint Resolve per_nat_trans : mcltt.
 Lemma per_ne_sym : forall m n,
     {{ Dom m ≈ n ∈ per_ne }} ->
     {{ Dom n ≈ m ∈ per_ne }}.
-Proof with solve [eauto using per_bot_sym].
+Proof with mautosolve.
   intros * [].
   econstructor...
 Qed.
@@ -138,7 +139,7 @@ Lemma per_ne_trans : forall m n l,
     {{ Dom m ≈ n ∈ per_ne }} ->
     {{ Dom n ≈ l ∈ per_ne }} ->
     {{ Dom m ≈ l ∈ per_ne }}.
-Proof with solve [eauto using per_bot_trans].
+Proof with mautosolve.
   intros * [].
   inversion_clear 1.
   econstructor...
@@ -151,13 +152,13 @@ Lemma per_univ_elem_right_irrel : forall i i' A B R B' R',
     per_univ_elem i A B R ->
     per_univ_elem i' A B' R' ->
     R = R'.
-Proof with solve [eauto].
+Proof with mautosolve.
   intros * Horig.
   remember A as A' in |- *.
   gen A' B' R'.
   induction Horig using per_univ_elem_ind; intros * Heq Hright;
     subst; invert_per_univ_elem Hright; unfold per_univ;
-    try congruence.
+    trivial.
   specialize (IHHorig _ _ _ eq_refl equiv_a_a').
   subst.
   extensionality f.
@@ -186,7 +187,7 @@ Lemma per_univ_elem_sym : forall i A B R,
       (forall a b,
           {{ Dom a ≈ b ∈ R }} ->
           {{ Dom b ≈ a ∈ R }}).
-Proof with solve [try econstructor; eauto using per_bot_sym, per_nat_sym, per_ne_sym].
+Proof with (try econstructor; mautosolve).
   induction 1 using per_univ_elem_ind; subst.
   - split.
     + apply per_univ_elem_core_univ'...
@@ -219,9 +220,8 @@ Corollary per_univ_sym : forall i A B R,
     per_univ_elem i A B R ->
     per_univ_elem i B A R.
 Proof.
-  intros.
-  apply per_univ_elem_sym.
-  assumption.
+  intros * ?%per_univ_elem_sym.
+  firstorder.
 Qed.
 
 Corollary per_elem_sym : forall i A B a b R,
@@ -229,12 +229,11 @@ Corollary per_elem_sym : forall i A B a b R,
     R a b ->
     R b a.
 Proof.
-  intros * ?.
-  eapply per_univ_elem_sym.
-  eassumption.
+  intros * ?%per_univ_elem_sym.
+  firstorder.
 Qed.
 
-Lemma per_univ_elem_left_irrel : forall i i' A B R A' R',
+Corollary per_univ_elem_left_irrel : forall i i' A B R A' R',
     per_univ_elem i A B R ->
     per_univ_elem i' A' B R' ->
     R = R'.
@@ -243,7 +242,7 @@ Proof.
   eauto using per_univ_elem_right_irrel.
 Qed.
 
-Lemma per_univ_elem_cross_irrel : forall i i' A B R B' R',
+Corollary per_univ_elem_cross_irrel : forall i i' A B R B' R',
     per_univ_elem i A B R ->
     per_univ_elem i' B' A R' ->
     R = R'.
@@ -284,7 +283,7 @@ Lemma per_univ_elem_trans : forall i A1 A2 R,
           R a1 a2 ->
           R a2 a3 ->
           R a1 a3).
-Proof with solve [eauto using per_bot_trans | econstructor; eauto].
+Proof with ((econstructor + per_univ_elem_econstructor); mautosolve).
   induction 1 using per_univ_elem_ind;
     [> split;
      [ intros * HT2; invert_per_univ_elem HT2; clear HT2
@@ -309,7 +308,7 @@ Proof with solve [eauto using per_bot_trans | econstructor; eauto].
     destruct_rel_mod_eval.
     destruct_rel_mod_app.
     per_univ_elem_irrel_rewrite...
-  - per_univ_elem_econstructor...
+  - idtac...
 Qed.
 
 Corollary per_univ_trans : forall i j A1 A2 A3 R,
@@ -317,9 +316,8 @@ Corollary per_univ_trans : forall i j A1 A2 A3 R,
     per_univ_elem j A2 A3 R ->
     per_univ_elem i A1 A3 R.
 Proof.
-  intros * ?.
-  apply per_univ_elem_trans.
-  assumption.
+  intros * ?%per_univ_elem_trans.
+  firstorder.
 Qed.
 
 Corollary per_elem_trans : forall i A1 A2 a1 a2 a3 R,
@@ -328,9 +326,8 @@ Corollary per_elem_trans : forall i A1 A2 a1 a2 a3 R,
     R a2 a3 ->
     R a1 a3.
 Proof.
-  intros * ?.
-  eapply per_univ_elem_trans.
-  eassumption.
+  intros * ?% per_univ_elem_trans.
+  firstorder.
 Qed.
 
 Lemma per_univ_elem_cumu : forall {i a0 a1 R},
@@ -399,9 +396,8 @@ Corollary per_ctx_sym : forall Γ Δ R,
     {{ DF Γ ≈ Δ ∈ per_ctx_env ↘ R }} ->
     {{ DF Δ ≈ Γ ∈ per_ctx_env ↘ R }}.
 Proof.
-  intros.
-  apply per_ctx_env_sym.
-  assumption.
+  intros * ?%per_ctx_env_sym.
+  firstorder.
 Qed.
 
 Corollary per_env_sym : forall Γ Δ R o p,
@@ -409,12 +405,11 @@ Corollary per_env_sym : forall Γ Δ R o p,
     {{ Dom o ≈ p ∈ R }} ->
     {{ Dom p ≈ o ∈ R }}.
 Proof.
-  intros * ?.
-  eapply per_ctx_env_sym.
-  eassumption.
+  intros * ?%per_ctx_env_sym.
+  firstorder.
 Qed.
 
-Lemma per_ctx_env_left_irrel : forall Γ Γ' Δ R R',
+Corollary per_ctx_env_left_irrel : forall Γ Γ' Δ R R',
     {{ DF Γ ≈ Δ ∈ per_ctx_env ↘ R }} ->
     {{ DF Γ' ≈ Δ ∈ per_ctx_env ↘ R' }} ->
     R = R'.
@@ -423,7 +418,7 @@ Proof.
   eauto using per_ctx_env_right_irrel.
 Qed.
 
-Lemma per_ctx_env_cross_irrel : forall Γ Δ Δ' R R',
+Corollary per_ctx_env_cross_irrel : forall Γ Δ Δ' R R',
     {{ DF Γ ≈ Δ ∈ per_ctx_env ↘ R }} ->
     {{ DF Δ' ≈ Γ ∈ per_ctx_env ↘ R' }} ->
     R = R'.
@@ -474,16 +469,14 @@ Proof with solve [eauto using per_univ_trans].
   - rename tail_rel0 into tail_rel.
     econstructor; eauto.
     + eapply IHper_ctx_env...
-    + simpl in *.
-      intros.
+    + intros.
       assert (tail_rel p p) by (etransitivity; [| symmetry]; eauto).
-      destruct_rel_mod_eval.
+      (on_all_hyp: fun H => destruct_rel_by_assumption tail_rel H).
       per_univ_elem_irrel_rewrite.
       econstructor...
   - assert (tail_rel d{{{ p1 ↯ }}} d{{{ p3 ↯ }}}) by mauto.
     eexists.
-    simpl in *.
-    destruct_rel_mod_eval.
+    (on_all_hyp: fun H => destruct_rel_by_assumption tail_rel H).
     per_univ_elem_irrel_rewrite.
     eapply per_elem_trans...
 Qed.
@@ -493,9 +486,8 @@ Corollary per_ctx_trans : forall Γ1 Γ2 Γ3 R,
     {{ DF Γ2 ≈ Γ3 ∈ per_ctx_env ↘ R }} ->
     {{ DF Γ1 ≈ Γ3 ∈ per_ctx_env ↘ R }}.
 Proof.
-  intros * ?.
-  apply per_ctx_env_trans.
-  assumption.
+  intros * ?% per_ctx_env_trans.
+  firstorder.
 Qed.
 
 Corollary per_env_trans : forall Γ1 Γ2 R p1 p2 p3,
@@ -504,7 +496,6 @@ Corollary per_env_trans : forall Γ1 Γ2 R p1 p2 p3,
     {{ Dom p2 ≈ p3 ∈ R }} ->
     {{ Dom p1 ≈ p3 ∈ R }}.
 Proof.
-  intros * ?.
-  eapply per_ctx_env_trans.
-  eassumption.
+  intros * ?% per_ctx_env_trans.
+  firstorder.
 Qed.
diff --git a/theories/Core/Semantic/Realizability.v b/theories/Core/Semantic/Realizability.v
index ba2ff1cd..54b0936a 100644
--- a/theories/Core/Semantic/Realizability.v
+++ b/theories/Core/Semantic/Realizability.v
@@ -7,11 +7,10 @@ Import Domain_Notations.
 Lemma per_nat_then_per_top : forall {n m},
     {{ Dom n ≈ m ∈ per_nat }} ->
     {{ Dom ⇓ ℕ n ≈ ⇓ ℕ m ∈ per_top }}.
-Proof with solve [eexists; firstorder (econstructor; eauto)].
-  induction 1; simpl in *; intros s.
-  - idtac...
-  - specialize (IHper_nat s) as [? []]...
-  - specialize (H s) as [? []]...
+Proof with solve [destruct_conjs; eexists; repeat econstructor; eauto].
+  induction 1; simpl in *; intros s;
+    try specialize (IHper_nat s);
+    try specialize (H s)...
 Qed.
 
 #[export]
@@ -23,13 +22,14 @@ Lemma realize_per_univ_elem_gen : forall {i a a' R},
     /\ (forall {c c'}, {{ Dom c ≈ c' ∈ per_bot }} -> {{ Dom ⇑ a c ≈ ⇑ a' c' ∈ R }})
     /\ (forall {b b'}, {{ Dom b ≈ b' ∈ R }} -> {{ Dom ⇓ a b ≈ ⇓ a' b' ∈ per_top }}).
 Proof with (solve [try (try (eexists; split); econstructor); mauto]).
-  intros * H; simpl in H.
+  intros * H. simpl in H.
   induction H using per_univ_elem_ind; repeat split; intros.
   - subst...
   - eexists.
     per_univ_elem_econstructor...
-  - destruct H2.
-    specialize (H1 _ _ _ H2) as [? []].
+  - destruct_by_head per_univ.
+    specialize (H1 _ _ _ H2).
+    destruct_conjs.
     intro s.
     specialize (H1 s) as [? []]...
   - idtac...
@@ -41,17 +41,17 @@ Proof with (solve [try (try (eexists; split); econstructor); mauto]).
     destruct_rel_mod_eval.
     specialize (H10 (S s)) as [? []].
     specialize (H3 s) as [? []]...
-  - rewrite H2; clear H2.
+  - (on_all_hyp: fun H => rewrite H in *; clear H).
     intros c0 c0' equiv_c0_c0'.
-    destruct_all.
+    destruct_conjs.
     destruct_rel_mod_eval.
     econstructor; try solve [econstructor; eauto].
     enough ({{ Dom c ⇓ A c0 ≈ c' ⇓ A' c0' ∈ per_bot }}) by eauto.
     intro s.
     specialize (H3 s) as [? []].
     specialize (H5 _ _ equiv_c0_c0' s) as [? []]...
-  - rewrite H2 in *; clear H2.
-    destruct_all.
+  - (on_all_hyp: fun H => rewrite H in *; clear H).
+    destruct_conjs.
     intro s.
     assert {{ Dom ⇑! A s ≈ ⇑! A' s ∈ in_rel }} by eauto using var_per_bot.
     destruct_rel_mod_eval.
@@ -72,8 +72,7 @@ Corollary per_univ_then_per_top_typ : forall {i a a' R},
     {{ DF a ≈ a' ∈ per_univ_elem i ↘ R }} ->
     {{ Dom a ≈ a' ∈ per_top_typ }}.
 Proof.
-  intros.
-  eapply realize_per_univ_elem_gen; eauto.
+  intros * ?%realize_per_univ_elem_gen; firstorder.
 Qed.
 
 #[export]
@@ -83,8 +82,7 @@ Corollary per_bot_then_per_elem : forall {i a a' R c c'},
     {{ DF a ≈ a' ∈ per_univ_elem i ↘ R }} ->
     {{ Dom c ≈ c' ∈ per_bot }} -> {{ Dom ⇑ a c ≈ ⇑ a' c' ∈ R }}.
 Proof.
-  intros.
-  eapply realize_per_univ_elem_gen; eauto.
+  intros * ?%realize_per_univ_elem_gen; firstorder.
 Qed.
 
 (** We cannot add [per_bot_then_per_elem] as a hint
@@ -95,8 +93,7 @@ Corollary per_elem_then_per_top : forall {i a a' R b b'},
     {{ DF a ≈ a' ∈ per_univ_elem i ↘ R }} ->
     {{ Dom b ≈ b' ∈ R }} -> {{ Dom ⇓ a b ≈ ⇓ a' b' ∈ per_top }}.
 Proof.
-  intros.
-  eapply realize_per_univ_elem_gen; eauto.
+  intros * ?%realize_per_univ_elem_gen; firstorder.
 Qed.
 
 #[export]
diff --git a/theories/Core/Syntactic/CtxEq.v b/theories/Core/Syntactic/CtxEq.v
index 88d2bd4a..9d3e1ac7 100644
--- a/theories/Core/Syntactic/CtxEq.v
+++ b/theories/Core/Syntactic/CtxEq.v
@@ -3,7 +3,7 @@ From Mcltt Require Export System.
 Import Syntax_Notations.
 
 Lemma ctx_eq_refl : forall {Γ}, {{ ⊢ Γ }} -> {{ ⊢ Γ ≈ Γ }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   induction 1...
 Qed.
 
@@ -11,7 +11,7 @@ Qed.
 Hint Resolve ctx_eq_refl : mcltt.
 
 Lemma ctx_eq_sym : forall {Γ Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ ⊢ Δ ≈ Γ }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   induction 1...
 Qed.
 
@@ -36,80 +36,46 @@ Module ctxeq_judg.
   ctxeq_sub_helper : forall {Γ Γ' σ}, {{ Γ ⊢s σ : Γ' }} -> forall {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢s σ : Γ' }}
   with
   ctxeq_sub_eq_helper : forall {Γ Γ' σ σ'}, {{ Γ ⊢s σ ≈ σ' : Γ' }} -> forall {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢s σ ≈ σ' : Γ' }}.
-  Proof with solve [mauto].
-    (* ctxeq_exp_helper *)
-    - intros * HM * HΓΔ. gen Δ.
-      inversion_clear HM;
-        (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.
-      all: try (rename B into C); try (rename A0 into B).
-      2-4: assert {{ Δ ⊢ B : Type@i }} as HB by eauto; assert {{ ⊢ Γ, B ≈ Δ, B }} by mauto; clear HB.
-      2-3: solve [mauto].
-
-      + assert {{ ⊢ Γ, ℕ ≈ Δ, ℕ }} by (econstructor; mauto).
-        assert {{ Δ, ℕ ⊢ B : Type@i }} by mauto.
-        econstructor...
-
-      + econstructor...
-
-      + assert (exists B i, {{ #x : B ∈ Δ }} /\ {{ Γ ⊢ A ≈ B : Type@i }} /\ {{ Δ ⊢ A ≈ B : Type@i }}); destruct_conjs...
-
-    (* ctxeq_exp_eq_helper *)
-    - intros * HMM' * HΓΔ. gen Δ.
-      inversion_clear HMM';
-        (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; destruct (presup_ctx_eq HΓΔ); mauto.
-      all: try (rename B into C); try (rename B' into C'); try (rename A0 into B); try (rename A' into B').
-      1-3: assert {{ ⊢ Γ, ℕ ≈ Δ, ℕ }} by (econstructor; mauto); assert {{ Δ, ℕ ⊢ B : Type@i }} by eauto; econstructor...
-      1-5: assert {{ Δ ⊢ B : Type@i }} by eauto; assert {{ ⊢ Γ, B ≈ Δ, B }}...
-
-      + assert (exists B i, {{ #x : B ∈ Δ }} /\ {{ Γ ⊢ A ≈ B : Type@i }} /\ {{ Δ ⊢ A ≈ B : Type@i }}); destruct_conjs...
-
-      + 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 }}...
-
-    (* ctxeq_sub_helper *)
-    - intros * Hσ * HΓΔ. gen Δ.
-      inversion_clear Hσ;
-        (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; destruct (presup_ctx_eq HΓΔ); mauto.
-      inversion_clear HΓΔ.
-      econstructor...
-
-    (* ctxeq_sub_eq_helper *)
-    - intros * Hσσ' * HΓΔ. gen Δ.
-      inversion_clear Hσσ';
-        (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; destruct (presup_ctx_eq HΓΔ); mauto.
-      inversion_clear HΓΔ.
-      eapply wf_sub_eq_conv...
-
-      Unshelve.
-      all: constructor.
+  Proof with mautosolve.
+    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;
+      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.
+    (* 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...
+    (* ctxeq_sub_helper & ctxeq_sub_eq_helper weakening cases *)
+    2-3: inversion_clear HΓΔ; econstructor...
+
+    (* 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 }}...
   Qed.
 
-  Lemma ctxeq_exp : forall {Γ Δ M A}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢ M : A }} -> {{ Δ ⊢ M : A }}.
+  Corollary ctxeq_exp : forall {Γ Δ M A}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢ M : A }} -> {{ Δ ⊢ M : A }}.
   Proof.
     eauto using ctxeq_exp_helper.
   Qed.
 
-  Lemma ctxeq_exp_eq : forall {Γ Δ M M' A}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢ M ≈ M' : A }} -> {{ Δ ⊢ M ≈ M' : A }}.
+  Corollary ctxeq_exp_eq : forall {Γ Δ M M' A}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢ M ≈ M' : A }} -> {{ Δ ⊢ M ≈ M' : A }}.
   Proof.
     eauto using ctxeq_exp_eq_helper.
   Qed.
 
-  Lemma ctxeq_sub : forall {Γ Δ σ Γ'}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢s σ : Γ' }} -> {{ Δ ⊢s σ : Γ' }}.
+  Corollary ctxeq_sub : forall {Γ Δ σ Γ'}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢s σ : Γ' }} -> {{ Δ ⊢s σ : Γ' }}.
   Proof.
     eauto using ctxeq_sub_helper.
   Qed.
 
-  Lemma ctxeq_sub_eq : forall {Γ Δ σ σ' Γ'}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢s σ ≈ σ' : Γ' }} -> {{ Δ ⊢s σ ≈ σ' : Γ' }}.
+  Corollary ctxeq_sub_eq : forall {Γ Δ σ σ' Γ'}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢s σ ≈ σ' : Γ' }} -> {{ Δ ⊢s σ ≈ σ' : Γ' }}.
   Proof.
     eauto using ctxeq_sub_eq_helper.
   Qed.
@@ -121,12 +87,11 @@ End ctxeq_judg.
 Export ctxeq_judg.
 
 Lemma ctx_eq_trans : forall {Γ0 Γ1 Γ2}, {{ ⊢ Γ0 ≈ Γ1 }} -> {{ ⊢ Γ1 ≈ Γ2 }} -> {{ ⊢ Γ0 ≈ Γ2 }}.
-Proof with solve [mauto].
-  intros * HΓ01 HΓ12.
+Proof with mautosolve.
+  intros * HΓ01.
   gen Γ2.
-  induction HΓ01 as [|Γ0 ? T0 i01 T1]; intros; mauto.
-  rename HΓ12 into HT1Γ12.
-  inversion_clear HT1Γ12 as [|? Γ2' ? i12 T2].
+  induction HΓ01 as [|Γ0 ? T0 i01 T1]; mauto.
+  inversion_clear 1 as [|? Γ2' ? i12 T2].
   clear Γ2; rename Γ2' into Γ2.
   set (i := max i01 i12).
   assert {{ Γ0 ⊢ T0 : Type@i }} by mauto using lift_exp_max_left.
diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index 614afe36..9a86ff89 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -43,169 +43,157 @@ Lemma presup_exp : forall {Γ M A}, {{ Γ ⊢ M : A }} -> {{ ⊢ Γ }} /\ exists
 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].
-  (* presup_exp *)
-  - intros * HM.
-    inversion_clear HM; (on_all_hyp: gen_presup_IH presup_exp presup_exp_eq presup_sub_eq);
+  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;
-      repeat split; mauto.
-    all: try (rename B into C); try (rename B' into C'); try (rename A0 into B); try (rename A' into B').
-
-    + eexists.
-      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...
-
-  - intros * HMM'.
-    set (WkWksucc := {{{ Wk∘Wk ,, succ #1 }}}).
-    inversion_clear HMM'; (on_all_hyp: gen_presup_IH presup_exp presup_exp_eq presup_sub_eq);
-      clear presup_exp presup_exp_eq presup_sub_eq;
-      repeat split; mauto.
-    all: try (rename B into C); try (rename B' into C'); try (rename A0 into B); try (rename A' into B');
-      try (rename N into L); try (rename N' into L');
-      try (rename M0 into N); try (rename MZ into NZ); try (rename MS into NS);
-      try (rename M'0 into N'); try (rename MZ' into NZ'); try (rename MS' into NS');
-      try (rename M' into N').
-
-    + assert {{ Γ ⊢s Id ,, N ≈ Id ,, N' : Γ, ℕ }} by mauto.
-      assert {{ Γ ⊢ B[Id ,, N] ≈ B[Id ,, N'] : Type@i }} by mauto.
-      assert {{ Γ ⊢ B[Id ,, N] ≈ B'[Id ,, N'] : Type@i }} by mauto.
-      assert {{ Γ ⊢ B[Id ,, zero] ≈ B'[Id ,, zero] : Type@i }} by mauto.
-      assert {{ Γ ⊢ NZ' : B'[Id ,, zero] }} by mauto.
-      assert {{ Γ, ℕ, B ⊢ NS' : B'[WkWksucc] }} by mauto.
-      assert {{ Γ, ℕ, B' ⊢ NS' : B'[WkWksucc] }} by mauto.
-      enough {{ Γ ⊢ rec N' return B' | zero -> NZ' | succ -> NS' end : B'[Id ,, N'] }}...
-
-    + assert {{ Γ ⊢ B[(Id,,N)][σ] ≈ B[(Id,,N)∘σ] : Type@i }} by mauto.
-      assert {{ Γ ⊢ B[(Id,,N)∘σ] ≈ B[σ,,N[σ]] : Type@i }} by mauto.
-      enough {{ Γ ⊢ B[(Id,,N)][σ] ≈ B[σ,,N[σ]] : Type@i }}...
-
-    + assert {{ Γ ⊢s Id,,N[σ] : Γ, ℕ }} by mauto.
-      assert {{ Γ, ℕ ⊢s q σ : Δ, ℕ }} by mauto.
-      assert {{ Γ ⊢ B[q σ][(Id,,N[σ])] ≈ B[q σ∘(Id,,N[σ])] : Type@i }} 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.
-      assert {{ Γ ⊢ zero : ℕ[σ] }} by mauto.
-      assert {{ Γ ⊢s q σ∘(Id ,, zero) ≈ σ ,, zero : Δ, ℕ }} by mauto.
-      assert {{ Γ ⊢s σ ≈ Id∘σ : Δ }} by mauto.
-      assert {{ Γ ⊢s σ ,, zero ≈ Id∘σ ,, zero[σ] : Δ, ℕ }} by mauto.
-      assert {{ Γ ⊢s Id∘σ ,, zero[σ] ≈ (Id ,, zero)∘σ : Δ, ℕ }} by mauto.
-      assert {{ Γ ⊢s q σ∘(Id ,, zero) ≈ (Id ,, zero)∘σ : Δ, ℕ }} by mauto.
-      assert {{ Γ ⊢ B[q σ][Id ,, zero] ≈ B[Id ,, zero][σ] : Type@i }} by mauto.
-      assert {{ Γ ⊢ NZ[σ] : B[q σ][Id ,, zero] }} by mauto.
-      set (Γ' := {{{ Γ, ℕ, B[q σ] }}}).
-      assert {{ Γ' ⊢s q (q σ) : Δ, ℕ, B }} by mauto.
-      assert {{ Γ' ⊢s q σ∘WkWksucc ≈ WkWksucc∘q (q σ) : Δ, ℕ }} by mauto.
-      assert {{ Γ' ⊢ B[q σ][WkWksucc] ≈ B[WkWksucc][q (q σ)] : Type@i }} by mauto.
-      enough {{ Γ' ⊢ NS[q (q σ)] : B[q σ][WkWksucc] }}...
-
-    + set (recN := {{{ rec N return B | zero -> NZ | succ -> NS end }}}).
-      assert {{ Γ ⊢ recN : B[Id ,, N] }} by mauto.
-      assert {{ Γ ⊢s WkWksucc∘(Id ,, N ,, recN) ≈ (Wk∘Wk)∘(Id ,, N ,, recN) ,, (succ #1)[(Id ,, N ,, recN)] : Γ, ℕ }}
-        by (eapply sub_eq_extend_compose_nat; mauto).
-      assert {{ Γ ⊢s Id ,, N ,, recN : Γ, ℕ, B }} by mauto.
-      assert {{ Γ ⊢s (Wk∘Wk)∘(Id ,, N ,, recN) : Γ }} by mauto.
-      assert {{ Γ ⊢s (Wk∘Wk)∘(Id ,, N ,, recN) ≈ Wk∘(Wk∘(Id ,, N ,, recN)) : Γ }} by mauto.
-      assert {{ Γ ⊢s Wk∘(Wk∘(Id ,, N ,, recN)) ≈ Wk∘(Id ,, N) : Γ }} by mauto.
-      assert {{ Γ ⊢s (Wk∘Wk)∘(Id ,, N ,, recN) ≈ Id : Γ }} by mauto.
-      assert {{ Γ ⊢ #1[Id ,, N ,, recN] ≈ #0[Id ,, N] : ℕ }} by mauto.
-      assert {{ Γ ⊢ succ #1[Id ,, N ,, recN] ≈ succ N : ℕ }} by mauto.
-      assert {{ Γ ⊢ (succ #1)[Id ,, N ,, recN] ≈ succ N : ℕ }} by mauto.
-      assert {{ Γ ⊢s (Wk∘Wk)∘(Id ,, N ,, recN) ,, (succ #1)[Id ,, N ,, recN] ≈ Id ,, succ N : Γ , ℕ }} by mauto.
-      assert {{ Γ ⊢s WkWksucc∘(Id ,, N ,, recN) ≈ Id ,, succ N : Γ , ℕ }} by mauto.
-      assert {{ Γ ⊢ B[WkWksucc∘(Id ,, N ,, recN)] ≈ B[Id ,, succ N] : Type@i }} by mauto.
-      enough {{ Γ ⊢ B[WkWksucc][Id ,, N ,, recN] ≈ B[Id ,, succ N] : Type@i }}...
-
-    + 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.
-      enough {{ Γ ⊢ λ B' N' : Π B' C }}...
-
-    + 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 using lift_exp_max_left.
-      assert {{ Δ, B ⊢ C : Type@(max i i0) }} by mauto using lift_exp_max_right.
-      assert {{ Γ ⊢ Π B[σ] C[q σ] ≈ Π B[σ] C[q σ] : Type@(max i i0) }} by mauto.
-      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...
-
-    + assert {{ Γ ⊢s Id ,, L ≈ Id ,, L' : Γ, B }} by (econstructor; mauto).
-      enough {{ Γ ⊢ C[Id ,, L] ≈ C[Id ,, L'] : Type@i }}...
-
-    + assert {{ Γ ⊢ N[σ] : Π B[σ] C[q σ] }} by mauto.
-      assert {{ Γ ⊢ L[σ] : B[σ] }} by mauto.
-      assert {{ Γ ⊢s (Id ,, L)∘σ ≈ Id∘σ ,, L[σ] : Δ, B }} by (econstructor; mauto).
-      assert {{ Γ ⊢s (Id ,, L)∘σ ≈ σ ,, L[σ] : Δ, B }} by mauto.
-      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 {{ Γ ⊢ 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 }}...
-
-    + assert {{ Γ, B ⊢ B[Wk] : Type@i }} by mauto.
-      assert {{ Γ, B, B[Wk] ⊢ C[q Wk] : Type@i }} by mauto.
-      assert {{ Γ, B ⊢ M[Wk] : (Π B C)[Wk] }} by mauto.
-      assert {{ Γ, B ⊢ M[Wk] : Π B[Wk] C[q Wk] }} by mauto.
-      assert {{ Γ, B ⊢ #0 : B[Wk] }} by mauto.
-      assert {{ Γ, B ⊢s Id ,, #0 : Γ, B, B[Wk] }} by mauto.
-      assert {{ Γ, B ⊢ M[Wk] #0 : C[q Wk][Id,,#0] }} by mauto.
-      assert {{ Γ, B ⊢ M[Wk] #0 : C[q Wk∘(Id,,#0)] }} by mauto.
-      assert {{ Γ, B ⊢ #0 : B[Wk][Id] }} by mauto.
-      assert {{ Γ, B ⊢s Id ,, #0 : Γ, B, B[Wk] }} by mauto.
-      assert {{ Γ, B ⊢s Wk : Γ }} by mauto.
-      assert {{ Γ, B ⊢s Wk∘(Id ,, # 0) ≈ Id : Γ, B }} by mauto.
-      assert {{ Γ, B ⊢s Wk∘Id ≈ (Wk∘Wk)∘(Id ,, # 0) : Γ }} by mauto.
-      assert {{ Γ, B, B[Wk] ⊢ #0 : B[Wk][Wk] }} by mauto.
-      assert {{ Γ, B, B[Wk] ⊢ #0 : B[Wk∘Wk] }} by mauto.
-      assert {{ Γ, B ⊢s q Wk ∘ (Id ,, #0) ≈ (Wk∘Wk)∘(Id ,, #0) ,, #0[Id ,, #0] : Γ, B }} by mauto.
-      assert {{ Γ, B ⊢s (Wk∘Wk)∘(Id ,, #0) ≈ Wk∘(Wk∘(Id ,, #0)) : Γ }} by mauto.
-      assert {{ Γ, B ⊢s (Wk∘Wk)∘(Id ,, #0) ≈ Wk∘Id : Γ }} by mauto.
-      assert {{ Γ, B ⊢ #0[Id ,, #0] ≈ #0 : B[Wk][Id] }} by mauto.
-      assert {{ Γ, B ⊢ #0 ≈ #0[Id] : B[Wk][Id] }} by mauto.
-      assert {{ Γ, B ⊢ #0[Id ,, #0] ≈ #0[Id] : B[Wk][Id] }} by mauto.
-      assert {{ Γ, B ⊢ #0[Id ,, #0] ≈ #0[Id] : B[Wk∘Id] }} by mauto.
-      assert {{ Γ, B ⊢ #0[Id ,, #0] ≈ #0[Id] : B[(Wk∘Wk)∘(Id ,, #0)] }} by mauto.
-      assert {{ Γ, B ⊢s (Wk∘Wk)∘(Id ,, #0) ,, #0[Id ,, #0] ≈ Wk∘Id ,, #0[Id] : Γ, B }} by mauto.
-      assert {{ Γ, B ⊢s Wk∘Id ,, #0[Id] ≈ Id : Γ, B }} by mauto.
-      assert {{ Γ, B ⊢s q Wk ∘ (Id ,, #0) ≈ Id : Γ, B }} by mauto.
-      assert {{ Γ, B ⊢ M[Wk] #0 : C[Id] }} by mauto.
-      enough {{ Γ, B ⊢ M[Wk] #0 : C }}...
-
-    + assert {{ Γ ⊢s Wk∘(σ ,, N') ≈ σ : Δ }} by mauto.
-      assert {{ Γ ⊢ B[Wk∘(σ ,, N')] ≈ B[σ] : Type@i }} by mauto.
-      assert {{ Δ, B ⊢s Wk : Δ }} by mauto.
-      assert {{ Γ ⊢ B[Wk][σ ,, N'] ≈ B[σ] : Type@i }} by mauto.
-      enough {{ Γ ⊢ #0[σ ,, N'] : B[Wk][σ ,, N'] }}...
-
-    + assert (exists i, {{ Δ ⊢ C : Type@i }}) as [i'] by mauto.
-      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.
-      enough {{ Γ ⊢ #(S x)[σ ,, N] : C[Wk][σ ,, N] }}...
-
-    + assert (exists i, {{ Δ ⊢ C : Type@i }}) as []...
-
-  - intros * Hσσ'.
-    inversion_clear Hσσ'; (on_all_hyp: gen_presup_IH presup_exp presup_exp_eq presup_sub_eq);
-      clear presup_exp presup_exp_eq presup_sub_eq;
-      repeat split; mauto.
-
-    + econstructor...
-
-    + assert (exists i, {{ Γ0 ⊢ A : Type@i }}) as [] by mauto.
-      assert {{ Γ ⊢ #0[σ] : A[Wk][σ] }} by mauto.
-      enough {{ Γ ⊢ #0[σ] : A[Wk∘σ] }}...
-
-  Unshelve.
-  all: constructor.
+    repeat split; mauto;
+    try (rename B into C); try (rename B' into C'); try (rename A0 into B); try (rename A' into B');
+    try (rename N into L); try (rename N' into L');
+    try (rename M0 into N); try (rename MZ into NZ); try (rename MS into NS);
+    try (rename M'0 into N'); try (rename MZ' into NZ'); try (rename MS' into NS');
+    try (rename M' into N').
+  (* presup_exp cases *)
+  - eexists.
+    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...
+
+  (* presup_exp_eq cases *)
+  - assert {{ Γ ⊢s Id ,, N ≈ Id ,, N' : Γ, ℕ }} by mauto.
+    assert {{ Γ ⊢ B[Id ,, N] ≈ B[Id ,, N'] : Type@i }} by mauto.
+    assert {{ Γ ⊢ B[Id ,, N] ≈ B'[Id ,, N'] : Type@i }} by mauto.
+    assert {{ Γ ⊢ B[Id ,, zero] ≈ B'[Id ,, zero] : Type@i }} by mauto.
+    assert {{ Γ ⊢ NZ' : B'[Id ,, zero] }} by mauto.
+    assert {{ Γ, ℕ, B ⊢ NS' : B'[WkWksucc] }} by mauto.
+    assert {{ Γ, ℕ, B' ⊢ NS' : B'[WkWksucc] }} by mauto.
+    enough {{ Γ ⊢ rec N' return B' | zero -> NZ' | succ -> NS' end : B'[Id ,, N'] }}...
+
+  - assert {{ Γ ⊢ B[(Id,,N)][σ] ≈ B[(Id,,N)∘σ] : Type@i }} by mauto.
+    assert {{ Γ ⊢ B[(Id,,N)∘σ] ≈ B[σ,,N[σ]] : Type@i }} by mauto.
+    enough {{ Γ ⊢ B[(Id,,N)][σ] ≈ B[σ,,N[σ]] : Type@i }}...
+
+  - assert {{ Γ ⊢s Id,,N[σ] : Γ, ℕ }} by mauto.
+    assert {{ Γ, ℕ ⊢s q σ : Δ, ℕ }} by mauto.
+    assert {{ Γ ⊢ B[q σ][(Id,,N[σ])] ≈ B[q σ∘(Id,,N[σ])] : Type@i }} 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.
+    assert {{ Γ ⊢ zero : ℕ[σ] }} by mautosolve.
+    assert {{ Γ ⊢s q σ∘(Id ,, zero) ≈ σ ,, zero : Δ, ℕ }} by mauto.
+    assert {{ Γ ⊢s σ ≈ Id∘σ : Δ }} by mauto.
+    assert {{ Γ ⊢s σ ,, zero ≈ Id∘σ ,, zero[σ] : Δ, ℕ }} by mauto.
+    assert {{ Γ ⊢s Id∘σ ,, zero[σ] ≈ (Id ,, zero)∘σ : Δ, ℕ }} by mauto.
+    assert {{ Γ ⊢s q σ∘(Id ,, zero) ≈ (Id ,, zero)∘σ : Δ, ℕ }} by mauto.
+    assert {{ Γ ⊢ B[q σ][Id ,, zero] ≈ B[Id ,, zero][σ] : Type@i }} by mauto.
+    assert {{ Γ ⊢ NZ[σ] : B[q σ][Id ,, zero] }} by mauto.
+    set (Γ' := {{{ Γ, ℕ, B[q σ] }}}).
+    assert {{ Γ' ⊢s q (q σ) : Δ, ℕ, B }} by mauto.
+    assert {{ Γ' ⊢s q σ∘WkWksucc ≈ WkWksucc∘q (q σ) : Δ, ℕ }} by mauto.
+    assert {{ Γ' ⊢ B[q σ][WkWksucc] ≈ B[WkWksucc][q (q σ)] : Type@i }} by mauto.
+    enough {{ Γ' ⊢ NS[q (q σ)] : B[q σ][WkWksucc] }}...
+
+  - set (recN := {{{ rec N return B | zero -> NZ | succ -> NS end }}}).
+    set (IdNrecN := {{{ Id ,, N ,, recN }}}).
+    assert {{ Γ ⊢ recN : B[Id ,, N] }} by mauto.
+    assert {{ Γ ⊢s WkWksucc∘IdNrecN ≈ (Wk∘Wk)∘IdNrecN ,, (succ #1)[IdNrecN] : Γ, ℕ }}
+      by (eapply sub_eq_extend_compose_nat; mauto).
+    assert {{ Γ ⊢s Id ,, N ,, recN : Γ, ℕ, B }} by mauto.
+    assert {{ Γ ⊢s (Wk∘Wk)∘IdNrecN : Γ }} by mauto.
+    assert {{ Γ ⊢s (Wk∘Wk)∘IdNrecN ≈ Wk∘(Wk∘IdNrecN) : Γ }} by mauto.
+    assert {{ Γ ⊢s Wk∘(Wk∘IdNrecN) ≈ Wk∘(Id ,, N) : Γ }} by mauto.
+    assert {{ Γ ⊢s (Wk∘Wk)∘IdNrecN ≈ Id : Γ }} by mauto.
+    assert {{ Γ ⊢ #1[Id ,, N ,, recN] ≈ #0[Id ,, N] : ℕ }} by mauto.
+    assert {{ Γ ⊢ succ #1[Id ,, N ,, recN] ≈ succ N : ℕ }} by mauto.
+    assert {{ Γ ⊢ (succ #1)[Id ,, N ,, recN] ≈ succ N : ℕ }} by mauto.
+    assert {{ Γ ⊢s (Wk∘Wk)∘IdNrecN ,, (succ #1)[Id ,, N ,, recN] ≈ Id ,, succ N : Γ , ℕ }} by mauto.
+    assert {{ Γ ⊢s WkWksucc∘IdNrecN ≈ Id ,, succ N : Γ , ℕ }} by mauto.
+    assert {{ Γ ⊢ B[WkWksucc∘IdNrecN] ≈ B[Id ,, succ N] : Type@i }} by mauto.
+    enough {{ Γ ⊢ B[WkWksucc][IdNrecN] ≈ B[Id ,, succ N] : Type@i }}...
+
+  - 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.
+    enough {{ Γ ⊢ λ B' N' : Π B' C }}...
+
+  - 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 using lift_exp_max_left.
+    assert {{ Δ, B ⊢ C : Type@(max i i0) }} by mauto using lift_exp_max_right.
+    assert {{ Γ ⊢ Π B[σ] C[q σ] ≈ Π B[σ] C[q σ] : Type@(max i i0) }} by mauto.
+    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...
+
+  - assert {{ Γ ⊢s Id ,, L ≈ Id ,, L' : Γ, B }} by (econstructor; mauto).
+    enough {{ Γ ⊢ C[Id ,, L] ≈ C[Id ,, L'] : Type@i }}...
+
+  - assert {{ Γ ⊢ N[σ] : Π B[σ] C[q σ] }} by mauto.
+    assert {{ Γ ⊢ L[σ] : B[σ] }} by mauto.
+    assert {{ Γ ⊢s (Id ,, L)∘σ ≈ Id∘σ ,, L[σ] : Δ, B }} by (econstructor; mauto).
+    assert {{ Γ ⊢s (Id ,, L)∘σ ≈ σ ,, L[σ] : Δ, B }} by mauto.
+    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 {{ Γ ⊢ 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 }}...
+
+  - set (Id0 := {{{ Id ,, #0 }}}).
+    assert {{ Γ, B ⊢ B[Wk] : Type@i }} by mauto.
+    assert {{ Γ, B, B[Wk] ⊢ C[q Wk] : Type@i }} by mauto.
+    assert {{ Γ, B ⊢ M[Wk] : (Π B C)[Wk] }} by mauto.
+    assert {{ Γ, B ⊢ M[Wk] : Π B[Wk] C[q Wk] }} by mauto.
+    assert {{ Γ, B ⊢ #0 : B[Wk] }} by mauto.
+    assert {{ Γ, B ⊢s Id0 : Γ, B, B[Wk] }} by mauto.
+    assert {{ Γ, B ⊢ M[Wk] #0 : C[q Wk][Id0] }} by mauto.
+    assert {{ Γ, B ⊢ M[Wk] #0 : C[q Wk ∘ Id0] }} by mauto.
+    assert {{ Γ, B ⊢ #0 : B[Wk][Id] }} by mauto.
+    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 ≈ (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 ⊢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.
+    assert {{ Γ, B ⊢ #0[Id0] ≈ #0 : B[Wk][Id] }} by mauto.
+    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.
+    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.
+    enough {{ Γ, B ⊢ M[Wk] #0 : C }}...
+
+  - assert {{ Γ ⊢s Wk∘(σ ,, N') ≈ σ : Δ }} by mauto.
+    assert {{ Γ ⊢ B[Wk∘(σ ,, N')] ≈ B[σ] : Type@i }} by mauto.
+    assert {{ Δ, B ⊢s Wk : Δ }} by mauto.
+    assert {{ Γ ⊢ B[Wk][σ ,, N'] ≈ B[σ] : Type@i }} by mauto.
+    enough {{ Γ ⊢ #0[σ ,, N'] : B[Wk][σ ,, N'] }}...
+
+  - assert (exists i, {{ Δ ⊢ C : Type@i }}) as [i'] by mauto.
+    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.
+    enough {{ Γ ⊢ #(S x)[σ ,, N] : C[Wk][σ ,, N] }}...
+
+  - assert (exists i, {{ Δ ⊢ C : Type@i }}) as []...
+
+  (* presup_sub_eq cases *)
+  - econstructor...
+
+  - assert (exists i, {{ Γ0 ⊢ A : Type@i }}) as [] by mauto.
+    assert {{ Γ ⊢ #0[σ] : A[Wk][σ] }} by mauto.
+    enough {{ Γ ⊢ #0[σ] : A[Wk∘σ] }}...
 Qed.
 
 #[export]
diff --git a/theories/Core/Syntactic/System/Lemmas.v b/theories/Core/Syntactic/System/Lemmas.v
index b57cddc7..a0ff08fc 100644
--- a/theories/Core/Syntactic/System/Lemmas.v
+++ b/theories/Core/Syntactic/System/Lemmas.v
@@ -2,110 +2,104 @@ From Mcltt Require Import Base LibTactics System.Definitions.
 Import Syntax_Notations.
 
 Lemma ctx_decomp : forall {Γ A}, {{ ⊢ Γ , A }} -> {{ ⊢ Γ }} /\ exists i, {{ Γ ⊢ A : Type@i }}.
-Proof with solve [eauto].
-  inversion 1; subst...
+Proof with now eauto.
+  inversion 1...
 Qed.
 
 #[export]
 Hint Resolve ctx_decomp : mcltt.
 
-Lemma ctx_decomp_left : forall {Γ A}, {{ ⊢ Γ , A }} -> {{ ⊢ Γ }}.
-Proof with solve [eauto].
-  intros.
-  eapply ctx_decomp...
+Corollary ctx_decomp_left : forall {Γ A}, {{ ⊢ Γ , A }} -> {{ ⊢ Γ }}.
+Proof with easy.
+  intros * ?%ctx_decomp...
 Qed.
 
-Lemma ctx_decomp_right : forall {Γ A}, {{ ⊢ Γ , A }} -> exists i, {{ Γ ⊢ A : Type@i }}.
-Proof with solve [eauto].
-  intros.
-  eapply ctx_decomp...
+Corollary ctx_decomp_right : forall {Γ A}, {{ ⊢ Γ , A }} -> exists i, {{ Γ ⊢ A : Type@i }}.
+Proof with easy.
+  intros * ?%ctx_decomp...
 Qed.
 
 #[export]
 Hint Resolve ctx_decomp_left ctx_decomp_right : mcltt.
 
 Lemma lift_exp_ge : forall {Γ A n m}, n <= m -> {{ Γ ⊢ A : Type@n }} -> {{ Γ ⊢ A : Type@m }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   induction 1...
 Qed.
 
 #[export]
 Hint Resolve lift_exp_ge : mcltt.
 
-Lemma lift_exp_max_left : forall {Γ A n} m, {{ Γ ⊢ A : Type@n }} -> {{ Γ ⊢ A : Type@(max n m) }}.
-Proof with solve [mauto].
+Corollary lift_exp_max_left : forall {Γ A n} m, {{ Γ ⊢ A : Type@n }} -> {{ Γ ⊢ A : Type@(max n m) }}.
+Proof with mautosolve.
   intros.
   assert (n <= max n m) by lia...
 Qed.
 
-Lemma lift_exp_max_right : forall {Γ A} n {m}, {{ Γ ⊢ A : Type@m }} -> {{ Γ ⊢ A : Type@(max n m) }}.
-Proof with solve [mauto].
+Corollary lift_exp_max_right : forall {Γ A} n {m}, {{ Γ ⊢ A : Type@m }} -> {{ Γ ⊢ A : Type@(max n m) }}.
+Proof with mautosolve.
   intros.
   assert (m <= max n m) by lia...
 Qed.
 
 Lemma lift_exp_eq_ge : forall {Γ A A' n m}, n <= m -> {{ Γ ⊢ A ≈ A': Type@n }} -> {{ Γ ⊢ A ≈ A' : Type@m }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   induction 1; subst...
 Qed.
 
 #[export]
 Hint Resolve lift_exp_eq_ge : mcltt.
 
-Lemma lift_exp_eq_max_left : forall {Γ A A' n} m, {{ Γ ⊢ A ≈ A' : Type@n }} -> {{ Γ ⊢ A ≈ A' : Type@(max n m) }}.
-Proof with solve [mauto].
+Corollary lift_exp_eq_max_left : forall {Γ A A' n} m, {{ Γ ⊢ A ≈ A' : Type@n }} -> {{ Γ ⊢ A ≈ A' : Type@(max n m) }}.
+Proof with mautosolve.
   intros.
   assert (n <= max n m) by lia...
 Qed.
 
-Lemma lift_exp_eq_max_right : forall {Γ A A'} n {m}, {{ Γ ⊢ A ≈ A' : Type@m }} -> {{ Γ ⊢ A ≈ A' : Type@(max n m) }}.
-Proof with solve [mauto].
+Corollary lift_exp_eq_max_right : forall {Γ A A'} n {m}, {{ Γ ⊢ A ≈ A' : Type@m }} -> {{ Γ ⊢ A ≈ A' : Type@(max n m) }}.
+Proof with mautosolve.
   intros.
   assert (m <= max n m) by lia...
 Qed.
 
 Lemma presup_ctx_eq : forall {Γ Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ ⊢ Γ }} /\ {{ ⊢ Δ }}.
-Proof with solve [mauto].
-  induction 1 as [|* ? []]...
+Proof with mautosolve.
+  induction 1; destruct_pairs...
 Qed.
 
-Lemma presup_ctx_eq_left : forall {Γ Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ ⊢ Γ }}.
-Proof with solve [eauto].
-  intros.
-  eapply proj1, presup_ctx_eq...
+Corollary presup_ctx_eq_left : forall {Γ Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ ⊢ Γ }}.
+Proof with easy.
+  intros * ?%presup_ctx_eq...
 Qed.
 
-Lemma presup_ctx_eq_right : forall {Γ Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ ⊢ Δ }}.
-Proof with solve [eauto].
-  intros.
-  eapply presup_ctx_eq...
+Corollary presup_ctx_eq_right : forall {Γ Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ ⊢ Δ }}.
+Proof with easy.
+  intros * ?%presup_ctx_eq...
 Qed.
 
 #[export]
 Hint Resolve presup_ctx_eq presup_ctx_eq_left presup_ctx_eq_right : mcltt.
 
 Lemma presup_sub_ctx : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ ⊢ Γ }} /\ {{ ⊢ Δ }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   induction 1; destruct_pairs...
 Qed.
 
-Lemma presup_sub_ctx_left : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ ⊢ Γ }}.
-Proof with solve [eauto].
-  intros.
-  eapply proj1, presup_sub_ctx...
+Corollary presup_sub_ctx_left : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ ⊢ Γ }}.
+Proof with easy.
+  intros * ?%presup_sub_ctx...
 Qed.
 
-Lemma presup_sub_ctx_right : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ ⊢ Δ }}.
-Proof with solve [eauto].
-  intros.
-  eapply presup_sub_ctx...
+Corollary presup_sub_ctx_right : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ ⊢ Δ }}.
+Proof with easy.
+  intros * ?%presup_sub_ctx...
 Qed.
 
 #[export]
 Hint Resolve presup_sub_ctx presup_sub_ctx_left presup_sub_ctx_right : mcltt.
 
 Lemma presup_exp_ctx : forall {Γ M A}, {{ Γ ⊢ M : A }} -> {{ ⊢ Γ }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   induction 1...
 Qed.
 
@@ -113,30 +107,26 @@ Qed.
 Hint Resolve presup_exp_ctx : mcltt.
 
 Lemma presup_sub_eq_ctx : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Γ }} /\ {{ ⊢ Δ }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   induction 1; destruct_pairs...
 Qed.
 
-Lemma presup_sub_eq_ctx_left : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Γ }}.
-Proof with solve [eauto].
-  intros.
-  eapply proj1, presup_sub_eq_ctx...
+Corollary presup_sub_eq_ctx_left : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Γ }}.
+Proof with easy.
+  intros * ?%presup_sub_eq_ctx...
 Qed.
 
-Lemma presup_sub_eq_ctx_right : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Δ }}.
-Proof with solve [eauto].
-  intros.
-  eapply presup_sub_eq_ctx...
+Corollary presup_sub_eq_ctx_right : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Δ }}.
+Proof with easy.
+  intros * ?%presup_sub_eq_ctx...
 Qed.
 
 #[export]
 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 solve [mauto].
+Proof with mautosolve.
   induction 1...
-  Unshelve.
-  all: constructor.
 Qed.
 
 #[export]
@@ -169,13 +159,13 @@ Proof.
 Qed.
 
 Lemma exp_eq_sub_cong_typ2' : forall {Δ Γ A σ τ i}, {{ Δ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢s σ ≈ τ : Δ }} -> {{ Γ ⊢ A[σ] ≈ A[τ] : Type@i }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
   eapply wf_exp_eq_conv...
 Qed.
 
 Lemma exp_eq_sub_compose_typ : forall {Ψ Δ Γ A σ τ i}, {{ Ψ ⊢ A : Type@i }} -> {{ Δ ⊢s σ : Ψ }} -> {{ Γ ⊢s τ : Δ }} -> {{ Γ ⊢ A[σ][τ] ≈ A[σ∘τ] : Type@i }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
   eapply wf_exp_eq_conv...
 Qed.
@@ -192,38 +182,32 @@ Qed.
 Hint Resolve exp_eq_typ_sub_sub : mcltt.
 
 Lemma vlookup_0_typ : forall {Γ i}, {{ ⊢ Γ }} -> {{ Γ, Type@i ⊢ # 0 : Type@i }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
   eapply wf_conv...
-  Unshelve.
-  all: constructor.
 Qed.
 
 Lemma vlookup_1_typ : forall {Γ i A j}, {{ ⊢ Γ }} -> {{ Γ, Type@i ⊢ A : Type@j }} -> {{ Γ, Type@i, A ⊢ # 1 : Type@i }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
   assert {{ ⊢ Γ, Type@i }} by mauto.
-  assert {{ ⊢ Γ, Type@i, A }} by mauto.
+  assert {{ ⊢ Γ, Type@i, A }} by mautosolve.
   eapply wf_conv...
-  Unshelve.
-  all: constructor.
 Qed.
 
 #[export]
 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 solve [mauto].
+Proof with mautosolve.
   intros.
-  assert {{ ⊢ Δ }} by mauto.
-  assert {{ Γ ⊢ M : Type@i[σ] }} by mauto.
+  assert {{ ⊢ Δ }} by mautosolve.
+  assert {{ Γ ⊢ M : Type@i[σ] }} by mautosolve.
   eapply wf_exp_eq_conv...
-  Unshelve.
-  constructor.
 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 solve [mauto].
+Proof with mautosolve.
   inversion 4 as [? Δ'|]; subst.
   assert {{ ⊢ Δ' }} by mauto.
   eapply wf_exp_eq_conv...
@@ -233,58 +217,51 @@ Qed.
 Hint Resolve exp_eq_var_0_sub_typ exp_eq_var_1_sub_typ : mcltt.
 
 Lemma exp_eq_var_0_weaken_typ : forall {Γ A i}, {{ ⊢ Γ , A }} -> {{ #0 : Type@i[Wk] ∈ Γ }} -> {{ Γ , A ⊢ #0[Wk] ≈ #1 : Type@i }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   inversion_clear 1.
   inversion 1 as [? Γ'|]; subst.
   assert {{ ⊢ Γ' }} by mauto.
-  eapply wf_exp_eq_conv; only 1: solve [mauto].
-  eapply exp_eq_typ_sub_sub; [|solve [mauto]]...
+  eapply wf_exp_eq_conv...
 Qed.
 
 #[export]
 Hint Resolve exp_eq_var_0_weaken_typ : mcltt.
 
 Lemma sub_extend_typ : forall {Γ σ Δ M i}, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ M : Type@i }} -> {{ Γ ⊢s (σ ,, M) : Δ , Type@i }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
-  assert {{ ⊢ Δ }} by mauto.
+  assert {{ ⊢ Δ }} by mautosolve.
   econstructor...
-  Unshelve.
-  constructor.
 Qed.
 
 #[export]
 Hint Resolve sub_extend_typ : mcltt.
 
 Lemma sub_eq_extend_cong_typ' : forall {Γ σ σ' Δ M M' i}, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ Γ ⊢ M ≈ M' : Type@i }} -> {{ Γ ⊢s (σ ,, M) ≈ (σ' ,, M') : Δ , Type@i }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
-  assert {{ ⊢ Δ }} by mauto.
+  assert {{ ⊢ Δ }} by mautosolve.
   econstructor...
-  Unshelve.
-  constructor.
 Qed.
 
 Lemma sub_eq_extend_compose_typ : forall {Γ τ Γ' σ Γ'' A i M j}, {{ Γ' ⊢s σ : Γ'' }} -> {{ Γ'' ⊢ A : Type@i }} -> {{ Γ' ⊢ M : Type@j }} -> {{ Γ ⊢s τ : Γ' }} -> {{ Γ ⊢s (σ ,, M) ∘ τ ≈ ((σ ∘ τ) ,, M[τ]) : Γ'' , Type@j }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
   econstructor...
 Qed.
 
 Lemma sub_eq_p_extend_typ : forall {Γ σ Γ' M i}, {{ Γ' ⊢s σ : Γ }} -> {{ Γ' ⊢ M : Type@i }} -> {{ Γ' ⊢s Wk ∘ (σ ,, M) ≈ σ : Γ }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
-  assert {{ ⊢ Γ }} by mauto.
-  econstructor; only 3: solve [mauto]...
-  Unshelve.
-  constructor.
+  assert {{ ⊢ Γ }} by mautosolve.
+  econstructor; revgoals...
 Qed.
 
 #[export]
 Hint Resolve sub_eq_extend_cong_typ' sub_eq_extend_compose_typ sub_eq_p_extend_typ : mcltt.
 
 Lemma exp_eq_sub_sub_compose_cong_typ : forall {Γ Δ Δ' Ψ σ τ σ' τ' A i}, {{ Ψ ⊢ A : Type@i }} -> {{ Δ ⊢s σ : Ψ }} -> {{ Δ' ⊢s σ' : Ψ }} -> {{ Γ ⊢s τ : Δ }} -> {{ Γ ⊢s τ' : Δ' }} -> {{ Γ ⊢s σ∘τ ≈ σ'∘τ' : Ψ }} -> {{ Γ ⊢ A[σ][τ] ≈ A[σ'][τ'] : Type@i }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
   assert {{ Γ ⊢ A[σ][τ] ≈ A[σ∘τ] : Type@i }} by mauto.
   assert {{ Γ ⊢ A[σ∘τ] ≈ A[σ'∘τ'] : Type@i }} by mauto.
@@ -296,30 +273,25 @@ Hint Resolve exp_eq_sub_sub_compose_cong_typ : mcltt.
 
 Lemma exp_sub_nat : forall {Δ Γ M σ}, {{ Δ ⊢ M : ℕ }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ M[σ] : ℕ }}.
 Proof.
-  mauto.
-  Unshelve.
-  constructor.
+  mautosolve.
 Qed.
 
 Lemma exp_eq_sub_cong_nat1 : forall {Δ Γ M M' σ}, {{ Δ ⊢ M ≈ M' : ℕ }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ M[σ] ≈ M'[σ] : ℕ }}.
 Proof.
-  mauto.
-  Unshelve.
-  constructor.
+  mautosolve.
 Qed.
 
 Lemma exp_eq_sub_cong_nat2' : forall {Δ Γ M σ τ}, {{ Δ ⊢ M : ℕ }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢s σ ≈ τ : Δ }} -> {{ Γ ⊢ M[σ] ≈ M[τ] : ℕ }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
   eapply wf_exp_eq_conv...
-  Unshelve.
-  constructor.
 Qed.
 
 Lemma exp_eq_sub_compose_nat : forall {Ψ Δ Γ M σ τ}, {{ Ψ ⊢ M : ℕ }} -> {{ Δ ⊢s σ : Ψ }} -> {{ Γ ⊢s τ : Δ }} -> {{ Γ ⊢ M[σ][τ] ≈ M[σ∘τ] : ℕ }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
   eapply wf_exp_eq_conv...
+  (* This existential comes from wf_exp_eq_conv, on which it is harder to use "unshelve" *)
   Unshelve.
   constructor.
 Qed.
@@ -344,104 +316,86 @@ Qed.
 Hint Resolve exp_eq_nat_sub_sub_to_nat_sub : mcltt.
 
 Lemma vlookup_0_nat : forall {Γ}, {{ ⊢ Γ }} -> {{ Γ, ℕ ⊢ # 0 : ℕ }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
   assert {{ Γ, ℕ ⊢ # 0 : ℕ[Wk] }}...
-  Unshelve.
-  all: constructor.
 Qed.
 
 Lemma vlookup_1_nat : forall {Γ A i}, {{ ⊢ Γ }} -> {{ Γ, ℕ ⊢ A : Type@i }} -> {{ Γ, ℕ, A ⊢ # 1 : ℕ }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
-  assert {{ ⊢ Γ, ℕ }} by mauto.
-  assert {{ ⊢ Γ, ℕ, A }} by mauto.
+  assert {{ ⊢ Γ, ℕ }} by mautosolve.
+  assert {{ ⊢ Γ, ℕ, A }} by mautosolve.
   assert {{ Γ, ℕ, A ⊢ #1 : ℕ[Wk][Wk] }}...
-  Unshelve.
-  all: constructor.
 Qed.
 
 #[export]
 Hint Resolve vlookup_0_nat vlookup_1_nat : mcltt.
 
 Lemma exp_eq_var_0_sub_nat : forall {Γ σ Δ M}, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ M : ℕ }} -> {{ Γ ⊢ #0[σ ,, M] ≈ M : ℕ }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
   assert {{ ⊢ Δ }} by mauto.
-  assert {{ Γ ⊢ M : ℕ[σ] }} by mauto.
+  assert {{ Γ ⊢ M : ℕ[σ] }} by mautosolve.
   assert {{ Γ ⊢ #0[σ,, M] ≈ M : ℕ[σ] }}...
-  Unshelve.
-  all: constructor.
 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 solve [mauto].
+Proof with mautosolve.
   inversion 4 as [? Δ'|]; subst.
   assert {{ ⊢ Δ' }} by mauto.
   assert {{ Γ ⊢ #1[σ,, M] ≈ #0[σ] : ℕ[Wk][σ] }}...
-  Unshelve.
-  constructor.
 Qed.
 
 #[export]
 Hint Resolve exp_eq_var_0_sub_nat exp_eq_var_1_sub_nat : mcltt.
 
 Lemma exp_eq_var_0_weaken_nat : forall {Γ A}, {{ ⊢ Γ , A }} -> {{ #0 : ℕ[Wk] ∈ Γ }} -> {{ Γ , A ⊢ #0[Wk] ≈ #1 : ℕ }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   inversion 1; subst.
   inversion 1 as [? Γ'|]; subst.
   assert {{ ⊢ Γ' }} by mauto.
   assert {{ Γ', ℕ, A ⊢ #0[Wk] ≈ # 1 : ℕ[Wk][Wk] }}...
-  Unshelve.
-  constructor.
 Qed.
 
 #[export]
 Hint Resolve exp_eq_var_0_weaken_nat : mcltt.
 
 Lemma sub_extend_nat : forall {Γ σ Δ M}, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ M : ℕ }} -> {{ Γ ⊢s (σ ,, M) : Δ , ℕ }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
   assert {{ ⊢ Δ }} by mauto.
   econstructor...
-  Unshelve.
-  all: constructor.
 Qed.
 
 #[export]
 Hint Resolve sub_extend_nat : mcltt.
 
 Lemma sub_eq_extend_cong_nat' : forall {Γ σ σ' Δ M M'}, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ Γ ⊢ M ≈ M' : ℕ }} -> {{ Γ ⊢s (σ ,, M) ≈ (σ' ,, M') : Δ , ℕ }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
   assert {{ ⊢ Δ }} by mauto.
   econstructor...
-  Unshelve.
-  all: constructor.
 Qed.
 
 Lemma sub_eq_extend_compose_nat : forall {Γ τ Γ' σ Γ'' A i M}, {{ Γ' ⊢s σ : Γ'' }} -> {{ Γ'' ⊢ A : Type@i }} -> {{ Γ' ⊢ M : ℕ }} -> {{ Γ ⊢s τ : Γ' }} -> {{ Γ ⊢s (σ ,, M) ∘ τ ≈ ((σ ∘ τ) ,, M[τ]) : Γ'' , ℕ }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
   econstructor...
-  Unshelve.
-  all: constructor.
 Qed.
 
 Lemma sub_eq_p_extend_nat : forall {Γ σ Γ' M}, {{ Γ' ⊢s σ : Γ }} -> {{ Γ' ⊢ M : ℕ }} -> {{ Γ' ⊢s Wk ∘ (σ ,, M) ≈ σ : Γ }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
   assert {{ ⊢ Γ }} by mauto.
-  econstructor; only 3: solve [mauto]...
-  Unshelve.
-  all: constructor.
+  econstructor; only 3: mautosolve...
 Qed.
 
 #[export]
 Hint Resolve sub_eq_extend_cong_nat' sub_eq_extend_compose_nat sub_eq_p_extend_nat : mcltt.
 
 Lemma exp_eq_sub_sub_compose_cong_nat : forall {Γ Δ Δ' Ψ σ τ σ' τ' M}, {{ Ψ ⊢ M : ℕ }} -> {{ Δ ⊢s σ : Ψ }} -> {{ Δ' ⊢s σ' : Ψ }} -> {{ Γ ⊢s τ : Δ }} -> {{ Γ ⊢s τ' : Δ' }} -> {{ Γ ⊢s σ∘τ ≈ σ'∘τ' : Ψ }} -> {{ Γ ⊢ M[σ][τ] ≈ M[σ'][τ'] : ℕ }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
   assert {{ Γ ⊢ M[σ][τ] ≈ M[σ∘τ] : ℕ }} by mauto.
   assert {{ Γ ⊢ M[σ∘τ] ≈ M[σ'∘τ'] : ℕ }} by mauto.
@@ -452,7 +406,7 @@ Qed.
 Hint Resolve exp_eq_sub_sub_compose_cong_nat : mcltt.
 
 Lemma exp_eq_sub_sub_compose_cong : forall {Γ Δ Δ' Ψ σ τ σ' τ' M A i}, {{ Ψ ⊢ A : Type@i }} -> {{ Ψ ⊢ M : A }} -> {{ Δ ⊢s σ : Ψ }} -> {{ Δ' ⊢s σ' : Ψ }} -> {{ Γ ⊢s τ : Δ }} -> {{ Γ ⊢s τ' : Δ' }} -> {{ Γ ⊢s σ∘τ ≈ σ'∘τ' : Ψ }} -> {{ Γ ⊢ M[σ][τ] ≈ M[σ'][τ'] : A[σ∘τ] }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
   assert {{ Γ ⊢ M[σ][τ] ≈ M[σ∘τ] : A[σ∘τ] }} by mauto.
   assert {{ Γ ⊢ M[σ∘τ] ≈ M[σ'∘τ'] : A[σ∘τ] }} by mauto.
@@ -464,7 +418,7 @@ Qed.
 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 solve [mauto].
+Proof with mautosolve.
   intros * HΓ.
   induction 1; inversion_clear HΓ; [|assert (exists i, {{ Γ ⊢ A : Type@i }}) as [] by eauto]...
 Qed.
@@ -473,7 +427,7 @@ Qed.
 Hint Resolve ctx_lookup_wf : mcltt.
 
 Lemma ctxeq_ctx_lookup : forall {Γ Δ A x}, {{ ⊢ Γ ≈ Δ }} -> {{ #x : A ∈ Γ }} -> exists B i, {{ #x : B ∈ Δ }} /\ {{ Γ ⊢ A ≈ B : Type@i }} /\ {{ Δ ⊢ A ≈ B : Type@i }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros * HΓΔ Hx; gen Δ.
   induction Hx as [|* ? IHHx]; inversion_clear 1 as [|? ? ? ? ? HΓΔ'];
     [|specialize (IHHx _ HΓΔ')]; destruct_conjs; repeat eexists...
@@ -483,7 +437,7 @@ Qed.
 Hint Resolve ctxeq_ctx_lookup : mcltt.
 
 Lemma sub_id_extend : forall {Γ M A i}, {{ Γ ⊢ A : Type@i }} -> {{ Γ ⊢ M : A }} -> {{ Γ ⊢s Id,,M : Γ, A }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
   econstructor...
 Qed.
@@ -492,7 +446,7 @@ Qed.
 Hint Resolve sub_id_extend : mcltt.
 
 Lemma sub_eq_p_id_extend : forall {Γ M A i}, {{ Γ ⊢ A : Type@i }} -> {{ Γ ⊢ M : A }} -> {{ Γ ⊢s Wk∘(Id ,, M) ≈ Id : Γ }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
   econstructor...
 Qed.
@@ -501,14 +455,14 @@ Qed.
 Hint Resolve sub_eq_p_id_extend : mcltt.
 
 Lemma sub_q : forall {Γ A i σ Δ}, {{ Δ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ , A[σ] ⊢s q σ : Δ , A }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
   assert {{ Γ, A[σ] ⊢ # 0 : A[σ][Wk] }} by mauto.
-  econstructor; [econstructor| |]...
+  econstructor...
 Qed.
 
 Lemma sub_q_typ : forall {Γ σ Δ i}, {{ Γ ⊢s σ : Δ }} -> {{ Γ , Type@i ⊢s q σ : Δ , Type@i }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
   assert {{ ⊢ Δ }} by mauto.
   assert {{ Γ, Type@i ⊢s σ ∘ Wk : Δ }} by (econstructor; mauto).
@@ -517,7 +471,7 @@ Proof with solve [mauto].
 Qed.
 
 Lemma sub_q_nat : forall {Γ σ Δ}, {{ Γ ⊢s σ : Δ }} -> {{ Γ , ℕ ⊢s q σ : Δ , ℕ }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
   assert {{ ⊢ Δ }} by mauto.
   assert {{ Γ, ℕ ⊢s σ ∘ Wk : Δ }} by (econstructor; mauto).
@@ -529,7 +483,7 @@ Qed.
 Hint Resolve sub_q sub_q_typ sub_q_nat : mcltt.
 
 Lemma exp_eq_var_1_sub_q_sigma_nat : forall {Γ A i σ Δ}, {{ Δ, ℕ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ, ℕ, A[q σ] ⊢ #1[q (q σ)] ≈ #1 : ℕ }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
   assert {{ ⊢ Δ }} by mauto.
   assert {{ ⊢ Δ, ℕ }} by mauto.
@@ -554,7 +508,7 @@ Proof.
 Qed.
 
 Lemma sub_weak_compose_weak_extend_succ_var_1 : forall {Γ A i}, {{ Γ, ℕ ⊢ A : Type@i }} -> {{ Γ, ℕ, A ⊢s Wk∘Wk,,succ #1 : Γ, ℕ }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
   assert {{ ⊢ Γ, ℕ }} by mauto.
   assert {{ ⊢ Γ }} by mauto.
@@ -562,16 +516,14 @@ Proof with solve [mauto].
 Qed.
 
 Lemma sub_eq_id_extend_nat_compose_sigma : forall {Γ M σ Δ}, {{ Γ ⊢s σ : Δ }} -> {{ Δ ⊢ M : ℕ }} -> {{ Γ ⊢s (Id,,M)∘σ ≈ σ,,M[σ] : Δ, ℕ }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
-  assert {{ Γ ⊢s (Id ,, M)∘σ ≈ Id∘σ ,, M[σ] : Δ, ℕ }} by (eapply sub_eq_extend_compose_nat; mauto).
+  assert {{ Γ ⊢s (Id ,, M)∘σ ≈ Id∘σ ,, M[σ] : Δ, ℕ }} by (eapply sub_eq_extend_compose_nat; mautosolve).
   assert {{ Γ ⊢s Id∘σ ,, M[σ] ≈ σ ,, M[σ] : Δ, ℕ }} by (eapply sub_eq_extend_cong_nat'; mauto)...
-  Unshelve.
-  constructor.
 Qed.
 
 Lemma sub_eq_id_extend_compose_sigma : forall {Γ M A σ Δ i}, {{ Γ ⊢s σ : Δ }} -> {{ Δ ⊢ A : Type@i }} -> {{ Δ ⊢ M : A }} -> {{ Γ ⊢s (Id,,M)∘σ ≈ σ,,M[σ] : Δ, A }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
   assert {{ Γ ⊢s (Id ,, M)∘σ ≈ Id∘σ ,, M[σ] : Δ, A }} by (eapply wf_sub_eq_extend_compose; mauto).
   assert {{ Γ ⊢ M[σ] ≈ M[σ] : A[σ] }} by mauto.
@@ -582,7 +534,7 @@ Qed.
 Hint Resolve sub_id_extend_zero sub_weak_compose_weak_extend_succ_var_1 sub_eq_id_extend_nat_compose_sigma sub_eq_id_extend_compose_sigma : mcltt.
 
 Lemma sub_eq_sigma_compose_weak_id_extend : forall {Γ M A i σ Δ}, {{ Γ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ M : A }} -> {{ Γ ⊢s (σ∘Wk)∘(Id,,M) ≈ σ : Δ }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
   assert {{ Γ ⊢s Id,,M : Γ, A }} by mauto.
   assert {{ Γ ⊢s (σ∘Wk)∘(Id,,M) ≈ σ∘(Wk∘(Id ,, M)) : Δ }} by mauto.
@@ -594,7 +546,7 @@ Qed.
 Hint Resolve sub_eq_sigma_compose_weak_id_extend : mcltt.
 
 Lemma sub_eq_q_sigma_id_extend : forall {Γ M A i σ Δ}, {{ Δ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ M : A[σ] }} -> {{ Γ ⊢s q σ∘(Id,,M) ≈ σ,,M : Δ, A }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
   assert {{ Γ ⊢s Id ,, M : Γ, A[σ] }} by mauto.
   assert {{ Γ, A[σ] ⊢ #0 : A[σ][Wk] }} by mauto.
@@ -611,7 +563,7 @@ 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 solve [mauto].
+Proof with mautosolve.
   intros.
   assert {{ ⊢ Γ }} by mauto.
   assert {{ Γ, A[σ] ⊢ #0 : A[σ][Wk] }} by mauto.
@@ -622,7 +574,7 @@ Qed.
 Hint Resolve sub_eq_p_q_sigma : mcltt.
 
 Lemma sub_eq_p_q_sigma_nat : forall {Γ σ Δ}, {{ Γ ⊢s σ : Δ }} -> {{ Γ, ℕ ⊢s Wk∘q σ ≈ σ∘Wk : Δ }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
   assert {{ ⊢ Γ }} by mauto.
   assert {{ Γ, ℕ ⊢ #0 : ℕ }}...
@@ -632,7 +584,7 @@ Qed.
 Hint Resolve sub_eq_p_q_sigma_nat : mcltt.
 
 Lemma sub_eq_p_p_q_q_sigma_nat : forall {Γ A i σ Δ}, {{ Δ, ℕ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ, ℕ, A[q σ] ⊢s Wk∘(Wk∘q (q σ)) ≈ (σ∘Wk)∘Wk : Δ }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
   assert {{ ⊢ Γ }} by mauto.
   assert {{ Γ, ℕ, A[q σ] ⊢s Wk∘q (q σ) ≈ q σ ∘ Wk : Δ, ℕ }} by mauto.
@@ -647,7 +599,7 @@ Qed.
 Hint Resolve sub_eq_p_p_q_q_sigma_nat : mcltt.
 
 Lemma sub_eq_q_sigma_compose_weak_weak_extend_succ_var_1 : forall {Γ A i σ Δ}, {{ Δ, ℕ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ, ℕ, A[q σ] ⊢s q σ∘(Wk∘Wk,,succ #1) ≈ (Wk∘Wk,,succ #1)∘q (q σ) : Δ, ℕ }}.
-Proof with solve [mauto].
+Proof with mautosolve.
   intros.
   assert {{ ⊢ Δ }} by mauto.
   assert {{ Γ, ℕ ⊢s Wk : Γ }} by mauto.
@@ -656,7 +608,7 @@ Proof with solve [mauto].
   set (WkWksucc := {{{ Wk∘Wk ,, succ #1 }}}).
   assert {{ Γ' ⊢s Wk ∘ Wk : Γ }} by mauto.
   assert {{ Γ' ⊢s WkWksucc : Γ, ℕ }} by mauto.
-  assert {{ Γ' ⊢s q σ∘WkWksucc ≈ (σ∘Wk)∘WkWksucc ,, #0[WkWksucc] : Δ, ℕ }} by mauto.
+  assert {{ Γ' ⊢s q σ∘WkWksucc ≈ (σ∘Wk)∘WkWksucc ,, #0[WkWksucc] : Δ, ℕ }} by mautosolve.
   assert {{ Γ' ⊢ #1 : ℕ }} by mauto.
   assert {{ Γ' ⊢ succ #1 : ℕ }} by mauto.
   assert {{ Γ' ⊢s Wk∘WkWksucc ≈ Wk∘Wk : Γ }} by mauto.
@@ -676,8 +628,6 @@ Proof with solve [mauto].
   assert {{ Δ, ℕ, A ⊢ #1 : ℕ }} by mauto.
   assert {{ Δ, ℕ, A ⊢ succ #1 : ℕ }} by mauto.
   assert {{ Γ' ⊢s (Wk∘Wk)∘q (q σ) ,, (succ #1)[q (q σ)] ≈ WkWksucc∘q (q σ) : Δ, ℕ }}...
-  Unshelve.
-  all: constructor.
 Qed.
 
 #[export]
diff --git a/theories/LibTactics.v b/theories/LibTactics.v
index 464910a1..c3ca18e6 100644
--- a/theories/LibTactics.v
+++ b/theories/LibTactics.v
@@ -151,3 +151,5 @@ 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].