diff --git a/erasure/theories/EEtaExpanded.v b/erasure/theories/EEtaExpanded.v
index 6599720d2..870ab6e9c 100644
--- a/erasure/theories/EEtaExpanded.v
+++ b/erasure/theories/EEtaExpanded.v
@@ -719,7 +719,7 @@ Proof.
     solve_all.
   - eapply In_All in H. simp_eta.
     move=> /andP[] etarel etav.
-    eapply EEtaExpanded.isEtaExp_mkApps_intro. simp_eta. solve_all.
+    eapply EEtaExpanded.isEtaExp_mkApps_intro. now simp_eta. solve_all.
   - eapply In_All in H0. simp_eta.
     move=> /andP[] etau etav.
     eapply EEtaExpanded.isEtaExp_mkApps_intro; auto. solve_all.
diff --git a/erasure/theories/Typed/OptimizeCorrectness.v b/erasure/theories/Typed/OptimizeCorrectness.v
index b7b406d9c..257621f50 100644
--- a/erasure/theories/Typed/OptimizeCorrectness.v
+++ b/erasure/theories/Typed/OptimizeCorrectness.v
@@ -3191,7 +3191,7 @@ Proof.
     now eapply (isEtaExp_lift _ _ [_] []).
     eapply IHm; eauto. now move/andP: etal.
     eapply IHm. eapply (isEtaExp_mkApps_intro _ _ _ [_]).
-    now eapply (isEtaExp_lift _ _ [_] []). constructor; eauto. simp_eta.
+    now eapply (isEtaExp_lift _ _ [_] []). constructor; eauto. now simp_eta.
     eapply IHm. eapply (isEtaExp_mkApps_intro _ _ _ [_]); eauto. constructor; eauto.
     all:now move/andP: etal.
 Qed.
diff --git a/pcuic/theories/PCUICParallelReductionConfluence.v b/pcuic/theories/PCUICParallelReductionConfluence.v
index f40a9060c..886f13f3c 100644
--- a/pcuic/theories/PCUICParallelReductionConfluence.v
+++ b/pcuic/theories/PCUICParallelReductionConfluence.v
@@ -1785,7 +1785,7 @@ Section Rho.
           erewrite H; trea.
         + simp rho. simpl. f_equal; eauto.
           erewrite -> rho_rename_pred; tea => //.
-          simp rho.
+          now simp rho.
         + simp rho. simpl. simp rho. f_equal; eauto.
           erewrite -> rho_rename_pred; tea => //.
 
@@ -1850,7 +1850,8 @@ Section Rho.
         simp rho. simpl.
         f_equal; auto.
         erewrite rho_rename_pred; tea=> //.
-        now rewrite !map_map_compose in H0. simp rho.
+        now rewrite !map_map_compose in H0.
+        now simp rho.
 
     - (* Proj construct/cofix reduction *)
       simpl.