diff --git a/theories/Core/Semantic/Evaluation/Lemmas.v b/theories/Core/Semantic/Evaluation/Lemmas.v
index f194bead..ca603fcc 100644
--- a/theories/Core/Semantic/Evaluation/Lemmas.v
+++ b/theories/Core/Semantic/Evaluation/Lemmas.v
@@ -14,51 +14,47 @@ 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 using.
+  Proof with ((on_all_hyp: fun H => erewrite H in *; eauto); eauto) using.
     induction Heval1
       using eval_exp_mut_ind
       with (P0 := functional_eval_natrec_prop)
            (P1 := functional_eval_app_prop)
            (P2 := functional_eval_sub_prop);
-      unfold_functional_eval; mauto;
-      intros; inversion_clear Heval2; subst; do 2 f_equal;
-      (on_all_hyp: fun H => try erewrite H in *; mauto); mauto.
+      unfold_functional_eval;
+      inversion_clear 1; do 2 f_equal...
   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 using.
+  Proof with ((on_all_hyp: fun H => erewrite H in *; eauto); eauto) using.
     induction Heval1
       using eval_natrec_mut_ind
       with (P := functional_eval_exp_prop)
            (P1 := functional_eval_app_prop)
            (P2 := functional_eval_sub_prop);
-      unfold_functional_eval; mauto;
-      intros; inversion Heval2; clear Heval2; subst; do 2 f_equal;
-      (on_all_hyp: fun H => try erewrite H in *; mauto); mauto.
+      unfold_functional_eval;
+      inversion_clear 1; do 2 f_equal...
   Qed.
 
   Lemma functional_eval_app : forall m n r1 (Heval1 : {{ $| m & n |↘ r1 }}), functional_eval_app_prop m n r1 Heval1.
-  Proof using.
+  Proof with ((on_all_hyp: fun H => erewrite H in *; eauto); eauto) using.
     induction Heval1
       using eval_app_mut_ind
       with (P := functional_eval_exp_prop)
            (P0 := functional_eval_natrec_prop)
            (P2 := functional_eval_sub_prop);
-      unfold_functional_eval; mauto;
-      intros; inversion Heval2; clear Heval2; subst; do 2 f_equal;
-      (on_all_hyp: fun H => try erewrite H in *; mauto); mauto.
+      unfold_functional_eval;
+      inversion_clear 1; do 2 f_equal...
   Qed.
 
   Lemma functional_eval_sub : forall σ p p1 (Heval1 : {{ ⟦ σ ⟧s p ↘ p1 }}), functional_eval_sub_prop σ p p1 Heval1.
-  Proof using.
+  Proof with ((on_all_hyp: fun H => erewrite H in *; eauto); eauto) using.
     induction Heval1
       using eval_sub_mut_ind
       with (P := functional_eval_exp_prop)
            (P0 := functional_eval_natrec_prop)
            (P1 := functional_eval_app_prop);
-      unfold_functional_eval; mauto;
-      intros; inversion Heval2; clear Heval2; subst; do 2 f_equal;
-      (on_all_hyp: fun H => try erewrite H in *; mauto); mauto.
+      unfold_functional_eval;
+      inversion_clear 1; do 2 f_equal...
   Qed.
 End functional_eval.
 
@@ -66,14 +62,15 @@ End functional_eval.
 Hint Resolve functional_eval_exp functional_eval_natrec functional_eval_app functional_eval_sub : mcltt.
 
 Ltac functional_eval_rewrite_clear1 :=
+  let tactic_error o1 o2 := fail 3 "functional_eval equality between" o1 "and" o2 "cannot be solved by mauto" in
   match goal with
   | H1 : {{ ⟦ ~?M ⟧ ~?p ↘ ~?m1 }}, H2 : {{ ⟦ ~?M ⟧ ~?p ↘ ~?m2 }} |- _ =>
-      clean replace m2 with m1 by mauto; clear H2
+      clean replace m2 with m1 by first [solve [mauto] | tactic_error m2 m1]; clear H2
   | H1 : {{ $| ~?m & ~?n |↘ ~?r1 }}, H2 : {{ $| ~?m & ~?n |↘ ~?r2 }} |- _ =>
-      clean replace r2 with r1 by mauto; clear H2
+      clean replace r2 with r1 by first [solve [mauto] | tactic_error r2 r1]; clear H2
   | H1 : {{ rec ~?m ⟦return ~?A | zero -> ~?MZ | succ -> ~?MS end⟧ ~?p ↘ ~?r1 }}, H2 : {{ rec ~?m ⟦return ~?A | zero -> ~?MZ | succ -> ~?MS end⟧ ~?p ↘ ~?r2 }} |- _ =>
-      clean replace r2 with r1 by mauto; clear H2
+      clean replace r2 with r1 by first [solve [mauto] | tactic_error r2 r1]; clear H2
   | H1 : {{ ⟦ ~?σ ⟧s ~?p ↘ ~?p1 }}, H2 : {{ ⟦ ~?σ ⟧s ~?p ↘ ~?p2 }} |- _ =>
-      clean replace p2 with p1 by mauto; clear H2
+      clean replace p2 with p1 by first [solve [mauto] | tactic_error p2 p1]; clear H2
   end.
 Ltac functional_eval_rewrite_clear := repeat functional_eval_rewrite_clear1.
diff --git a/theories/Core/Semantic/PER/Definitions.v b/theories/Core/Semantic/PER/Definitions.v
index de2e898d..1323d94c 100644
--- a/theories/Core/Semantic/PER/Definitions.v
+++ b/theories/Core/Semantic/PER/Definitions.v
@@ -210,6 +210,7 @@ Ltac per_univ_elem_econstructor :=
 (** Context/Environment PER *)
 
 Definition rel_typ (i : nat) (A : typ) (p : env) (A' : typ) (p' : env) R' := rel_mod_eval (per_univ_elem i) A p A' p' R'.
+Arguments rel_typ _ _ _ _ _ _ /.
 
 Definition per_total : relation env := fun p p' => True.
 
