From 4676c4736864e1ca7ccd1da9766473a72518443a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Fri, 23 Aug 2024 17:14:38 +0200
Subject: [PATCH] Fixes after merge

---
 erasure-plugin/theories/Erasure.v            |  2 +-
 erasure-plugin/theories/ErasureCorrectness.v |  4 +-
 erasure/theories/ECoInductiveToInductive.v   | 14 +++---
 erasure/theories/EOptimizePropDiscr.v        |  2 +-
 erasure/theories/ERemoveParams.v             |  1 -
 erasure/theories/EReorderCstrs.v             | 25 +++++-----
 erasure/theories/EUnboxing.v                 | 48 ++++++++++----------
 erasure/theories/EWcbvEvalNamed.v            | 12 ++---
 erasure/theories/Typed/OptimizeCorrectness.v |  4 +-
 9 files changed, 56 insertions(+), 56 deletions(-)

diff --git a/erasure-plugin/theories/Erasure.v b/erasure-plugin/theories/Erasure.v
index 83d2ed7d6..e18bfe218 100644
--- a/erasure-plugin/theories/Erasure.v
+++ b/erasure-plugin/theories/Erasure.v
@@ -796,7 +796,7 @@ Proof.
   eapply hkn in hl' as [decl' [hl''hct]].
   rewrite hl''hct. destruct decl'; cbn in *. destruct decl. cbn in *. subst o0.
   rewrite H. rewrite /ExAst.trans_oib /=.
-  rewrite /ExAst.trans_ctors. now rewrite map_length.
+  rewrite /ExAst.trans_ctors. now rewrite length_map.
 Qed.
 
 From Equations Require Import Equations.
