diff --git a/theories/Core/Semantic/PER/Definitions.v b/theories/Core/Semantic/PER/Definitions.v
index 3e38aafa..52b9535b 100644
--- a/theories/Core/Semantic/PER/Definitions.v
+++ b/theories/Core/Semantic/PER/Definitions.v
@@ -209,7 +209,7 @@ Section Per_univ_elem_ind_def.
           motive i elem_rel d{{{ ⇑ a b }}} d{{{ ⇑ a' b' }}}).
 
   #[local]
-  Ltac def_simp := simp per_univ_elem in *.
+  Ltac def_simp := simp per_univ_elem in *; mauto 3.
 
   #[derive(equations=no, eliminator=no), tactic="def_simp"]
   Equations per_univ_elem_ind' (i : nat) (R : relation domain) (a b : domain)
diff --git a/theories/Core/Semantic/PER/Lemmas.v b/theories/Core/Semantic/PER/Lemmas.v
index 01ec4fed..826c36ea 100644
--- a/theories/Core/Semantic/PER/Lemmas.v
+++ b/theories/Core/Semantic/PER/Lemmas.v
@@ -535,8 +535,8 @@ Qed.
 Instance per_elem_PER {i R a b} `(H : per_univ_elem i R a b) : PER R.
 Proof.
   split.
-  - eauto using (per_elem_sym _ _ _ _ _ _ H).
-  - eauto using (per_elem_trans _ _ _ _ _ _ _ H).
+  - pose proof (fun m m' => per_elem_sym _ _ _ _ m m' H). eauto.
+  - pose proof (fun m0 m1 m2 => per_elem_trans _ _ _ _ m0 m1 m2 H); eauto.
 Qed.
 
 (* This lemma gets rid of the unnecessary PER premise. *)
@@ -995,8 +995,8 @@ Qed.
 Instance per_env_PER {R Γ Δ} (H : per_ctx_env R Γ Δ) : PER R.
 Proof.
   split.
-  - auto using (per_env_sym _ _ _ _ _ H).
-  - eauto using (per_env_trans _ _ _ _ _ _ H).
+  - pose proof (fun ρ ρ' => per_env_sym _ _ _ ρ ρ' H); auto.
+  - pose proof (fun ρ0 ρ1 ρ2 => per_env_trans _ _ _ ρ0 ρ1 ρ2 H); eauto.
 Qed.
 
 (* This lemma removes the PER argument *)
diff --git a/theories/Core/Soundness/LogicalRelation/Definitions.v b/theories/Core/Soundness/LogicalRelation/Definitions.v
index 9802d177..9c512399 100644
--- a/theories/Core/Soundness/LogicalRelation/Definitions.v
+++ b/theories/Core/Soundness/LogicalRelation/Definitions.v
@@ -229,7 +229,7 @@ Section GluingInduction.
   .
 
   #[local]
-  Ltac def_simp := simp glu_univ_elem in *.
+  Ltac def_simp := simp glu_univ_elem in *; mauto 3.
 
   #[derive(equations=no, eliminator=no), tactic="def_simp"]
   Equations glu_univ_elem_ind i P El a
diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
index 49f2ba8a..df1780b4 100644
--- a/theories/Core/Soundness/LogicalRelation/Lemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -823,7 +823,7 @@ Proof.
     apply_predicate_equivalence;
     invert_per_ctx_env Hper;
     handle_per_ctx_env_irrel;
-    gintuition.
+    try firstorder.
 
   rename i0 into j.
   rename Γ0 into Γ'.
diff --git a/theories/Core/Soundness/Realizability.v b/theories/Core/Soundness/Realizability.v
index 764fa7c6..e5d45e6c 100644
--- a/theories/Core/Soundness/Realizability.v
+++ b/theories/Core/Soundness/Realizability.v
@@ -31,7 +31,7 @@ Lemma var_arith : forall Γ1 Γ2 (A : typ),
     length (Γ1 ++ A :: Γ2) - length Γ2 - 1 = length Γ1.
 Proof.
   intros.
-  rewrite List.app_length. simpl.
+  rewrite List.length_app. simpl.
   lia.
 Qed.
 
@@ -64,7 +64,7 @@ Proof.
 
     rewrite <- @exp_eq_sub_compose_typ; mauto 2.
     deepexec wf_ctx_sub_ctx_lookup ltac:(fun H => destruct H as [Γ1' [? [Γ2' [? [-> [? [-> []]]]]]]]).
-    repeat rewrite List.app_length in *.
+    repeat rewrite List.length_app in *.
     replace (length Γ1) with (length Γ1') in * by lia.
     clear_refl_eqs.
     replace (length Γ2) with (length Γ2') by (simpl in *; lia).
diff --git a/theories/Core/Soundness/SubtypingCases.v b/theories/Core/Soundness/SubtypingCases.v
index b799fbc6..b587db7c 100644
--- a/theories/Core/Soundness/SubtypingCases.v
+++ b/theories/Core/Soundness/SubtypingCases.v
@@ -29,7 +29,7 @@ Proof.
   handle_per_univ_elem_irrel.
   unfold univ_glu_exp_pred' in *.
   destruct_conjs.
-  eapply mk_glu_rel_exp_with_sub''; gintuition mauto using per_univ_elem_cumu_max_left, per_univ_elem_cumu_max_right.
+  eapply mk_glu_rel_exp_with_sub''; intuition mauto using per_univ_elem_cumu_max_left, per_univ_elem_cumu_max_right.
   eapply glu_univ_elem_per_subtyp_trm_conv; mauto.
   assert (i <= max i k) by lia.
   eapply glu_univ_elem_typ_cumu_ge; revgoals; mauto.
diff --git a/theories/Core/Soundness/TermStructureCases.v b/theories/Core/Soundness/TermStructureCases.v
index b0467bb1..883a3854 100644
--- a/theories/Core/Soundness/TermStructureCases.v
+++ b/theories/Core/Soundness/TermStructureCases.v
@@ -67,7 +67,7 @@ Proof.
     rename a into b.
     rename a0 into a.
     assert {{ Dom a ≈ a ∈ per_univ k }} as [] by mauto.
-    eapply mk_glu_rel_exp_with_sub''; gintuition mauto using per_univ_elem_cumu_max_right.
+    eapply mk_glu_rel_exp_with_sub''; intuition mauto using per_univ_elem_cumu_max_right.
     assert {{ ⊢ Γ, B }} by mauto 3.
     assert {{ Δ ⊢ A[Wk][σ] ≈ A[Wk∘σ] : Type@j }} by mauto 3.
     assert {{ Δ ⊢ A[Wk][σ] ≈ A[Wk∘σ] : Type@(max j k) }} as -> by mauto 3 using lift_exp_eq_max_left.
diff --git a/theories/LibTactics.v b/theories/LibTactics.v
index 61e23ad5..af0b538d 100644
--- a/theories/LibTactics.v
+++ b/theories/LibTactics.v
@@ -432,17 +432,13 @@ Hint Extern 1 (subrelation (@subrelation ?A) _) => (let H := fresh "H" in intros
 #[export]
 Instance predicate_implication_equivalence Ts : subrelation (@predicate_equivalence Ts) (@predicate_implication Ts).
 Proof.
-  induction Ts; gintuition.
-
-  intros ? ? H v.
-  apply IHTs.
-  exact (H v).
+  induction Ts; firstorder eauto 2.
 Qed.
 
 Add Parametric Morphism Ts : (@predicate_implication Ts)
     with signature (@predicate_equivalence Ts) ==> (@predicate_equivalence Ts) ==> iff as predicate_implication_morphism.
 Proof.
-  induction Ts; split; intros; gintuition.
+  induction Ts; split; intros; try firstorder.
   - rewrite <- H.
     transitivity x0; try eassumption.
     rewrite H0; reflexivity.
@@ -466,7 +462,7 @@ Class PERElem (A : Type) (P : A -> Prop) (R : A -> A -> Prop) :=
   Instance PERProper (A : Type) (P : A -> Prop) (R : A -> A -> Prop) `(Ins : PERElem A P R) a (H : P a) :
   Proper R a.
 Proof.
-  cbv. auto using per_elem.
+  cbv. pose proof per_elem; auto.
 Qed.