diff --git a/theories/Core/Semantic/PER/Lemmas.v b/theories/Core/Semantic/PER/Lemmas.v
index 858203b4..aa9a4997 100644
--- a/theories/Core/Semantic/PER/Lemmas.v
+++ b/theories/Core/Semantic/PER/Lemmas.v
@@ -7,7 +7,8 @@ Lemma per_bot_sym : forall m n,
     {{ Dom n ≈ m ∈ per_bot }}.
 Proof with solve [eauto].
   intros * H s.
-  destruct (H s) as [? []]...
+  pose proof H s.
+  destruct_conjs...
 Qed.
 
 #[export]
@@ -19,8 +20,8 @@ Lemma per_bot_trans : forall m n l,
     {{ Dom m ≈ l ∈ per_bot }}.
 Proof with solve [eauto].
   intros * Hmn Hnl s.
-  destruct (Hmn s) as [? []].
-  destruct (Hnl s) as [? []].
+  pose proof (Hmn s, Hnl s).
+  destruct_conjs.
   functional_read_rewrite_clear...
 Qed.
 
@@ -30,7 +31,7 @@ Hint Resolve per_bot_trans : mcltt.
 Lemma var_per_bot : forall {n},
     {{ Dom !n ≈ !n ∈ per_bot }}.
 Proof.
-  intros n s. repeat econstructor.
+  intros ? ?. repeat econstructor.
 Qed.
 
 #[export]
@@ -41,7 +42,8 @@ Lemma per_top_sym : forall m n,
     {{ Dom n ≈ m ∈ per_top }}.
 Proof with solve [eauto].
   intros * H s.
-  destruct (H s) as [? []]...
+  pose proof H s.
+  destruct_conjs...
 Qed.
 
 #[export]
@@ -53,8 +55,8 @@ Lemma per_top_trans : forall m n l,
     {{ Dom m ≈ l ∈ per_top }}.
 Proof with solve [eauto].
   intros * Hmn Hnl s.
-  destruct (Hmn s) as [? []].
-  destruct (Hnl s) as [? []].
+  pose proof (Hmn s, Hnl s).
+  destruct_conjs.
   functional_read_rewrite_clear...
 Qed.
 
@@ -78,7 +80,8 @@ Lemma per_top_typ_sym : forall m n,
     {{ Dom n ≈ m ∈ per_top_typ }}.
 Proof with solve [eauto].
   intros * H s.
-  destruct (H s) as [? []]...
+  pose proof H s.
+  destruct_conjs...
 Qed.
 
 #[export]
@@ -90,23 +93,18 @@ Lemma per_top_typ_trans : forall m n l,
     {{ Dom m ≈ l ∈ per_top_typ }}.
 Proof with solve [eauto].
   intros * Hmn Hnl s.
-  destruct (Hmn s) as [? []].
-  destruct (Hnl s) as [? []].
+  pose proof (Hmn s, Hnl s).
+  destruct_conjs.
   functional_read_rewrite_clear...
 Qed.
 
 #[export]
 Hint Resolve per_top_typ_trans : mcltt.
 
-Lemma PER_per_top_typ : PER per_top_typ.
-Proof with solve [mauto].
-  econstructor...
-Qed.
-
 Lemma per_nat_sym : forall m n,
     {{ Dom m ≈ n ∈ per_nat }} ->
     {{ Dom n ≈ m ∈ per_nat }}.
-Proof with solve [mauto].
+Proof with solve [eauto using per_bot_sym].
   induction 1; econstructor...
 Qed.
 
@@ -117,9 +115,9 @@ 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 [mauto].
+Proof with solve [eauto using per_bot_trans].
   intros * H. gen l.
-  induction H; intros * H'; inversion_clear H'; econstructor...
+  induction H; inversion_clear 1; econstructor...
 Qed.
 
 #[export]
@@ -128,7 +126,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 [mauto].
+Proof with solve [eauto using per_bot_sym].
   intros * [].
   econstructor...
 Qed.
@@ -140,9 +138,9 @@ 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 [mauto].
-  intros * [] Hnl.
-  inversion_clear Hnl.
+Proof with solve [eauto using per_bot_trans].
+  intros * [].
+  inversion_clear 1.
   econstructor...
 Qed.
 
@@ -153,60 +151,62 @@ 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.
+Proof with solve [eauto].
   intros * Horig.
   remember A as A' in |- *.
   gen A' B' R'.
   induction Horig using per_univ_elem_ind; intros * Heq Hright;