diff --git a/erasure-plugin/theories/ErasureCorrectness.v b/erasure-plugin/theories/ErasureCorrectness.v
index 77fb2d0e8..d5a51f67b 100644
--- a/erasure-plugin/theories/ErasureCorrectness.v
+++ b/erasure-plugin/theories/ErasureCorrectness.v
@@ -1878,7 +1878,7 @@ Section PCUICErase.
       now eapply EEtaExpandedFix.expanded_isEtaExp. }
     specialize (H0 H1).
     eapply (obseq_lambdabox (Σ', f') (Σ', v'')) in obseq.
-    epose proof (ETransformPresAppLam.transform_lam _ _ _ (t := lambdabox_pres_app) (Σ', v'') prev H0).
+    epose proof (ETransformPresAppLam.transform_lam _ _ _ (t0 := lambdabox_pres_app) (Σ', v'') prev H0).
     rewrite -obseq. exact H2. cbn. red; tauto.
   Qed.
 
@@ -1933,7 +1933,7 @@ Section PCUICErase.
       now eapply EEtaExpandedFix.expanded_isEtaExp. }
     specialize (H0 H1).
     eapply (obseq_lambdabox (Σ', f') (Σ', v'')) in obseq.
-    epose proof (ETransformPresAppLam.transform_lam _ _ _ (t := lambdabox_pres_app) (Σ', v'') prev H0).
+    epose proof (ETransformPresAppLam.transform_lam _ _ _ (t0 := lambdabox_pres_app) (Σ', v'') prev H0).
     rewrite -obseq. exact H2. cbn. red; tauto.
   Qed.
 
diff --git a/erasure/theories/ECoInductiveToInductive.v b/erasure/theories/ECoInductiveToInductive.v
index 602321dcb..681b70597 100644
--- a/erasure/theories/ECoInductiveToInductive.v
+++ b/erasure/theories/ECoInductiveToInductive.v
@@ -120,7 +120,7 @@ Section trans.
   Proof using Type.
     induction t in k |- * using EInduction.term_forall_list_ind; simpl; auto;
     intros; try easy;
-    rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?map_length;
+    rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?length_map;
     unfold test_def in *;
     simpl closed in *; try solve [simpl subst; simpl closed; f_equal; auto; rtoProp; solve_all]; try easy.
     - destruct GlobalContextMap.lookup_inductive_kind as [[]|] => /= //; solve_all.
@@ -172,7 +172,7 @@ Section trans.
   Proof using Type.
     induction b in k |- * using EInduction.term_forall_list_ind; simpl; auto;
     intros cl; try easy;
-    rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?map_length;
+    rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?length_map;
     unfold test_def in *;
     simpl closed in *; try solve [simpl subst; simpl closed; f_equal; auto; rtoProp; solve_all]; try easy.
     - destruct (k ?= n)%nat; auto.
@@ -211,7 +211,7 @@ Section trans.
   Lemma trans_fix_subst mfix : EGlobalEnv.fix_subst (map (map_def trans) mfix) = map trans (EGlobalEnv.fix_subst mfix).
   Proof using Type.
     unfold EGlobalEnv.fix_subst.
-    rewrite map_length.
+    rewrite length_map.
     generalize #|mfix|.
     induction n; simpl; auto.
     f_equal; auto.
@@ -511,7 +511,7 @@ Proof.
   rewrite /iota_red.
   eapply ECSubst.closed_substl => //.
   now rewrite forallb_rev forallb_skipn.
-  now rewrite List.rev_length hskip Nat.add_0_r.
+  now rewrite List.length_rev hskip Nat.add_0_r.
 Qed.
 
 Lemma isFix_mkApps t l : isFix (mkApps t l) = isFix t && match l with [] => true | _ => false end.
@@ -646,7 +646,7 @@ Proof.
     1,3,4:eapply eval_iota_block; eauto;
       [now rewrite -is_propositional_cstr_trans|
         rewrite nth_error_map H2 //|now len|
-        try (cbn; rewrite -H4 !skipn_length map_length //)].
+        try (cbn; rewrite -H4 !length_skipn length_map //)].
     eapply eval_iota_block.
     1,3,4: eauto.
     + now rewrite -is_propositional_cstr_trans.
@@ -696,7 +696,7 @@ Qed.
     rewrite closedn_mkApps in ev1.
     move: ev1 => /andP [] clfix clargs.
     eapply EWcbvEval.eval_fix; eauto.
-    rewrite map_length.
+    rewrite length_map.
     eapply trans_cunfold_fix; tea.
     eapply closed_fix_subst. tea.
     rewrite trans_mkApps in IHev3. apply IHev3.
@@ -713,7 +713,7 @@ Qed.
     simpl in *. eapply EWcbvEval.eval_fix_value. auto. auto. auto.
     eapply trans_cunfold_fix; eauto.
     eapply closed_fix_subst => //.
-    now rewrite map_length.
+    now rewrite length_map.
 
   - move/andP => [] clf cla.
     eapply eval_closed in ev1 => //.
diff --git a/erasure/theories/EOptimizePropDiscr.v b/erasure/theories/EOptimizePropDiscr.v
index 96758cceb..c84417735 100644
--- a/erasure/theories/EOptimizePropDiscr.v
+++ b/erasure/theories/EOptimizePropDiscr.v
@@ -604,7 +604,7 @@ Proof.
     rewrite closedn_mkApps in ev1.
     move: ev1 => /andP [] clfix clargs.
     eapply EWcbvEval.eval_fix; eauto.
-    rewrite map_length.
+    rewrite length_map.
     eapply remove_match_on_box_cunfold_fix; tea.
     eapply closed_fix_subst. tea.
     rewrite remove_match_on_box_mkApps in IHev3. apply IHev3.
diff --git a/erasure/theories/ERemoveParams.v b/erasure/theories/ERemoveParams.v
index bce58d14f..a01e774f9 100644
--- a/erasure/theories/ERemoveParams.v
+++ b/erasure/theories/ERemoveParams.v
@@ -1100,7 +1100,6 @@ Proof.
     destruct g eqn:hg => /= //. subst g.
     destruct nth_error => //. rtoProp; intuition auto. len.
     simp_strip. toAll; solve_all.
-    toAll. solve_all.
   - cbn -[strip] in H0 |- *.
     rewrite lookup_env_strip. destruct lookup_env eqn:hl => // /=.
     destruct g eqn:hg => /= //. subst g. cbn in H0. now rtoProp.
diff --git a/erasure/theories/EReorderCstrs.v b/erasure/theories/EReorderCstrs.v
index 71f288ea0..3e3e92bef 100644
--- a/erasure/theories/EReorderCstrs.v
+++ b/erasure/theories/EReorderCstrs.v
@@ -438,8 +438,6 @@ Definition wf_inductives_mapping Σ (m : inductives_mapping) : bool :=
   forallb (wf_inductive_mapping Σ) m.
 
 Section reorder_proofs.
-  Context {efl : EEnvFlags}.
-  Context {wca : cstr_as_blocks = false}.
   Context (Σ : global_declarations) (m : inductives_mapping).
   Context (wfm : wf_inductives_mapping Σ m).
 
@@ -585,7 +583,7 @@ Section reorder_proofs.
   Lemma lookup_constructor_reorder i n :
     option_map (fun '(mib, oib, c) => (reorder_inductive_decl m (inductive_mind i) mib, reorder_one_ind m (inductive_mind i) (inductive_ind i) oib, c)) (lookup_constructor Σ i n) =
     lookup_constructor (reorder_env m Σ) i (lookup_constructor_ordinal m i n).
-  Proof.
+  Proof using Type wfm.
     rewrite /lookup_constructor lookup_inductive_reorder.
     destruct lookup_inductive as [[mib oib]|] eqn:hind => //=.
     destruct nth_error eqn:hnth => //=.
@@ -637,6 +635,9 @@ Section reorder_proofs.
     rewrite /reorder_one_ind. destruct lookup_inductive_assoc as [[na tags]|]=> //.
   Qed.
 
+  Context {efl : EEnvFlags}.
+  Context {wca : cstr_as_blocks = false}.
+
   Lemma wf_glob_ind_projs {p pinfo} :
     wf_glob Σ ->
     lookup_projection Σ p = Some pinfo ->
@@ -740,7 +741,7 @@ Section reorder_proofs.
     intros wfΣ.
     induction t in k |- * using EInduction.term_forall_list_ind; simpl; auto;
     intros; try easy;
-    rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?map_length;
+    rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?length_map;
     unfold wf_fix_gen, test_def in *;
     simpl closed in *; try solve [simpl subst; simpl closed; f_equal; auto; bool; solve_all]; try easy.
     - bool. rewrite -lookup_constant_reorder. destruct lookup_constant => //=; bool.
@@ -820,7 +821,7 @@ Section reorder_proofs.
     intros wfΣ.
     induction b in k |- * using EInduction.term_forall_list_ind; simpl; auto;
     intros wft; try easy;
-    rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?map_length;
+    rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?length_map;
     unfold wf_fix, test_def in *;
     simpl closed in *; try solve [simpl subst; simpl closed; f_equal; auto; rtoProp; solve_all]; try easy.
     - destruct (k ?= n0)%nat; auto.
@@ -863,14 +864,14 @@ Section reorder_proofs.
     unfold EGlobalEnv.iota_red.
     rewrite optimize_substl //.
     rewrite forallb_rev forallb_skipn //.
-    now rewrite List.rev_length.
+    now rewrite List.length_rev.
     now rewrite map_rev map_skipn.
   Qed.
 
   Lemma optimize_fix_subst mfix : EGlobalEnv.fix_subst (map (map_def optimize) mfix) = map optimize (EGlobalEnv.fix_subst mfix).
   Proof using Type.
     unfold EGlobalEnv.fix_subst.
-    rewrite map_length.
+    rewrite length_map.
     generalize #|mfix|.
     induction n; simpl; auto.
     f_equal; auto.
@@ -879,7 +880,7 @@ Section reorder_proofs.
   Lemma optimize_cofix_subst mfix : EGlobalEnv.cofix_subst (map (map_def optimize) mfix) = map optimize (EGlobalEnv.cofix_subst mfix).
   Proof using Type.
     unfold EGlobalEnv.cofix_subst.
-    rewrite map_length.
+    rewrite length_map.
     generalize #|mfix|.
     induction n; simpl; auto.
     f_equal; auto.
@@ -1073,7 +1074,7 @@ Proof.
   rewrite /iota_red.
   eapply ECSubst.closed_substl => //.
   now rewrite forallb_rev forallb_skipn.
-  now rewrite List.rev_length hskip Nat.add_0_r.
+  now rewrite List.length_rev hskip Nat.add_0_r.
 Qed.
 
 Lemma isFix_mkApps t l : isFix (mkApps t l) = isFix t && match l with [] => true | _ => false end.
@@ -1214,7 +1215,7 @@ Proof.
     eapply eval_wellformed in ev1 => //.
     move/(@wf_mkApps hastapp): ev1 => [] wff wfargs.
     eapply eval_fix; eauto.
-    rewrite map_length.
+    rewrite length_map.
     unshelve (eapply optimize_cunfold_fix; tea); tea.
     rewrite optimize_mkApps in IHev3. apply IHev3.
     rewrite wellformed_mkApps // wfargs.
@@ -1229,7 +1230,7 @@ Proof.
     rewrite optimize_mkApps in IHev1 |- *.
     simpl in *. eapply eval_fix_value. auto. auto. auto.
     unshelve (eapply optimize_cunfold_fix; eauto); tea.
-    now rewrite map_length.
+    now rewrite length_map.
 
   - move/andP => [] /andP[] hasapp clf cla.
     eapply eval_wellformed in ev1 => //.
@@ -1555,7 +1556,7 @@ Definition reorder_program_wf {efl : EEnvFlags} {wca : cstr_as_blocks = false} (
 Proof.
   intros []; split.
   now unshelve eapply reorder_env_wf.
-  cbn. now eapply (@wf_optimize _ wca).
+  cbn. now eapply (@wf_optimize _ _ wfm efl wca).
 Qed.
 
 Definition reorder_program_expanded {efl : EEnvFlags} (p : eprogram) m (wfm : wf_inductives_mapping p.1 m) :
diff --git a/erasure/theories/EUnboxing.v b/erasure/theories/EUnboxing.v
index 5cf20e76c..87f31709f 100644
--- a/erasure/theories/EUnboxing.v
+++ b/erasure/theories/EUnboxing.v
@@ -118,7 +118,7 @@ Section unbox.
   Proof using Type Σ.
     revert k. induction t using EInduction.term_forall_list_ind; simp unbox; rewrite -?unbox_equation_1; toAll; simpl;
     intros; try easy;
-    rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?map_length;
+    rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?length_map;
     unfold test_def in *;
     simpl closed in *;
     try solve [simpl; subst; simpl closed; f_equal; auto; rtoProp; solve_all; solve_all]; try easy.
@@ -198,7 +198,7 @@ Section unbox.
     intros cla etaa; move cla before a. move etaa before a.
     funelim (unbox b); cbn; simp unbox isEtaExp; rewrite -?isEtaExp_equation_1 -?unbox_equation_1; toAll; simpl;
     intros; try easy;
-    rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?map_length;
+    rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?length_map;
     unfold test_def in *;
     simpl closed in *; try solve [simpl subst; simpl closed; f_equal; auto; rtoProp; solve_all]; try easy.
 
@@ -263,7 +263,7 @@ Section unbox.
       { destruct v; cbn; congruence. }
       rewrite unbox_mkApps //.
       rewrite isEtaExp_Constructor // in H1.
-      move/andP: H1. rewrite map_length. move=> [] etaapp etav.
+      move/andP: H1. rewrite length_map. move=> [] etaapp etav.
       cbn -[lookup_inductive_pars].
       unfold isEtaExp_app in etaapp.
       rewrite GlobalContextMap.lookup_inductive_pars_spec in Heq.
@@ -280,7 +280,7 @@ Section unbox.
       rewrite unbox_mkApps //.
       rewrite isEtaExp_Constructor // in H1.
       rewrite GlobalContextMap.lookup_inductive_pars_spec in Heq.
-      move/andP: H1. rewrite map_length. move=> [] etaapp etav.
+      move/andP: H1. rewrite length_map. move=> [] etaapp etav.
       cbn -[lookup_inductive_pars].
       unfold isEtaExp_app in etaapp.
       destruct lookup_constructor_pars_args as [[pars args]|] eqn:eqpars => //.
@@ -316,7 +316,7 @@ Section unbox.
   Lemma unbox_fix_subst mfix : EGlobalEnv.fix_subst (map (map_def unbox) mfix) = map unbox (EGlobalEnv.fix_subst mfix).
   Proof using Type.
     unfold EGlobalEnv.fix_subst.
-    rewrite map_length.
+    rewrite length_map.
     generalize #|mfix|.
     induction n; simpl; auto.
     f_equal; auto. now simp unbox.
@@ -325,7 +325,7 @@ Section unbox.
   Lemma unbox_cofix_subst mfix : EGlobalEnv.cofix_subst (map (map_def unbox) mfix) = map unbox (EGlobalEnv.cofix_subst mfix).
   Proof using Type.
     unfold EGlobalEnv.cofix_subst.
-    rewrite map_length.
+    rewrite length_map.
     generalize #|mfix|.
     induction n; simpl; auto.
     f_equal; auto. now simp unbox.
@@ -926,7 +926,7 @@ Proof.
     rewrite H2 in H1.
     econstructor; eauto.
     * rewrite nth_error_map H3 //.
-    * len. cbn in H4, H5. rewrite skipn_length. lia.
+    * len. cbn in H4, H5. rewrite length_skipn. lia.
     * cbn -[unbox]. rewrite skipn_0. len.
     * cbn -[unbox].
       have etaargs : forallb (isEtaExp Σ) args.
@@ -950,7 +950,7 @@ Proof.
     rewrite unbox_mkApps // /= in e1.
     simp_unbox in e1.
     eapply eval_fix; tea.
-    * rewrite map_length.
+    * rewrite length_map.
       eapply unbox_cunfold_fix; tea.
       eapply closed_fix_subst. tea.
       move: i8; rewrite closedn_mkApps => /andP[] //.
@@ -971,7 +971,7 @@ Proof.
     { move: i4.
       rewrite closedn_mkApps. now move/andP => []. }
     { move: i6. rewrite isEtaExp_mkApps_napp // /= => /andP[] //. now simp isEtaExp. }
-    now rewrite map_length.
+    now rewrite length_map.
 
   - rewrite unbox_tApp //. simp_unbox in e0.
     simp_unbox in e1.
@@ -1016,7 +1016,7 @@ Proof.
     rewrite (constructor_isprop_pars_decl_lookup H2) in e0.
     eapply eval_proj; eauto.
     move: (@is_propositional_cstr_unbox Σ p.(proj_ind) 0). now rewrite H2. simpl.
-    len. rewrite skipn_length. cbn in H3. lia.
+    len. rewrite length_skipn. cbn in H3. lia.
     rewrite nth_error_skipn nth_error_map /= H4 //.
 
   - simp_unbox. eapply eval_proj_prop => //.
@@ -1035,7 +1035,7 @@ Proof.
     + constructor. cbn [atom]. rewrite wcon lookup_constructor_unbox H //.
     + rewrite /cstr_arity /=.
       move: H0; rewrite /cstr_arity /=.
-      rewrite skipn_length map_length => ->. lia.
+      rewrite length_skipn length_map => ->. lia.
     + cbn in H0. eapply All2_skipn, All2_map.
       eapply All2_impl; tea; cbn -[unbox].
       intros x y []; auto.
@@ -1110,7 +1110,7 @@ Proof.
     destruct EAst.ind_ctors => //.
     destruct nth_error => //.
     all: eapply H; auto.
-  - unfold wf_fix_gen in *. rewrite map_length. rtoProp; intuition auto. toAll; solve_all.
+  - unfold wf_fix_gen in *. rewrite length_map. rtoProp; intuition auto. toAll; solve_all.
     now rewrite -unbox_isLambda. toAll; solve_all.
   - primProp. rtoProp; intuition eauto; solve_all_k 6.
   - move:H1; rewrite !wellformed_mkApps //. rtoProp; intuition auto.
@@ -1375,7 +1375,7 @@ Proof.
     rewrite (lookup_inductive_pars_spec (proj1 (proj1 H))).
     eapply expanded_tConstruct_app.
     eapply unbox_declared_constructor; tea.
-    len. rewrite skipn_length /= /EAst.cstr_arity /=.
+    len. rewrite length_skipn /= /EAst.cstr_arity /=.
     rewrite /EAst.cstr_arity in H0. lia.
     solve_all. eapply All_skipn. solve_all.
 Qed.
@@ -1457,7 +1457,7 @@ Qed.
     intros wfΣ.
     induction t in k |- * using EInduction.term_forall_list_ind; simpl; auto;
     intros; try easy;
-    rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?map_length;
+    rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?length_map;
     unfold wf_fix_gen, test_def in *;
     simpl closed in *; try solve [simpl subst; simpl closed; f_equal; auto; rtoProp; solve_all]; try easy.
     - rtoProp. split; eauto. destruct args; eauto.
@@ -1485,7 +1485,7 @@ Qed.
     intros wfΣ.
     induction b in k |- * using EInduction.term_forall_list_ind; simpl; auto;
     intros wft; try easy;
-    rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?map_length;
+    rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?length_map;
     unfold wf_fix, test_def in *;
     simpl closed in *; try solve [simpl subst; simpl closed; f_equal; auto; rtoProp; solve_all]; try easy.
     - destruct (k ?= n0)%nat; auto.
@@ -1530,14 +1530,14 @@ Qed.
     unfold EGlobalEnv.iota_red.
     rewrite unbox_substl //.
     rewrite forallb_rev forallb_skipn //.
-    now rewrite List.rev_length.
+    now rewrite List.length_rev.
     now rewrite map_rev map_skipn.
   Qed.
 
   Lemma unbox_fix_subst mfix : EGlobalEnv.fix_subst (map (map_def unbox) mfix) = map unbox (EGlobalEnv.fix_subst mfix).
   Proof using Type.
     unfold EGlobalEnv.fix_subst.
-    rewrite map_length.
+    rewrite length_map.
     generalize #|mfix|.
     induction n; simpl; auto.
     f_equal; auto.
@@ -1546,7 +1546,7 @@ Qed.
   Lemma unbox_cofix_subst mfix : EGlobalEnv.cofix_subst (map (map_def unbox) mfix) = map unbox (EGlobalEnv.cofix_subst mfix).
   Proof using Type.
     unfold EGlobalEnv.cofix_subst.
-    rewrite map_length.
+    rewrite length_map.
     generalize #|mfix|.
     induction n; simpl; auto.
     f_equal; auto.
@@ -1766,7 +1766,7 @@ Proof.
   rewrite /iota_red.
   eapply ECSubst.closed_substl => //.
   now rewrite forallb_rev forallb_skipn.
-  now rewrite List.rev_length hskip Nat.add_0_r.
+  now rewrite List.length_rev hskip Nat.add_0_r.
 Qed.
 
 Definition disable_prop_cases fl := {| with_prop_case := false; with_guarded_fix := fl.(@with_guarded_fix) ; with_constructor_as_block := false |}.
@@ -1889,7 +1889,7 @@ Proof.
     eapply eval_wellformed in ev1 => //.
     move/wf_mkApps: ev1 => [] wff wfargs.
     eapply eval_fix; eauto.
-    rewrite map_length.
+    rewrite length_map.
     eapply unbox_cunfold_fix; tea.
     rewrite unbox_mkApps in IHev3. apply IHev3.
     rewrite wellformed_mkApps // wfargs.
@@ -1903,7 +1903,7 @@ Proof.
     rewrite unbox_mkApps in IHev1 |- *.
     simpl in *. eapply eval_fix_value. auto. auto. auto.
     eapply unbox_cunfold_fix; eauto.
-    now rewrite map_length.
+    now rewrite length_map.
 
   - move/andP => [] clf cla.
     eapply eval_wellformed in ev1 => //.
@@ -1960,15 +1960,15 @@ Proof.
     eapply eval_iota; tea.
     rewrite /constructor_isprop_pars_decl -lookup_constructor_unbox // H //= //.
     rewrite H0 H1; reflexivity. cbn. reflexivity. len. len.
-    rewrite skipn_length. lia.
+    rewrite length_skipn. lia.
     unfold iota_red. cbn.
     rewrite (substl_rel _ _ (unbox Σ a)) => //.
     { eapply nth_error_forallb in wfargs; tea.
       eapply wf_unbox in wfargs => //.
       now eapply wellformed_closed in wfargs. }
     pose proof (wellformed_projection_args wfΣ hl'). cbn in H1.
-    rewrite nth_error_rev. len. rewrite skipn_length. lia.
-    rewrite List.rev_involutive. len. rewrite skipn_length.
+    rewrite nth_error_rev. len. rewrite length_skipn. lia.
+    rewrite List.rev_involutive. len. rewrite length_skipn.
     rewrite nth_error_skipn nth_error_map.
     rewrite e2 -H1.
     assert((ind_npars mdecl + cstr_nargs cdecl - ind_npars mdecl) = cstr_nargs cdecl) by lia.
diff --git a/erasure/theories/EWcbvEvalNamed.v b/erasure/theories/EWcbvEvalNamed.v
index 0cb96358b..478c313ba 100644
--- a/erasure/theories/EWcbvEvalNamed.v
+++ b/erasure/theories/EWcbvEvalNamed.v
@@ -1123,7 +1123,7 @@ Proof.
     destruct nth_error as [ [] | ]; cbn in *; eauto. len.
   - move: H0; rewrite /wf_brs; cbn; destruct lookup_env as [ [] | ] eqn:E; cbn in *; eauto.
     destruct nth_error as [ [] | ]; cbn in *; eauto. intros eq.
-    solve_all. rewrite map_length. rewrite <- app_length.
+    solve_all. rewrite length_map. rewrite <- length_app.
     eapply a; eauto. len. rewrite gen_many_fresh_length. eauto.
   - destruct lookup_env as [ [] | ] eqn:E; cbn in *; eauto.
     erewrite lookup_annotate_env; eauto. cbn.
@@ -1139,7 +1139,7 @@ Proof.
       destruct dbody; cbn in *; eauto.
       eapply IHAll.
   - solve_all. unfold wf_fix in *. rtoProp. split.
-    rewrite map2_length gen_many_fresh_length map_length.
+    rewrite map2_length gen_many_fresh_length length_map.
     { eapply Nat.ltb_lt in H0. eapply Nat.ltb_lt. lia. }
     solve_all. clear H0. unfold test_def in *. cbn in *.
     eapply All_impl in H2. 2:{ intros ? [[] ].
@@ -1149,25 +1149,25 @@ Proof.
       }
       revert H2.
       generalize ((List.rev (gen_many_fresh Γ (map dname m)) ++ Γ)).
-      intros. rewrite map2_length gen_many_fresh_length map_length Nat.min_id.
+      intros. rewrite map2_length gen_many_fresh_length length_map Nat.min_id.
       revert H2. generalize (#|m| + #|Γ|).
       intros.
       induction m in Γ, n, n0, l, H2 |- *.
       + econstructor.
       + invs H2. cbn. destruct a; cbn. destruct dname; cbn; econstructor; eauto.
   - solve_all. unfold wf_fix in *. rtoProp. split.
-    rewrite map2_length gen_many_fresh_length map_length.
+    rewrite map2_length gen_many_fresh_length length_map.
     { eapply Nat.ltb_lt in H0. eapply Nat.ltb_lt. lia. }
     solve_all. clear H0. unfold test_def in *. cbn in *.
     eapply All_impl in H1. 2:{ intros ? [i].
     specialize (i (List.rev (gen_many_fresh Γ (map dname m)) ++ Γ)).
-      revert i. rewrite ?List.rev_length app_length ?List.rev_length gen_many_fresh_length ?List.rev_length map_length. intros r.
+      revert i. rewrite ?List.length_rev length_app ?List.length_rev gen_many_fresh_length ?List.length_rev length_map. intros r.
       eapply r in i0. exact i0.
       eapply incl_appr. eauto.
       }
     revert H1.
     generalize ((List.rev (gen_many_fresh Γ (map dname m)) ++ Γ)).
-    intros. rewrite map2_length gen_many_fresh_length map_length Nat.min_id.
+    intros. rewrite map2_length gen_many_fresh_length length_map Nat.min_id.
     revert H1. generalize (#|m| + #|Γ|).
     intros.
     induction m in Γ, n, n0, l, H1 |- *.
diff --git a/erasure/theories/Typed/OptimizeCorrectness.v b/erasure/theories/Typed/OptimizeCorrectness.v
index c4a58f8ac..d4f69390b 100644
--- a/erasure/theories/Typed/OptimizeCorrectness.v
+++ b/erasure/theories/Typed/OptimizeCorrectness.v
@@ -3621,7 +3621,7 @@ Section dearg.
       rewrite Hmask.
       rtoProp; intuition eauto; solve_all.
       cbn [wellformed]. rtoProp; intuition eauto. len.
-      rewrite mapi_length map_length. rewrite /wf_brs.
+      rewrite mapi_length length_map. rewrite /wf_brs.
       { unfold EGlobalEnv.lookup_inductive. cbn.
         move: hl. cbn.
         rewrite !lookup_env_trans_env lookup_env_dearg_env.
@@ -3629,7 +3629,7 @@ Section dearg.
         rewrite !nth_error_map. unfold dearg_mib. rewrite Hmask. cbn.
         rewrite nth_error_mapi. destruct nth_error => //=.
         intros [= <- <-].
-        move: H; cbn. now rewrite /trans_ctors !map_length !mapi_length. }
+        move: H; cbn. now rewrite /trans_ctors !length_map !mapi_length. }
       cbn.
       unfold mapi. clear clos_args IHt H.
       unfold valid_case_masks in H3. rewrite Hmask in H3.