-    try solve [induction Hright using per_univ_elem_ind; congruence].
-  subst.
-  invert_per_univ_elem Hright; try congruence.
+    subst; invert_per_univ_elem Hright; unfold per_univ;
+    try congruence.
   specialize (IHHorig _ _ _ eq_refl equiv_a_a').
   subst.
   extensionality f.
   extensionality f'.
-  rewrite H2, H10.
+  (on_all_hyp: fun H => rewrite H).
   extensionality c.
   extensionality c'.
   extensionality equiv_c_c'.
   destruct_rel_mod_eval.
   functional_eval_rewrite_clear.
-  specialize (H12 _ _ _ eq_refl H5).
-  congruence.
+  f_equal...
 Qed.
 
+#[local]
 Ltac per_univ_elem_right_irrel_rewrite1 :=
   match goal with
   | H1 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }}, H2 : {{ DF ~?A ≈ ~?B' ∈ per_univ_elem ?i ↘ ?R2 }} |- _ =>
-      clean replace R2 with R1 by (eauto using per_univ_elem_right_irrel)
+      clean replace R2 with R1 by first [solve [eauto using per_univ_elem_right_irrel] | fail 3]
   end.
+#[local]
 Ltac per_univ_elem_right_irrel_rewrite := repeat per_univ_elem_right_irrel_rewrite1.  
 
 Lemma per_univ_elem_sym : forall i A B R,
     per_univ_elem i A B R ->
-    per_univ_elem i B A R /\ (forall a b, {{ Dom a ≈ b ∈ R }} -> {{ Dom b ≈ a ∈ R }}).
-Proof with solve [try econstructor; mauto].
+    per_univ_elem i B A 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].
   induction 1 using per_univ_elem_ind; subst.
   - split.
     + apply per_univ_elem_core_univ'...
-    + intros * [].
-      specialize (H1 _ _ _ H0) as []...
+    + intros * [? []%H1]...
   - split...
-  - destruct IHper_univ_elem as [? ?].
-    setoid_rewrite H2.
+  - destruct_conjs.
+    (on_all_hyp: fun H => setoid_rewrite H).
     split.
     + per_univ_elem_econstructor; eauto.
       intros.
-      assert (in_rel c' c) by firstorder.
+      assert (in_rel c' c) by eauto.
       assert (in_rel c c) by (etransitivity; eassumption).
       destruct_rel_mod_eval.
       functional_eval_rewrite_clear.
       per_univ_elem_right_irrel_rewrite...
     + enough (forall a b : domain,
                  (forall (c c' : domain) (equiv_c_c' : in_rel c c'), rel_mod_app (out_rel c c' equiv_c_c') a c b c') ->
-                 (forall (c c' : domain) (equiv_c_c' : in_rel c c'), rel_mod_app (out_rel c c' equiv_c_c') b c a c')) by firstorder.
+                 (forall (c c' : domain) (equiv_c_c' : in_rel c c'), rel_mod_app (out_rel c c' equiv_c_c') b c a c')) by eauto.
       intros.
-      assert (in_rel c' c) by firstorder.
+      assert (in_rel c' c) by eauto.
       assert (in_rel c c) by (etransitivity; eassumption).
       destruct_rel_mod_eval.
       destruct_rel_mod_app.
@@ -219,16 +219,19 @@ 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 * HS.
-  apply per_univ_elem_sym; assumption.
+  intros.
+  apply per_univ_elem_sym.
+  assumption.
 Qed.
 
 Corollary per_elem_sym : forall i A B a b R,
     per_univ_elem i A B R ->
-    R a b -> R b a.
+    R a b ->
+    R b a.
 Proof.
-  intros * HS.
-  eapply per_univ_elem_sym; eassumption.
+  intros * ?.
+  eapply per_univ_elem_sym.
+  eassumption.
 Qed.
 
 Lemma per_univ_elem_left_irrel : forall i i' A B R A' R',
@@ -236,7 +239,7 @@ Lemma per_univ_elem_left_irrel : forall i i' A B R A' R',
     per_univ_elem i' A' B R' ->
     R = R'.
 Proof.
-  intros * []%per_univ_elem_sym []%per_univ_elem_sym.
+  intros * ?%per_univ_sym ?%per_univ_sym.
   eauto using per_univ_elem_right_irrel.
 Qed.
 
@@ -245,22 +248,23 @@ Lemma per_univ_elem_cross_irrel : forall i i' A B R B' R',
     per_univ_elem i' B' A R' ->
     R = R'.
 Proof.
-  intros * ? []%per_univ_elem_sym.
+  intros * ? ?%per_univ_sym.
   eauto using per_univ_elem_right_irrel.
 Qed.
 
 Ltac do_per_univ_elem_irrel_rewrite1 :=
+  let tactic_error o1 o2 := fail 3 "per_univ_elem_irrel equality between" o1 "and" o2 "cannot be solved by eauto" in
   match goal with
     | H1 : {{ DF ~?A ≈ ~_ ∈ per_univ_elem ?i ↘ ?R1 }},
         H2 : {{ DF ~?A ≈ ~_ ∈ per_univ_elem ?i' ↘ ?R2 }} |- _ =>
-        clean replace R2 with R1 by (eauto using per_univ_elem_right_irrel)
+        clean replace R2 with R1 by first [solve [eauto using per_univ_elem_right_irrel] | tactic_error R2 R1]
     | H1 : {{ DF ~_ ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }},
         H2 : {{ DF ~_ ≈ ~?B ∈ per_univ_elem ?i' ↘ ?R2 }} |- _ =>
-        clean replace R2 with R1 by (eauto using per_univ_elem_left_irrel)
+        clean replace R2 with R1 by first [solve [eauto using per_univ_elem_left_irrel] | tactic_error R2 R1]
     | H1 : {{ DF ~?A ≈ ~_ ∈ per_univ_elem ?i ↘ ?R1 }},
         H2 : {{ DF ~_ ≈ ~?A ∈ per_univ_elem ?i' ↘ ?R2 }} |- _ =>
         (* Order matters less here as H1 and H2 cannot be exchanged *)
-        clean replace R2 with R1 by (symmetry; eauto using per_univ_elem_cross_irrel)
+        clean replace R2 with R1 by first [solve [symmetry; eauto using per_univ_elem_cross_irrel] | tactic_error R2 R1]
     end.
 
 Ltac do_per_univ_elem_irrel_rewrite :=
@@ -276,12 +280,15 @@ Lemma per_univ_elem_trans : forall i A1 A2 R,
     (forall j A3,
         per_univ_elem j A2 A3 R ->
         per_univ_elem i A1 A3 R) /\
-      (forall a1 a2 a3, R a1 a2 -> R a2 a3 -> R a1 a3).
-Proof with solve [mauto| firstorder (econstructor; eauto)].
+      (forall a1 a2 a3,
+          R a1 a2 ->
+          R a2 a3 ->
+          R a1 a3).
+Proof with solve [eauto using per_bot_trans | econstructor; eauto].
   induction 1 using per_univ_elem_ind;
     [> split;
-       [ intros * HT2; invert_per_univ_elem HT2; clear HT2
-       | intros * HTR1 HTR2 ] ..]; mauto.
+     [ intros * HT2; invert_per_univ_elem HT2; clear HT2
+     | intros * HTR1 HTR2 ] ..]; mauto.
   - destruct HTR1, HTR2.
     per_univ_elem_irrel_rewrite.
     specialize (H1 _ _ _ H2) as [].
@@ -289,20 +296,20 @@ Proof with solve [mauto| firstorder (econstructor; eauto)].
   - idtac...
   - per_univ_elem_irrel_rewrite.
     rename in_rel0 into in_rel.
-    destruct IHper_univ_elem as [? _].
-    per_univ_elem_econstructor; mauto.
+    destruct IHper_univ_elem as [].
+    per_univ_elem_econstructor; eauto.
     intros.
     assert (in_rel c c) by (etransitivity; [ | symmetry]; eassumption).
     destruct_rel_mod_eval.
     per_univ_elem_irrel_rewrite...
-  - destruct IHper_univ_elem as [? ?].
+  - destruct IHper_univ_elem as [].
     rewrite H2 in *.
     intros.
     assert (in_rel c' c') by (etransitivity; [symmetry | ]; eassumption).
     destruct_rel_mod_eval.
     destruct_rel_mod_app.
     per_univ_elem_irrel_rewrite...
-  - try per_univ_elem_econstructor...
+  - per_univ_elem_econstructor...
 Qed.
 
 Corollary per_univ_trans : forall i j A1 A2 A3 R,
@@ -310,26 +317,29 @@ 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 * HT1.
-  apply per_univ_elem_trans; assumption.
+  intros * ?.
+  apply per_univ_elem_trans.
+  assumption.
 Qed.
 
 Corollary per_elem_trans : forall i A1 A2 a1 a2 a3 R,
     per_univ_elem i A1 A2 R ->
-    R a1 a2 -> R a2 a3 -> R a1 a3.
+    R a1 a2 ->
+    R a2 a3 ->
+    R a1 a3.
 Proof.
-  intros * HT1.
-  eapply per_univ_elem_trans; eassumption.
+  intros * ?.
+  eapply per_univ_elem_trans.
+  eassumption.
 Qed.
 
 Lemma per_univ_elem_cumu : forall {i a0 a1 R},
     {{ DF a0 ≈ a1 ∈ per_univ_elem i ↘ R }} ->
     {{ DF a0 ≈ a1 ∈ per_univ_elem (S i) ↘ R }}.
-Proof with solve [mauto].
+Proof with solve [eauto].
   simpl.
   induction 1 using per_univ_elem_ind; subst.
-  - eapply per_univ_elem_core_univ'.
-    lia.
+  - eapply per_univ_elem_core_univ'...
   - per_univ_elem_econstructor.
   - per_univ_elem_econstructor; mauto.
     intros.
@@ -345,16 +355,14 @@ Lemma per_ctx_env_right_irrel : forall Γ Δ Δ' R R',
 Proof.
   intros * Horig; gen Δ' R'.
   induction Horig; intros * Hright;
-    try solve [inversion Hright; congruence].
-  subst.
-  inversion_clear Hright.
+    inversion Hright; subst; try congruence.
   specialize (IHHorig _ _ equiv_Γ_Γ'0).
   subst.
-  enough (head_rel = head_rel0) by (subst; easy).
+  enough (head_rel = head_rel0) by now subst.
   extensionality p.
   extensionality p'.
   extensionality equiv_p_p'.
-  unfold rel_typ in *.
+  simpl in *.
   destruct_rel_mod_eval.
   per_univ_elem_irrel_rewrite.
   congruence.
@@ -362,20 +370,24 @@ Qed.
 
 Lemma per_ctx_env_sym : forall Γ Δ R,
     {{ DF Γ ≈ Δ ∈ per_ctx_env ↘ R }} ->
-    {{ DF Δ ≈ Γ ∈ per_ctx_env ↘ R }} /\ (forall o p, {{ Dom o ≈ p ∈ R }} -> {{ Dom p ≈ o ∈ R }}).
-Proof with solve [eauto].
+    {{ DF Δ ≈ Γ ∈ per_ctx_env ↘ R }} /\
+      (forall o p,
+          {{ Dom o ≈ p ∈ R }} ->
+          {{ Dom p ≈ o ∈ R }}).
+Proof with solve [eauto using per_univ_sym].
   simpl.
-  induction 1; firstorder; try solve [econstructor; eauto]; unfold rel_typ in *.
-  - econstructor; eauto; firstorder.
+  induction 1; split; try solve [econstructor; eauto]; simpl in *; destruct_conjs.
+  - econstructor; eauto.
+    intros.
     assert (tail_rel p' p) by eauto.
     assert (tail_rel p p) by (etransitivity; eauto).
     destruct_rel_mod_eval.
     per_univ_elem_irrel_rewrite.
-    econstructor; eauto.
-    apply per_univ_sym...
+    econstructor...
   - subst.
-    firstorder.
-    assert (tail_rel d{{{ p ↯ }}} d{{{ o ↯ }}}) by (unfold Symmetric in *; eauto).
+    intros.
+    destruct_conjs.
+    assert (tail_rel d{{{ p ↯ }}} d{{{ o ↯ }}}) by eauto.
     assert (tail_rel d{{{ p ↯ }}} d{{{ p ↯ }}}) by (etransitivity; eauto).
     destruct_rel_mod_eval.
     eexists.
@@ -383,12 +395,31 @@ Proof with solve [eauto].
     eapply per_elem_sym...
 Qed.
 
+Corollary per_ctx_sym : forall Γ Δ R,
+    {{ DF Γ ≈ Δ ∈ per_ctx_env ↘ R }} ->
+    {{ DF Δ ≈ Γ ∈ per_ctx_env ↘ R }}.
+Proof.
+  intros.
+  apply per_ctx_env_sym.
+  assumption.
+Qed.
+
+Corollary per_env_sym : forall Γ Δ R o p,
+    {{ DF Γ ≈ Δ ∈ per_ctx_env ↘ R }} ->
+    {{ Dom o ≈ p ∈ R }} ->
+    {{ Dom p ≈ o ∈ R }}.
+Proof.
+  intros * ?.
+  eapply per_ctx_env_sym.
+  eassumption.
+Qed.
+
 Lemma per_ctx_env_left_irrel : forall Γ Γ' Δ R R',
     {{ DF Γ ≈ Δ ∈ per_ctx_env ↘ R }} ->
     {{ DF Γ' ≈ Δ ∈ per_ctx_env ↘ R' }} ->
     R = R'.
 Proof.
-  intros * []%per_ctx_env_sym []%per_ctx_env_sym.
+  intros * ?%per_ctx_sym ?%per_ctx_sym.
   eauto using per_ctx_env_right_irrel.
 Qed.
 
@@ -397,22 +428,23 @@ Lemma per_ctx_env_cross_irrel : forall Γ Δ Δ' R R',
     {{ DF Δ' ≈ Γ ∈ per_ctx_env ↘ R' }} ->
     R = R'.
 Proof.
-  intros * ? []%per_ctx_env_sym.
+  intros * ? ?%per_ctx_sym.
   eauto using per_ctx_env_right_irrel.
 Qed.
 
 Ltac do_per_ctx_env_irrel_rewrite1 :=
+  let tactic_error o1 o2 := fail 3 "per_ctx_env_irrel equality between" o1 "and" o2 "cannot be solved by mauto" in
   match goal with
     | H1 : {{ DF ~?Γ ≈ ~_ ∈ per_ctx_env ↘ ?R1 }},
         H2 : {{ DF ~?Γ ≈ ~_ ∈ per_ctx_env ↘ ?R2 }} |- _ =>
-        clean replace R2 with R1 by (eauto using per_ctx_env_right_irrel)
+        clean replace R2 with R1 by first [solve [eauto using per_ctx_env_right_irrel] | tactic_error R2 R1]
     | H1 : {{ DF ~_ ≈ ~?Δ ∈ per_ctx_env ↘ ?R1 }},
         H2 : {{ DF ~_ ≈ ~?Δ ∈ per_ctx_env ↘ ?R2 }} |- _ =>
-        clean replace R2 with R1 by (eauto using per_ctx_env_left_irrel)
+        clean replace R2 with R1 by first [solve [eauto using per_ctx_env_left_irrel] | tactic_error R2 R1]
     | H1 : {{ DF ~?Γ ≈ ~_ ∈ per_ctx_env ↘ ?R1 }},
         H2 : {{ DF ~_ ≈ ~?Γ ∈ per_ctx_env ↘ ?R2 }} |- _ =>
         (* Order matters less here as H1 and H2 cannot be exchanged *)
-        clean replace R2 with R1 by (symmetry; eauto using per_ctx_env_cross_irrel)
+        clean replace R2 with R1 by first [solve [symmetry; eauto using per_ctx_env_cross_irrel] | tactic_error R2 R1]
     end.
 
 Ltac do_per_ctx_env_irrel_rewrite :=
@@ -428,27 +460,51 @@ Lemma per_ctx_env_trans : forall Γ1 Γ2 R,
     (forall Γ3,
         {{ DF Γ2 ≈ Γ3 ∈ per_ctx_env ↘ R }} ->
         {{ DF Γ1 ≈ Γ3 ∈ per_ctx_env ↘ R }}) /\
-      (forall p1 p2 p3, {{ Dom p1 ≈ p2 ∈ R }} -> {{ Dom p2 ≈ p3 ∈ R }} -> {{ Dom p1 ≈ p3 ∈ R }}).
-Proof with solve [eauto].
+      (forall p1 p2 p3,
+          {{ Dom p1 ≈ p2 ∈ R }} ->
+          {{ Dom p2 ≈ p3 ∈ R }} ->
+          {{ Dom p1 ≈ p3 ∈ R }}).
+Proof with solve [eauto using per_univ_trans].
   simpl.
   induction 1; subst;
-    [> split; [intros * HT2; inversion HT2; subst; eauto; clear HT2 | intros * HRT1 HRT2; eauto] ..];
+    [> split;
+     [ inversion 1; subst; eauto
+     | intros; destruct_conjs; unfold per_total; eauto] ..];
     per_ctx_env_irrel_rewrite.
   - rename tail_rel0 into tail_rel.
     econstructor; eauto.
     + eapply IHper_ctx_env...
-    + unfold rel_typ in *.
+    + simpl in *.
       intros.
-      assert (tail_rel p p) by (etransitivity; [| symmetry]; eassumption).
+      assert (tail_rel p p) by (etransitivity; [| symmetry]; eauto).
       destruct_rel_mod_eval.
       per_univ_elem_irrel_rewrite.
-      econstructor; eauto.
-      eapply per_univ_trans; [| eassumption]...
-  - destruct HRT1, HRT2, IHper_ctx_env.
-    assert (tail_rel d{{{ p1 ↯ }}} d{{{ p3 ↯ }}}) by mauto.
+      econstructor...
+  - assert (tail_rel d{{{ p1 ↯ }}} d{{{ p3 ↯ }}}) by mauto.
     eexists.
-    unfold rel_typ in *.
+    simpl in *.
     destruct_rel_mod_eval.
     per_univ_elem_irrel_rewrite.
     eapply per_elem_trans...
 Qed.
+
+Corollary per_ctx_trans : forall Γ1 Γ2 Γ3 R,
+    {{ DF Γ1 ≈ Γ2 ∈ per_ctx_env ↘ R }} ->
+    {{ DF Γ2 ≈ Γ3 ∈ per_ctx_env ↘ R }} ->
+    {{ DF Γ1 ≈ Γ3 ∈ per_ctx_env ↘ R }}.
+Proof.
+  intros * ?.
+  apply per_ctx_env_trans.
+  assumption.
+Qed.
+
+Corollary per_env_trans : forall Γ1 Γ2 R p1 p2 p3,
+    {{ DF Γ1 ≈ Γ2 ∈ per_ctx_env ↘ R }} ->
+    {{ Dom p1 ≈ p2 ∈ R }} ->
+    {{ Dom p2 ≈ p3 ∈ R }} ->
+    {{ Dom p1 ≈ p3 ∈ R }}.
+Proof.
+  intros * ?.
+  eapply per_ctx_env_trans.
+  eassumption.
+Qed.
diff --git a/theories/Core/Semantic/Readback/Lemmas.v b/theories/Core/Semantic/Readback/Lemmas.v
index 2b303fd4..f4f3f870 100644
--- a/theories/Core/Semantic/Readback/Lemmas.v
+++ b/theories/Core/Semantic/Readback/Lemmas.v
@@ -11,39 +11,36 @@ Section functional_read.
   Ltac unfold_functional_read := unfold functional_read_nf_prop, functional_read_ne_prop, functional_read_typ_prop in *.
 
   Lemma functional_read_nf : forall s m M1 (Hread1: {{ Rnf m in s ↘ M1 }}), functional_read_nf_prop s m M1 Hread1.
-  Proof using Type with mauto .
+  Proof with (functional_eval_rewrite_clear; f_equal; solve [eauto]) using.
     intros *.
     induction Hread1
       using read_nf_mut_ind
       with (P0 := functional_read_ne_prop)
            (P1 := functional_read_typ_prop);
-      unfold_functional_read; mauto;
-      intros; inversion Hread2; clear Hread2; subst;
-      functional_eval_rewrite_clear; f_equal...
+      unfold_functional_read;
+      inversion_clear 1...
   Qed.
 
   Lemma functional_read_ne : forall s m M1 (Hread1 : {{ Rne m in s ↘ M1 }}), functional_read_ne_prop s m M1 Hread1.
-  Proof using Type with mauto.
+  Proof with (functional_eval_rewrite_clear; f_equal; solve [eauto]) using.
     intros *.
     induction Hread1
       using read_ne_mut_ind
       with (P := functional_read_nf_prop)
            (P1 := functional_read_typ_prop);
-      unfold_functional_read; mauto;
-      intros; inversion Hread2; clear Hread2; subst;
-      functional_eval_rewrite_clear; f_equal...
+      unfold_functional_read;
+      inversion_clear 1...
   Qed.
 
   Lemma functional_read_typ : forall s m M1 (Hread1 : {{ Rtyp m in s ↘ M1 }}), functional_read_typ_prop s m M1 Hread1.
-  Proof using Type with mauto.
+  Proof with (functional_eval_rewrite_clear; f_equal; solve [eauto]) using.
     intros *.
     induction Hread1
       using read_typ_mut_ind
       with (P := functional_read_nf_prop)
            (P0 := functional_read_ne_prop);
-      unfold_functional_read; mauto;
-      intros; inversion Hread2; clear Hread2; subst;
-      functional_eval_rewrite_clear; f_equal...
+      unfold_functional_read;
+      inversion_clear 1...
   Qed.
 End functional_read.
 
@@ -51,12 +48,13 @@ End functional_read.
 Hint Resolve functional_read_nf functional_read_ne functional_read_typ : mcltt.
 
 Ltac functional_read_rewrite_clear1 :=
+  let tactic_error o1 o2 := fail 3 "functional_read equality between" o1 "and" o2 "cannot be solved by mauto" in
   match goal with
   | H1 : {{ Rnf ~?m in ?s ↘ ~?M1 }}, H2 : {{ Rnf ~?m in ?s ↘ ~?M2 }} |- _ =>
-      clean replace M2 with M1 by mauto; clear H2
+      clean replace M2 with M1 by first [solve [mauto] | tactic_error M2 M1]; clear H2
   | H1 : {{ Rne ~?m in ?s ↘ ~?M1 }}, H2 : {{ Rne ~?m in ?s ↘ ~?M2 }} |- _ =>
-      clean replace M2 with M1 by mauto; clear H2
+      clean replace M2 with M1 by first [solve [mauto] | tactic_error M2 M1]; clear H2
   | H1 : {{ Rtyp ~?m in ?s ↘ ~?M1 }}, H2 : {{ Rtyp ~?m in ?s ↘ ~?M2 }} |- _ =>
-      clean replace M2 with M1 by mauto; clear H2
+      clean replace M2 with M1 by first [solve [mauto] | tactic_error M2 M1]; clear H2
   end.
 Ltac functional_read_rewrite_clear := repeat functional_read_rewrite_clear1.
diff --git a/theories/Core/Semantic/Realizability.v b/theories/Core/Semantic/Realizability.v
index 528907f1..ba2ff1cd 100644
--- a/theories/Core/Semantic/Realizability.v
+++ b/theories/Core/Semantic/Realizability.v
@@ -7,13 +7,11 @@ Import Domain_Notations.
 Lemma per_nat_then_per_top : forall {n m},
     {{ Dom n ≈ m ∈ per_nat }} ->
     {{ Dom ⇓ ℕ n ≈ ⇓ ℕ m ∈ per_top }}.
-Proof.
-  induction 1; simpl in *; intros.
-  - eexists; firstorder econstructor.
-  - specialize (IHper_nat s) as [? []].
-    eexists; firstorder (econstructor; eauto).
-  - specialize (H s) as [? []].
-    eexists; firstorder (econstructor; eauto).
+Proof with solve [eexists; firstorder (econstructor; eauto)].
+  induction 1; simpl in *; intros s.
+  - idtac...
+  - specialize (IHper_nat s) as [? []]...
+  - specialize (H s) as [? []]...
 Qed.
 
 #[export]
@@ -27,15 +25,14 @@ Lemma realize_per_univ_elem_gen : forall {i a a' R},
 Proof with (solve [try (try (eexists; split); econstructor); mauto]).
   intros * H; simpl in H.
   induction H using per_univ_elem_ind; repeat split; intros.
-  - subst; intro s...
+  - subst...
   - eexists.
-    per_univ_elem_econstructor.
-    eauto.
+    per_univ_elem_econstructor...
   - destruct H2.
-    specialize (H1 _ _ _ H2) as [? [? ?]].
+    specialize (H1 _ _ _ H2) as [? []].
     intro s.
-    specialize (H1 s) as [? [? ?]]...
-  - intro s...
+    specialize (H1 s) as [? []]...
+  - idtac...
   - idtac...
   - eauto using per_nat_then_per_top.
   - destruct IHper_univ_elem as [? []].
@@ -46,60 +43,60 @@ Proof with (solve [try (try (eexists; split); econstructor); mauto]).
     specialize (H3 s) as [? []]...
   - rewrite H2; clear H2.
     intros c0 c0' equiv_c0_c0'.
-    destruct IHper_univ_elem as [? []].
+    destruct_all.
     destruct_rel_mod_eval.
     econstructor; try solve [econstructor; eauto].
-    enough ({{ Dom c ⇓ A c0 ≈ c' ⇓ A' c0' ∈ per_bot }}) by mauto.
+    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 [? [? ?]]...
+    specialize (H3 s) as [? []].
+    specialize (H5 _ _ equiv_c0_c0' s) as [? []]...
   - rewrite H2 in *; clear H2.
-    destruct IHper_univ_elem as [? []].
+    destruct_all.
     intro s.
     assert {{ Dom ⇑! A s ≈ ⇑! A' s ∈ in_rel }} by eauto using var_per_bot.
     destruct_rel_mod_eval.
     destruct_rel_mod_app.
-    assert {{ Dom ⇓ a fa ≈ ⇓ a' f'a' ∈ per_top }} by mauto.
+    assert {{ Dom ⇓ a fa ≈ ⇓ a' f'a' ∈ per_top }} by eauto.
     specialize (H2 s) as [? []].
     specialize (H16 (S s)) as [? []]...
   - intro s.
-    specialize (H s) as [? []]...
+    (on_all_hyp: fun H => destruct (H s) as [? []])...
   - idtac...
   - intro s.
-    specialize (H s) as [? []].
-    inversion_clear H0.
-    specialize (H2 s) as [? []]...
+    (on_all_hyp: fun H => specialize (H s) as [? []]).
+    (on_all_hyp: fun H => inversion_clear H; let n := numgoals in guard n <= 1).
+    (on_all_hyp: fun H => specialize (H s) as [? []])...
 Qed.
 
-Lemma per_univ_then_per_top_typ : forall {i a a' R},
+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; mauto.
+  eapply realize_per_univ_elem_gen; eauto.
 Qed.
 
 #[export]
 Hint Resolve per_univ_then_per_top_typ : mcltt.
 
-Lemma per_bot_then_per_elem : forall {i a a' R c c'},
+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; mauto.
+  eapply realize_per_univ_elem_gen; eauto.
 Qed.
 
 (** We cannot add [per_bot_then_per_elem] as a hint
     because we don't know what "R" is (i.e. the pattern becomes higher-order.)
     In fact, Coq complains it cannot add one if we try. *)
 
-Lemma per_elem_then_per_top : forall {i a a' R b b'},
+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; mauto.
+  eapply realize_per_univ_elem_gen; eauto.
 Qed.
 
 #[export]
diff --git a/theories/Core/Syntactic/CtxEq.v b/theories/Core/Syntactic/CtxEq.v
index 34517e9a..88d2bd4a 100644
--- a/theories/Core/Syntactic/CtxEq.v
+++ b/theories/Core/Syntactic/CtxEq.v
@@ -26,7 +26,6 @@ Module ctxeq_judg.
   | {{ ~?Γ ⊢ ~?M ≈ ~?N : ~?A }} => pose proof ctxeq_exp_eq_helper _ _ _ _ H
   | {{ ~?Γ ⊢s ~?σ : ~?Δ }} => pose proof ctxeq_sub_helper _ _ _ H
   | {{ ~?Γ ⊢s ~?σ ≈ ~?τ : ~?Δ }} => pose proof ctxeq_sub_eq_helper _ _ _ _ H
-  | _ => idtac
   end.
 
   #[local]
@@ -43,10 +42,9 @@ Module ctxeq_judg.
       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; destruct (presup_ctx_eq HΓΔ); mauto.
+        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.
-      2-4: assert {{ ⊢ Γ, B ≈ Δ, B }} by mauto; clear HB.
+      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).
@@ -55,7 +53,7 @@ Module ctxeq_judg.
 
       + econstructor...
 
-      + assert (exists B i, {{ #x : B ∈ Δ }} /\ {{ Γ ⊢ A ≈ B : Type@i }} /\ {{ Δ ⊢ A ≈ B : Type@i }}) as [? [? [? [? ?]]]]...
+      + assert (exists B i, {{ #x : B ∈ Δ }} /\ {{ Γ ⊢ A ≈ B : Type@i }} /\ {{ Δ ⊢ A ≈ B : Type@i }}); destruct_conjs...
 
     (* ctxeq_exp_eq_helper *)
     - intros * HMM' * HΓΔ. gen Δ.
@@ -64,16 +62,14 @@ Module ctxeq_judg.
         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).
-      1-3: assert {{ Δ, ℕ ⊢ B : Type@i }} by eauto.
-      1-3: econstructor...
-      1-5: assert {{ Δ ⊢ B : Type@i }} by eauto.
-      1-5: assert {{ ⊢ Γ, B ≈ Δ, 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 }}) as [? [? [? [? ?]]]]...
+      + 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.
+        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 *)
diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index 94b86e53..614afe36 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -13,7 +13,6 @@ Ltac gen_presup_ctx H :=
       let HΓ := fresh "HΓ" in
       let HΔ := fresh "HΔ" in
       pose proof presup_sub_ctx H as [HΓ HΔ]
-  | _ => idtac
   end.
 
 #[local]
@@ -46,17 +45,26 @@ with presup_sub_eq : forall {Γ Δ σ σ'}, {{ Γ ⊢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); clear presup_exp presup_exp_eq presup_sub_eq; repeat split; mauto.
+    inversion_clear HM; (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.
+    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').
+      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.
@@ -186,7 +194,10 @@ Proof with solve [mauto].
     + 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.
+    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.
diff --git a/theories/Core/Syntactic/System/Lemmas.v b/theories/Core/Syntactic/System/Lemmas.v
index e16fa52b..b57cddc7 100644
--- a/theories/Core/Syntactic/System/Lemmas.v
+++ b/theories/Core/Syntactic/System/Lemmas.v
@@ -2,7 +2,7 @@ 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 [mauto].
+Proof with solve [eauto].
   inversion 1; subst...
 Qed.
 
@@ -12,13 +12,13 @@ Hint Resolve ctx_decomp : mcltt.
 Lemma ctx_decomp_left : forall {Γ A}, {{ ⊢ Γ , A }} -> {{ ⊢ Γ }}.
 Proof with solve [eauto].
   intros.
-  eapply proj1, ctx_decomp...
+  eapply ctx_decomp...
 Qed.
 
 Lemma ctx_decomp_right : forall {Γ A}, {{ ⊢ Γ , A }} -> exists i, {{ Γ ⊢ A : Type@i }}.
 Proof with solve [eauto].
   intros.
-  eapply proj2, ctx_decomp...
+  eapply ctx_decomp...
 Qed.
 
 #[export]
@@ -78,7 +78,7 @@ Qed.
 Lemma presup_ctx_eq_right : forall {Γ Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ ⊢ Δ }}.
 Proof with solve [eauto].
   intros.
-  eapply proj2, presup_ctx_eq...
+  eapply presup_ctx_eq...
 Qed.
 
 #[export]
@@ -86,7 +86,7 @@ Hint Resolve presup_ctx_eq presup_ctx_eq_left presup_ctx_eq_right : mcltt.
 
 Lemma presup_sub_ctx : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ ⊢ Γ }} /\ {{ ⊢ Δ }}.
 Proof with solve [mauto].
-  induction 1; repeat destruct_one_pair...
+  induction 1; destruct_pairs...
 Qed.
 
 Lemma presup_sub_ctx_left : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ ⊢ Γ }}.
@@ -98,7 +98,7 @@ Qed.
 Lemma presup_sub_ctx_right : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ ⊢ Δ }}.
 Proof with solve [eauto].
   intros.
-  eapply proj2, presup_sub_ctx...
+  eapply presup_sub_ctx...
 Qed.
 
 #[export]
@@ -114,7 +114,7 @@ Hint Resolve presup_exp_ctx : mcltt.
 
 Lemma presup_sub_eq_ctx : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Γ }} /\ {{ ⊢ Δ }}.
 Proof with solve [mauto].
-  induction 1; repeat destruct_one_pair...
+  induction 1; destruct_pairs...
 Qed.
 
 Lemma presup_sub_eq_ctx_left : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Γ }}.
@@ -126,7 +126,7 @@ Qed.
 Lemma presup_sub_eq_ctx_right : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Δ }}.
 Proof with solve [eauto].
   intros.
-  eapply proj2, presup_sub_eq_ctx...
+  eapply presup_sub_eq_ctx...
 Qed.
 
 #[export]
@@ -234,8 +234,7 @@ 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].
-  intros * ?.
-  assert {{ ⊢ Γ }} by mauto.
+  inversion_clear 1.
   inversion 1 as [? Γ'|]; subst.
   assert {{ ⊢ Γ' }} by mauto.
   eapply wf_exp_eq_conv; only 1: solve [mauto].
@@ -276,7 +275,7 @@ Lemma sub_eq_p_extend_typ : forall {Γ σ Γ' M i}, {{ Γ' ⊢s σ : Γ }} -> {{
 Proof with solve [mauto].
   intros.
   assert {{ ⊢ Γ }} by mauto.
-  econstructor; only 1,3: solve [mauto]...
+  econstructor; only 3: solve [mauto]...
   Unshelve.
   constructor.
 Qed.
@@ -389,8 +388,7 @@ 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].
-  intros * ?.
-  assert {{ ⊢ Γ }} by mauto.
+  inversion 1; subst.
   inversion 1 as [? Γ'|]; subst.
   assert {{ ⊢ Γ' }} by mauto.
   assert {{ Γ', ℕ, A ⊢ #0[Wk] ≈ # 1 : ℕ[Wk][Wk] }}...
@@ -434,7 +432,7 @@ Lemma sub_eq_p_extend_nat : forall {Γ σ Γ' M}, {{ Γ' ⊢s σ : Γ }} -> {{ 
 Proof with solve [mauto].
   intros.
   assert {{ ⊢ Γ }} by mauto.
-  econstructor; only 1,3: solve [mauto]...
+  econstructor; only 3: solve [mauto]...
   Unshelve.
   all: constructor.
 Qed.
@@ -477,8 +475,8 @@ 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].
   intros * HΓΔ Hx; gen Δ.
-  induction Hx as [|* ? IHHx]; intros; inversion_clear HΓΔ as [|? ? ? ? ? HΓΔ'];
-    [|destruct (IHHx _ HΓΔ') as [? [? [? [? ?]]]]]; repeat eexists; repeat split...
+  induction Hx as [|* ? IHHx]; inversion_clear 1 as [|? ? ? ? ? HΓΔ'];
+    [|specialize (IHHx _ HΓΔ')]; destruct_conjs; repeat eexists...
 Qed.
 
 #[export]
diff --git a/theories/LibTactics.v b/theories/LibTactics.v
index 2a38ce55..5e65860b 100644
--- a/theories/LibTactics.v
+++ b/theories/LibTactics.v
@@ -1,4 +1,4 @@
-From Coq Require Export Program.Tactics Lia.
+From Coq Require Export Program.Equality Program.Tactics Lia.
 
 Create HintDb mcltt discriminated.
 
@@ -27,7 +27,7 @@ Ltac unmark_all := unfold __mark__ in *.
 
 Ltac on_all_marked_hyp tac :=
   match goal with
-  | [ H : __mark__ _ ?A |- _ ] => unmark H; tac H; on_all_marked_hyp tac; mark H
+  | [ H : __mark__ _ ?A |- _ ] => unmark H; tac H; on_all_marked_hyp tac; try mark H
   | _ => idtac
   end.
 Tactic Notation "on_all_marked_hyp:" tactic4(tac) := on_all_marked_hyp tac.