diff --git a/.vscode/metacoq.code-workspace b/.vscode/metacoq.code-workspace
index f69bd9643..acfd61685 100644
--- a/.vscode/metacoq.code-workspace
+++ b/.vscode/metacoq.code-workspace
@@ -106,5 +106,6 @@
 		"**/.DS_Store": true,
 		"**/Thumbs.db": true
 	},
+	"coq-lsp.check_only_on_request": true,
   }
 }
diff --git a/erasure-plugin/src/g_metacoq_erasure.mlg b/erasure-plugin/src/g_metacoq_erasure.mlg
index 3efd45e9e..84d490c08 100644
--- a/erasure-plugin/src/g_metacoq_erasure.mlg
+++ b/erasure-plugin/src/g_metacoq_erasure.mlg
@@ -25,7 +25,6 @@ type erasure_command_args =
   | Time
   | Typed
   | BypassQeds
-  | Fast
 
 let pr_char c = str (Char.escaped c)
 
@@ -46,24 +45,19 @@ type erasure_config =
   { unsafe : bool;
     time : bool;
     typed : bool;
-    bypass_qeds : bool;
-    fast : bool;
-    }
+    bypass_qeds : bool }
 
 let default_config =
   { unsafe = false;
     time = false;
     typed = false;
-    bypass_qeds = false;
-    fast = false }
+    bypass_qeds = false }
 
 let make_erasure_config config =
   let open Erasure0 in
   { enable_unsafe = if config.unsafe then all_unsafe_passes else no_unsafe_passes ;
     enable_typed_erasure = config.typed;
-    enable_fast_remove_params = config.fast;
     dearging_config = default_dearging_config;
-    inductives_mapping = [];
     inlined_constants = Kernames.KernameSet.empty }
 
 let time_opt config str fn arg =
@@ -76,8 +70,9 @@ let check config env evm c =
   let time str f arg = time_opt config str f arg in
   let term = time (str"Quoting") (Ast_quoter.quote_term_rec ~bypass:config.bypass_qeds env evm) (EConstr.to_constr evm c) in
   let erasure_config = make_erasure_config config in
+  let mapping = [] in
   let erase =
-    time (str"Erasure") (Erasure0.erase_and_print_template_program erasure_config) term
+    time (str"Erasure") (Erasure0.erase_and_print_template_program erasure_config mapping) term
   in
   Feedback.msg_notice (pr_char_list erase)
 
@@ -92,7 +87,6 @@ let interp_erase args env evm c =
         | Time -> aux {config with time = true} args
         | Typed -> aux {config with typed = true} args
         | BypassQeds -> aux {config with bypass_qeds = true} args
-        | Fast -> aux {config with fast = true} args
     in aux default_config args
   in
   check config env evm c
@@ -123,7 +117,6 @@ ARGUMENT EXTEND erase_args
 | [ "-time" ] -> { Time }
 | [ "-typed" ] -> { Typed }
 | [ "-bypass-qeds" ] -> { BypassQeds }
-| [ "-fast" ] -> { Fast }
 END
 
 VERNAC COMMAND EXTEND MetaCoqErase CLASSIFIED AS QUERY
diff --git a/erasure-plugin/theories/ETransform.v b/erasure-plugin/theories/ETransform.v
index 3af3e47a8..1e58c8f01 100644
--- a/erasure-plugin/theories/ETransform.v
+++ b/erasure-plugin/theories/ETransform.v
@@ -976,7 +976,7 @@ Program Definition coinductive_to_inductive_transformation (efl : EEnvFlags)
   {has_cstrblocks : cstr_as_blocks = true} :
   Transform.t _ _ EAst.term EAst.term _ _
     (eval_eprogram_env block_wcbv_flags) (eval_eprogram block_wcbv_flags) :=
-  {| name := "transforming co-inductive to inductive types";
+  {| name := "transforming co-inductive to lazy inductive types";
     transform p _ := ECoInductiveToInductive.trans_program p ;
     pre p := wf_eprogram_env efl p ;
     post p := wf_eprogram efl p ;
@@ -1020,42 +1020,59 @@ Qed.
 
 From MetaCoq.Erasure Require Import EReorderCstrs.
 
-Axiom trust_reorder_cstrs_wf :
-  forall efl : EEnvFlags,
-  WcbvFlags ->
-  forall (m : inductives_mapping) (input : Transform.program E.global_context term),
-  wf_eprogram efl input -> wf_eprogram efl (reorder_program m input).
-Axiom trust_reorder_cstrs_pres :
-  forall (efl : EEnvFlags) (wfl : WcbvFlags) (m : inductives_mapping) (p : Transform.program E.global_context term)
-  (v : term),
-  wf_eprogram efl p ->
-  eval_eprogram wfl p v -> exists v' : term, eval_eprogram wfl (reorder_program m p) v' /\ v' = reorder m v.
+Definition eval_eprogram_mapping (wfl : WcbvFlags) (p : inductives_mapping * eprogram) t :=
+  eval_eprogram wfl p.2 t.
 
-Program Definition reorder_cstrs_transformation (efl : EEnvFlags) (wfl : WcbvFlags) (m : inductives_mapping) :
-  Transform.t _ _ EAst.term EAst.term _ _
-    (eval_eprogram wfl) (eval_eprogram wfl) :=
-  {| name := "reoder inductive constructors ";
-    transform p _ := EReorderCstrs.reorder_program m p ;
-    pre p := wf_eprogram efl p ;
-    post p := wf_eprogram efl p ;
-    obseq p hp p' v v' := v' = EReorderCstrs.reorder m v |}.
+Definition eval_eprogram_env_mapping (wfl : WcbvFlags) (p : inductives_mapping * eprogram_env) t :=
+  eval_eprogram_env wfl p.2 t.
+
+Definition to_program (e : eprogram_env) : eprogram :=
+  (e.1, e.2).
+
+Program Definition reorder_cstrs_transformation {efl : EEnvFlags} {wca : cstr_as_blocks = false} {has_app : has_tApp}
+  (wfl : WcbvFlags) {wcon : with_constructor_as_block = false} :
+  Transform.t _ _ _ EAst.term _ _
+    (eval_eprogram_env_mapping wfl) (eval_eprogram wfl) :=
+  {| name := "reorder inductive constructors ";
+    transform p _ := EReorderCstrs.reorder_program p.1 (to_program p.2) ;
+    pre p := [/\ wf_eprogram_env efl p.2, EEtaExpandedFix.expanded_eprogram_env p.2 & wf_inductives_mapping p.2.1 p.1] ;
+    post p := wf_eprogram efl p /\ EEtaExpandedFix.expanded_eprogram p;
+    obseq p hp p' v v' := v' = EReorderCstrs.reorder p.1 v |}.
 
 Next Obligation.
-  move=> efl wfl m. cbn. now apply trust_reorder_cstrs_wf.
+  move=> efl wca hasapp wfl wcb [m p] [wfp exp wfm]. split => //.
+  now unshelve eapply reorder_program_wf. cbn.
+  now eapply reorder_program_expanded_fix.
 Qed.
 Next Obligation.
-  red. eapply trust_reorder_cstrs_pres.
+  red. intros efl wca hasapp wfl wcb [m p] v [wfp wfm] evp.
+  destruct evp as [ev].
+  unshelve eapply EReorderCstrs.optimize_correct in ev; trea.
+  2,3:apply wfp.
+  exists (reorder m v). split => //.
 Qed.
 
 #[global]
-Axiom trust_reorder_cstrs_transformation_ext : forall (efl : EEnvFlags) (wfl : WcbvFlags) (m : inductives_mapping),
-  TransformExt.t (reorder_cstrs_transformation efl wfl m)
-    (fun p p' => extends p.1 p'.1) (fun p p' => extends p.1 p'.1).
+Instance reorder_cstrs_transformation_ext {efl : EEnvFlags} (wca : cstr_as_blocks = false) (has_app : has_tApp) (wfl : WcbvFlags)
+  {wcon : with_constructor_as_block = false} :
+  TransformExt.t (reorder_cstrs_transformation (wca := wca) (has_app := has_app) wfl (wcon:=wcon))
+    (fun p p' => p.1 = p'.1 /\ extends p.2.1 p'.2.1) (fun p p' => extends p.1 p'.1).
+Proof.
+  red. intros p p' pr pr' [eq ext].
+  red; cbn. rewrite -eq. eapply EReorderCstrs.optimize_extends_env; eauto.
+  move: pr'; cbn. now intros []. apply pr. apply pr'.
+Qed.
 
 #[global]
-Axiom trust_reorder_cstrs_transformation_ext' : forall (efl : EEnvFlags) (wfl : WcbvFlags) (m : inductives_mapping),
-  TransformExt.t (reorder_cstrs_transformation efl wfl m)
-    extends_eprogram extends_eprogram.
+Instance reorder_cstrs_transformation_ext' {efl : EEnvFlags} (wca : cstr_as_blocks = false) (has_app : has_tApp) (wfl : WcbvFlags)
+  {wcon : with_constructor_as_block = false} :
+  TransformExt.t (reorder_cstrs_transformation (wca := wca) (has_app := has_app) wfl (wcon:=wcon))
+    (fun p p' => p.1 = p'.1 /\ extends_eprogram_env p.2 p'.2) extends_eprogram.
+Proof.
+  red. intros p p' pr pr' [eq [ext eq']]. cbn.
+  red. cbn. rewrite -eq -eq'. split => //. eapply EReorderCstrs.optimize_extends_env; eauto.
+  move: pr'; cbn. now intros []. apply pr. apply pr'.
+Qed.
 
 From MetaCoq.Erasure Require Import EUnboxing.
 
diff --git a/erasure-plugin/theories/Erasure.v b/erasure-plugin/theories/Erasure.v
index a36fbe6da..83d2ed7d6 100644
--- a/erasure-plugin/theories/Erasure.v
+++ b/erasure-plugin/theories/Erasure.v
@@ -34,7 +34,6 @@ Local Obligation Tactic := program_simpl.
 
 Record unsafe_passes :=
   { cofix_to_lazy : bool;
-    reorder_constructors : bool;
     inlining : bool;
     unboxing : bool;
     betared : bool }.
@@ -42,9 +41,7 @@ Record unsafe_passes :=
 Record erasure_configuration := {
   enable_unsafe : unsafe_passes;
   enable_typed_erasure : bool;
-  enable_fast_remove_params : bool;
   dearging_config : dearging_config;
-  inductives_mapping : EReorderCstrs.inductives_mapping;
   inlined_constants : KernameSet.t
   }.
 
@@ -56,7 +53,6 @@ Definition default_dearging_config :=
 
 Definition make_unsafe_passes b :=
   {| cofix_to_lazy := b;
-     reorder_constructors := b;
      inlining := b;
      unboxing := b;
      betared := b |}.
@@ -65,12 +61,10 @@ Definition no_unsafe_passes := make_unsafe_passes false.
 Definition all_unsafe_passes := make_unsafe_passes true.
 
 (* This runs the cofix -> fix/lazy translation as well as inlining and
-  beta-redex simplification,  which are not verified. It does not change
-  representation by reordering constructors or unboxing. *)
+  beta-redex simplification,  which are not verified. It does do unboxing. *)
 
 Definition default_unsafe_passes :=
   {| cofix_to_lazy := true;
-      reorder_constructors := false;
       inlining := true;
       unboxing := false;
       betared := true |}.
@@ -79,17 +73,13 @@ Definition default_erasure_config :=
   {| enable_unsafe := default_unsafe_passes;
      dearging_config := default_dearging_config;
      enable_typed_erasure := true;
-     enable_fast_remove_params := true;
-     inductives_mapping := [];
      inlined_constants := KernameSet.empty |}.
 
 (* This runs only the verified phases without the typed erasure and "fast" remove params *)
 Definition safe_erasure_config :=
   {| enable_unsafe := no_unsafe_passes;
      enable_typed_erasure := false;
-     enable_fast_remove_params := false;
      dearging_config := default_dearging_config;
-     inductives_mapping := [];
      inlined_constants := KernameSet.empty |}.
 
 Axiom assume_welltyped_template_program_expansion :
@@ -135,8 +125,6 @@ Program Definition optional_unsafe_transforms econf :=
     (* Coinductives & cofixpoints are translated to inductive types and thunked fixpoints *)
     coinductive_to_inductive_transformation efl
       (has_app := eq_refl) (has_box := eq_refl) (has_rel := eq_refl) (has_pars := eq_refl) (has_cstrblocks := eq_refl)) ▷
-  ETransform.optional_self_transform passes.(reorder_constructors)
-    (reorder_cstrs_transformation efl final_wcbv_flags econf.(inductives_mapping)) ▷
   ETransform.optional_self_transform passes.(unboxing)
     (rebuild_wf_env_transform (efl := efl) false false ▷
       unbox_transformation efl final_wcbv_flags) ▷
@@ -149,26 +137,22 @@ Program Definition optional_unsafe_transforms econf :=
      betared_transformation efl final_wcbv_flags).
 
 Next Obligation.
-  destruct (enable_unsafe econf) as [[] [] [] [] []]; cbn in * => //; intuition auto.
+  destruct (enable_unsafe econf) as [[] [] [] []]; cbn in * => //; intuition auto.
 Qed.
 Next Obligation.
-  destruct (enable_unsafe econf) as [[] [] [] [] []]; cbn in * => //; intuition auto.
+  destruct (enable_unsafe econf) as [[] [] [] []]; cbn in * => //; intuition auto.
 Qed.
 Next Obligation.
-  destruct (enable_unsafe econf) as [[] [] [] [] []]; cbn in * => //; intuition auto.
-Qed.
-Next Obligation.
-  destruct (enable_unsafe econf) as [[] [] [] [] []]; cbn in * => //; intuition auto.
+  destruct (enable_unsafe econf) as [[] [] [] []]; cbn in * => //; intuition auto.
 Qed.
 
 Program Definition verified_lambdabox_pipeline {guard : abstract_guard_impl}
   (efl := EWellformed.all_env_flags)
-  : Transform.t _ _ EAst.term EAst.term _ _
+  : Transform.t _ _ _ EAst.term _ _
    (* Standard evaluation, with cases on prop, guarded fixpoints, applied constructors *)
-   (EProgram.eval_eprogram_env default_wcbv_flags)
+   (eval_eprogram_env default_wcbv_flags)
    (* Target evaluation, with no more cases on prop, unguarded fixpoints, constructors as block *)
    (EProgram.eval_eprogram final_wcbv_flags) :=
-
   (* Simulation of the guarded fixpoint rules with a single unguarded one:
     the only "stuck" fixpoints remaining are unapplied.
     This translation is a noop on terms and environments.  *)
@@ -203,9 +187,276 @@ Next Obligation.
   now eapply ETransform.expanded_eprogram_env_expanded_eprogram_cstrs.
 Qed.
 
+Program Definition verified_lambdabox_pipeline_mapping {guard : abstract_guard_impl}
+  (efl := EWellformed.all_env_flags)
+  : Transform.t _ _ _ EAst.term _ _
+   (* Standard evaluation, with cases on prop, guarded fixpoints, applied constructors *)
+   (eval_eprogram_env_mapping default_wcbv_flags)
+   (* Target evaluation, with no more cases on prop, unguarded fixpoints, constructors as block *)
+   (EProgram.eval_eprogram final_wcbv_flags) :=
+  (* Reorder constructors according to the mapping *)
+  reorder_cstrs_transformation (wca := eq_refl) (has_app := eq_refl) default_wcbv_flags (wcon := eq_refl) ▷
+  (* Rebuild the efficient lookup table *)
+  rebuild_wf_env_transform (efl := efl) true true ▷
+  (* Extract as usual *)
+  verified_lambdabox_pipeline.
+
+(* At the end of erasure we get a well-formed program (well-scoped globally and localy), without
+   parameters in inductive declarations. The constructor applications are also transformed to a first-order
+   "block"  application, of the right length, and the evaluation relation does not need to consider guarded
+   fixpoints or case analyses on propositional content. All fixpoint bodies start with a lambda as well.
+   Finally, projections are inlined to cases, so no `tProj` remains. *)
+
+Import EGlobalEnv EWellformed.
+
+Definition eval_pcuic_program_mapping (p : inductives_mapping * pcuic_program) t :=
+  PCUICTransform.eval_pcuic_program p.2 t.
+
+Import EReorderCstrs (wf_tags_list).
+
+Definition wf_pcuic_inductive_mapping (Σ : PCUICAst.PCUICEnvironment.global_env) (m : inductive_mapping) : bool :=
+  let '(ind, (_, cstrs)) := m in
+  match PCUICAst.PCUICLookup.lookup_inductive Σ ind with
+  | Some (mib, oib) => wf_tags_list cstrs #|oib.(PCUICAst.PCUICEnvironment.ind_ctors)|
+  | None => true
+  end.
+
+Definition wf_pcuic_inductives_mapping Σ m := forallb (wf_pcuic_inductive_mapping Σ) m.
+
+Import ErasureFunction ErasureFunctionProperties.
+
+Import PCUICAst.PCUICEnvironment Extract EReorderCstrs EDeps EGlobalEnv.
+
+Lemma lookup_env_filter Σ f kn :
+  fresh_global kn Σ ->
+  lookup_env (filter f Σ) kn = None.
+Proof.
+  induction 1; cbn => //.
+  destruct f. cbn. case: eqb_spec. intros ->. contradiction.
+  eauto. eauto.
+Qed.
+
+Lemma lookup_env_filter_deps {efl : EEnvFlags} {Σ f i p} :
+  wf_glob Σ ->
+  lookup_env Σ i = Some p ->
+  lookup_env (filter f Σ) i = Some p \/
+  lookup_env (filter f Σ) i = None.
+Proof.
+  move=> wfΣ.
+  induction Σ in wfΣ |- *; cbn => //.
+  case: eqb_spec.
+  - intros -> [= <-]. destruct f. left. cbn. now rewrite eqb_refl.
+    right. depelim wfΣ. cbn. now apply lookup_env_filter.
+  - intros diff hl.
+    destruct f. cbn. case: eqb_spec.
+    intros ->. contradiction. intros _. depelim wfΣ.
+    now specialize (IHΣ wfΣ hl).
+    depelim wfΣ.
+    now specialize (IHΣ wfΣ hl).
+Qed.
+
+Lemma lookup_env_filter_deps_None {efl : EEnvFlags} {Σ f i} :
+  wf_glob Σ ->
+  lookup_env Σ i = None ->
+  lookup_env (filter f Σ) i = None.
+Proof.
+  move=> wfΣ.
+  induction Σ in wfΣ |- *; cbn => //.
+  case: eqb_spec.
+  - intros -> [= <-].
+  - intros diff hl.
+    destruct f. cbn. case: eqb_spec.
+    intros ->. contradiction. intros _. depelim wfΣ.
+    now specialize (IHΣ wfΣ hl).
+    depelim wfΣ.
+    now specialize (IHΣ wfΣ hl).
+Qed.
+
+Lemma lookup_inductive_filter_deps_Some {efl : EEnvFlags} {Σ f i p} :
+  wf_glob Σ ->
+  lookup_inductive Σ i = Some p ->
+  lookup_inductive (filter f Σ) i = Some p \/
+  lookup_inductive (filter f Σ) i = None.
+Proof.
+  move => wfΣ.
+  rewrite /lookup_inductive /lookup_minductive.
+  destruct lookup_env eqn:hle => //=.
+  eapply lookup_env_filter_deps in hle as [-> | ->] => //; destruct g => //=. now left.
+  now right.
+Qed.
+
+Lemma lookup_inductive_filter_deps_None {efl : EEnvFlags} {Σ f i} :
+  wf_glob Σ ->
+  lookup_inductive Σ i = None ->
+  lookup_inductive (filter f Σ) i = None.
+Proof.
+  move => wfΣ.
+  rewrite /lookup_inductive /lookup_minductive.
+  destruct lookup_env eqn:hle => //=; try destruct g => //=.
+  eapply (lookup_env_filter_deps) in hle as [-> | ->] => //; destruct g => //=.
+  eapply (lookup_env_filter_deps) in hle as [-> | ->] => //; destruct g => //=.
+  eapply (lookup_env_filter_deps_None) in hle as -> => //; destruct g => //=.
+Qed.
+
+Lemma erases_global_lookup_env_constant Σ Σ' kn :
+  erases_global Σ Σ' ->
+  forall d, PCUICAst.PCUICEnvironment.lookup_env Σ kn = Some (ConstantDecl d) ->
+  exists d', lookup_env Σ' kn = Some (EAst.ConstantDecl d').
+Proof.
+  destruct Σ as [? ? ?]. rewrite /erases_global //=.
+  induction 1; cbn => //.
+  - intros d. case: eqb_spec.
+    + intros ->. intros [=]; subst. now eexists.
+    + intros diff. cbn in *. eauto.
+  - intros d. case: eqb_spec.
+    + intros ->. intros [=]; subst.
+    + intros diff. cbn in *. eauto.
+Qed.
+
+Lemma erases_global_lookup_env_inductive Σ Σ' kn :
+  erases_global Σ Σ' ->
+  forall d, PCUICAst.PCUICEnvironment.lookup_env Σ kn = Some (InductiveDecl d) ->
+  exists d', lookup_env Σ' kn = Some (EAst.InductiveDecl d') /\ erases_mutual_inductive_body d d'.
+Proof.
+  destruct Σ as [? ? ?]. rewrite /erases_global //=.
+  induction 1; cbn => //.
+  - intros d. case: eqb_spec.
+    + intros ->. intros [=]; subst.
+    + intros diff. cbn in *. eauto.
+  - intros d. case: eqb_spec.
+    + intros ->. intros [=]; subst. now eexists.
+    + intros diff. cbn in *. eauto.
+Qed.
+
+Lemma erases_global_lookup_env_none Σ Σ' kn :
+  erases_global Σ Σ' ->
+  PCUICAst.PCUICEnvironment.lookup_env Σ kn = None ->
+  lookup_env Σ' kn = None.
+Proof.
+  destruct Σ as [? ? ?]. rewrite /erases_global //=.
+  induction 1; cbn => //.
+  - case: eqb_spec.
+    + intros ->. intros [=]; subst.
+    + intros diff. cbn in *. eauto.
+  - case: eqb_spec.
+    + intros ->. intros [=]; subst.
+    + intros diff. cbn in *. eauto.
+Qed.
+
+Lemma erases_wf_inductives_mapping {Σ : global_env_ext} {Σ' deps m} :
+  PCUICTyping.wf_ext Σ ->
+  erases_global Σ Σ' ->
+  wf_pcuic_inductives_mapping Σ m ->
+  EReorderCstrs.wf_inductives_mapping (filter_deps deps Σ') m.
+Proof.
+  move=> wfΣ  er.
+  have wfΣ' := ErasureCorrectness.erases_global_wf_glob _ (fst wfΣ) er.
+  rewrite /wf_pcuic_inductives_mapping /wf_inductives_mapping.
+  solve_all. move: H.
+  rewrite /wf_pcuic_inductive_mapping /wf_inductive_mapping.
+  destruct x as [ind [na tags]].
+  have eral := EDeps.erases_global_all_deps _ _ (PCUICElimination.wf_ext_wf _ wfΣ) er.
+  have trind := ErasureProperties.trans_lookup_inductive eral ind.
+  destruct PCUICAst.PCUICLookup.lookup_inductive as [[mib oib]|] eqn:li.
+  specialize (trind _ _ eq_refl).
+  - intros wftags.
+    destruct trind as [mib' [oib' [hli' hctors]]].
+    rewrite (filter_deps_filter (efl := all_env_flags)) //.
+    set (f := fun x => _).
+    eapply (lookup_inductive_filter_deps_Some (efl := all_env_flags) (f:=f)) in hli' as [H|H] => //; rewrite H //.
+    congruence.
+  - intros _. clear trind.
+    destruct (lookup_inductive (filter_deps deps Σ') ind) eqn:li' => //.
+    apply False_rect. move: li'.
+    rewrite (filter_deps_filter (efl:=all_env_flags)) //.
+    generalize (fun x : KernameSet.elt × EAst.global_decl => flip KernameSet.mem (global_deps Σ' deps) x.1).
+    intros f li'.
+    have nli : lookup_inductive Σ' ind = None.
+    { clear -wfΣ wfΣ' er li.
+      move: li. rewrite /PCUICAst.PCUICLookup.lookup_inductive /lookup_inductive.
+      rewrite /PCUICAst.PCUICLookup.lookup_inductive_gen /lookup_minductive.
+      rewrite /PCUICAst.PCUICLookup.lookup_minductive_gen /lookup_minductive.
+      destruct PCUICAst.PCUICEnvironment.lookup_env eqn:hle => //=. destruct g => //.
+      eapply erases_global_lookup_env_constant in hle as [? ->]; tea => //.
+      eapply erases_global_lookup_env_inductive in hle as [? [-> ?]]; tea => //=.
+      depelim H.
+      destruct nth_error eqn:hnth => // _.
+      destruct (nth_error (EAst.ind_bodies _) _) eqn:hnth' => //=.
+      eapply nth_error_Some_length in hnth'. eapply nth_error_None in hnth. eapply Forall2_length in H. lia.
+      intros _.
+      eapply erases_global_lookup_env_none in hle as ->; tea => //. }
+    now rewrite (lookup_inductive_filter_deps_None wfΣ' nli) in li'.
+Qed.
+
+
+Program Definition erase_transform_mapping {guard : abstract_guard_impl} : Transform.t _ _ _ _ PCUICAst.term EAst.term
+  eval_pcuic_program_mapping (eval_eprogram_env_mapping EWcbvEval.default_wcbv_flags) :=
+ {| name := "erasure";
+    pre p := wf_pcuic_inductives_mapping p.2.1 p.1 /\ pre erase_transform p.2 ;
+    transform p hp := let nhs := proj2 hp in
+      (p.1, transform erase_transform p.2 nhs) ;
+   post p := EReorderCstrs.wf_inductives_mapping p.2.1.(EEnvMap.GlobalContextMap.global_decls) p.1 /\ post erase_transform p.2;
+   obseq p hp p' := obseq erase_transform p.2 (proj2 hp) p'.2 |}.
+
+Local Obligation Tactic := idtac.
+Next Obligation.
+  cbn -[erase_transform]. intros.
+  split. 2:eapply (correctness erase_transform).
+  destruct input as [m prog]; cbn [fst snd] in *.
+  destruct p.
+  unfold erase_transform; cbn [transform].
+  unfold erase_program, erase_pcuic_program;
+  set (egf := erase_global_fast _ _ _ _ _);
+  set (ef := ErasureFunction.erase _ _ _ _ _);
+  cbn -[egf ef]; unfold erase_global_fast in egf; rewrite /egf; clear egf ef;
+  set (deps := EAstUtils.term_global_deps _); clearbody deps;
+  match goal with
+  |- context [erase_global_deps_fast ?deps ?X_type ?X ?decls (normalization_in:=?normalization_in) ?hprefix ] =>
+    have heq := @erase_global_deps_fast_erase_global_deps deps X_type X decls normalization_in hprefix
+  end; cbn in heq; specialize (heq (fun Σ eq => f_equal declarations eq));
+  destruct heq as [nin' eq]; rewrite eq; clear eq.
+  rewrite erase_global_deps_erase_global.
+  cbn -[ErasureFunction.erase_global].
+  match goal with
+  |- context [@erase_global ?X_type ?X ?decls ?SN ?eq] =>
+  have erg := @erases_global_erase_global X_type X _ _ SN eq
+  end.
+  cbn in erg. specialize (erg _ eq_refl).
+  cbn in p. destruct p as [[wt] ?].
+  set (eg := erase_global _ _ _) in erg |- *. clearbody eg.
+  have := erases_wf_inductives_mapping (Σ' := eg) (fst wt) erg i.
+  intros h. eauto.
+Qed.
+
+Next Obligation.
+  intros g p v pr ev. cbn.
+  now apply (preservation erase_transform).
+Qed.
+
+Program Definition pcuic_expand_lets_transform_mapping {cf : checker_flags} K : Transform.t _ _ _ _ PCUICAst.term PCUICAst.term
+  eval_pcuic_program_mapping eval_pcuic_program_mapping :=
+ {| name := "let expansion in constructors";
+    pre p := wf_pcuic_inductives_mapping p.2.1 p.1 /\ pre (pcuic_expand_lets_transform K) p.2 ;
+    transform p hp := let nhs := proj2 hp in
+      (p.1, transform (pcuic_expand_lets_transform K) p.2 nhs) ;
+   post p := wf_pcuic_inductives_mapping p.2.1 p.1 /\ post (pcuic_expand_lets_transform K) p.2;
+   obseq p hp p' := obseq (pcuic_expand_lets_transform K) p.2 (proj2 hp) p'.2 |}.
+Next Obligation.
+  cbn. intros cf K input []. split => //.
+  - move: H; rewrite /wf_pcuic_inductives_mapping.
+    solve_all. move: H; rewrite /wf_pcuic_inductive_mapping.
+    destruct x as [ind [na tags]].
+    rewrite /PCUICAst.PCUICLookup.lookup_inductive /PCUICAst.PCUICLookup.lookup_inductive_gen /PCUICAst.PCUICLookup.lookup_minductive_gen.
+    rewrite PCUICExpandLetsCorrectness.trans_lookup. destruct PCUICAst.PCUICEnvironment.lookup_env => //. destruct g => //=.
+    rewrite nth_error_mapi. destruct nth_error => //=. now len.
+  - unshelve eapply (correctness (pcuic_expand_lets_transform K)). apply H0.
+Qed.
+Next Obligation.
+  intros cf K p v pr ev. now eapply (preservation (pcuic_expand_lets_transform K)).
+Qed.
+
 Program Definition verified_erasure_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) :
- Transform.t _ _
-  PCUICAst.term EAst.term _ _
+ Transform.t _ _ _ EAst.term _ _
   PCUICTransform.eval_pcuic_program
   (EProgram.eval_eprogram final_wcbv_flags) :=
   (* a bunch of nonsense for normalization preconditions *)
@@ -219,6 +470,37 @@ Program Definition verified_erasure_pipeline {guard : abstract_guard_impl} (efl
   (* Erasure of proofs terms in Prop and types *)
   erase_transform ▷
   verified_lambdabox_pipeline.
+Next Obligation.
+  intros guard efl K T1 p.
+  cbn. intuition eauto. now eapply H2. now eapply H2.
+Qed.
+Next Obligation.
+  intros guard efl K T1 p. cbn. intuition auto.
+Qed.
+
+Program Definition verified_erasure_pipeline_mapping {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) :
+ Transform.t _ _ _ EAst.term _ _
+  eval_pcuic_program_mapping
+  (EProgram.eval_eprogram final_wcbv_flags) :=
+  (* a bunch of nonsense for normalization preconditions *)
+  let K ty (T : ty -> _) p
+    := let p := T p in
+       (PCUICTyping.wf_ext p -> PCUICSN.NormalizationIn p) /\
+         (PCUICTyping.wf_ext p -> PCUICWeakeningEnvSN.normalizationInAdjustUniversesIn p) in
+  let T1 (p:global_env_ext_map) := p in
+  (* Branches of cases are expanded to bind only variables, constructor types are expanded accordingly *)
+  pcuic_expand_lets_transform_mapping (K _ T1) ▷
+  (* Erasure of proofs terms in Prop and types *)
+  erase_transform_mapping ▷
+  verified_lambdabox_pipeline_mapping.
+Next Obligation.
+  intros guard efl K T1 p.
+  cbn. intuition eauto. now eapply H3. now eapply H3.
+Qed.
+Next Obligation.
+  intros guard efl K T1 p. cbn. intuition auto.
+  split; eauto.
+Qed.
 
 Import EGlobalEnv EWellformed.
 
@@ -236,24 +518,143 @@ Proof.
   eexists;reflexivity.
 Qed.
 
-Lemma verified_lambdabox_pipeline_extends {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) :
-  TransformExt.t verified_lambdabox_pipeline (fun p p' => extends (EEnvMap.GlobalContextMap.global_decls p.1)
-  (EEnvMap.GlobalContextMap.global_decls p'.1)) (fun p p' => extends p.1 p'.1).
+Instance verified_lambdabox_pipeline_extends {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) :
+  TransformExt.t verified_lambdabox_pipeline
+    (fun p p' =>
+      extends (EEnvMap.GlobalContextMap.global_decls p.1) (EEnvMap.GlobalContextMap.global_decls p'.1)) (fun p p' => extends p.1 p'.1).
 Proof.
   unfold verified_lambdabox_pipeline. tc.
 Qed.
 
+Instance verified_lambdabox_pipeline_mapping_extends {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) :
+  TransformExt.t verified_lambdabox_pipeline_mapping
+    (fun p p' =>
+      p.1 = p'.1 /\
+      extends (EEnvMap.GlobalContextMap.global_decls p.2.1) (EEnvMap.GlobalContextMap.global_decls p'.2.1)) (fun p p' => extends p.1 p'.1).
+Proof.
+  unfold verified_lambdabox_pipeline_mapping. tc.
+Qed.
+
 Lemma verified_lambdabox_pipeline_extends' {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) :
   TransformExt.t verified_lambdabox_pipeline extends_eprogram_env extends_eprogram.
 Proof.
   unfold verified_lambdabox_pipeline. tc.
 Qed.
 
-Program Definition pre_erasure_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) :
+Lemma verified_lambdabox_pipeline_mapping_extends' {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) :
+  TransformExt.t verified_lambdabox_pipeline_mapping (fun p p' => p.1 = p'.1 /\ extends_eprogram_env p.2 p'.2) extends_eprogram.
+Proof.
+  unfold verified_lambdabox_pipeline_mapping. tc.
+Qed.
+
+Definition eval_template_program_mapping (p : inductives_mapping * template_program) t :=
+  TemplateProgram.eval_template_program p.2 t.
+
+Definition eval_template_program_env_mapping (p : inductives_mapping * template_program_env) t :=
+  TemplateProgram.eval_template_program_env p.2 t.
+
+Definition wf_template_inductive_mapping (Σ : Env.global_env) (m : inductive_mapping) : bool :=
+  let '(ind, (_, cstrs)) := m in
+  match Template.Ast.lookup_inductive Σ ind with
+  | Some (mib, oib) => wf_tags_list cstrs #|oib.(Env.ind_ctors)|
+  | None => true
+  end.
+
+Definition wf_template_inductives_mapping Σ m := forallb (wf_template_inductive_mapping Σ) m.
+
+Program Definition build_template_program_env_mapping {cf : checker_flags} K :
+  Transform.t _ _ _ _ _ _ eval_template_program_mapping eval_template_program_env_mapping :=
+ {| name := name (build_template_program_env K);
+    pre p := wf_template_inductives_mapping p.2.1 p.1 /\ pre (build_template_program_env K) p.2 ;
+    transform p hp := let nhs := proj2 hp in
+      (p.1, transform (build_template_program_env K) p.2 nhs) ;
+   post p := wf_template_inductives_mapping p.2.1 p.1 /\ post (build_template_program_env K) p.2;
+   obseq p hp p' := obseq (build_template_program_env K) p.2 (proj2 hp) p'.2 |}.
+Next Obligation.
+  cbn; intros  cf K input [? []]. intuition auto.
+Qed.
+Next Obligation.
+  cbn; intros  cf K ? ? [? []] ev. cbn.
+  now unshelve eapply (preservation (build_template_program_env K)).
+Qed.
+
+Lemma lookup_lookup_global_env_None (Σ : GlobalEnvMap.t) kn :
+  Env.lookup_env Σ kn = None ->
+  Env.lookup_global (eta_global_declarations Σ (Env.declarations Σ)) kn = None.
+Proof.
+  intros hl.
+  induction Σ => // /=. induction env => //=. cbn in hl.
+  rewrite /eta_global_declarations. cbn in *. rewrite lookup_global_map_on_snd hl //.
+Qed.
+
+Lemma eta_lookup_inductive_ctors (Σ : GlobalEnvMap.t) ind :
+  option_map (fun '(mib, oib) => #|Env.ind_ctors oib|) (Ast.lookup_inductive Σ ind) = option_map (fun '(mib, oib) => #|Env.ind_ctors oib|) (Ast.lookup_inductive (eta_expand_global_env Σ) ind).
+Proof.
+  rewrite /Ast.lookup_inductive /eta_expand_global_env /lookup_inductive_gen /lookup_minductive_gen.
+  destruct Env.lookup_env eqn:le => //.
+  cbn. eapply eta_lookup_global in le. rewrite le /=.
+  destruct g => //=. rewrite nth_error_map. destruct nth_error => //=. len.
+  cbn. now eapply lookup_lookup_global_env_None in le as ->.
+Qed.
+
+Program Definition eta_expand_mapping K :
+  Transform.t _ _ _ _ _ _ eval_template_program_env_mapping eval_template_program_mapping :=
+ {| name := name (eta_expand K);
+    pre p := wf_template_inductives_mapping p.2.1 p.1 /\ pre (eta_expand K) p.2 ;
+    transform p hp := let nhs := proj2 hp in
+      (p.1, transform (eta_expand K) p.2 nhs) ;
+   post p := wf_template_inductives_mapping p.2.1 p.1 /\ post (eta_expand K) p.2;
+   obseq p hp p' := obseq (eta_expand K) p.2 (proj2 hp) p'.2 |}.
+Next Obligation.
+  cbn; intros K input [? ?]. split. 2:now unshelve eapply (correctness (eta_expand K)).
+  move: H. rewrite /wf_template_inductives_mapping.
+  solve_all. move: H.
+  rewrite /wf_template_inductive_mapping.
+  destruct x as [ind [na tags]].
+  have eqe := eta_lookup_inductive_ctors input.2.1 ind.
+  do 2 destruct Ast.lookup_inductive as [[? ?]|]; cbn in *; congruence.
+Qed.
+Next Obligation.
+  cbn; intros K ? ? [? []] ev. cbn.
+  now unshelve eapply (preservation (eta_expand K)).
+Qed.
+
+Program Definition template_to_pcuic_mapping K :
+  Transform.t _ _ _ _ _ _ eval_template_program_mapping eval_pcuic_program_mapping :=
+ {| name := name (template_to_pcuic_transform K);
+    pre p := wf_template_inductives_mapping p.2.1 p.1 /\ pre (template_to_pcuic_transform K) p.2 ;
+    transform p hp := let nhs := proj2 hp in
+      (p.1, transform (template_to_pcuic_transform K) p.2 nhs) ;
+   post p := wf_pcuic_inductives_mapping p.2.1 p.1 /\ post (template_to_pcuic_transform K) p.2;
+   obseq p hp p' := obseq (template_to_pcuic_transform K) p.2 (proj2 hp) p'.2 |}.
+Next Obligation.
+  cbn; intros K input [wfm pre].
+  pose proof (correctness (template_to_pcuic_transform K) _ pre) as post.
+  split. 2:now unshelve eapply (correctness (template_to_pcuic_transform K)).
+  move: wfm. rewrite /wf_template_inductives_mapping.
+  solve_all. move: H.
+  rewrite /wf_template_inductive_mapping /wf_pcuic_inductive_mapping.
+  unfold Ast.lookup_inductive, PCUICAst.PCUICLookup.lookup_inductive, Ast.lookup_inductive_gen,
+    PCUICAst.PCUICLookup.lookup_inductive_gen,
+    PCUICAst.PCUICLookup.lookup_minductive_gen,
+    Ast.lookup_minductive_gen, lookup_minductive_gen.
+  cbn. destruct post as [[[wtr _]] _]. cbn in wtr.
+  destruct x as [ind [na tags]].
+  destruct pre as [[wta] _].
+  have trl := TemplateToPCUICCorrectness.trans_lookup input.2.1 (inductive_mind ind) wta.1 wtr.1.
+  destruct Env.lookup_env; cbn in *; rewrite trl //.
+  destruct g => //=. rewrite nth_error_map. destruct nth_error => //=. len.
+Qed.
+Next Obligation.
+  cbn; intros K ? ? [? []] ev. cbn.
+  now unshelve eapply (preservation (template_to_pcuic_transform K)).
+Qed.
+
+Program Definition pre_erasure_pipeline (efl := EWellformed.all_env_flags) :
  Transform.t _ _
-  Ast.term PCUICAst.term _ _
-  TemplateProgram.eval_template_program
-   PCUICTransform.eval_pcuic_program :=
+  _ _ _ _
+  eval_template_program
+  PCUICTransform.eval_pcuic_program :=
   (* a bunch of nonsense for normalization preconditions *)
   let K ty (T : ty -> _) p
     := let p := T p in
@@ -261,7 +662,7 @@ Program Definition pre_erasure_pipeline {guard : abstract_guard_impl} (efl := EW
          (PCUICTyping.wf_ext p -> PCUICWeakeningEnvSN.normalizationInAdjustUniversesIn p) in
   let T1 (p:global_env_ext_map) := p in
   let T2 (p:global_env_ext_map) := T1 (build_global_env_map (PCUICExpandLets.trans_global_env p.1), p.2) in
-  let T3 (p:global_env) := T2 (TemplateToPCUIC.trans_global_env p, Monomorphic_ctx) in
+  let T3 (p:Env.global_env) := T2 (TemplateToPCUIC.trans_global_env p, Monomorphic_ctx) in
   let T4 (p:GlobalEnvMap.t) := T3 (eta_expand_global_env p) in
   (* Build an efficient lookup map for the following eta-expansion phase *)
   build_template_program_env (K _ T4) ▷
@@ -269,22 +670,75 @@ Program Definition pre_erasure_pipeline {guard : abstract_guard_impl} (efl := EW
   eta_expand (K _ T3) ▷
   (* Casts are removed, application is binary, case annotations are inferred from the global environment *)
   template_to_pcuic_transform (K _ T2).
+Next Obligation.
+  intros efl K T1 T2 T3 T4 p. cbn. intuition eauto.
+Qed.
+Next Obligation.
+  intros efl K T1 T2 T3 T4 p. cbn. intuition eauto.
+Qed.
 
-Program Definition erasure_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) : Transform.t _ _
-  Ast.term EAst.term _ _
-  TemplateProgram.eval_template_program
+Program Definition pre_erasure_pipeline_mapping (efl := EWellformed.all_env_flags) :
+ Transform.t _ _
+  _ _ _ _
+  eval_template_program_mapping
+  eval_pcuic_program_mapping :=
+  (* a bunch of nonsense for normalization preconditions *)
+  let K ty (T : ty -> _) p
+    := let p := T p in
+       (PCUICTyping.wf_ext p -> PCUICSN.NormalizationIn p) /\
+         (PCUICTyping.wf_ext p -> PCUICWeakeningEnvSN.normalizationInAdjustUniversesIn p) in
+  let T1 (p:global_env_ext_map) := p in
+  let T2 (p:global_env_ext_map) := T1 (build_global_env_map (PCUICExpandLets.trans_global_env p.1), p.2) in
+  let T3 (p:Env.global_env) := T2 (TemplateToPCUIC.trans_global_env p, Monomorphic_ctx) in
+  let T4 (p:GlobalEnvMap.t) := T3 (eta_expand_global_env p) in
+  (* Build an efficient lookup map for the following eta-expansion phase *)
+  build_template_program_env_mapping (K _ T4) ▷
+  (* Eta-expand constructors and fixpoint *)
+  eta_expand_mapping (K _ T3) ▷
+  (* Casts are removed, application is binary, case annotations are inferred from the global environment *)
+  template_to_pcuic_mapping (K _ T2).
+Next Obligation.
+  intros efl K T1 T2 T3 T4 p. cbn. intuition eauto.
+Qed.
+Next Obligation.
+  intros efl K T1 T2 T3 T4 p. cbn. intuition eauto.
+Qed.
+
+Program Definition erasure_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) : Transform.t _ _ _ _ _ _
+  eval_template_program
   (EProgram.eval_eprogram final_wcbv_flags) :=
   pre_erasure_pipeline ▷
   verified_erasure_pipeline.
 
-Program Definition verified_lambdabox_typed_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) econf :
-  Transform.t _ _ EAst.term EAst.term _ _
-    (EProgram.eval_eprogram_env {| with_prop_case := false; with_guarded_fix := true; with_constructor_as_block := false |})
+Next Obligation.
+  intros guard efl p; cbn. intuition auto.
+Qed.
+
+Program Definition erasure_pipeline_mapping {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) : Transform.t _ _ _ _ _ _
+  eval_template_program_mapping
+  (EProgram.eval_eprogram final_wcbv_flags) :=
+  pre_erasure_pipeline_mapping ▷
+  verified_erasure_pipeline_mapping.
+
+Next Obligation.
+  intros guard efl p; cbn. intuition auto.
+Qed.
+
+Local Obligation Tactic := program_simpl.
+
+Program Definition verified_lambdabox_typed_pipeline (efl := EWellformed.all_env_flags)
+  (wfl := {| with_prop_case := false; with_guarded_fix := true; with_constructor_as_block := false |}) econf :
+  Transform.t _ _ _ EAst.term _ _
+    (eval_eprogram_env_mapping wfl)
     (EProgram.eval_eprogram final_wcbv_flags) :=
+  (* Reorder constructors according to the mapping *)
+  reorder_cstrs_transformation (wca := eq_refl) (has_app := eq_refl) wfl (wcon := eq_refl) ▷
+  (* Rebuild the efficient lookup table *)
+  rebuild_wf_env_transform (efl := efl) true true ▷
    (* Simulation of the guarded fixpoint rules with a single unguarded one:
      the only "stuck" fixpoints remaining are unapplied.
      This translation is a noop on terms and environments.  *)
-   guarded_to_unguarded_fix (fl := {| with_prop_case := false; with_guarded_fix := true; with_constructor_as_block := false |}) (wcon := eq_refl) eq_refl ▷
+  guarded_to_unguarded_fix (fl := {| with_prop_case := false; with_guarded_fix := true; with_constructor_as_block := false |}) (wcon := eq_refl) eq_refl ▷
    (* Remove all constructor parameters *)
    remove_params_optimization (wcon := eq_refl) ▷
    (* Rebuild the efficient lookup table *)
@@ -319,12 +773,254 @@ Qed.
 
 Local Obligation Tactic := intros; eauto.
 
+Definition eval_typed_eprogram_mapping (wfl : WcbvFlags) (p : inductives_mapping × (ExAst.global_env × EAst.term)) t :=
+  eval_typed_eprogram wfl p.2 t.
+
+Lemma wf_inductive_mapping_trans {Σ Σ' m} :
+  (forall kn decl, ExAst.lookup_inductive Σ' kn = Some decl ->
+    exists decl', PCUICAst.lookup_inductive Σ kn = Some decl' /\ #|ind_ctors decl'.2| = #|ExAst.ind_ctors decl|) ->
+  wf_pcuic_inductive_mapping Σ m ->
+  wf_inductive_mapping (ExAst.trans_env Σ') m.
+Proof.
+  intros hkn.
+  rewrite /wf_pcuic_inductive_mapping /wf_inductive_mapping.
+  destruct m as [ind [na tags]].
+  destruct lookup_inductive as [decl|]eqn:hl => //.
+  have [pdecl [hl' htr]] : exists p, ExAst.lookup_inductive Σ' ind = Some p /\ ExAst.trans_oib p = decl.2.
+  { move: hl; rewrite /lookup_inductive /ExAst.lookup_inductive.
+    rewrite /lookup_minductive /= /ExAst.lookup_minductive.
+    rewrite OptimizeCorrectness.lookup_env_trans_env.
+    destruct ExAst.lookup_env => //=. destruct g => //=.
+    rewrite nth_error_map //=. destruct nth_error => //=. intros [= <-].
+    now eexists. }
+  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.
+Qed.
+
+From Equations Require Import Equations.
+
+Lemma nth_error_map_In {A B} (l : list A) (f : forall x, In x l -> B) n o :
+  nth_error (map_In l f) n = Some o ->
+  exists a (ha : In a l), nth_error l n = Some a /\ o = f a ha.
+Proof.
+  funelim (map_In l f); cbn.
+  - rewrite nth_error_nil => //.
+  - destruct n; cbn.
+    * intros [= <-]; now eexists.
+    * intros h. have [a [hin []]]:= H _ _ h.
+      intros -> ->. exists a. exists (or_intror hin). split => //.
+Qed.
+
+Lemma map_In_length {A B} (l : list A) (f : forall x, In x l -> B) :
+  #|map_In l f| = #|l|.
+Proof. funelim (map_In l f); cbn; auto; lia. Qed.
+
+Lemma lookup_inductive_erase_global_decls_deps {X_type X} {decls : global_env} {prop incl ignore} {kn} {decl} :
+  ExAst.lookup_inductive (@Erasure.erase_global_decls_deps_recursive X_type X (declarations decls) (universes decls) (retroknowledge decls) prop incl ignore) kn = Some decl ->
+  exists decl', PCUICAst.lookup_inductive decls kn = Some decl' /\ #|ind_ctors decl'.2| = #|ExAst.ind_ctors decl|.
+Proof.
+  rewrite /ExAst.lookup_inductive /ExAst.lookup_minductive.
+  destruct decls as [univs' decls retro].
+  cbn. unfold ExAst.lookup_env.
+  induction decls as [|[kn' []]] in X, prop, incl |- *. cbn => //.
+  - cbn [Erasure.erase_global_decls_deps_recursive] => //.
+    destruct KernameSet.mem; cbn [ExAst.lookup_env Erasure.erase_global_decl];
+    try destruct Erasure.erase_constant_decl => //=;
+    unfold PCUICAst.lookup_inductive;
+    unfold PCUICAst.PCUICEnvironment.lookup_env; cbn;
+    unfold PCUICAst.lookup_inductive_gen, PCUICAst.lookup_minductive_gen.
+    * unfold ExAst.lookup_env. cbn.
+      case: eqb_spec.
+      + intros <-. now cbn.
+      + intros diff. cbn in IHdecls. eapply IHdecls.
+    * case: eqb_spec.
+      + intros <-. now cbn.
+      + intros diff. eapply IHdecls.
+    * case: eqb_spec.
+      + intros heq.
+        pose proof (PCUICWfEnv.abstract_env_exists X) as [[Σ abs]].
+        pose proof (PCUICWfEnv.abstract_env_wf _ abs) as [].
+        pose proof (prop _ abs). subst Σ. cbn in X0.
+        eapply wf_fresh_globals in X0. cbn in  X0.
+        depelim X0. clear abs.
+        match goal with
+        |- context [@Erasure.erase_global_decls_deps_recursive ?X_type ?X ?decls ?univs ?retro ?prop ?incl ?ignore ] =>
+        set (iprop := prop); set (iincl := incl)
+        (* have hcor := @ErasureCorrectness.erase_global_decls_deps_recursive_correct X_type X decls univs retro prop incl ignore (fun _ => eq_refl) *)
+        end.
+        intros h; specialize (IHdecls _ iprop iincl h).
+        destruct IHdecls as [decl'' []].
+        subst kn'. move: H0.
+        rewrite /PCUICAst.lookup_inductive /PCUICAst.lookup_inductive_gen.
+        rewrite /PCUICAst.lookup_minductive /PCUICAst.lookup_minductive_gen. cbn.
+        destruct lookup_global eqn:hl => //=.
+        eapply PCUICAst.fresh_global_iff_lookup_global_None in H. rewrite H in hl. congruence.
+      + intros diff. eapply IHdecls.
+  - cbn [Erasure.erase_global_decls_deps_recursive] => //.
+    destruct KernameSet.mem; cbn [ExAst.lookup_env Erasure.erase_global_decl];
+    unfold PCUICAst.lookup_inductive;
+    unfold PCUICAst.PCUICEnvironment.lookup_env; cbn;
+    unfold PCUICAst.lookup_inductive_gen, PCUICAst.lookup_minductive_gen.
+    * unfold ExAst.lookup_env. cbn.
+      case: eqb_spec.
+      + intros <-. cbn.
+        destruct nth_error eqn:hmi => //. intros [= <-].
+        eapply nth_error_map_In in hmi as [oib [hin [hnth ->]]].
+        exists (m, oib); rewrite hnth. split => //=.
+        now rewrite /Erasure.erase_ind_body map_In_length.
+      + intros diff. eapply IHdecls.
+    * case: eqb_spec.
+      + intros heq.
+        pose proof (PCUICWfEnv.abstract_env_exists X) as [[Σ abs]].
+        pose proof (PCUICWfEnv.abstract_env_wf _ abs) as [].
+        pose proof (prop _ abs). subst Σ. cbn in X0.
+        eapply wf_fresh_globals in X0. cbn in  X0.
+        depelim X0. clear abs.
+        match goal with
+        |- context [@Erasure.erase_global_decls_deps_recursive ?X_type ?X ?decls ?univs ?retro ?prop ?incl ?ignore ] =>
+        set (iprop := prop); set (iincl := incl)
+        (* have hcor := @ErasureCorrectness.erase_global_decls_deps_recursive_correct X_type X decls univs retro prop incl ignore (fun _ => eq_refl) *)
+        end.
+        intros h; specialize (IHdecls _ iprop iincl h).
+        destruct IHdecls as [decl'' []].
+        subst kn'. move: H0.
+        rewrite /PCUICAst.lookup_inductive /PCUICAst.lookup_inductive_gen.
+        rewrite /PCUICAst.lookup_minductive /PCUICAst.lookup_minductive_gen. cbn.
+        destruct lookup_global eqn:hl => //=.
+        eapply PCUICAst.fresh_global_iff_lookup_global_None in H. rewrite H in hl. congruence.
+      + intros diff. eapply IHdecls.
+Qed.
+
+Local Obligation Tactic := program_simpl.
+
+Program Definition typed_erase_transform_mapping :
+  Transform.t _ _ _ _ _ _ eval_pcuic_program_mapping (eval_typed_eprogram_mapping default_wcbv_flags) :=
+ {| name := name typed_erase_transform;
+    pre p := wf_pcuic_inductives_mapping p.2.1 p.1 /\ pre typed_erase_transform p.2 ;
+    transform p hp := let nhs := proj2 hp in
+      (p.1, transform typed_erase_transform p.2 nhs) ;
+   post p := wf_inductives_mapping (ExAst.trans_env p.2.1) p.1 /\ post typed_erase_transform p.2;
+   obseq p hp p' := obseq typed_erase_transform p.2 (proj2 hp) p'.2 |}.
+
+Next Obligation.
+Proof.
+  destruct s. cbn -[ExAst.trans_env typed_erase_transform]. split => //.
+  2:{ eapply (correctness typed_erase_transform). }
+  move: i; rewrite /wf_pcuic_inductives_mapping /wf_inductives_mapping.
+  solve_all.
+  destruct w as [wf wt].
+  eapply wf_inductive_mapping_trans; tea.
+  intros kn d.
+  eapply lookup_inductive_erase_global_decls_deps.
+Qed.
+Next Obligation.
+  cbn. intros p v pr. eapply (preservation typed_erase_transform).
+Qed.
+
+Lemma lookup_inductive_map_on_snd_remove_decl Σ Σ' kn :
+  lookup_inductive (map (on_snd (EOptimizePropDiscr.remove_match_on_box_decl Σ')) Σ) kn = lookup_inductive Σ kn.
+Proof.
+  rewrite /lookup_inductive /lookup_minductive.
+  rewrite EGenericGlobalMap.lookup_env_map_snd. destruct lookup_env => //=.
+  destruct g => //.
+Qed.
+
+Program Definition remove_match_on_box_typed_transform_mapping {fl} {wcon : with_constructor_as_block = false} {efl : EEnvFlags} {hastrel : has_tRel} {hastbox : has_tBox} :
+  Transform.t _ _ _ _ _ _ (eval_typed_eprogram_mapping fl) (eval_typed_eprogram_mapping (disable_prop_cases fl)) :=
+  let tr := (remove_match_on_box_typed_transform (fl:=fl) (wcon := wcon) (hastrel := hastrel) (hastbox := hastbox)) in
+ {| name := name tr;
+    pre p := wf_inductives_mapping (ExAst.trans_env p.2.1) p.1 /\ pre tr p.2 ;
+    transform p hp := let nhs := proj2 hp in (p.1, transform tr p.2 nhs) ;
+    post p := wf_inductives_mapping (ExAst.trans_env p.2.1) p.1 /\ post tr p.2;
+     obseq p hp p' := obseq tr p.2 (proj2 hp) p'.2 |}.
+
+Next Obligation.
+Proof.
+  split. 2:{ cbn. now unshelve eapply (correctness remove_match_on_box_typed_transform). }
+  cbn.
+  move: i; rewrite /wf_inductives_mapping; solve_all.
+  move: H; rewrite /wf_inductive_mapping.
+  rewrite /remove_match_on_box_typed_env.
+  rewrite -map_trans_env.
+  destruct x as [ind [na tags]]. now rewrite lookup_inductive_map_on_snd_remove_decl.
+Qed.
+Next Obligation.
+  intros p v pr ev.
+  now unshelve eapply (preservation remove_match_on_box_typed_transform).
+Qed.
+
+Definition eval_typed_eprogram_masks_mapping (fl : WcbvFlags) (p : inductives_mapping × ((option Optimize.dearg_set × ExAst.global_env) × EAst.term)) t :=
+  eval_typed_eprogram_masks fl p.2 t.
+
+Program Definition dearging_checks_transform_mapping {efl : EEnvFlags} (cf : ETransform.dearging_config) {hastrel : has_tRel} {hastbox : has_tBox} :
+  Transform.t _ _ _ _ _ _ (eval_typed_eprogram_mapping opt_wcbv_flags) (eval_typed_eprogram_masks_mapping opt_wcbv_flags) :=
+  let tr := (dearging_checks_transform (efl:=efl) cf (hastrel := hastrel) (hastbox := hastbox)) in
+ {| name := name tr;
+    pre p := wf_inductives_mapping (ExAst.trans_env p.2.1) p.1 /\ pre tr p.2 ;
+    transform p hp := let nhs := proj2 hp in (p.1, transform tr p.2 nhs) ;
+    post p := wf_inductives_mapping (ExAst.trans_env p.2.1.2) p.1 /\ post tr p.2;
+    obseq p hp p' := obseq tr p.2 (proj2 hp) p'.2 |}.
+Next Obligation.
+Proof.
+  split => //.
+Qed.
+Next Obligation.
+Proof.
+  intros p v pr ev. now unshelve eapply (preservation (dearging_checks_transform cf)).
+Qed.
+
+Program Definition dearging_transform_mapping (cf : ETransform.dearging_config) :
+  Transform.t _ _ _ _ _ _ (eval_typed_eprogram_masks_mapping opt_wcbv_flags) (eval_eprogram_mapping opt_wcbv_flags)  :=
+  let tr := (dearging_transform cf) in
+ {| name := name tr;
+    pre p := wf_inductives_mapping (ExAst.trans_env p.2.1.2) p.1 /\ pre tr p.2 ;
+    transform p hp := let nhs := proj2 hp in (p.1, transform tr p.2 nhs) ;
+    post p := wf_inductives_mapping p.2.1 p.1 /\ post tr p.2;
+    obseq p hp p' := obseq tr p.2 (proj2 hp) p'.2 |}.
+Next Obligation.
+Proof.
+  split => //.
+  2:{ now unshelve eapply (correctness (dearging_transform cf)). }
+  move: H; rewrite /wf_inductives_mapping; solve_all.
+  move: H; rewrite /wf_inductive_mapping. destruct x as [ind [na tags]].
+  rewrite /dearg. destruct input.2.1.1 => //.
+  rewrite /OptimizeCorrectness.dearg_env.
+  rewrite /lookup_inductive /lookup_minductive /=.
+  rewrite !OptimizeCorrectness.lookup_env_trans_env.
+  rewrite OptimizeCorrectness.lookup_env_debox_env_types option_map_two /=.
+  rewrite OptimizeCorrectness.lookup_env_dearg_env option_map_two /=.
+  destruct ExAst.lookup_env => //=; destruct g => //=.
+  rewrite !nth_error_map option_map_two /=.
+  rewrite /Optimize.dearg_mib /=. destruct Optimize.get_mib_masks => //=.
+  rewrite !nth_error_mapi.
+  1-2:destruct nth_error eqn:hnth => //=; len.
+  intros _. destruct o => //=. destruct p => //.
+Qed.
+Next Obligation.
+Proof.
+  intros p v pr ev. now unshelve eapply (preservation (dearging_transform cf)).
+Qed.
+
+Program Definition rebuild_wf_env_transform_mapping {fl : WcbvFlags} {efl : EEnvFlags} (with_exp with_fix : bool) :
+  Transform.t _ _ _ _ _ _ (eval_eprogram_mapping fl) (eval_eprogram_env_mapping fl) :=
+  let tr := @rebuild_wf_env_transform fl efl with_exp with_fix in
+ {| name := name tr;
+    pre p := wf_inductives_mapping p.2.1 p.1 /\ pre tr p.2 ;
+    transform p hp := let nhs := proj2 hp in (p.1, transform tr p.2 nhs) ;
+    post p := wf_inductives_mapping p.2.1.(EEnvMap.GlobalContextMap.global_decls) p.1 /\ post tr p.2;
+    obseq p hp p' := obseq tr p.2 (proj2 hp) p'.2 |}.
+Next Obligation.
+Proof.
+  intros p v pr ev. now unshelve eapply (preservation (rebuild_wf_env_transform _ _)).
+Qed.
+
 Program Definition verified_typed_erasure_pipeline {guard : abstract_guard_impl}
   (efl := EWellformed.all_env_flags)
   econf :
-  Transform.t _ _
-   PCUICAst.term EAst.term _ _
-   PCUICTransform.eval_pcuic_program
+  Transform.t _ _ _ _ _ _
+   eval_pcuic_program_mapping
    (EProgram.eval_eprogram final_wcbv_flags) :=
    (* a bunch of nonsense for normalization preconditions *)
    let K ty (T : ty -> _) p
@@ -333,32 +1029,30 @@ Program Definition verified_typed_erasure_pipeline {guard : abstract_guard_impl}
           (PCUICTyping.wf_ext p -> PCUICWeakeningEnvSN.normalizationInAdjustUniversesIn p) in
    let T1 (p:global_env_ext_map) := p in
    (* Branches of cases are expanded to bind only variables, constructor types are expanded accordingly *)
-   pcuic_expand_lets_transform (K _ T1) ▷
+   pcuic_expand_lets_transform_mapping (K _ T1) ▷
    (* Erasure of proofs terms in Prop and types *)
-   typed_erase_transform ▷
+   typed_erase_transform_mapping ▷
    (* Remove match on box early for dearging *)
-   remove_match_on_box_typed_transform (wcon := eq_refl) (hastrel := eq_refl) (hastbox := eq_refl) ▷
+   remove_match_on_box_typed_transform_mapping (wcon := eq_refl) (hastrel := eq_refl) (hastbox := eq_refl) ▷
    (* Check if the preconditions for dearging are valid, otherwise dearging will be the identity *)
-   dearging_checks_transform econf.(dearging_config) (hastrel := eq_refl) (hastbox := eq_refl) ▷
-   dearging_transform econf.(dearging_config) ▷
-   rebuild_wf_env_transform true true ▷
+   dearging_checks_transform_mapping econf.(dearging_config) (hastrel := eq_refl) (hastbox := eq_refl) ▷
+   dearging_transform_mapping econf.(dearging_config) ▷
+   rebuild_wf_env_transform_mapping true true ▷
    verified_lambdabox_typed_pipeline econf.
 
   Next Obligation.
-    cbn in H. split; cbn; intuition eauto.
+    unfold pre_remove_match_on_box_typed. split; intuition eauto.
   Qed.
   Next Obligation.
-    cbn in H |- *; intuition eauto.
+    split; intuition auto.
   Qed.
 
 Program Definition typed_erasure_pipeline {guard : abstract_guard_impl}
-  (efl := EWellformed.all_env_flags)
-  econf :
-  Transform.t _ _
-   Ast.term EAst.term _ _
-   TemplateProgram.eval_template_program
+  (efl := EWellformed.all_env_flags) econf :
+  Transform.t _ _ _ _ _ _
+   eval_template_program_mapping
    (EProgram.eval_eprogram final_wcbv_flags) :=
-   pre_erasure_pipeline ▷
+   pre_erasure_pipeline_mapping ▷
    verified_typed_erasure_pipeline econf.
 
 (* At the end of erasure we get a well-formed program (well-scoped globally and localy), without
@@ -369,61 +1063,6 @@ Program Definition typed_erasure_pipeline {guard : abstract_guard_impl}
 
 Import EGlobalEnv EWellformed.
 
-Program Definition erasure_pipeline_fast {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) econf :=
-  (* a bunch of nonsense for normalization preconditions *)
-  let K ty (T : ty -> _) p
-    := let p := T p in
-       (PCUICTyping.wf_ext p -> PCUICSN.NormalizationIn p) /\
-         (PCUICTyping.wf_ext p -> PCUICWeakeningEnvSN.normalizationInAdjustUniversesIn p) in
-  let T1 (p:global_env_ext_map) := p in
-  let T2 (p:global_env_ext_map) := T1 (build_global_env_map (PCUICExpandLets.trans_global_env p.1), p.2) in
-  let T3 (p:global_env) := T2 (TemplateToPCUIC.trans_global_env p, Monomorphic_ctx) in
-  let T4 (p:GlobalEnvMap.t) := T3 (eta_expand_global_env p) in
-  build_template_program_env (K _ T4) ▷
-  eta_expand (K _ T3) ▷
-  template_to_pcuic_transform (K _ T2) ▷
-  pcuic_expand_lets_transform (K _ T1) ▷
-  erase_transform ▷
-  guarded_to_unguarded_fix (wcon := eq_refl) eq_refl ▷
-  remove_params_fast_optimization (wcon := eq_refl)  ▷
-  rebuild_wf_env_transform (efl := ERemoveParams.switch_no_params EWellformed.all_env_flags) true false ▷
-  remove_match_on_box_trans (efl := ERemoveParams.switch_no_params EWellformed.all_env_flags) (wcon := eq_refl) (hastrel := eq_refl) (hastbox := eq_refl) ▷
-  rebuild_wf_env_transform (efl := ERemoveParams.switch_no_params EWellformed.all_env_flags) true false ▷
-  inline_projections_optimization (fl := EWcbvEval.target_wcbv_flags) (wcon := eq_refl) (hastrel := eq_refl) (hastbox := eq_refl) ▷
-  let efl := EInlineProjections.disable_projections_env_flag (ERemoveParams.switch_no_params EWellformed.all_env_flags) in
-  rebuild_wf_env_transform (efl :=  efl) true false ▷
-  constructors_as_blocks_transformation (efl := efl) (has_app := eq_refl) (has_pars := eq_refl) (has_rel := eq_refl) (has_box := eq_refl) (has_cstrblocks := eq_refl) ▷
-  optional_unsafe_transforms econf.
-Next Obligation.
-  destruct H; split => //. now eapply ETransform.expanded_eprogram_env_expanded_eprogram_cstrs.
-Qed.
-Next Obligation.
-  cbn in H. split; cbn; intuition eauto.
-Qed.
-Next Obligation.
-  cbn in H. split; cbn; intuition eauto.
-Qed.
-Next Obligation.
-  cbn in H. split; cbn; intuition eauto.
-Qed.
-Next Obligation.
-  cbn in H. split; cbn; intuition eauto.
-Qed.
-Next Obligation.
-  cbn in H. split; cbn; intuition eauto.
-Qed.
-Next Obligation.
-  cbn in H. unfold optional_unsafe_transforms.
-  cbn.
-  destruct enable_unsafe as [[] ? ? ? ?]=> //.
-Qed.
-Next Obligation.
-  cbn in H. split; cbn; intuition eauto.
-Qed.
-
-Definition run_erase_program_fast {guard : abstract_guard_impl} (econf : erasure_configuration) :=
-  run (erasure_pipeline_fast econf).
-
 Local Open Scope string_scope.
 
 Axiom fake_guard_impl_properties :
@@ -447,6 +1086,8 @@ Global Existing Instance fake_normalization.
   the environment is wellformed and the term well-typed (e.g. when it comes directly from a
   Coq definition). *)
 
+Axiom assume_that_we_only_erase_on_wellformed_inductive_mappings : forall {cf : checker_flags},
+  forall (p : Ast.Env.program) (m : inductives_mapping), wf_template_inductives_mapping p.1 m.
 
 Axiom assume_that_we_only_erase_on_welltyped_programs : forall {cf : checker_flags},
   forall (p : Ast.Env.program), squash (TemplateProgram.wt_template_program p).
@@ -454,19 +1095,19 @@ Axiom assume_that_we_only_erase_on_welltyped_programs : forall {cf : checker_fla
 (* This also optionally runs the cofix to fix translation *)
 Program Definition run_erase_program {guard : abstract_guard_impl} econf :=
   if econf.(enable_typed_erasure) then run (typed_erasure_pipeline econf)
-  else if econf.(enable_fast_remove_params) then
-    run (erasure_pipeline_fast econf)
-  else run (erasure_pipeline ▷ (optional_unsafe_transforms econf)).
+  else run (erasure_pipeline_mapping ▷ (optional_unsafe_transforms econf)).
 Next Obligation.
 Proof.
   unfold optional_unsafe_transforms; cbn.
   destruct enable_unsafe as [[] ? ? ? ?]=> //.
 Qed.
 
-Program Definition erase_and_print_template_program econf (p : Ast.Env.program) : string :=
-  let p' := run_erase_program econf p _ in
+Program Definition erase_and_print_template_program econf (m : inductives_mapping) (p : Ast.Env.program) : string :=
+  let p' := run_erase_program econf (m, p) _ in
   time "Pretty printing" EPretty.print_program p'.
 Next Obligation.
+  split.
+  now eapply assume_that_we_only_erase_on_wellformed_inductive_mappings.
   split.
   now eapply assume_that_we_only_erase_on_welltyped_programs.
   cbv [PCUICWeakeningEnvSN.normalizationInAdjustUniversesIn].
@@ -474,26 +1115,13 @@ Next Obligation.
   split; typeclasses eauto.
 Qed.
 
-Definition erasure_fast_config :=
-  {| enable_unsafe := no_unsafe_passes;
-     dearging_config := default_dearging_config;
-     enable_typed_erasure := false;
-     enable_fast_remove_params := true;
-     inductives_mapping := [];
-     inlined_constants := KernameSet.empty |}.
-
-Program Definition erase_fast_and_print_template_program (p : Ast.Env.program) : string :=
-  erase_and_print_template_program erasure_fast_config p.
-
 Definition typed_erasure_config :=
   {| enable_unsafe := no_unsafe_passes;
       dearging_config := default_dearging_config;
       enable_typed_erasure := true;
-      enable_fast_remove_params := true;
-      inductives_mapping := [];
       inlined_constants := KernameSet.empty |}.
 
-(* Parameterized by a configuration for dearging, allowing to, e.g., override masks. *)
+(* TODO: Parameterize by a configuration for dearging, allowing to, e.g., override masks. *)
 Program Definition typed_erase_and_print_template_program (p : Ast.Env.program)
   : string :=
-  erase_and_print_template_program typed_erasure_config p.
+  erase_and_print_template_program typed_erasure_config [] p.
diff --git a/erasure-plugin/theories/ErasureCorrectness.v b/erasure-plugin/theories/ErasureCorrectness.v
index d5a51f67b..77fb2d0e8 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 _ _ _ (t0 := lambdabox_pres_app) (Σ', v'') prev H0).
+    epose proof (ETransformPresAppLam.transform_lam _ _ _ (t := 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 _ _ _ (t0 := lambdabox_pres_app) (Σ', v'') prev H0).
+    epose proof (ETransformPresAppLam.transform_lam _ _ _ (t := lambdabox_pres_app) (Σ', v'') prev H0).
     rewrite -obseq. exact H2. cbn. red; tauto.
   Qed.
 
diff --git a/erasure/theories/EAstUtils.v b/erasure/theories/EAstUtils.v
index 2058db50c..24e3beeef 100644
--- a/erasure/theories/EAstUtils.v
+++ b/erasure/theories/EAstUtils.v
@@ -318,9 +318,16 @@ Definition is_box c :=
   | _ => false
   end.
 
+Definition isLazy c :=
+  match c with
+  | tLazy _ => true
+  | _ => false
+  end.
+
 Definition isFixApp t := isFix (head t).
 Definition isConstructApp t := isConstruct (head t).
 Definition isPrimApp t := isPrim (head t).
+Definition isLazyApp t := isLazy (head t).
 
 Lemma isFixApp_mkApps f l : isFixApp (mkApps f l) = isFixApp f.
 Proof. rewrite /isFixApp head_mkApps //. Qed.
@@ -328,6 +335,8 @@ Lemma isConstructApp_mkApps f l : isConstructApp (mkApps f l) = isConstructApp f
 Proof. rewrite /isConstructApp head_mkApps //. Qed.
 Lemma isPrimApp_mkApps f l : isPrimApp (mkApps f l) = isPrimApp f.
 Proof. rewrite /isPrimApp head_mkApps //. Qed.
+Lemma isLazyApp_mkApps f l : isLazyApp (mkApps f l) = isLazyApp f.
+Proof. rewrite /isLazyApp head_mkApps //. Qed.
 
 Lemma is_box_mkApps f a : is_box (mkApps f a) = is_box f.
 Proof.
@@ -347,6 +356,8 @@ Lemma nisBox_mkApps f args : ~~ isBox f -> ~~ isBox (mkApps f args).
 Proof. destruct args using rev_case => //. rewrite mkApps_app /= //. Qed.
 Lemma nisPrim_mkApps f args : ~~ isPrim f -> ~~ isPrim (mkApps f args).
 Proof. destruct args using rev_case => //. rewrite mkApps_app /= //. Qed.
+Lemma nisLazy_mkApps f args : ~~ isLazy f -> ~~ isLazy (mkApps f args).
+Proof. destruct args using rev_case => //. rewrite mkApps_app /= //. Qed.
 
 Definition string_of_def {A : Set} (f : A -> string) (def : def A) :=
   "(" ^ string_of_name (dname def) ^ "," ^ f (dbody def) ^ ","
diff --git a/erasure/theories/ECoInductiveToInductive.v b/erasure/theories/ECoInductiveToInductive.v
index b75cb8b5a..602321dcb 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, ?length_map;
+    rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?map_length;
     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, ?length_map;
+    rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?map_length;
     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 length_map.
+    rewrite map_length.
     generalize #|mfix|.
     induction n; simpl; auto.
     f_equal; auto.
@@ -383,6 +383,7 @@ Proof.
       unfold lookup_inductive in hl.
       destruct lookup_minductive => //. }
   - rewrite !GlobalContextMap.lookup_inductive_kind_spec.
+    move: H2; rewrite /wf_brs.
     destruct lookup_inductive as [[mdecl idecl]|] eqn:hl => //.
     assert (map (on_snd (trans Σ)) l = map (on_snd (trans Σ')) l) as -> by solve_all.
     rewrite (extends_lookup_inductive_kind H0 H1) //.
@@ -510,7 +511,7 @@ Proof.
   rewrite /iota_red.
   eapply ECSubst.closed_substl => //.
   now rewrite forallb_rev forallb_skipn.
-  now rewrite List.length_rev hskip Nat.add_0_r.
+  now rewrite List.rev_length hskip Nat.add_0_r.
 Qed.
 
 Lemma isFix_mkApps t l : isFix (mkApps t l) = isFix t && match l with [] => true | _ => false end.
@@ -645,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 !length_skipn length_map //)].
+        try (cbn; rewrite -H4 !skipn_length map_length //)].
     eapply eval_iota_block.
     1,3,4: eauto.
     + now rewrite -is_propositional_cstr_trans.
@@ -695,7 +696,7 @@ Qed.
     rewrite closedn_mkApps in ev1.
     move: ev1 => /andP [] clfix clargs.
     eapply EWcbvEval.eval_fix; eauto.
-    rewrite length_map.
+    rewrite map_length.
     eapply trans_cunfold_fix; tea.
     eapply closed_fix_subst. tea.
     rewrite trans_mkApps in IHev3. apply IHev3.
@@ -712,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 length_map.
+    now rewrite map_length.
 
   - move/andP => [] clf cla.
     eapply eval_closed in ev1 => //.
@@ -1013,7 +1014,7 @@ Proof.
     destruct lookup_env eqn:hl => // /=; intros; rtoProp; eauto.
     destruct g eqn:hg => /= //; intros; rtoProp; eauto.
     repeat split; eauto. destruct cstr_as_blocks; rtoProp; repeat split; len; eauto. 1: solve_all.
-  - rewrite lookup_env_trans //.
+  - rewrite /wf_brs; cbn; rewrite lookup_env_trans //.
     destruct lookup_env eqn:hl => // /=.
     destruct g eqn:hg => /= //. subst g.
     destruct nth_error => /= //.
diff --git a/erasure/theories/EConstructorsAsBlocks.v b/erasure/theories/EConstructorsAsBlocks.v
index a7a0aedd5..a83352c57 100644
--- a/erasure/theories/EConstructorsAsBlocks.v
+++ b/erasure/theories/EConstructorsAsBlocks.v
@@ -649,6 +649,28 @@ Proof.
     eapply IHt1. cbn in Hwf'. rtoProp. intuition.
 Qed.
 
+Lemma transform_blocks_isLazyApp {efl : EEnvFlags} {Σ : GlobalContextMap.t} t :
+  has_cstr_params = false ->
+  wf_glob Σ -> wellformed Σ 0 t ->
+  isLazyApp (transform_blocks Σ t) = isLazyApp t.
+Proof.
+  intros haspars Hwf Hwf'.
+  induction t; try now cbn; eauto.
+  eapply transform_blocks_tApp; eauto.
+  destruct decompose_app.
+  destruct construct_viewc.
+  - rewrite GlobalContextMap.lookup_constructor_pars_args_spec.
+    destruct lookup_constructor_pars_args as [ [[]] | ]; eauto.
+    cbn. destruct chop. intros (? & ? & ?). subst.
+    rewrite -[tApp _ _](mkApps_app _ _ [t2]).
+    rewrite !isLazyApp_mkApps. cbn. reflexivity.
+  - change (tApp t1 t2) with (mkApps t1 [t2]).
+    change (tApp (transform_blocks Σ t1) (transform_blocks Σ t2)) with
+    (mkApps (transform_blocks Σ t1) [transform_blocks Σ t2]).
+    rewrite !isLazyApp_mkApps.
+    eapply IHt1. cbn in Hwf'. rtoProp. intuition.
+Qed.
+
 Lemma lookup_env_transform_blocks {Σ : GlobalContextMap.t} kn :
   lookup_env (transform_blocks_env Σ) kn =
   option_map (transform_blocks_decl Σ) (lookup_env Σ kn).
@@ -716,7 +738,7 @@ Proof.
     rewrite /lookup_constructor_pars_args in H3.
     destruct lookup_constructor as [[[] ?]|]=> //. cbn in H3.
     eapply Nat.leb_le in H3. intuition auto. apply/eqb_spec. lia.
-  - now rewrite lookup_inductive_transform_blocks.
+  - len. move: H2. rewrite /wf_brs. now rewrite lookup_inductive_transform_blocks.
   - now rewrite lookup_constructor_transform_blocks.
   - unfold wf_fix in *. rtoProp. solve_all. solve_all. now eapply isLambda_transform_blocks.
   - unfold wf_fix in *. rtoProp. solve_all.
@@ -1126,17 +1148,20 @@ Proof.
       * rewrite GlobalContextMap.lookup_constructor_pars_args_spec;
           destruct lookup_constructor_pars_args as [ [[]] | ] eqn:hpa; eauto.
         cbn [plus]. destruct chop eqn:heqch.
-        intros [hl [ht ha]]. rewrite ht in H1. rewrite isConstructApp_mkApps isPrimApp_mkApps orb_true_r in H1 => //.
+        intros [hl [ht ha]]. rewrite ht in H1. rewrite isConstructApp_mkApps
+          isPrimApp_mkApps isLazyApp_mkApps orb_true_r in H1 => //.
       * eapply eval_app_cong; eauto.
         revert H1.
         destruct f'; try now cbn; tauto.
         intros H. cbn in H.
         rewrite transform_blocks_isConstructApp; eauto.
         rewrite transform_blocks_isPrimApp; eauto.
-        rewrite negb_or in H. move/andP: H => [] ncstr nprim.
+        rewrite transform_blocks_isLazyApp; eauto.
+        rewrite !negb_or in H. move/andP: H => [] /andP [] ncstr nprim nlazy.
         destruct (isConstructApp (tApp f'1 f'2)) eqn:heq'.
         -- cbn in ncstr. congruence.
-        -- eapply transform_blocks_tApp; eauto. clear -nprim.
+        -- eapply transform_blocks_tApp; eauto. clear -nprim nlazy.
+          move/negbTE: nlazy ->. move/negbTE: nprim -> => /=.
            destruct decompose_app.
            destruct construct_viewc; try now cbn; eauto.
            rewrite GlobalContextMap.lookup_constructor_pars_args_spec;
@@ -1187,6 +1212,11 @@ Proof.
     eapply All2_over_undep in a. eapply All2_Set_All2 in ev. eapply All2_All2_Set. solve_all.
     now destruct b.
     now destruct a0.
+  - intros evl evt' [evt wft wflt etat etalt].
+    intros [evt'' wft' wfv etat' etav].
+    simp transform_blocks; rewrite -!transform_blocks_equation_1.
+    econstructor; eauto.
+    now simp transform_blocks in evt; rewrite -!transform_blocks_equation_1 in evt.
   - intros. destruct t; try solve [constructor; cbn in H, H0 |- *; try congruence].
     cbn -[lookup_constructor] in H |- *. destruct args => //.
     destruct lookup_constructor eqn:hl => //.
diff --git a/erasure/theories/EDeps.v b/erasure/theories/EDeps.v
index 9f6c273d8..28dfbbd49 100644
--- a/erasure/theories/EDeps.v
+++ b/erasure/theories/EDeps.v
@@ -61,9 +61,10 @@ Proof.
   - depelim er.
     econstructor; eauto.
   - depelim er.
-    econstructor; eauto.
+    econstructor; eauto. now len.
+    clear H3.
     induction X; [easy|].
-    depelim H3.
+    depelim H4.
     constructor; [|easy].
     now cbn.
   - depelim er.
@@ -115,9 +116,9 @@ Proof.
   - depelim er.
     econstructor; eauto.
   - depelim er.
-    econstructor; eauto.
+    econstructor; eauto. now len. clear H3.
     induction X; [easy|].
-    depelim H3.
+    depelim H4.
     constructor; [|easy].
     now cbn.
   - depelim er.
@@ -175,9 +176,10 @@ Proof.
   - depelim er.
     cbn. econstructor; eauto.
   - depelim er.
-    econstructor; [easy|easy|easy|easy|easy|].
+    econstructor; [easy|easy|easy|easy|easy| | ].
+    now len. clear H3.
     induction X; [easy|].
-    depelim H3.
+    depelim H4.
     constructor; [|easy].
     now cbn.
   - depelim er.
@@ -290,14 +292,14 @@ Proof.
     unfold EGlobalEnv.iota_red.
     apply erases_deps_substl.
     + intuition auto.
-      apply erases_deps_mkApps_inv in H4.
+      apply erases_deps_mkApps_inv in H5.
       now apply Forall_rev, Forall_skipn.
     + eapply nth_error_forall in e2; [|now eauto].
       assumption.
   - congruence.
   - depelim er.
     subst brs; cbn in *.
-    depelim H3.
+    depelim H4.
     cbn in *.
     apply IHev2.
     apply erases_deps_substl; [|easy].
@@ -325,9 +327,9 @@ Proof.
   - depelim er.
     specialize (IHev1 er).
     apply erases_deps_mkApps_inv in IHev1 as (? & ?).
-    depelim H4.
+    depelim H5.
     apply IHev2.
-    econstructor; [easy|easy|easy|easy| |easy].
+    econstructor; [easy|easy|easy|easy| |easy|easy ].
     apply erases_deps_mkApps; [|easy].
     now eapply erases_deps_cunfold_cofix; eauto.
   - depelim er.
@@ -354,6 +356,7 @@ Proof.
   - depelim er; depelim X; constructor; eauto.
     eapply All2_over_undep in a0. solve_all.
   - easy.
+  - easy.
 Qed.
 
 #[global]
@@ -397,6 +400,7 @@ Lemma erases_deps_forall_ind Σ Σ'
         erases_one_inductive_body idecl idecl' ->
         erases_deps Σ Σ' discr ->
         P discr ->
+        #|idecl'.(ind_ctors)| = #|brs| ->
         Forall (fun br : _ × Extract.E.term => erases_deps Σ Σ' br.2) brs ->
         Forall (fun br => P br.2) brs ->
         P (Extract.E.tCase p discr brs))
@@ -437,7 +441,7 @@ Proof.
   - eauto.
   - eapply Hcase; try eassumption.
     + now apply f.
-    + revert brs H3.
+    + clear H3; revert brs H4.
       fix f' 2.
       intros brs []; [now constructor|].
       constructor; [now apply f|now apply f'].
@@ -622,6 +626,14 @@ Proof.
   repeat eapply conj; try eassumption. cbn in *. now rewrite H8, H9.
 Qed.
 
+Lemma Forall2_nth_error_left {A B} {P} {l : list A} {l' : list B} : Forall2 P l l' ->
+  forall n x, nth_error l n = Some x ->
+  exists x', nth_error l' n = Some x' /\ P x x'.
+Proof.
+  induction 1; destruct n; simpl; auto; try discriminate.
+  intros x' [= ->]. eexists; eauto.
+Qed.
+
 Lemma erases_deps_single Σ Σ' Γ t T et :
   wf_ext Σ ->
   Σ;;; Γ |- t : T ->
@@ -653,6 +665,11 @@ Proof.
     econstructor; eauto.
     destruct H2. destruct x1; eauto. destruct H1.
     eapply Forall2_All2 in H2. eapply All2_nth_error in H2; eauto.
+    { eapply Forall2_length in H0. eapply All2i_length in brs_ty.
+      eapply All2_length in X. rewrite <- H0.
+      depelim H2. destruct H1 as [].
+      destruct x1 as []. eapply Forall2_nth_error_left in H2 as [x' []]; tea.
+      rewrite H4 in H2; noconf H2. depelim H7. eapply Forall2_length in H2. lia. }
     clear -wf brs_ty X H0 Σer.
     subst predctx ptm.
     clear X.
@@ -711,14 +728,6 @@ Proof.
     depelim H0; depelim p1; depelim X; cbn in *; try constructor; cbn; intuition eauto. solve_all.
 Qed.
 
-Lemma Forall2_nth_error_left {A B} {P} {l : list A} {l' : list B} : Forall2 P l l' ->
-  forall n x, nth_error l n = Some x ->
-  exists x', nth_error l' n = Some x' /\ P x x'.
-Proof.
-  induction 1; destruct n; simpl; auto; try discriminate.
-  intros x' [= ->]. eexists; eauto.
-Qed.
-
 Lemma erases_global_all_deps Σ Σ' :
   wf Σ ->
   erases_global Σ Σ' ->
diff --git a/erasure/theories/EEtaExpandedFix.v b/erasure/theories/EEtaExpandedFix.v
index 6245e36e6..aeebbb004 100644
--- a/erasure/theories/EEtaExpandedFix.v
+++ b/erasure/theories/EEtaExpandedFix.v
@@ -1058,7 +1058,7 @@ Lemma eval_etaexp {fl : WcbvFlags} {efl : EEnvFlags} {wcon : with_constructor_as
 Proof.
   intros etaΣ wfΣ.
   induction 1 as [ | ? ? ? ? ? ? ? ? IHs | | | | | ? ? ? ? ? ? ? ? ? ? ? IHs | ? ? ? ? ? ? ? ? ? ? ? IHs
-    | ? ? ? ? ? ? ? ? ? ? IHs | | | | | | | | | | | ] using eval_mkApps_rect; try now congruence.
+    | ? ? ? ? ? ? ? ? ? ? IHs | | | | | | | | | | | | ] using eval_mkApps_rect; try now congruence.
   all:try simp isEtaExp; rewrite -?isEtaExp_equation_1 => //.
   6:{
     move/isEtaExp_tApp'.
@@ -1377,6 +1377,7 @@ Proof.
   - solve_all.
     depelim X; solve_all. eapply All2_over_undep in a. subst a0 a';
       depelim H; constructor; solve_all. solve_all.
+  - simp_eta in IHeval1. eauto.
 Qed.
 
 Lemma isEtaExp_fixapp_mon {mfix idx n n'} : n <= n' -> isEtaExp_fixapp mfix idx n -> isEtaExp_fixapp mfix idx n'.
@@ -1963,6 +1964,8 @@ Proof.
   - intros hexp. simp_eta in hexp. depelim X; repeat constructor; eauto.
     eapply All2_over_undep in a. subst a0 a'. solve_all. depelim hexp; cbn in *. destruct p.
     eapply All2_All2_Set. solve_all. solve_all. depelim hexp. destruct p. solve_all.
+  - intros hexp. simp_eta in hexp. econstructor; eauto. apply IHeval2.
+    specialize (IHeval1 hexp). eapply eval_etaexp in IHeval1. now simp_eta in IHeval1. all:eauto.
   - intros hexp. now eapply eval_atom.
     Unshelve. all: eauto.
 Qed.
diff --git a/erasure/theories/EGenericGlobalMap.v b/erasure/theories/EGenericGlobalMap.v
index 797eedcf3..d209122f9 100644
--- a/erasure/theories/EGenericGlobalMap.v
+++ b/erasure/theories/EGenericGlobalMap.v
@@ -324,7 +324,7 @@ Proof.
     destruct g eqn:hg => /= //; intros; rtoProp; eauto.
     rewrite gen_transform_inductive_decl_id.
     repeat split; eauto. destruct cstr_as_blocks; rtoProp; repeat split; eauto. solve_all.
-  - rewrite lookup_env_gen_transform //.
+  - rewrite /wf_brs. cbn. rewrite lookup_env_gen_transform //.
     destruct lookup_env eqn:hl => // /=.
     destruct g eqn:hg => /= //. subst g.
     rewrite gen_transform_inductive_decl_id.
diff --git a/erasure/theories/EGenericMapEnv.v b/erasure/theories/EGenericMapEnv.v
index c5a0b4853..1fa0d2bed 100644
--- a/erasure/theories/EGenericMapEnv.v
+++ b/erasure/theories/EGenericMapEnv.v
@@ -279,7 +279,7 @@ Proof.
     destruct lookup_env eqn:hl => // /=; intros; rtoProp; eauto.
     destruct g eqn:hg => /= //; intros; rtoProp; eauto.
     repeat split; eauto. destruct cstr_as_blocks; rtoProp; repeat split; eauto. solve_all.
-  - rewrite lookup_env_gen_transform //.
+  - rewrite /wf_brs; cbn. rewrite lookup_env_gen_transform //.
     destruct lookup_env eqn:hl => // /=.
     destruct g eqn:hg => /= //. subst g.
     destruct nth_error => /= //.
diff --git a/erasure/theories/EImplementBox.v b/erasure/theories/EImplementBox.v
index e6cb5ef84..f49a16a8e 100644
--- a/erasure/theories/EImplementBox.v
+++ b/erasure/theories/EImplementBox.v
@@ -388,6 +388,15 @@ Proof.
   rewrite (isPrimApp_mkApps _ [_]). eauto.
 Qed.
 
+Lemma implement_box_isLazyApp {efl : EEnvFlags} {Σ : global_declarations} t :
+  isLazyApp (implement_box t) = isLazyApp t.
+Proof.
+  induction t; try now cbn; eauto.
+  simp implement_box.
+  rewrite (isLazyApp_mkApps _ [t2]).
+  rewrite (isLazyApp_mkApps _ [_]). eauto.
+Qed.
+
 Lemma lookup_env_implement_box {Σ : global_declarations} kn :
   lookup_env (implement_box_env Σ) kn =
   option_map (implement_box_decl) (lookup_env Σ kn).
@@ -472,7 +481,8 @@ Proof.
     all: destruct cstr_as_blocks; rtoProp; try split; eauto.
     + solve_all.
     + destruct block_args; cbn in *; eauto.
-  - rewrite lookup_inductive_implement_box. intuition auto. solve_all.
+  - rewrite /wf_brs; cbn -[lookup_inductive implement_box].
+    rewrite lookup_inductive_implement_box. intuition auto. solve_all. solve_all.
     replace (#|x.1| + S m) with ((#|x.1| + m) + 1) by lia.
     eapply wellformed_lift. eauto.
   - rewrite lookup_constructor_implement_box. intuition auto.
@@ -670,6 +680,7 @@ Proof.
     intros H. cbn in H.
     rewrite implement_box_isConstructApp; eauto.
     rewrite implement_box_isPrimApp; eauto.
+    rewrite implement_box_isLazyApp; eauto.
   - intros; repeat match goal with [H : MCProd.and3 _ _ _ |- _] => destruct H end.
     simp implement_box in *.
     eapply eval_construct_block; tea. eauto.
@@ -680,6 +691,9 @@ Proof.
   - intros wf H; depelim H; simp implement_box; repeat constructor.
     destruct a0. eapply All2_over_undep in a. eapply All2_All2_Set, All2_map.
     cbn -[implement_box]. solve_all. now destruct H. now destruct a0.
+  - intros evt evt' [] [].
+    simp implement_box. simp implement_box in e.
+    econstructor; eauto.
   - intros. destruct t; try solve [constructor; cbn in H, H0 |- *; try congruence].
     cbn -[lookup_constructor] in H |- *. destruct args => //.
 Qed.
diff --git a/erasure/theories/EInlineProjections.v b/erasure/theories/EInlineProjections.v
index 2108bcd84..8be042bea 100644
--- a/erasure/theories/EInlineProjections.v
+++ b/erasure/theories/EInlineProjections.v
@@ -74,7 +74,7 @@ Qed.
 Lemma wellformed_projection_args {efl : EEnvFlags} {Σ p mdecl idecl cdecl pdecl} :
   wf_glob Σ ->
   lookup_projection Σ p = Some (mdecl, idecl, cdecl, pdecl) ->
-  p.(proj_arg) < cdecl.(cstr_nargs).
+  #|idecl.(ind_ctors)| = 1 /\ p.(proj_arg) < cdecl.(cstr_nargs).
 Proof.
   intros wfΣ.
   rewrite /lookup_projection /lookup_constructor /lookup_inductive.
@@ -161,10 +161,10 @@ Section optimize.
     - rewrite GlobalContextMap.lookup_projection_spec.
       destruct lookup_projection as [[[[mdecl idecl] cdecl] pdecl]|] eqn:hl; auto => //.
       simpl.
-      have arglen := wellformed_projection_args wfΣ hl.
+      have [ncstrs arglen] := wellformed_projection_args wfΣ hl.
       apply lookup_projection_lookup_constructor, lookup_constructor_lookup_inductive in hl.
-      rewrite hl /= andb_true_r.
-      rewrite IHt //=; len. apply Nat.ltb_lt.
+      rewrite /wf_brs hl /= andb_true_r.
+      rewrite IHt //=; len. rewrite ncstrs. apply Nat.ltb_lt.
       lia.
     - len. rtoProp; solve_all. solve_all.
       now eapply isLambda_optimize. solve_all.
@@ -710,13 +710,14 @@ Proof.
     * destruct with_guarded_fix.
       + move: i.
         rewrite !negb_or.
-        rewrite optimize_mkApps !isFixApp_mkApps !isConstructApp_mkApps !isPrimApp_mkApps.
+        rewrite optimize_mkApps !isFixApp_mkApps !isConstructApp_mkApps !isPrimApp_mkApps
+          !isLazyApp_mkApps.
         destruct args using rev_case => // /=. rewrite map_app !mkApps_app /= //.
         rewrite !andb_true_r.
         rtoProp; intuition auto;  destruct v => /= //.
       + move: i.
         rewrite !negb_or.
-        rewrite optimize_mkApps !isConstructApp_mkApps !isPrimApp_mkApps.
+        rewrite optimize_mkApps !isConstructApp_mkApps !isPrimApp_mkApps !isLazyApp_mkApps.
         destruct args using rev_case => // /=. rewrite map_app !mkApps_app /= //.
         destruct v => /= //.
   - intros; rtoProp; intuition eauto.
@@ -725,6 +726,8 @@ Proof.
     eapply All2_Set_All2 in ev. eapply All2_All2_Set. primProp.
     subst a0 a'; cbn in *. depelim H0; cbn in *. intuition auto; solve_all.
     primProp; depelim H0; intuition eauto.
+  - intros wf; econstructor; eauto. eapply IHev2.
+    eapply eval_wellformed in ev1; tea => //.
   - destruct t => //.
     all:constructor; eauto.
     cbn [atom optimize] in i |- *.
@@ -792,9 +795,11 @@ Proof.
     rewrite GlobalContextMap.lookup_projection_spec.
     destruct lookup_projection as [[[[mdecl idecl] cdecl] pdecl]|] eqn:hl'; auto => //.
     simpl.
+    rewrite /wf_brs.
     rewrite (lookup_constructor_lookup_inductive (lookup_projection_lookup_constructor hl')) /=.
     rewrite hrel IHt //= andb_true_r.
-    have hargs' := wellformed_projection_args wfΣ hl'.
+    have [-> hargs'] := wellformed_projection_args wfΣ hl'.
+    rtoProp; intuition auto.
     apply Nat.ltb_lt. len.
   - cbn. unfold wf_fix; rtoProp; intuition auto; solve_all. now eapply isLambda_optimize.
   - cbn. unfold wf_fix; rtoProp; intuition auto; solve_all.
@@ -820,7 +825,7 @@ Proof.
     destruct lookup_env eqn:hl => // /=; intros; rtoProp; eauto.
     destruct g eqn:hg => /= //; intros; rtoProp; eauto.
     repeat split; eauto. destruct cstr_as_blocks; rtoProp; repeat split; eauto. solve_all.
-  - rewrite lookup_env_optimize //.
+  - rewrite /wf_brs; cbn; rewrite lookup_env_optimize //.
     destruct lookup_env eqn:hl => // /=.
     destruct g eqn:hg => /= //. subst g.
     destruct nth_error => /= //.
diff --git a/erasure/theories/EOptimizePropDiscr.v b/erasure/theories/EOptimizePropDiscr.v
index 87d73c4a9..96758cceb 100644
--- a/erasure/theories/EOptimizePropDiscr.v
+++ b/erasure/theories/EOptimizePropDiscr.v
@@ -378,7 +378,9 @@ Proof.
   - destruct cstr_as_blocks; rtoProp; eauto. f_equal. solve_all. destruct args; inv H2. reflexivity.
   - rewrite !GlobalContextMap.inductive_isprop_and_pars_spec.
     assert (map (on_snd (remove_match_on_box Σ)) l = map (on_snd (remove_match_on_box Σ')) l) as -> by solve_all.
-    rewrite (extends_inductive_isprop_and_pars H0 H1 H2).
+    assert (iss : isSome (lookup_inductive Σ p.1)).
+    { move: H2; rewrite /wf_brs; destruct lookup_inductive => //. }
+    rewrite (extends_inductive_isprop_and_pars H0 H1 iss).
     destruct inductive_isprop_and_pars as [[[]]|].
     destruct map => //. f_equal; eauto.
     destruct l0 => //. destruct p0 => //. f_equal; eauto.
@@ -602,7 +604,7 @@ Proof.
     rewrite closedn_mkApps in ev1.
     move: ev1 => /andP [] clfix clargs.
     eapply EWcbvEval.eval_fix; eauto.
-    rewrite length_map.
+    rewrite map_length.
     eapply remove_match_on_box_cunfold_fix; tea.
     eapply closed_fix_subst. tea.
     rewrite remove_match_on_box_mkApps in IHev3. apply IHev3.
@@ -715,22 +717,24 @@ Proof.
     * destruct with_guarded_fix.
       + move: i.
         rewrite !negb_or.
-        rewrite remove_match_on_box_mkApps !isFixApp_mkApps !isConstructApp_mkApps !isPrimApp_mkApps.
+        rewrite remove_match_on_box_mkApps !isFixApp_mkApps !isConstructApp_mkApps !isPrimApp_mkApps !isLazyApp_mkApps.
         destruct args using rev_case => // /=. rewrite map_app !mkApps_app /= //.
         rewrite !andb_true_r.
         rtoProp; intuition auto.
         destruct v => /= //.
         destruct v => /= //.
         destruct v => /= //.
+        destruct v => /= //.
       + move: i.
         rewrite !negb_or.
-        rewrite remove_match_on_box_mkApps !isConstructApp_mkApps !isPrimApp_mkApps.
+        rewrite remove_match_on_box_mkApps !isConstructApp_mkApps !isPrimApp_mkApps !isLazyApp_mkApps.
         destruct args using rev_case => // /=. rewrite map_app !mkApps_app /= //.
         destruct v => /= //.
   - depelim X; repeat constructor.
     eapply All2_over_undep in a. eapply All2_All2_Set. eapply All2_Set_All2 in ev. subst a0 a'; cbn in *.
     rewrite /test_array_model /= in H. rtoProp; intuition auto; solve_all. eapply e.
     cbn in H. rewrite /test_array_model /= in H. now move/andP: H => [].
+  - intros. econstructor; eauto. eapply IHev2. eapply eval_closed in ev1; tea.
   - destruct t => //.
     all:constructor; eauto. cbn [atom remove_match_on_box] in i |- *.
     rewrite -lookup_constructor_remove_match_on_box //. destruct args => //.
@@ -847,7 +851,7 @@ Proof.
     destruct lookup_env eqn:hl => // /=; intros; rtoProp; eauto.
     destruct g eqn:hg => /= //; intros; rtoProp; eauto.
     repeat split; eauto. destruct cstr_as_blocks; rtoProp; repeat split; len; eauto. 1: solve_all.
-  - rewrite lookup_env_remove_match_on_box //.
+  - rewrite /wf_brs; cbn. rewrite lookup_env_remove_match_on_box //.
     destruct lookup_env eqn:hl => // /=.
     destruct g eqn:hg => /= //. subst g.
     destruct nth_error => /= //.
diff --git a/erasure/theories/EProgram.v b/erasure/theories/EProgram.v
index 925bc9f76..e05c56212 100644
--- a/erasure/theories/EProgram.v
+++ b/erasure/theories/EProgram.v
@@ -18,6 +18,9 @@ Local Obligation Tactic := program_simpl.
 
 Import EGlobalEnv EWellformed.
 
+Definition inductive_mapping : Set := Kernames.inductive * (bytestring.string * list nat).
+Definition inductives_mapping := list inductive_mapping.
+
 Definition eprogram := (EAst.global_context * EAst.term).
 Definition eprogram_env := (EEnvMap.GlobalContextMap.t * EAst.term).
 
diff --git a/erasure/theories/ERemoveParams.v b/erasure/theories/ERemoveParams.v
index 2810058df..bce58d14f 100644
--- a/erasure/theories/ERemoveParams.v
+++ b/erasure/theories/ERemoveParams.v
@@ -780,6 +780,14 @@ Proof.
   all:rewrite !isPrimApp_mkApps //.
 Qed.
 
+Lemma strip_isLazyApp Σ f :
+  isLazyApp f = isLazyApp (strip Σ f).
+Proof.
+  funelim (strip Σ f); cbn -[strip] => //.
+  all:rewrite map_InP_spec.
+  all:rewrite !isLazyApp_mkApps //.
+Qed.
+
 Lemma lookup_inductive_pars_is_prop_and_pars {Σ ind b pars} :
   inductive_isprop_and_pars Σ ind = Some (b, pars) ->
   lookup_inductive_pars Σ (inductive_mind ind) = Some pars.
@@ -1012,8 +1020,8 @@ Proof.
   - rewrite !strip_tApp //.
     eapply eval_app_cong; tea.
     move: H1. eapply contraNN.
-    rewrite -strip_isLambda -strip_isConstructApp -strip_isFixApp -strip_isBox -strip_isPrimApp //.
-    rewrite -strip_isFix //.
+    rewrite -strip_isLambda -strip_isConstructApp -strip_isFixApp -strip_isBox -strip_isPrimApp
+      -strip_isLazyApp // -strip_isFix //.
 
   - rewrite !strip_mkApps // /=.
     rewrite (lookup_constructor_lookup_inductive_pars H).
@@ -1031,6 +1039,8 @@ Proof.
     eapply All2_over_undep in a. eapply All2_Set_All2 in ev. eapply All2_All2_Set. solve_all. now destruct b.
     now destruct a0.
 
+  - simp_strip. simp_strip in e0. econstructor; tea.
+
   - destruct t => //.
     all:constructor; eauto. simp strip.
     cbn [atom strip] in H |- *.
@@ -1085,10 +1095,12 @@ Proof.
     destruct g eqn:hg => /= //. subst g.
     destruct nth_error => //. destruct nth_error => //.
   - cbn -[strip].
+    rtoProp. move: H2. rewrite /wf_brs; cbn -[strip].
     rewrite lookup_env_strip. cbn in H1. destruct lookup_env eqn:hl => // /=.
     destruct g eqn:hg => /= //. subst g.
-    destruct nth_error => //. rtoProp; intuition auto.
-    simp_strip. all:toAll; solve_all.
+    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.
@@ -1132,7 +1144,7 @@ Proof.
     destruct cstr_as_blocks => //; repeat split; eauto.
     destruct nth_error => /= //.
     destruct nth_error => /= //.
-  - rewrite lookup_env_strip //.
+  - rewrite /wf_brs; cbn; rewrite lookup_env_strip //.
     destruct lookup_env eqn:hl => // /=.
     destruct g eqn:hg => /= //. subst g.
     destruct nth_error => /= //.
diff --git a/erasure/theories/EReorderCstrs.v b/erasure/theories/EReorderCstrs.v
index 3e029f23e..71f288ea0 100644
--- a/erasure/theories/EReorderCstrs.v
+++ b/erasure/theories/EReorderCstrs.v
@@ -1,37 +1,81 @@
-From Coq Require Import List String Arith Lia.
+From Coq Require Import List String Arith Lia ssreflect ssrbool Morphisms.
 Import ListNotations.
 From Equations Require Import Equations.
 Set Equations Transparent.
 
 From MetaCoq.PCUIC Require Import PCUICAstUtils.
 From MetaCoq.Utils Require Import MCList bytestring utils monad_utils.
-From MetaCoq.Erasure Require Import EPrimitive EAst ESpineView EEtaExpanded EInduction ERemoveParams Erasure EGlobalEnv.
+From MetaCoq.Erasure Require Import EProgram EPrimitive EAst ESpineView EEtaExpanded EInduction ERemoveParams Erasure EGlobalEnv
+  EAstUtils ELiftSubst EWellformed ECSubst EWcbvEval.
 
 Import Kernames.
 Import MCMonadNotation.
 
-Definition inductive_mapping : Set := Kernames.inductive * (bytestring.string * list nat).
-Definition inductives_mapping := list inductive_mapping.
+Lemma lookup_declared_constructor {Σ id mdecl idecl cdecl} :
+  lookup_constructor Σ id.1 id.2 = Some (mdecl, idecl, cdecl) ->
+  declared_constructor Σ id mdecl idecl cdecl.
+Proof.
+  rewrite /lookup_constructor /declared_constructor.
+  rewrite /declared_inductive /lookup_inductive.
+  rewrite /declared_minductive /lookup_minductive.
+  destruct lookup_env => //=. destruct g => //=.
+  destruct nth_error eqn:hn => //. destruct (nth_error _ id.2) eqn:hn' => //.
+  intros [= <- <- <-]. intuition auto.
+Qed.
 
-Fixpoint lookup_inductive {A} (Σ : list (inductive × A)) (kn : inductive) {struct Σ} : option A :=
+Fixpoint lookup_inductive_assoc {A} (Σ : list (inductive × A)) (kn : inductive) {struct Σ} : option A :=
     match Σ with
     | [] => None
-    | d :: tl => if kn == d.1 then Some d.2 else lookup_inductive tl kn
+    | d :: tl => if kn == d.1 then Some d.2 else lookup_inductive_assoc tl kn
     end.
 
-Section Reorder.
-  Context (Σ : global_declarations).
-  Context (mapping : inductives_mapping).
+Section Tags.
 
-  Definition lookup_constructor_mapping i m :=
-    '(tyna, tags) <- lookup_inductive mapping i ;;
-    List.nth_error tags m.
-
-  Definition lookup_constructor_ordinal i m :=
-    match lookup_constructor_mapping i m with
-    | None => m
-    | Some m' => m'
+  Fixpoint find_tag (l : list nat) (idx : nat) (tag : nat) : option nat :=
+    match l with
+    | [] => None
+    | tag' :: tags => if tag == tag' then Some idx
+      else find_tag tags (S idx) tag
     end.
+  (* e.g. for bool: [ 1 0 ], i.e true (0 in Coq) is mapped to 1 and false (1 in Coq) is mapped to 0 *)
+  Definition new_tag tags tag := find_tag tags 0 tag.
+  Definition old_tag (tags : list nat) tag := nth_error tags tag.
+
+  (*Lemma old_of_new tags oldidx :
+    old_tag tags oldidx >>= new_tag tags = Some oldidx.
+  Proof.
+    rewrite /old_tag /new_tag.
+    destruct nth_error eqn:hnth => //=. 2:admit.
+    revert hnth.
+    rewrite -{2}[oldidx]Nat.add_0_r. generalize 0.
+    induction tags in oldidx, n |- *.
+    - intros n0. now rewrite nth_error_nil.
+    - cbn. intros n0 hnth. case: eqb_spec.
+      intros ->. destruct oldidx => //. (* tags are unique *) admit.
+      intros neq.
+      destruct oldidx.
+      * cbn in hnth. now noconf hnth.
+      * cbn in hnth. rewrite (IHtags oldidx) //. f_equal. lia.
+  Qed.*)
+
+  Lemma new_tag_spec tags newidx oldidx :
+    new_tag tags newidx = Some oldidx ->
+    old_tag tags oldidx = Some newidx.
+  Proof.
+    rewrite /old_tag /new_tag.
+    rewrite -{2}[oldidx]Nat.sub_0_r. generalize 0.
+    induction tags in oldidx |- *.
+    - intros n0. now rewrite nth_error_nil.
+    - cbn. intros n0. case: eqb_spec.
+      * move=> -> [= ->]. now rewrite Nat.sub_diag.
+      * intros neq h. specialize (IHtags _ _ h).
+        case H: (oldidx - n0) => [|n].
+        + cbn. assert (oldidx - S n0 = 0). lia. rewrite H0 in IHtags.
+          destruct tags; cbn in * => //.
+          noconf IHtags. rewrite eqb_refl in h. noconf h. lia.
+        + cbn. destruct oldidx; try lia. rewrite Nat.sub_succ in IHtags.
+          assert (oldidx - n0 = n) by lia. now rewrite H0 in IHtags.
+  Qed.
 
   Definition reorder_list_opt {A} tags (brs : list A) : option (list A) :=
     mapopt (nth_error brs) tags.
@@ -39,8 +83,277 @@ Section Reorder.
   Definition reorder_list {A} tags (l : list A) :=
     option_get l (reorder_list_opt tags l).
 
+  Fixpoint one_to_one_map n l :=
+      match n with
+      | 0 => l == nil
+      | S n =>
+        existsb (fun x => x == n) l && one_to_one_map n (remove Nat.eq_dec n l)
+      end.
+
+  Definition wf_tags (l : list nat) :=
+    forallb (fun n => n <? #|l|) l && one_to_one_map #|l| l.
+
+  Lemma find_tag_None tags n idx :
+    find_tag tags n idx = None ->
+    Forall (fun tag => tag <> idx) tags.
+  Proof.
+    induction tags in n |- *; cbn; auto.
+    case: eqb_spec => [->|neq] // h.
+    specialize (IHtags _ h). constructor; auto.
+  Qed.
+
+  Lemma one_to_one_map_spec l : one_to_one_map #|l| l ->
+    forall i, i < #|l| <-> In i l.
+  Proof.
+    move: (Nat.le_refl #|l|).
+    generalize #|l| at 2 3 4 as n. induction n in l |- *; cbn.
+    - move=> hl _ i; split => //. lia. move: l hl; case => //=; try lia.
+    - move=> hl /andP[] /existsb_exists => [[x [inx xeqn]]] hone i.
+      specialize (IHn (remove Nat.eq_dec n l)).
+      apply eqb_eq in xeqn. subst x.
+      forward IHn.
+      have hlt := remove_length_lt Nat.eq_dec l n inx. lia.
+      specialize (IHn hone).
+      case: (eqb_spec i n) => [->|neq]. intuition auto.
+      split => hi. assert (i < n) by lia.
+      now have := proj1 (IHn _) H => /(in_remove Nat.eq_dec).
+      suff: i < n by lia. apply <- IHn.
+      apply (in_in_remove Nat.eq_dec) => //.
+  Qed.
+
+  Lemma find_tag_wf tags idx :
+    wf_tags tags ->
+    new_tag tags idx = None ->
+    #|tags| <= idx.
+  Proof.
+    rewrite /wf_tags => /andP[] /forallb_All hwf.
+    move => /one_to_one_map_spec hone /find_tag_None /Forall_forall hdiff.
+    case: (Nat.leb_spec #|tags| idx) => // hlt.
+    elim (hdiff idx). apply hone, hlt. reflexivity.
+  Qed.
+
+  Lemma mapopt_spec {A B} (f : A -> option B) (l : list A) :
+    (forall i x, nth_error l i = Some x -> exists x', f x = Some x') ->
+    exists l', mapopt f l = Some l' /\
+    (forall i x, nth_error l i = Some x -> exists x', f x = Some x' /\ nth_error l' i = f x).
+  Proof.
+    induction l; cbn.
+    - intros hf. exists []. split => // i x. rewrite nth_error_nil //.
+    - intros hf. forward IHl.
+      { intros i x hx. apply (hf (S i) x hx). }
+      destruct IHl as [l' [exl' hl']].
+      specialize (hf 0 a eq_refl) as [x' eqx'].
+      destruct (f a) eqn:fa.
+      * noconf eqx'. rewrite exl'.
+        eexists; split => //.
+        intros i x hnth. destruct i; cbn in *. now noconf hnth.
+        now apply hl'.
+      * discriminate.
+  Qed.
+
+  Lemma mapopt_inv_spec {B} (f : nat -> option B) (l : list nat) :
+    (forall i x, nth_error l i = Some x -> exists x', f x = Some x') ->
+    exists l', mapopt f l = Some l' /\ #|l| = #|l'| /\
+    (forall i x, nth_error l' i = Some x -> exists x', nth_error l i = Some x' /\ f x' = Some x).
+  Proof.
+    induction l; cbn.
+    - intros hf. exists []. split => //; split => // i x. rewrite nth_error_nil //.
+    - intros hf. forward IHl.
+      { intros i x hx. apply (hf (S i) x hx). }
+      destruct IHl as [l' [exl' hl']].
+      specialize (hf 0 a eq_refl) as [x' eqx'].
+      rewrite eqx' exl'. eexists; split => //= //. split => //. lia.
+      intros.
+      destruct hl' as [hl hl']. destruct i. cbn in *. noconf H. exists a. now split => //.
+      now apply hl'.
+  Qed.
+
+  (*Lemma mapopt_spec' {B} (f : nat -> option B) (l : list nat) :
+    (forall i x, nth_error l i = Some x -> exists x', f x = Some x') ->
+    exists l', mapopt f l = Some l' /\
+    (forall i x, nth_error l i = Some x -> exists b, f x = Some b /\ nth_error l' x = Some b).
+  Proof.
+    induction l; cbn.
+    - intros hf. exists []. split => // i x. rewrite nth_error_nil //.
+    - intros hf. forward IHl.
+      { intros i x hx. apply (hf (S i) x hx). }
+      destruct IHl as [l' [exl' hl']].
+      pose proof (hf 0 a eq_refl) as [x' eqx'].
+      destruct (f a) eqn:fa => //.
+      noconf eqx'. rewrite exl'.
+      eexists; split => //.
+      intros i x hnth. destruct i; cbn in *. noconf hnth.
+      * exists x'. split => //. destruct a; cbn. congruence.
+        apply hl'.
+      * discriminate.
+  Qed. *)
+
+  Lemma reorder_list_opt_spec {A} (l : list A) (tags : list nat) (htags : wf_tags tags) :
+    #|l| = #|tags| ->
+    exists l', reorder_list_opt tags l = Some l' /\
+    (forall i k, old_tag tags i = Some k -> exists x, nth_error l k = Some x /\ nth_error l' i = nth_error l k).
+  Proof.
+    rewrite /reorder_list_opt.
+    rewrite /wf_tags in htags.
+    intros hlen.
+    move/andP: htags => [] htags _.
+    have optH := mapopt_spec (nth_error l) tags.
+    forward optH.
+    { intros i x hnth. solve_all. eapply All_nth_error in htags; tea. apply Nat.ltb_lt in htags.
+      rewrite -hlen in htags.
+      apply nth_error_Some in htags. destruct (nth_error l x) eqn:hnth'; try congruence. now eexists. }
+    destruct optH as [l' [heq hl']].
+    setoid_rewrite heq. eexists; split => //.
+  Qed.
+
+  Lemma reorder_list_opt_In {A} (l : list A) (tags : list nat) l' :
+    reorder_list_opt tags l = Some l' ->
+    (forall x, In x l' -> In x l).
+  Proof.
+    rewrite /reorder_list_opt.
+    induction tags in l, l' |- *; cbn.
+    - intros [= <-] x [].
+    - destruct nth_error eqn:hnth => //.
+      destruct mapopt eqn:hmap => //.
+      intros [= <-] x [->|].
+      now eapply nth_error_In in hnth.
+      eapply IHtags; tea.
+  Qed.
+
+  (* Lemma reorder_list_spec {A} (tags : list nat) (l : list A) n i :
+    wf_tags tags -> #|l| = #|tags| ->
+    nth_error tags i = Some n ->
+    nth_error (reorder_list tags l) i = nth_error l n.
+  Proof.
+    intros wft hlt hnth.
+    rewrite /reorder_list.
+    now have [l' [-> hnth']] := reorder_list_opt_spec l tags wft hlt.
+  Qed. *)
+
+  (* Definition reorder_list_spec_maps {A} (l : list A) (tags : list nat) :
+    forall l', reorder_list_opt tags l = Some l' ->
+      (forall i k, maps_to tags i k -> nth_error l' k = nth_error l i).
+  Proof.
+    intros l'.
+    induction l; cbn.
+    - destruct l'; cbn.
+      intros [=] i k. now rewrite !nth_error_nil.
+      rewrite /reorder_list_opt /=.
+      destruct tags => //=. now rewrite nth_error_nil.
+    - rewrite /reorder_list_opt. *)
+
+  Definition inj_tags (tags : list nat) :=
+    forall i i' k, nth_error tags i = Some k -> nth_error tags i' = Some k -> i = i'.
+
+  Lemma reorder_list_opt_spec' {A} (l : list A) (tags : list nat) (htags : wf_tags tags) :
+    #|l| = #|tags| ->
+    (* inj_tags tags -> *)
+    exists l', reorder_list_opt tags l = Some l' /\
+    (forall oldidx a, nth_error l' oldidx = Some a ->
+      exists newidx, old_tag tags oldidx = Some newidx /\ nth_error l newidx = Some a).
+  Proof.
+    rewrite /reorder_list_opt.
+    rewrite /wf_tags in htags.
+    move: htags => /andP[] htags hone.
+    intros hlen.
+    have optH := mapopt_inv_spec (nth_error l) tags.
+    forward optH.
+    { intros i x hnth. solve_all. eapply All_nth_error in htags; tea. apply Nat.ltb_lt in htags.
+      rewrite -hlen in htags.
+      apply nth_error_Some in htags. destruct (nth_error l x) eqn:hnth'; try congruence. now eexists. }
+    destruct optH as [l' [heq hl']].
+    setoid_rewrite heq. eexists; split => //.
+    destruct hl' as [hlen' hl'].
+    intros newidx a hnth.
+    specialize (hl' _ _ hnth).
+    destruct hl' as [x' [eqx' hl']]. exists x'. split => //.
+  Qed.
+
+  Lemma reorder_list_spec' {A} (tags : list nat) (l : list A) n i x :
+    wf_tags tags -> #|l| = #|tags| ->
+    nth_error tags i = Some n -> (* tags[0] = 1 *)
+    nth_error l n = Some x -> (* l[1] = info *)
+    nth_error (reorder_list tags l) i = Some x. (* l'[0] = info*)
+  Proof.
+    intros wft hlt hnth hnth'.
+    rewrite /reorder_list.
+    have [l' [-> hnth'']] := reorder_list_opt_spec l tags wft hlt.
+    cbn. specialize (hnth'' _ _ hnth). destruct hnth'' as [? []]. congruence.
+  Qed.
+
+  Lemma reorder_list_spec_inv {A} (tags : list nat) (l : list A) n x :
+    wf_tags tags -> #|l| = #|tags| ->
+    nth_error (reorder_list tags l) n = Some x -> (* n is a new index, i an old one *)
+    exists i, nth_error tags n = Some i /\ nth_error l i = Some x.
+  Proof.
+    intros wft hlt.
+    rewrite /reorder_list.
+    have [l' [eq hnth'']] := reorder_list_opt_spec' l tags wft hlt; rewrite eq /= => hnth.
+    specialize (hnth'' _ _ hnth) as [oldidx []]. exists oldidx; now split.
+  Qed.
+
+
+  Lemma reorder_list_old_tag {A} (tags : list nat) (l : list A) oldidx newidx :
+    wf_tags tags -> #|l| = #|tags| ->
+    old_tag tags newidx = Some oldidx ->
+    nth_error (reorder_list tags l) newidx = nth_error l oldidx.
+  Proof.
+    rewrite /old_tag.
+    intros wft hlen ht.
+    destruct (nth_error l) eqn:hl => //=.
+    eapply (reorder_list_spec' tags l) in ht; tea.
+    move: wft => /andP[] wft hone.
+    solve_all. eapply All_nth_error in wft; tea.
+    apply Nat.ltb_lt in wft. rewrite -hlen in wft. apply nth_error_None in hl. lia.
+  Qed.
+
+(* Lemma reorder_list_old_tag' {A} (tags : list nat) (l : list A) oldidx newidx :
+    wf_tags tags -> #|l| = #|tags| ->
+    old_tag tags oldidx = Some newidx ->
+    nth_error (reorder_list tags l) oldidx = nth_error l newidx.
+  Proof.
+    rewrite /old_tag.
+    intros wft hlen ht.
+    destruct (nth_error l) eqn:hl => //=.
+    eapply (reorder_list_spec' tags l) in ht; tea.
+    move/andP: wft => [] wft hone.
+    unfold wf_tags in wft. solve_all. eapply All_nth_error in wft; tea.
+    apply Nat.ltb_lt in wft. rewrite -hlen in wft. apply nth_error_None in hl. lia.
+  Qed.
+*)
+
+  (* Lemma reorder_list_old_tag_inv {A} (tags : list nat) (l : list A) oldidx newidx :
+    wf_tags tags -> #|l| = #|tags| ->
+    old_tag tags oldidx = Some newidx ->
+    nth_error (reorder_list tags l) newidx = nth_error l oldidx.
+  Proof.
+    rewrite /old_tag.
+    intros wft hlen ht.
+    destruct (nth_error l) eqn:hl => //=.
+    eapply (reorder_list_spec tags l) in ht; tea.
+    unfold wf_tags in wft. solve_all. eapply All_nth_error in wft; tea.
+    apply Nat.ltb_lt in wft. rewrite -hlen in wft. apply nth_error_None in hl. lia.
+  Qed. *)
+
+
+End Tags.
+
+Section Reorder.
+  Context (Σ : global_declarations).
+  Context (mapping : inductives_mapping).
+
+  Definition lookup_constructor_mapping i c :=
+    '(tyna, tags) <- lookup_inductive_assoc mapping i ;;
+    new_tag tags c.
+
+  Definition lookup_constructor_ordinal i c :=
+    match lookup_constructor_mapping i c with
+    | None => c
+    | Some c' => c'
+    end.
+
   Definition reorder_branches (i : inductive) (brs : list (list BasicAst.name × term)) : list (list BasicAst.name × term) :=
-    match lookup_inductive mapping i with
+    match lookup_inductive_assoc mapping i with
     | None => brs
     | Some (tyna, tags) => reorder_list tags brs
     end.
@@ -52,11 +365,11 @@ Section Reorder.
     | tApp fn arg => tApp (reorder fn) (reorder arg)
     | tConst nm => tConst nm
     | tConstruct i m args => tConstruct i (lookup_constructor_ordinal i m) (map reorder args)
-    | tCase i mch brs => tCase i mch (reorder_branches i.1 (map (on_snd reorder) brs))
+    | tCase i mch brs => tCase i (reorder mch) (reorder_branches i.1 (map (on_snd reorder) brs))
     | tFix mfix idx => tFix (map (map_def reorder) mfix) idx
     | tCoFix mfix idx => tCoFix (map (map_def reorder) mfix) idx
-    | tProj (Kernames.mkProjection ind i arg) bod =>
-      tProj (Kernames.mkProjection ind i (lookup_constructor_ordinal ind arg)) (reorder bod)
+    | tProj p bod =>
+      tProj p (reorder bod)
     | tPrim p => tPrim (map_prim reorder p)
     | tLazy t => tLazy (reorder t)
     | tForce t => tForce (reorder t)
@@ -68,25 +381,26 @@ Section Reorder.
       {| cst_body := option_map reorder cb.(cst_body) |}.
 
     Definition reorder_one_ind kn i (oib : one_inductive_body) : one_inductive_body :=
-      match lookup_inductive mapping {| inductive_mind := kn; inductive_ind := i |} with
+      match lookup_inductive_assoc mapping {| inductive_mind := kn; inductive_ind := i |} with
       | None => oib
       | Some (tyna, tags) =>
         {| ind_name := oib.(ind_name);
            ind_propositional := oib.(ind_propositional);
            ind_kelim := oib.(ind_kelim);
            ind_ctors := reorder_list tags oib.(ind_ctors);
-           ind_projs := reorder_list tags oib.(ind_projs) |}
+           ind_projs := oib.(ind_projs) |}
       end.
 
     Definition reorder_inductive_decl kn idecl :=
-      {| ind_finite := idecl.(ind_finite); ind_npars := 0;
+      {| ind_finite := idecl.(ind_finite); ind_npars := idecl.(ind_npars);
          ind_bodies := mapi (reorder_one_ind kn) idecl.(ind_bodies) |}.
 
     Definition reorder_decl d :=
-      match d.2 with
-      | ConstantDecl cb => (d.1, ConstantDecl (reorder_constant_decl cb))
-      | InductiveDecl idecl => (d.1, InductiveDecl (reorder_inductive_decl d.1 idecl))
-      end.
+      let d' := match d.2 with
+      | ConstantDecl cb => ConstantDecl (reorder_constant_decl cb)
+      | InductiveDecl idecl => InductiveDecl (reorder_inductive_decl d.1 idecl)
+      end in
+      (d.1, d').
 
     Definition reorder_env Σ :=
       map (reorder_decl) Σ.
@@ -95,3 +409,1174 @@ End Reorder.
 
 Definition reorder_program mapping (p : program) : program :=
   (reorder_env mapping p.1, reorder mapping p.2).
+
+Definition wf_tags_list (tags : list nat) (n : nat) :=
+  (#|tags| == n) && wf_tags tags.
+
+Lemma nth_error_reorder {A} {l : list A} {tags n newidx} :
+  wf_tags_list tags #|l| ->
+  old_tag tags newidx = Some n ->
+  nth_error (reorder_list tags l) newidx = nth_error l n.
+Proof.
+  move=> /andP [] h. apply eqb_eq in h. move=> wft hnw.
+  pose proof (reorder_list_old_tag tags l n newidx wft).
+  now apply H.
+Qed.
+
+Definition wf_reordering ncstrs cstrs :=
+  (List.length cstrs == ncstrs) &&
+  one_to_one_map ncstrs cstrs.
+
+Definition wf_inductive_mapping (Σ : global_declarations) (m : inductive_mapping) : bool :=
+  let '(ind, (_, cstrs)) := m in
+  match EGlobalEnv.lookup_inductive Σ ind with
+  | Some (mib, oib) => wf_tags_list cstrs #|oib.(ind_ctors)|
+  | None => true
+  end.
+
+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).
+
+  Notation optimize := (reorder m).
+
+  Lemma optimize_mkApps f l : optimize (mkApps f l) = mkApps (optimize f) (map optimize l).
+  Proof using Type.
+    induction l using rev_ind; simpl; auto.
+    now rewrite mkApps_app /= IHl map_app /= mkApps_app /=.
+  Qed.
+
+  Lemma map_optimize_repeat_box n : map optimize (repeat tBox n) = repeat tBox n.
+  Proof using Type. by rewrite map_repeat. Qed.
+
+  (* move to globalenv *)
+
+  Lemma isLambda_optimize t : isLambda t -> isLambda (optimize t).
+  Proof. destruct t => //. Qed.
+  Lemma isBox_optimize t : isBox t -> isBox (optimize t).
+  Proof. destruct t => //. Qed.
+
+  Lemma lookup_env_reorder kn : lookup_env (reorder_env m Σ) kn = option_map (fun decl => snd (reorder_decl m (kn, decl))) (lookup_env Σ kn).
+  Proof.
+    clear wfm. induction Σ; cbn; auto.
+    case: eqb_spec => [->|hneq] //=.
+  Qed.
+
+  Lemma lookup_constant_reorder c : option_map (reorder_constant_decl m) (lookup_constant Σ c) = lookup_constant (reorder_env m Σ) c.
+  Proof.
+    rewrite /lookup_constant lookup_env_reorder.
+    destruct lookup_env => //=.
+    destruct g => //.
+  Qed.
+
+  Lemma lookup_inductive_reorder i :
+    lookup_inductive (reorder_env m Σ) i = option_map (fun '(mib, oib) =>
+      (reorder_inductive_decl m i.(inductive_mind) mib, reorder_one_ind m i.(inductive_mind) i.(inductive_ind) oib))
+       (lookup_inductive Σ i).
+  Proof.
+    unfold lookup_inductive, lookup_minductive.
+    unfold reorder_env. rewrite lookup_env_reorder.
+    destruct lookup_env => //=.
+    destruct g => //.
+    cbn. rewrite nth_error_mapi.
+    destruct nth_error => //=.
+  Qed.
+
+  Lemma lookup_inductive_assoc_spec {ind p} :
+    wf_inductives_mapping Σ m ->
+    lookup_inductive_assoc m ind = Some p ->
+    wf_inductive_mapping Σ (ind, p).
+  Proof.
+    clear. rewrite /wf_inductives_mapping.
+    induction m; cbn -[lookup_inductive wf_inductive_mapping] => //.
+    destruct eq_inductive eqn:heq => //.
+    - move=> /andP[] wfa wfi. intros [= <-].
+      apply eqb_eq in heq. subst ind. destruct a; apply wfa.
+    - move=> /andP[] wfa wfi. intros hl. now apply IHi.
+  Qed.
+
+  Lemma lookup_inductive_assoc_wf_tags {ind mib oib p} :
+    lookup_inductive Σ ind = Some (mib, oib) ->
+    lookup_inductive_assoc m ind = Some p ->
+    wf_tags_list (snd p) #|oib.(ind_ctors)|.
+  Proof.
+    move=> hl.
+    move/(lookup_inductive_assoc_spec wfm).
+    rewrite /wf_inductive_mapping hl.
+    now destruct p.
+  Qed.
+
+  Lemma ind_ctors_reorder {ind mib oib p} :
+    lookup_inductive Σ ind = Some (mib, oib) ->
+    lookup_inductive_assoc m ind = Some p ->
+    ind_ctors (reorder_one_ind m ind.(inductive_mind) ind.(inductive_ind) oib) =
+    reorder_list p.2 (ind_ctors oib).
+  Proof.
+    intros hli hia.
+    unfold reorder_one_ind.
+    destruct ind; rewrite hia. destruct p. now cbn.
+  Qed.
+
+  Lemma ind_ctors_no_reorder {ind mib oib} :
+    lookup_inductive Σ ind = Some (mib, oib) ->
+    lookup_inductive_assoc m ind = None ->
+    ind_ctors (reorder_one_ind m ind.(inductive_mind) ind.(inductive_ind) oib) =
+    ind_ctors oib.
+  Proof.
+    intros hli hia.
+    unfold reorder_one_ind.
+    now destruct ind; rewrite hia.
+  Qed.
+
+  Lemma nth_reorder_list_ctors {i mib oib na tags} :
+    lookup_inductive Σ i = Some (mib, oib) ->
+    lookup_inductive_assoc m i = Some (na, tags) ->
+    forall newidx n, old_tag tags newidx = Some n ->
+    nth_error (reorder_list tags oib.(ind_ctors)) newidx = nth_error oib.(ind_ctors) n.
+  Proof.
+    move=> hli hia idx hnew.
+    apply nth_error_reorder => //.
+    eapply (lookup_inductive_assoc_wf_tags (p:=(na, tags))); tea.
+  Qed.
+
+  Lemma map_opt_length {A B} (f : A -> option B) l :
+    match mapopt f l with
+    | None => True
+    | Some l' => #|l'| = #|l|
+    end.
+  Proof.
+    induction l; cbn; auto.
+    destruct (f a) => //.
+    destruct (mapopt f l) => //=. now f_equal.
+  Qed.
+
+  Lemma reorder_list_length {A} tags (l : list A): #|tags| = #|l| -> #|reorder_list tags l| = #|l|.
+  Proof.
+    move=> hl. rewrite /reorder_list.
+    case hr: reorder_list_opt => [l'|] //=.
+    move: hr; rewrite /reorder_list_opt.
+    have := map_opt_length (nth_error l) tags.
+    destruct mapopt => //. congruence.
+  Qed.
+
+  Lemma lookup_inductive_assoc_None_reorder_one_ind i oib :
+    lookup_inductive_assoc m i = None ->
+    reorder_one_ind m (inductive_mind i) (inductive_ind i) oib = oib.
+  Proof.
+    rewrite /reorder_one_ind. destruct i; move => -> //.
+  Qed.
+(*
+  Lemma lookup_inductive_assoc_None_reorder_inductive_decl i mib :
+    lookup_inductive_assoc m i = None ->
+    reorder_inductive_decl m (inductive_mind i) mib = mib.
+  Proof.
+    rewrite /reorder_inductive_decl.
+    intros hl. destruct mib; f_equal.
+    cbn; induction ind_bodies => //=. f_equal; eauto.
+    rewrite (lookup_inductive_assoc_None_reorder_one_ind {| inductive_mind := inductive_mind i; inductive_ind := 0 |}). //.
+
+  Qed. *)
+  Arguments eqb_eq {A H x y}.
+  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.
+    rewrite /lookup_constructor lookup_inductive_reorder.
+    destruct lookup_inductive as [[mib oib]|] eqn:hind => //=.
+    destruct nth_error eqn:hnth => //=.
+    destruct (lookup_inductive_assoc m i) as [(na, tags)|] eqn:hl.
+    have /andP[]  := lookup_inductive_assoc_wf_tags hind hl => //= /eqb_eq => hlen wft.
+    rewrite (ind_ctors_reorder hind hl). cbn.
+    destruct (nth_error _ (lookup_constructor_ordinal _ _ _)) eqn:hnth'.
+    rewrite /lookup_constructor_ordinal /lookup_constructor_mapping in hnth'.
+    rewrite hl /= in hnth'.
+    destruct (new_tag tags n) as [newidx|] eqn:ht.
+    - eapply new_tag_spec in ht.
+      now rewrite (nth_reorder_list_ctors hind hl _ n) in hnth'.
+    - move/nth_error_Some_length: hnth.
+      rewrite /new_tag in ht => hn.
+      eapply find_tag_wf in ht => //. lia.
+    - eapply nth_error_None in hnth'.
+      apply nth_error_Some_length in hnth.
+      rewrite reorder_list_length in hnth' => //.
+      move: hnth'.
+      rewrite /lookup_constructor_ordinal /lookup_constructor_mapping hl /=.
+      destruct (new_tag tags n) as [newidx|] eqn:ht.
+      eapply new_tag_spec in ht.
+      apply nth_error_Some_length in ht. lia.
+      rewrite /new_tag in ht => hn.
+      eapply find_tag_wf in ht => //. lia.
+    - rewrite /lookup_constructor_ordinal /lookup_constructor_mapping hl //=.
+      destruct i.
+      rewrite /reorder_one_ind hl //=. now rewrite hnth.
+    - apply nth_error_None in hnth.
+      rewrite /lookup_constructor_ordinal /lookup_constructor_mapping /=.
+      destruct lookup_inductive_assoc eqn:hl => //=.
+      have /andP[]  := lookup_inductive_assoc_wf_tags hind hl => //= /(eqb_eq (A:=nat)) => hlen wft.
+      destruct p as [na tags].
+      destruct (new_tag tags n) as [newidx|] eqn:ht.
+      + eapply new_tag_spec in ht.
+        move/andP: wft => [] ht' _.
+        eapply forallb_All in ht'. eapply All_nth_error in ht'; tea. apply Nat.ltb_lt in ht'. lia.
+      + rewrite /reorder_one_ind. destruct i; rewrite hl //=.
+        destruct nth_error eqn:hnth' => //.
+        apply nth_error_Some_length in hnth'. rewrite reorder_list_length in hnth'. cbn in hlen; lia. lia.
+      + rewrite lookup_inductive_assoc_None_reorder_one_ind //=.
+        destruct nth_error eqn:hnth' => //.
+        apply nth_error_Some_length in hnth'. lia.
+  Qed.
+
+  Lemma ind_projs_reorder mind ind oib :
+    ind_projs (reorder_one_ind m mind ind oib) = ind_projs oib.
+  Proof.
+    rewrite /reorder_one_ind. destruct lookup_inductive_assoc as [[na tags]|]=> //.
+  Qed.
+
+  Lemma wf_glob_ind_projs {p pinfo} :
+    wf_glob Σ ->
+    lookup_projection Σ p = Some pinfo ->
+    #|(ind_ctors pinfo.1.1.2)| = 1.
+  Proof.
+    intros wf.
+    rewrite /lookup_projection /lookup_constructor /lookup_inductive /lookup_minductive.
+    destruct lookup_env eqn:hl => //.
+    have := lookup_env_wellformed wf hl.
+    destruct g as [|mib] => //=.
+    destruct nth_error eqn:hind => //=.
+    destruct ind_ctors eqn:hctors => //=.
+    destruct (nth_error (ind_projs o) _) eqn:hprojs => //=.
+    intros wfmind [= <-]. cbn.
+    move: wfmind; rewrite /wf_minductive.
+    move/andP=> [] _ /forallb_All ha.
+    eapply All_nth_error in ha; tea.
+    move: ha; rewrite /wf_inductive /wf_projections.
+    destruct ind_projs => //. now rewrite nth_error_nil in hprojs.
+    rewrite hctors. destruct l => //.
+  Qed.
+
+
+  Lemma lookup_projection_ordinal p :
+    wf_glob Σ ->
+    isSome (lookup_projection Σ p) ->
+    lookup_constructor_ordinal m (proj_ind p) 0 = 0.
+  Proof.
+    move=> wf.
+    case hl: lookup_projection => [pro|] //= _.
+    have wfpro := wf_glob_ind_projs wf hl. move: hl.
+    rewrite /lookup_projection /lookup_constructor_ordinal.
+    destruct lookup_constructor as [[[mib oib] cb]|] eqn:hlc => //=.
+    destruct nth_error eqn:nthp => //=. intros [= <-]. cbn in wfpro.
+    rewrite /lookup_constructor_mapping.
+    destruct lookup_inductive_assoc as [[na tags]|] eqn:hla => //=.
+    destruct new_tag eqn:hnt => //=.
+    eapply new_tag_spec in hnt.
+    eapply lookup_inductive_assoc_spec in hla; tea.
+    rewrite /wf_inductive_mapping in hla.
+    eapply lookup_constructor_lookup_inductive in hlc. rewrite hlc in hla.
+    move/andP: hla. rewrite wfpro. rewrite /wf_tags => [] [] taglen /andP[] /forallb_All ht.
+    destruct tags as [|] => //. destruct tags as [|] => //.
+    destruct n => //. cbn in hnt. now rewrite nth_error_nil in hnt.
+  Qed.
+
+  Lemma lookup_projection_reorder p :
+    wf_glob Σ ->
+    isSome (lookup_projection Σ p) ->
+    lookup_projection (reorder_env m Σ) p = option_map (fun '(((mib, oib), c), pb) =>
+      (reorder_inductive_decl m p.(proj_ind).(inductive_mind) mib,
+        reorder_one_ind m p.(proj_ind).(inductive_mind) p.(proj_ind).(inductive_ind) oib,
+        c, pb))
+       (lookup_projection Σ p).
+  Proof.
+    intros wf iss. unfold lookup_projection.
+    rewrite -{1}(lookup_projection_ordinal _ wf iss) -lookup_constructor_reorder.
+    destruct lookup_constructor eqn:hlc => //=.
+    destruct p0 as [[mib oib] cb] => //=.
+    rewrite ind_projs_reorder //=.
+    destruct nth_error eqn:nthp => //=.
+  Qed.
+
+  Lemma All_reorder_list {A tags} {P : A -> Prop} {l} :
+    All P l ->
+    All P (reorder_list tags l).
+  Proof.
+    rewrite /reorder_list.
+    destruct reorder_list_opt as [l'|] eqn:hre => //=.
+    have hin := reorder_list_opt_In _ _ _ hre.
+    move/(All_Forall).
+    move/(Forall_forall _ _) => hl.
+    apply Forall_All, Forall_forall. intuition eauto.
+  Qed.
+
+  Lemma wf_ind_mapping_wf_brs {ind n nas tags} : wf_brs Σ ind n ->
+    lookup_inductive_assoc m ind = Some (nas, tags) ->
+    #|tags| = n.
+  Proof.
+    rewrite /wf_brs.
+    destruct lookup_inductive as [[mib oib]|] eqn:hli => //.
+    move=> /eqb_eq hlen hla.
+    have := lookup_inductive_assoc_wf_tags hli hla.
+    rewrite /wf_tags_list /= => /andP[] /eqb_eq hlt _. lia.
+  Qed.
+
+  Ltac rtoProp ::=
+  repeat match goal with
+  | H : is_true (_ && _) |- _ => apply andb_and in H; destruct H
+  | |- context [is_true (_ && _)] => rewrite andb_and
+  | H : is_true (_ || _) |- _ => move/orP: H => H; destruct H
+  | |- context [is_true (_ || _)] => apply/orP
+  end.
+
+
+
+  Lemma wf_optimize t k :
+    wf_glob Σ ->
+    wellformed Σ k t -> wellformed (reorder_env m Σ) k (optimize t).
+  Proof using Type wfm wca.
+    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;
+    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.
+      now destruct (cst_body c) => //=.
+    - rewrite wca in H *. move/andP: H => [] /andP[] -> iss isnil /=.
+      rewrite -lookup_constructor_reorder.
+      destruct lookup_constructor eqn:hl => //=.
+      destruct args => //.
+    - rtoProp; intuition auto; solve_all.
+      * rewrite /reorder_branches.
+        destruct lookup_inductive_assoc as [[na tags]|] eqn:hl => //=.
+        have lenreo := wf_ind_mapping_wf_brs H0 hl.
+        rewrite reorder_list_length. len. len.
+        move: H0. rewrite /wf_brs. destruct p as [[mind ind] i].
+        rewrite lookup_inductive_reorder. destruct lookup_inductive as [[mib oib]|]=> //=.
+        rewrite /reorder_one_ind hl /=. move/eqb_eq => hl'. rewrite reorder_list_length //. lia.
+        now apply Nat.eqb_eq. len.
+        move: H0. rewrite /wf_brs. destruct p as [[mind ind] i].
+        rewrite lookup_inductive_reorder. destruct lookup_inductive as [[mib oib]|]=> //=.
+        rewrite /reorder_one_ind hl /=. move/eqb_eq => hl'. now apply Nat.eqb_eq.
+      * rewrite /reorder_branches.
+        destruct lookup_inductive_assoc as [[nas tags]|].
+        eapply All_reorder_list.
+        all:solve_all.
+    - rtoProp; intuition auto.
+      rewrite lookup_projection_reorder //.
+      destruct lookup_projection => //.
+    - rtoProp; intuition auto; solve_all.
+      destruct (dbody x) => //.
+    - rtoProp; intuition auto; solve_all.
+      depelim H1; constructor; eauto. intuition auto.
+      cbn; solve_all.
+  Qed.
+
+  Instance mapopt_ext {A B} :
+    Proper (pointwise_relation A eq ==> eq ==> eq) (@mapopt A B).
+  Proof.
+    intros f g eqfg l ? <-.
+    induction l; cbn; auto.
+    rewrite (eqfg a). destruct (g a) => //.
+    now rewrite IHl.
+  Qed.
+
+  Lemma mapopt_option_map {A B C} (f : A -> option B) (g : B -> C) l :
+    mapopt (fun x => option_map g (f x)) l = option_map (map g) (mapopt f l).
+  Proof.
+    induction l; cbn; auto.
+    destruct (f a) => //=.
+    rewrite IHl. destruct (mapopt f l) => //.
+  Qed.
+
+  Lemma reorder_list_opt_map {A B} tags (f : A -> B) (l : list A) :
+    reorder_list_opt tags (map f l) = option_map (map f) (reorder_list_opt tags l).
+  Proof.
+    rewrite /reorder_list_opt.
+    have req : pointwise_relation nat eq (nth_error (map f l)) (fun x => option_map f (nth_error l x)).
+    { intros x. now rewrite nth_error_map. }
+    setoid_rewrite req. now rewrite mapopt_option_map.
+  Qed.
+
+  Lemma reorder_branches_map i f brs :
+    reorder_branches m i (map f brs) =
+    map f (reorder_branches m i brs).
+  Proof.
+    rewrite /reorder_branches.
+    destruct lookup_inductive_assoc as [[na tags]|] eqn:hl => //.
+    rewrite /reorder_list.
+    rewrite reorder_list_opt_map.
+    destruct (reorder_list_opt tags brs) => //=.
+  Qed.
+
+  Lemma optimize_csubst {a k b} n :
+    wf_glob Σ ->
+    wellformed Σ (k + n) b ->
+    optimize (ECSubst.csubst a k b) = ECSubst.csubst (optimize a) k (optimize b).
+  Proof using Type wfm wca.
+    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;
+    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.
+    - f_equal. rtoProp. rewrite wca in H0. now destruct args; inv H0.
+    - move/andP: wft => [] hasc /andP[] /andP[] hi hb hl. rewrite IHb. f_equal. unfold on_snd; solve_all.
+      repeat toAll. f_equal. solve_all.
+      rewrite -!reorder_branches_map map_map_compose. cbn. f_equal.
+      unfold on_snd; cbn.
+      solve_all. f_equal. unfold optimize in *.
+      rewrite a0 //. red; rewrite -b0. lia_f_equal.
+    - move/andP: wft => [] /andP[] hasf hp /andP[] hb hwfm.
+      f_equal. solve_all.
+      rewrite /map_def; destruct x => //=. f_equal.
+      apply a0; cbn in *. red; rewrite -b0. lia_f_equal.
+    - move/andP: wft => [] hasco /andP[] hp hb.
+      f_equal. solve_all.
+      rewrite /map_def; destruct x => //=. f_equal.
+      apply a0; cbn in *. red; rewrite -b. lia_f_equal.
+  Qed.
+
+  Lemma optimize_substl s t :
+    wf_glob Σ ->
+    forallb (wellformed Σ 0) s ->
+    wellformed Σ #|s| t ->
+    optimize (substl s t) = substl (map optimize s) (optimize t).
+  Proof using Type wfm wca.
+    intros wfΣ. induction s in t |- *; simpl; auto.
+    move/andP => [] cla cls wft.
+    rewrite IHs //. eapply wellformed_csubst => //.
+    f_equal. rewrite (optimize_csubst (S #|s|)) //.
+  Qed.
+
+  Lemma optimize_iota_red pars args br :
+    wf_glob Σ ->
+    forallb (wellformed Σ 0) args ->
+    wellformed Σ #|skipn pars args| br.2 ->
+    optimize (EGlobalEnv.iota_red pars args br) = EGlobalEnv.iota_red pars (map optimize args) (on_snd optimize br).
+  Proof using Type wfm wca.
+    intros wfΣ wfa wfbr.
+    unfold EGlobalEnv.iota_red.
+    rewrite optimize_substl //.
+    rewrite forallb_rev forallb_skipn //.
+    now rewrite List.rev_length.
+    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.
+    generalize #|mfix|.
+    induction n; simpl; auto.
+    f_equal; auto.
+  Qed.
+
+  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.
+    generalize #|mfix|.
+    induction n; simpl; auto.
+    f_equal; auto.
+  Qed.
+
+  Lemma optimize_cunfold_fix mfix idx n f :
+    wf_glob Σ ->
+    wellformed Σ 0 (tFix mfix idx) ->
+    cunfold_fix mfix idx = Some (n, f) ->
+    cunfold_fix (map (map_def optimize) mfix) idx = Some (n, optimize f).
+  Proof using Type wfm wca.
+    intros wfΣ hfix.
+    unfold cunfold_fix.
+    rewrite nth_error_map.
+    cbn in hfix. move/andP: hfix => [] /andP[] hasfix hlam /andP[] hidx hfix.
+    destruct nth_error eqn:hnth => //.
+    intros [= <- <-] => /=. f_equal.
+    rewrite optimize_substl //. eapply wellformed_fix_subst => //.
+    rewrite fix_subst_length.
+    eapply nth_error_forallb in hfix; tea. now rewrite Nat.add_0_r in hfix.
+    now rewrite optimize_fix_subst.
+  Qed.
+
+  Lemma optimize_cunfold_cofix mfix idx n f :
+    wf_glob Σ ->
+    wellformed Σ 0 (tCoFix mfix idx) ->
+    cunfold_cofix mfix idx = Some (n, f) ->
+    cunfold_cofix (map (map_def optimize) mfix) idx = Some (n, optimize f).
+  Proof using Type wfm wca.
+    intros wfΣ hfix.
+    unfold cunfold_cofix.
+    rewrite nth_error_map.
+    cbn in hfix. move/andP: hfix => [] hasfix /andP[] hidx hfix.
+    destruct nth_error eqn:hnth => //.
+    intros [= <- <-] => /=. f_equal.
+    rewrite optimize_substl //. eapply wellformed_cofix_subst => //.
+    rewrite cofix_subst_length.
+    eapply nth_error_forallb in hfix; tea. now rewrite Nat.add_0_r in hfix.
+    now rewrite optimize_cofix_subst.
+  Qed.
+
+End reorder_proofs.
+
+Import EGlobalEnv EExtends.
+
+Lemma extends_lookup_projection {efl : EEnvFlags} {Σ Σ' p} : extends Σ Σ' -> wf_glob Σ' ->
+  isSome (lookup_projection Σ p) ->
+  lookup_projection Σ p = lookup_projection Σ' p.
+Proof.
+  intros ext wf.
+  unfold lookup_projection.
+  destruct lookup_constructor as [[[mdecl idecl] cdecl]|] eqn:hl => //.
+  simpl.
+  rewrite (extends_lookup_constructor wf ext _ _ _ hl) //.
+Qed.
+
+(*
+Lemma wellformed_optimize_extends {wfl: EEnvFlags} {Σ} t :
+  forall n, EWellformed.wellformed Σ n t ->
+  forall {Σ'}, extends Σ Σ' -> wf_glob Σ' ->
+  optimize Σ t = optimize Σ' t.
+Proof.
+  induction t using EInduction.term_forall_list_ind; cbn -[lookup_constant lookup_inductive
+    GlobalContextMap.lookup_projection]; intros => //.
+  all:unfold wf_fix_gen in *; rtoProp; intuition auto.
+  5:{ destruct cstr_as_blocks; rtoProp. f_equal; eauto; solve_all. destruct args; cbn in *; eauto. }
+  all:f_equal; eauto; solve_all.
+  - rewrite !GlobalContextMap.lookup_projection_spec.
+    rewrite -(extends_lookup_projection H0 H1 H3).
+    destruct lookup_projection as [[[[]]]|]. f_equal; eauto.
+    now cbn in H3.
+Qed.
+
+Lemma wellformed_reorder_decl_extends {wfl: EEnvFlags} {Σ} t :
+  wf_global_decl Σ t ->
+  forall {Σ' : GlobalContextMap.t}, extends Σ Σ' -> wf_glob Σ' ->
+  reorder_decl Σ t = reorder_decl Σ' t.
+Proof.
+  destruct t => /= //.
+  intros wf Σ' ext wf'. f_equal. unfold optimize_constant_decl. f_equal.
+  destruct (cst_body c) => /= //. f_equal.
+  now eapply wellformed_optimize_extends.
+Qed.
+
+Lemma lookup_env_reorder_env_Some {efl : EEnvFlags} {Σ} kn d :
+  wf_glob Σ ->
+  GlobalContextMap.lookup_env Σ kn = Some d ->
+  ∑ Σ' : GlobalContextMap.t,
+    [× extends_prefix Σ' Σ, wf_global_decl Σ' d &
+      lookup_env (reorder_env Σ) kn = Some (reorder_decl Σ' d)].
+Proof.
+  rewrite GlobalContextMap.lookup_env_spec.
+  destruct Σ as [Σ map repr wf].
+  induction Σ in map, repr, wf |- *; simpl; auto => //.
+  intros wfg.
+  case: eqb_specT => //.
+  - intros ->. cbn. intros [= <-].
+    exists (GlobalContextMap.make Σ (fresh_globals_cons_inv wf)). split.
+    now eexists [_].
+    cbn. now depelim wfg.
+    f_equal. symmetry. eapply wellformed_reorder_decl_extends. cbn. now depelim wfg.
+    eapply extends_prefix_extends.
+    cbn. now exists [a]. now cbn. now cbn.
+  - intros _.
+    set (Σ' := GlobalContextMap.make Σ (fresh_globals_cons_inv wf)).
+    specialize (IHΣ (GlobalContextMap.map Σ') (GlobalContextMap.repr Σ') (GlobalContextMap.wf Σ')).
+    cbn in IHΣ. forward IHΣ. now depelim wfg.
+    intros hl. specialize (IHΣ hl) as [Σ'' [ext wfgd hl']].
+    exists Σ''. split => //.
+    * destruct ext as [? ->].
+      now exists (a :: x).
+    * rewrite -hl'. f_equal.
+      clear -wfg.
+      eapply map_ext_in => kn hin. unfold on_snd. f_equal.
+      symmetry. eapply wellformed_reorder_decl_extends => //. cbn.
+      eapply lookup_env_In in hin. 2:now depelim wfg.
+      depelim wfg. eapply lookup_env_wellformed; tea.
+      eapply extends_prefix_extends.
+      cbn. now exists [a]. now cbn.
+Qed.
+
+Lemma lookup_env_map_snd Σ f kn : lookup_env (List.map (on_snd f) Σ) kn = option_map f (lookup_env Σ kn).
+Proof.
+  induction Σ; cbn; auto.
+  case: eqb_spec => //.
+Qed.
+
+Lemma lookup_env_reorder_env_None {efl : EEnvFlags} {Σ} kn :
+  GlobalContextMap.lookup_env Σ kn = None ->
+  lookup_env (reorder_env Σ) kn = None.
+Proof.
+  rewrite GlobalContextMap.lookup_env_spec.
+  destruct Σ as [Σ map repr wf].
+  cbn. intros hl. rewrite lookup_env_map_snd hl //.
+Qed.
+*)
+
+Section reorder_mapping.
+  Context {efl : EEnvFlags}.
+  Context {wca : cstr_as_blocks = false}.
+
+  Context (mapping : inductives_mapping).
+  Context (Σ : global_context).
+  Context (wfm : wf_inductives_mapping Σ mapping).
+  Notation reorder := (reorder mapping).
+  Notation reorder_decl := (reorder_decl mapping).
+  Notation reorder_env := (reorder_env mapping).
+
+Lemma is_propositional_optimize ind :
+  wf_glob Σ ->
+  inductive_isprop_and_pars Σ ind = inductive_isprop_and_pars (reorder_env Σ) ind.
+Proof.
+  rewrite /inductive_isprop_and_pars => wf.
+  rewrite /lookup_inductive /lookup_minductive.
+  rewrite lookup_env_reorder.
+  destruct lookup_env as [[decl|]|] => //=.
+  rewrite nth_error_mapi. destruct nth_error => //=.
+  destruct o => //=. rewrite /reorder_one_ind /=.
+  destruct lookup_inductive_assoc as [[na tags]|]=> //=.
+Qed.
+
+Lemma lookup_inductive_pars_optimize ind :
+  wf_glob Σ ->
+  EGlobalEnv.lookup_inductive_pars Σ ind = EGlobalEnv.lookup_inductive_pars (reorder_env Σ) ind.
+Proof.
+  rewrite /lookup_inductive_pars => wf.
+  rewrite /lookup_inductive /lookup_minductive.
+  rewrite lookup_env_reorder.
+  destruct lookup_env as [[decl|]|] => //.
+Qed.
+
+Lemma is_propositional_cstr_optimize ind c :
+  wf_glob Σ ->
+  constructor_isprop_pars_decl Σ ind c = constructor_isprop_pars_decl (reorder_env Σ) ind (lookup_constructor_ordinal mapping ind c).
+Proof.
+  rewrite /constructor_isprop_pars_decl => wf.
+  rewrite -lookup_constructor_reorder //.
+  destruct lookup_constructor as [[[mib oib] cb]|] => //=.
+  rewrite /reorder_one_ind.
+  destruct lookup_inductive_assoc as [[na tags]|]=> //.
+Qed.
+
+Lemma closed_iota_red pars c args brs br :
+  forallb (closedn 0) args ->
+  nth_error brs c = Some br ->
+  #|skipn pars args| = #|br.1| ->
+  closedn #|br.1| br.2 ->
+  closed (iota_red pars args br).
+Proof.
+  intros clargs hnth hskip clbr.
+  rewrite /iota_red.
+  eapply ECSubst.closed_substl => //.
+  now rewrite forallb_rev forallb_skipn.
+  now rewrite List.rev_length hskip Nat.add_0_r.
+Qed.
+
+Lemma isFix_mkApps t l : isFix (mkApps t l) = isFix t && match l with [] => true | _ => false end.
+Proof.
+  induction l using rev_ind; cbn.
+  - now rewrite andb_true_r.
+  - rewrite mkApps_app /=. now destruct l => /= //; rewrite andb_false_r.
+Qed.
+
+Lemma constructor_isprop_pars_decl_inductive {ind c} {prop pars cdecl} :
+  constructor_isprop_pars_decl Σ ind c = Some (prop, pars, cdecl)  ->
+  inductive_isprop_and_pars Σ ind = Some (prop, pars).
+Proof.
+  rewrite /constructor_isprop_pars_decl /inductive_isprop_and_pars /lookup_constructor.
+  destruct lookup_inductive as [[mdecl idecl]|]=> /= //.
+  destruct nth_error => //. congruence.
+Qed.
+
+Lemma constructor_isprop_pars_decl_constructor {ind c} {mdecl idecl cdecl} :
+  lookup_constructor Σ ind c = Some (mdecl, idecl, cdecl) ->
+  constructor_isprop_pars_decl Σ ind c = Some (ind_propositional idecl, ind_npars mdecl, cdecl).
+Proof.
+  rewrite /constructor_isprop_pars_decl. intros -> => /= //.
+Qed.
+
+Lemma wf_mkApps {hasapp : has_tApp} k f args :
+  reflect (wellformed Σ k f /\ forallb (wellformed Σ k) args) (wellformed Σ k (mkApps f args)).
+Proof.
+  rewrite wellformed_mkApps //. eapply andP.
+Qed.
+
+Lemma substl_closed s t : closed t -> substl s t = t.
+Proof.
+  induction s in t |- *; cbn => //.
+  intros clt. rewrite csubst_closed //. now apply IHs.
+Qed.
+
+Lemma substl_rel s k a :
+  closed a ->
+  nth_error s k = Some a ->
+  substl s (tRel k) = a.
+Proof.
+  intros cla.
+  induction s in k |- *.
+  - rewrite nth_error_nil //.
+  - destruct k => //=.
+    * intros [= ->]. rewrite substl_closed //.
+    * intros hnth. now apply IHs.
+Qed.
+
+(* EEnvFlags is reorder_env_flags *)
+Lemma optimize_correct {fl} t v {withc : with_constructor_as_block = false} :
+  has_tApp ->
+  wf_glob Σ ->
+  @eval fl Σ t v ->
+  wellformed Σ 0 t ->
+  @eval fl (reorder_env Σ) (reorder t) (reorder v).
+Proof.
+  intros hastapp wfΣ ev.
+  induction ev; simpl in *.
+
+  - move/andP => [] /andP[] hasapp cla clt. econstructor; eauto.
+  - move/andP => [] /andP[] hasapp clf cla.
+    eapply eval_wellformed in ev2; tea => //.
+    eapply eval_wellformed in ev1; tea => //.
+    econstructor; eauto.
+    move: ev1 => /= /andP[] hasl ev1.
+    rewrite -(optimize_csubst _ _ wfm 1) //.
+    apply IHev3. eapply wellformed_csubst => //.
+
+  - move/andP => [] /andP[] haslet clb0 clb1.
+    intuition auto.
+    eapply eval_wellformed in ev1; tea => //.
+    forward IHev2 by eapply wellformed_csubst => //.
+    econstructor; eauto. rewrite -(optimize_csubst _ _ wfm 1) //.
+
+  - move/andP => [] hascase /andP[] /andP[] hl wfd wfbrs.
+    rewrite optimize_mkApps in IHev1.
+    eapply eval_wellformed in ev1 => //.
+    move/(@wf_mkApps hastapp): ev1 => [] wfc' wfargs.
+    eapply nth_error_forallb in wfbrs; tea.
+    rewrite Nat.add_0_r in wfbrs.
+    forward IHev2. eapply wellformed_iota_red; tea => //.
+    rewrite (optimize_iota_red _ _ wfm) in IHev2 => //. now rewrite e4.
+    econstructor; eauto.
+    rewrite -is_propositional_cstr_optimize //. tea.
+    rewrite reorder_branches_map nth_error_map.
+    rewrite /reorder_branches.
+    rewrite /lookup_constructor_ordinal /lookup_constructor_mapping.
+    destruct lookup_inductive_assoc as [[na tags]|] eqn:hla => //=.
+    rewrite /wf_brs in hl.
+    destruct lookup_inductive as [[mib oib]|] eqn:li => //. apply Nat.eqb_eq in hl.
+    have wftags := lookup_inductive_assoc_wf_tags _ _ wfm li hla.
+    have wfmap := lookup_inductive_assoc_spec _ _ wfm hla.
+    have wfbrl : #|brs| = #|ind_ctors oib|. lia.
+    have wftbrs : wf_tags_list tags #|brs|.
+    { now move: wftags; rewrite /wf_tags_list -wfbrl. }
+    destruct new_tag eqn:hnewt => //=.
+    * eapply new_tag_spec in hnewt.
+      rewrite (nth_error_reorder wftbrs hnewt) e2 //.
+    * move: wftbrs => /andP[] htbrs wftag.
+      eapply find_tag_wf in wftag; tea. apply nth_error_Some_length in e2.
+      apply eqb_eq in htbrs. lia.
+    * rewrite e2 //.
+    * len.
+    * len.
+
+  - congruence.
+
+  - move/andP => [] hascase /andP[] /andP[] hl wfd wfbrs.
+    eapply eval_wellformed in ev1 => //.
+    move: hl; rewrite /wf_brs.
+    destruct lookup_inductive as [[mib oib]|] eqn:li => //. move/Nat.eqb_eq.
+    len. cbn in wfbrs. subst brs. cbn in wfbrs. rewrite Nat.add_0_r in wfbrs.
+    move/andP: wfbrs => [] wfbrs _. cbn; intros hlen.
+    forward IHev2. eapply wellformed_substl; tea => //.
+    rewrite forallb_repeat //. len.
+    eapply eval_iota_sing; eauto.
+    rewrite -is_propositional_optimize //.
+    rewrite /reorder_branches.
+    destruct lookup_inductive_assoc as [[na tags]|] eqn:hla => //=.
+    have wftags := lookup_inductive_assoc_wf_tags _ _ wfm li hla.
+    have wfmap := lookup_inductive_assoc_spec _ _ wfm hla.
+    have wftbrs : wf_tags_list tags #|[(n, f4)]|.
+    { move: wftags; rewrite /wf_tags_list //=. now rewrite hlen. }
+    rewrite //=.
+    move: wftbrs => /andP[] /Nat.eqb_eq //=.
+    destruct tags => //=. destruct tags => //= _.
+    rewrite /wf_tags => /andP[] ht _. move: ht => //= /andP[] /Nat.ltb_lt.
+    destruct n0 => //. destruct n0 => //. cbn -[substl].
+    rewrite (optimize_substl Σ) in IHev2 => //.
+    * now rewrite forallb_repeat.
+    * now len.
+    * now rewrite map_repeat in IHev2.
+
+  - move/andP => [] /andP[] hasapp clf cla. rewrite optimize_mkApps in IHev1.
+    simpl in *.
+    eapply eval_wellformed in ev1 => //.
+    move/(@wf_mkApps hastapp): ev1 => [] wff wfargs.
+    eapply eval_fix; eauto.
+    rewrite map_length.
+    unshelve (eapply optimize_cunfold_fix; tea); tea.
+    rewrite optimize_mkApps in IHev3. apply IHev3.
+    rewrite wellformed_mkApps // wfargs.
+    eapply eval_wellformed in ev2; tas => //. rewrite ev2 /= !andb_true_r.
+    rewrite hastapp.
+    eapply wellformed_cunfold_fix; tea.
+
+  - move/andP => [] /andP[] hasapp clf cla.
+    eapply eval_wellformed in ev1 => //.
+    move/(@wf_mkApps hastapp): ev1 => [] clfix clargs.
+    eapply eval_wellformed in ev2; tas => //.
+    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.
+
+  - move/andP => [] /andP[] hasapp clf cla.
+    eapply eval_wellformed in ev1 => //.
+    eapply eval_wellformed in ev2; tas => //.
+    simpl in *. eapply eval_fix'. auto. auto.
+    unshelve (eapply optimize_cunfold_fix; eauto); tea.
+    eapply IHev2; tea. eapply IHev3.
+    apply/andP; split => //.
+    rewrite hastapp.
+    eapply wellformed_cunfold_fix; tea.
+
+  - move/andP => [] hascase /andP[] /andP[] hl cd clbrs. specialize (IHev1 cd).
+    eapply eval_wellformed in ev1; tea => //.
+    move/(@wf_mkApps hastapp): ev1 => [] wfcof wfargs.
+    forward IHev2.
+    rewrite hl wellformed_mkApps // /= wfargs clbrs !andb_true_r.
+    rewrite hascase.
+    eapply wellformed_cunfold_cofix; tea => //.
+    rewrite !optimize_mkApps /= in IHev1, IHev2.
+    eapply eval_cofix_case. tea.
+    unshelve (eapply optimize_cunfold_cofix; tea); tea.
+    exact IHev2.
+
+  - move/andP => [] /andP[] hasproj hl hd.
+    destruct lookup_projection as [[[[mdecl idecl] cdecl] pdecl]|] eqn:hl' => //.
+    eapply eval_wellformed in ev1 => //.
+    move/(@wf_mkApps hastapp): ev1 => [] wfcof wfargs.
+    forward IHev2.
+    { rewrite /= wellformed_mkApps // wfargs andb_true_r hasproj andb_true_r.
+      eapply wellformed_cunfold_cofix; tea. }
+    rewrite optimize_mkApps /= in IHev1.
+    eapply eval_cofix_proj. eauto.
+    unshelve (eapply optimize_cunfold_cofix; tea); tea.
+    rewrite optimize_mkApps in IHev2 => //.
+
+  - rewrite /declared_constant in isdecl.
+    rewrite /lookup_constant. rewrite isdecl /= => _.
+    destruct decl; cbn in e; subst cst_body.
+    econstructor.
+    rewrite /declared_constant.
+    rewrite lookup_env_reorder isdecl //=. cbn. reflexivity.
+    eapply IHev.
+    eapply lookup_env_wellformed in wfΣ; tea.
+    move: wfΣ. now rewrite /wf_global_decl /=.
+
+  - move=> /andP[] /andP[] hasproj iss cld.
+    eapply eval_wellformed in ev1; tea => //.
+    move/(@wf_mkApps hastapp): ev1 => [] wfc wfargs.
+    destruct lookup_projection as [[[[mdecl idecl] cdecl'] pdecl]|] eqn:hl' => //.
+    pose proof (lookup_projection_lookup_constructor hl').
+    rewrite (constructor_isprop_pars_decl_constructor H) in e1. noconf e1.
+    forward IHev1 by auto.
+    forward IHev2. eapply nth_error_forallb in wfargs; tea.
+    rewrite optimize_mkApps /= in IHev1.
+    have lp := lookup_projection_reorder _ _ wfm p wfΣ.
+    forward lp. now rewrite hl'.
+    rewrite hl' /= in lp.
+    have lpo := (lookup_projection_ordinal _ _ wfm p wfΣ).
+    forward lpo by now rewrite hl'.
+    rewrite lpo in IHev1.
+    eapply eval_proj; tea.
+    rewrite -lpo -is_propositional_cstr_optimize //.
+    rewrite /constructor_isprop_pars_decl // H //= // H0 H1 //.
+    len. rewrite nth_error_map e3 //.
+
+  - congruence.
+
+  - move/andP => [] /andP[] hasproj hl hd.
+    eapply eval_proj_prop; eauto.
+    rewrite -is_propositional_optimize //.
+
+  - move/andP=> [] /andP[] hasapp clf cla.
+    rewrite optimize_mkApps.
+    eapply eval_construct; tea.
+    rewrite -lookup_constructor_reorder //. now rewrite e0 //=.
+    rewrite optimize_mkApps in IHev1. now eapply IHev1.
+    now len.
+    now eapply IHev2.
+
+  - congruence.
+
+  - move/andP => [] /andP[] hasapp clf cla.
+    specialize (IHev1 clf). specialize (IHev2 cla).
+    eapply eval_app_cong; eauto.
+    eapply eval_to_value in ev1.
+    destruct ev1; simpl in *; eauto.
+    * depelim a0.
+      + destruct t => //; rewrite optimize_mkApps /=.
+      + now rewrite /= !orb_false_r orb_true_r in i.
+    * destruct with_guarded_fix.
+      + move: i.
+        rewrite !negb_or.
+        rewrite optimize_mkApps !isFixApp_mkApps !isConstructApp_mkApps !isPrimApp_mkApps
+          !isLazyApp_mkApps.
+        destruct args using rev_case => // /=. rewrite map_app !mkApps_app /= //.
+        rewrite !andb_true_r.
+        rtoProp; intuition auto;  destruct v => /= //.
+      + move: i.
+        rewrite !negb_or.
+        rewrite optimize_mkApps !isConstructApp_mkApps !isPrimApp_mkApps !isLazyApp_mkApps.
+        destruct args using rev_case => // /=. rewrite map_app !mkApps_app /= //.
+        destruct v => /= //.
+  - intros; rtoProp; intuition eauto.
+    depelim X; repeat constructor.
+    eapply All2_over_undep in a.
+    eapply All2_Set_All2 in ev. eapply All2_All2_Set. primProp.
+    subst a0 a'; cbn in *. depelim H0; cbn in *. intuition auto; solve_all.
+    primProp; depelim H0; intuition eauto.
+  - move=> /andP[] haslazy wf. econstructor; eauto. eapply IHev2.
+    eapply eval_wellformed in ev1; tea. move/andP: ev1 => []; tea => //.
+  - destruct t => //.
+    all:constructor; eauto.
+    cbn [atom reorder] in i |- *.
+    rewrite -lookup_constructor_reorder //.
+    destruct args. 2:cbn in *; eauto.
+    cbn -[lookup_constructor]. rtoProp; intuition auto.
+    destruct lookup_constructor => //.
+Qed.
+End reorder_mapping.
+
+Lemma wf_inductive_mapping_inv {efl : EEnvFlags} d Σ m :
+  wf_glob (d :: Σ) ->
+  wf_inductives_mapping (d :: Σ) m ->
+  (match d.2 with
+  | InductiveDecl mib =>
+    (forall i oib, nth_error mib.(ind_bodies) i = Some oib ->
+     match lookup_inductive_assoc m {| inductive_mind := d.1; inductive_ind := i |} with
+    | Some (na, tags) => wf_tags_list tags #|oib.(ind_ctors)|
+    | None => true
+    end)
+  | ConstantDecl _ => True
+  end) /\ wf_inductives_mapping Σ m.
+Proof.
+  rewrite /wf_inductives_mapping.
+  intros wfΣ wfm. split; revgoals. solve_all.
+  move: H; rewrite /wf_inductive_mapping.
+  destruct x as [ind [na tags]].
+  destruct lookup_inductive as [[mib oib]|] eqn:li => //=.
+  depelim wfΣ; cbn.
+  move: li. cbn. case: eqb_spec.
+  * intros <-.
+    destruct d0 => //. destruct nth_error eqn:hnth => //.
+    intros [= -> ->].
+    destruct lookup_env eqn:hle.
+    have:= lookup_env_Some_fresh hle. contradiction.
+    auto.
+  * intros neq. destruct lookup_env => //=. destruct g => //.
+    destruct nth_error => //. now intros [= -> ->].
+  * depelim wfΣ. move: li. cbn; case: eqb_spec.
+    + intros <-. destruct d0 => //.
+      destruct lookup_env eqn:hle => //.
+      have:= lookup_env_Some_fresh hle. contradiction.
+      destruct lookup_env eqn:hle => //.
+      have:= lookup_env_Some_fresh hle. contradiction.
+    + intros neq. destruct lookup_env => //=. destruct g => //.
+      destruct nth_error => //.
+  * depelim wfΣ; cbn.
+    destruct d0 => //.
+    intros i oib hnth.
+    destruct lookup_inductive_assoc as [[na tags]|] eqn:hla => //.
+    have hla' := lookup_inductive_assoc_wf_tags _ _ wfm _ hla.
+    eapply hla'.
+    rewrite /lookup_inductive /lookup_minductive /=.
+    rewrite eqb_refl. rewrite hnth. reflexivity.
+Qed.
+
+From MetaCoq.Erasure Require Import EEtaExpanded.
+
+Lemma optimize_expanded {Σ m} t :
+  wf_inductives_mapping Σ m -> expanded Σ t -> expanded (reorder_env m Σ) (reorder m t).
+Proof.
+  intros wfm.
+  induction 1 using expanded_ind.
+  all:try solve[constructor; eauto; solve_all].
+  all:rewrite ?optimize_mkApps.
+  - eapply expanded_mkApps_expanded => //. solve_all.
+  - cbn. econstructor; eauto.
+    rewrite /reorder_branches.
+    destruct lookup_inductive_assoc => //; solve_all.
+    eapply All_reorder_list. solve_all.
+  - cbn. eapply expanded_tFix. solve_all.
+    rewrite isLambda_optimize //.
+  - cbn.
+    eapply declared_constructor_lookup in H.
+    have hl := lookup_constructor_reorder _ _ wfm ind idx. rewrite H /= in hl.
+    eapply expanded_tConstruct_app; tea.
+    eapply lookup_declared_constructor. now symmetry.
+    now len. now solve_all.
+Qed.
+
+Lemma optimize_expanded_decl {Σ m kn t} :
+  wf_inductives_mapping Σ m ->
+  expanded_decl Σ t -> expanded_decl (reorder_env m Σ) (reorder_decl m (kn, t)).2.
+Proof.
+  destruct t as [[[]]|] => /= //.
+  unfold expanded_constant_decl => /=.
+  intros. now apply optimize_expanded.
+Qed.
+
+Lemma reorder_env_expanded {efl : EEnvFlags} {Σ m} :
+  wf_inductives_mapping Σ m ->
+  wf_glob Σ -> expanded_global_env Σ -> expanded_global_env (reorder_env m Σ).
+Proof.
+  intros wfm.
+  unfold expanded_global_env; move=> wfg exp.
+  induction exp; cbn; constructor; auto.
+  cbn in IHexp.
+  unshelve eapply IHexp; tea. eapply wf_inductive_mapping_inv; tea. now depelim wfg. cbn.
+  unshelve eapply (optimize_expanded_decl). now eapply wf_inductive_mapping_inv.
+  now destruct decl.
+Qed.
+
+From MetaCoq.Erasure Require Import EEtaExpandedFix.
+
+Lemma optimize_expanded_fix {Σ Γ m} t :
+  wf_inductives_mapping Σ m -> expanded Σ Γ t -> expanded (reorder_env m Σ) Γ (reorder m t).
+Proof.
+  intros wfm.
+  induction 1 using expanded_ind.
+  all:try solve[constructor; eauto; solve_all].
+  all:rewrite ?optimize_mkApps.
+  - cbn. eapply expanded_tRel_app; tea. len. solve_all.
+  - cbn. econstructor; eauto.
+    2:solve_all.
+    destruct f3 => //.
+  - cbn. econstructor; eauto.
+    rewrite /reorder_branches.
+    destruct lookup_inductive_assoc => //; solve_all.
+    eapply All_reorder_list. solve_all.
+  - cbn. eapply expanded_tFix. solve_all.
+    rewrite isLambda_optimize //.
+    now rewrite rev_map_spec map_map_compose /= -rev_map_spec.
+    solve_all. destruct args => //. rewrite nth_error_map /= H4 //.
+    len.
+  - cbn.
+    eapply declared_constructor_lookup in H.
+    have hl := lookup_constructor_reorder _ _ wfm ind idx. rewrite H /= in hl.
+    eapply expanded_tConstruct_app; tea.
+    eapply lookup_declared_constructor. now symmetry.
+    now len. now solve_all.
+Qed.
+
+Lemma optimize_expanded_decl_fix {Σ m kn t} :
+  wf_inductives_mapping Σ m ->
+  expanded_decl Σ t -> expanded_decl (reorder_env m Σ) (reorder_decl m (kn, t)).2.
+Proof.
+  destruct t as [[[]]|] => /= //.
+  unfold expanded_constant_decl => /=.
+  intros. now apply optimize_expanded_fix.
+Qed.
+
+Lemma reorder_env_expanded_fix {efl : EEnvFlags} {Σ m} :
+  wf_inductives_mapping Σ m ->
+  wf_glob Σ -> expanded_global_env Σ -> expanded_global_env (reorder_env m Σ).
+Proof.
+  intros wfm.
+  unfold expanded_global_env; move=> wfg exp.
+  induction exp; cbn; constructor; auto.
+  cbn in IHexp.
+  unshelve eapply IHexp; tea. eapply wf_inductive_mapping_inv; tea. now depelim wfg. cbn.
+  unshelve eapply (optimize_expanded_decl_fix). now eapply wf_inductive_mapping_inv.
+  now destruct decl.
+Qed.
+
+Lemma optimize_extends_env {efl : EEnvFlags} {Σ Σ'} m :
+  wf_inductives_mapping Σ' m ->
+  extends Σ Σ' ->
+  wf_glob Σ ->
+  wf_glob Σ' ->
+  extends (reorder_env m Σ) (reorder_env m Σ').
+Proof.
+  intros hast ext wf wf'.
+  rewrite /extends => kn decl.
+  rewrite !lookup_env_reorder.
+  specialize (ext kn).
+  destruct lookup_env eqn:hle => //. specialize (ext _ eq_refl).
+  rewrite ext. auto.
+Qed.
+
+Lemma reorder_env_wf {efl : EEnvFlags} {Σ m}
+  {wcb : cstr_as_blocks = false} :
+  wf_inductives_mapping Σ m ->
+  wf_glob Σ -> wf_glob (reorder_env m Σ).
+Proof.
+  intros wfg wfΣ.
+  induction wfΣ; cbn. constructor; eauto.
+  have wfdΣ : (wf_glob ((kn, d) :: Σ)) by constructor; auto.
+  have [wfd wfinv] := (wf_inductive_mapping_inv _ _ _ wfdΣ wfg). cbn in wfd.
+  constructor; eauto. destruct d; cbn.
+  - unfold wf_global_decl in H. cbn in H.
+    destruct (cst_body c) => //=. cbn in H.
+    unshelve (eapply wf_optimize); eauto.
+  - cbn in H. rewrite /wf_minductive in H. cbn in H.
+    rewrite /wf_minductive /=.
+    move/andP: H => [] -> H /=. solve_all.
+    have hfa := (forall_nth_error_Alli (fun i oib =>
+    is_true (match lookup_inductive_assoc m {| inductive_mind := kn; inductive_ind := i |} with
+    | Some p => let (_, tags) := p in wf_tags_list tags #|ind_ctors oib|
+    | None => true
+    end)) 0 (ind_bodies m0) wfd). clear wfd.
+    eapply Alli_All_mix in hfa; tea. clear H.
+    eapply (Alli_All (P:=fun _ x => wf_inductive x) (n:=0)); eauto.
+    eapply (fst (Alli_mapi _ _ _)).
+    eapply Alli_impl; tea. cbn.
+    intros n x [hla wf].
+    rewrite /reorder_one_ind.
+    destruct lookup_inductive_assoc as [[na tags]|] eqn:hla' => //.
+    move: wf. rewrite /wf_inductive /wf_projections /=.
+    destruct ind_projs => //. destruct ind_ctors => //. destruct l0 => //=.
+    move: hla; rewrite /wf_tags_list. destruct tags => //=.
+    destruct tags => //=. rewrite /wf_tags. move/andP=> [] hf _.
+    cbn in hf. rewrite andb_true_r in hf. apply Nat.leb_le in hf.
+    have -> : n0 = 0 by lia. now cbn.
+  - cbn. apply ErasureFunction.fresh_global_In.
+    rewrite map_map_compose /=. intros hin'. apply ErasureFunction.fresh_global_In in H0.
+    now apply H0.
+Qed.
+
+From MetaCoq.Erasure Require Import EProgram.
+
+Definition reorder_program_wf {efl : EEnvFlags} {wca : cstr_as_blocks = false} (p : eprogram) m (wfm : wf_inductives_mapping p.1 m) :
+  wf_eprogram efl p -> wf_eprogram efl (reorder_program m p).
+Proof.
+  intros []; split.
+  now unshelve eapply reorder_env_wf.
+  cbn. now eapply (@wf_optimize _ wca).
+Qed.
+
+Definition reorder_program_expanded {efl : EEnvFlags} (p : eprogram) m (wfm : wf_inductives_mapping p.1 m) :
+  wf_eprogram efl p ->
+  expanded_eprogram_cstrs p -> expanded_eprogram_cstrs (reorder_program m p).
+Proof.
+  unfold expanded_eprogram_env_cstrs.
+  move=> [wfe wft] /andP[] etae etat.
+  apply/andP; split.
+  cbn. eapply EEtaExpanded.expanded_global_env_isEtaExp_env, reorder_env_expanded => //.
+  now eapply isEtaExp_env_expanded_global_env.
+  eapply EEtaExpanded.expanded_isEtaExp.
+  now apply optimize_expanded, EEtaExpanded.isEtaExp_expanded.
+Qed.
+
+Definition reorder_program_expanded_fix {efl : EEnvFlags} (p : eprogram) m (wfm : wf_inductives_mapping p.1 m) :
+  wf_eprogram efl p ->
+  expanded_eprogram p -> expanded_eprogram (reorder_program m p).
+Proof.
+  unfold expanded_eprogram.
+  move=> [wfe wft] [] etae etat.
+  split. now eapply reorder_env_expanded_fix.
+  now eapply optimize_expanded_fix.
+Qed.
diff --git a/erasure/theories/EUnboxing.v b/erasure/theories/EUnboxing.v
index 87f31709f..5cf20e76c 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, ?length_map;
+    rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?map_length;
     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, ?length_map;
+    rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?map_length;
     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 length_map. move=> [] etaapp etav.
+      move/andP: H1. rewrite map_length. 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 length_map. move=> [] etaapp etav.
+      move/andP: H1. rewrite map_length. 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 length_map.
+    rewrite map_length.
     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 length_map.
+    rewrite map_length.
     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 length_skipn. lia.
+    * len. cbn in H4, H5. rewrite skipn_length. 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 length_map.
+    * rewrite map_length.
       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 length_map.
+    now rewrite map_length.
 
   - 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 length_skipn. cbn in H3. lia.
+    len. rewrite skipn_length. 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 length_skipn length_map => ->. lia.
+      rewrite skipn_length map_length => ->. 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 length_map. rtoProp; intuition auto. toAll; solve_all.
+  - unfold wf_fix_gen in *. rewrite map_length. 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 length_skipn /= /EAst.cstr_arity /=.
+    len. rewrite skipn_length /= /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, ?length_map;
+    rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?map_length;
     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, ?length_map;
+    rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?map_length;
     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.length_rev.
+    now rewrite List.rev_length.
     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 length_map.
+    rewrite map_length.
     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 length_map.
+    rewrite map_length.
     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.length_rev hskip Nat.add_0_r.
+  now rewrite List.rev_length 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 length_map.
+    rewrite map_length.
     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 length_map.
+    now rewrite map_length.
 
   - 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 length_skipn. lia.
+    rewrite skipn_length. 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 length_skipn. lia.
-    rewrite List.rev_involutive. len. rewrite length_skipn.
+    rewrite nth_error_rev. len. rewrite skipn_length. lia.
+    rewrite List.rev_involutive. len. rewrite skipn_length.
     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/EWcbvEval.v b/erasure/theories/EWcbvEval.v
index 94eee4f4b..ab327a72f 100644
--- a/erasure/theories/EWcbvEval.v
+++ b/erasure/theories/EWcbvEval.v
@@ -38,6 +38,7 @@ Definition atom `{wfl : WcbvFlags} Σ t :=
   | tBox
   | tCoFix _ _
   | tLambda _ _
+  | tLazy _
   | tFix _ _ => true
   | tConstruct ind c [] => negb with_constructor_as_block && isSome (lookup_constructor Σ ind c)
   | _ => false
@@ -261,7 +262,7 @@ Section Wcbv.
   | eval_app_cong f f' a a' :
       eval f f' ->
       ~~ (isLambda f' || (if with_guarded_fix then isFixApp f' else isFix f') || isBox f' || isConstructApp f'
-        || isPrimApp f')  ->
+        || isPrimApp f' || isLazyApp f')  ->
       eval a a' ->
       eval (tApp f a) (tApp f' a')
 
@@ -275,13 +276,12 @@ Section Wcbv.
     eval_primitive eval p p' ->
     eval (tPrim p) (tPrim p')
 
-  (*
-  | eval_lazy : eval (tLazy t) (tLazy t)
-  | eval_force t v v' : eval t (tLazy v) ->
+  | eval_force t v v' :
+    eval t (tLazy v) ->
     eval v v' ->
-    eval (tForce t) v' *)
+    eval (tForce t) v'
 
-  (** Atoms are values (includes abstractions, cofixpoints and constructors) *)
+  (** Atoms are values (includes abstractions, cofixpoints, constructors and lazy) *)
   | eval_atom t : atom Σ t -> eval t t.
 
   Hint Constructors eval : core.
@@ -620,7 +620,7 @@ Section eval_rect.
                                                  isBox f'
                                                  ||
                                                  isConstructApp f'
-                                                 || isPrimApp f'))
+                                                 || isPrimApp f' || isLazyApp f'))
                                            (e0 : eval Σ a a'),
                                            P a a' e0
                                            → P (tApp f16 a)
@@ -631,14 +631,17 @@ Section eval_rect.
 
     (forall p p' (ev : eval_primitive (eval Σ) p p'),
       eval_primitive_ind _ P _ _ ev ->
-      P (tPrim p) (tPrim p') (eval_prim _ _ _ ev))
+      P (tPrim p) (tPrim p') (eval_prim _ _ _ ev)) ->
+    (forall t t' v (ev1 : eval Σ t (tLazy t')) (ev2 : eval Σ t' v),
+      P _ _ ev1 -> P _ _ ev2 ->
+      P (tForce t) v (eval_force _ t t' v ev1 ev2))
 
-      → (∀ (t : term) (i : atom Σ t),
+    → (∀ (t : term) (i : atom Σ t),
           P t t (eval_atom Σ t i))
       → ∀ (t t0 : term) (e : eval Σ t t0),
           P t t0 e.
   Proof using Type.
-    intros ?????????????????????? H.
+    intros ??????????????????????? H.
     revert t t0 H.
     fix aux 3.
     move aux at top.
@@ -790,6 +793,7 @@ Section Wcbv.
         + destruct with_guarded_fix.
           now cbn in i1. now cbn in i1.
         + constructor.
+        + now destruct with_guarded_fix; cbn in i1.
         + cbn in i. destruct with_guarded_fix; cbn in i; rtoProp; intuition auto.
       * destruct b0 as (ind & c & mdecl & idecl & cdecl & args & [H1 H2 H3 H4]).
         rewrite -[tApp _ _](mkApps_app _ (firstn n l) [a']).
@@ -1063,7 +1067,7 @@ Section Wcbv.
       rewrite !mkApps_app /=.
       eapply eval_app_cong; tea.
       eapply IHargs => //.
-      rewrite isFixApp_mkApps // /= isConstructApp_mkApps // !negb_or isPrimApp_mkApps.
+      rewrite isFixApp_mkApps // /= isConstructApp_mkApps // !negb_or isPrimApp_mkApps isLazyApp_mkApps.
       rtoProp; intuition auto.
       apply nisLambda_mkApps => //.
       destruct with_guarded_fix => //; eapply nisFix_mkApps => //.
@@ -1309,15 +1313,15 @@ Section Wcbv.
         cbn in i. rtoProp; intuition auto.
       + exfalso. rewrite !negb_or in i. specialize (IHev1 _ ev'1); noconf IHev1.
         cbn in i. rewrite guarded in i. rtoProp; intuition auto.
-        rewrite isFixApp_mkApps in H3 => //.
+        rewrite isFixApp_mkApps in H4 => //.
       + exfalso. rewrite !negb_or in i. specialize (IHev1 _ ev'1); noconf IHev1.
         cbn in i. rewrite guarded in i. rtoProp; intuition auto.
-        rewrite isFixApp_mkApps in H3 => //.
+        rewrite isFixApp_mkApps in H4 => //.
       + exfalso. rewrite !negb_or in i. specialize (IHev1 _ ev'1); noconf IHev1.
         cbn in i. rewrite unguarded in i. now cbn in i.
       + exfalso. rewrite !negb_or in i. specialize (IHev1 _ ev'1); noconf IHev1.
         cbn in i. rtoProp; intuition auto.
-        now rewrite isConstructApp_mkApps in H1.
+        now rewrite isConstructApp_mkApps in H2.
       + specialize (IHev1 _ ev'1); noconf IHev1.
         specialize (IHev2 _ ev'2); noconf IHev2.
         now assert (i0 = i) as -> by now apply uip.
@@ -1334,6 +1338,7 @@ Section Wcbv.
       induction ev in a, ev0 |- *; depelim ev0; eauto.
       destruct a.
       f_equal; eauto. specialize (e0 _ e). now noconf e0.
+    - depelim ev'; go.
     - depelim ev'; try go.
       2: now assert (i0 = i) as -> by now apply uip.
       exfalso. invs i. rewrite e in H0. destruct args; cbn in H0; invs H0.
diff --git a/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v b/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v
index 891283ac8..dfbf65c88 100644
--- a/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v
+++ b/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v
@@ -331,7 +331,7 @@ Lemma eval_preserve_mkApps_ind :
      P f11 f' ->
      (forall t u (ev' : eval Σ t u), eval_depth ev' <= eval_depth ev -> Q 0 t -> P t u) →
      ~~ (isLambda f' || (if with_guarded_fix then isFixApp f' else isFix f') || isBox f'
-      || isConstructApp f' || isPrimApp f') →
+      || isConstructApp f' || isPrimApp f' || isLazyApp f') →
      eval Σ a a' → P a a' →
      P' (tApp f11 a) (tApp f' a')) →
   (∀ ind i mdecl idecl cdecl args args',
@@ -346,6 +346,11 @@ Lemma eval_preserve_mkApps_ind :
     eval_primitive_ind _ (fun x y _ => P x y) _ _ ev ->
     P' (tPrim p) (tPrim p')) ->
 
+  (forall t t' v, eval Σ t (tLazy t') -> eval Σ t' v ->
+    P t (tLazy t') ->
+    P t' v ->
+    P' (tForce t) v) ->
+
   (∀ t : term, atom Σ t → Q 0 t -> P' t t) ->
   ∀ (t t0 : term), Q 0 t -> eval Σ t t0 → P' t t0.
 Proof.
@@ -356,7 +361,7 @@ Proof.
   intros.
   pose proof (p := @Fix_F { t : _ & { t0 : _ & { qt : Q 0 t & eval Σ t t0 }}}).
   specialize (p (MR lt (fun x => eval_depth x.π2.π2.π2))).
-  set(foo := existT _ t (existT _ t0 (existT _ X17 H)) :  { t : _ & { t0 : _ & { qt : Q 0 t & eval Σ t t0 }}}).
+  set(foo := existT _ t (existT _ t0 (existT _ X18 H)) :  { t : _ & { t0 : _ & { qt : Q 0 t & eval Σ t t0 }}}).
   change t with (projT1 foo).
   change t0 with (projT1 (projT2 foo)).
   revert foo.
@@ -366,8 +371,8 @@ Proof.
   forward p.
   2:{ apply p. apply measure_wf, lt_wf. }
   clear p.
-  rename X17 into qt. rename X14 into Xcappexp.
-  rename X15 into Qprim, X16 into Qatom.
+  rename X18 into qt. rename X14 into Xcappexp.
+  rename X15 into Qprim, X16 into Qforce, X17 into Qatom.
   clear t t0 qt H.
   intros (t & t0 & qt & ev).
   intros IH.
@@ -567,6 +572,15 @@ Proof.
       + depelim p0. destruct p.
         eapply and_assum. unshelve eapply IH; tea. cbn; lia.
         intros; split => //; eapply P'Q; tea.
+  - eapply qpres in qt; depelim qt => //.
+    assert (Q 0 (tLazy v)).
+    { eapply P'Q; tea. eapply (IH _ _ q ev1); tea. now cbn; lia. }
+    eapply qpres in X14. depelim X14 => //.
+    eapply Qforce; tea.
+    + eapply and_assum. eapply (IH _ _ q ev1); eauto; cbn; lia.
+      intros hp'. split => //. eapply P'Q; tea.
+    + eapply and_assum. eapply (IH _ _ q0 ev2); eauto; cbn; lia.
+      intros hp'. split => //. eapply P'Q; tea.
   - eapply Qatom; tea.
 Qed.
 
@@ -602,7 +616,6 @@ Proof.
     split; intros; rtoProp; intuition auto; solve_all.
   - red.
     move=> hascase n ci discr brs. simpl.
-    destruct lookup_inductive eqn:hl => /= //.
     intros; rtoProp; intuition auto; solve_all.
   - red. simpl. move=> hasproj n p discr wf discr' wf'.
     simpl. rtoProp; intuition auto.
diff --git a/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v b/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v
index c4b52691a..44bfbf6a6 100644
--- a/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v
+++ b/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v
@@ -296,7 +296,7 @@ Lemma eval_preserve_mkApps_ind :
      P f11 f' ->
      (forall t u (ev' : eval Σ t u), eval_depth ev' <= eval_depth ev -> Q 0 t -> P t u) →
      ~~ (isLambda f' || (if with_guarded_fix then isFixApp f' else isFix f') || isBox f'
-      || isConstructApp f' || isPrimApp f') →
+      || isConstructApp f' || isPrimApp f' || isLazyApp f') →
      eval Σ a a' → P a a' →
      P' (tApp f11 a) (tApp f' a')) →
   (∀ ind i mdecl idecl cdecl args args',
@@ -311,6 +311,11 @@ Lemma eval_preserve_mkApps_ind :
     eval_primitive_ind _ (fun x y _ => P x y) _ _ ev ->
     P' (tPrim p) (tPrim p')) ->
 
+  (forall t t' v, eval Σ t (tLazy t') -> eval Σ t' v ->
+    P t (tLazy t') ->
+    P t' v ->
+    P' (tForce t) v) ->
+
   (∀ t : term, atom Σ t → Q 0 t -> P' t t) ->
   ∀ (t t0 : term), Q 0 t -> eval Σ t t0 → P' t t0.
 Proof.
@@ -320,7 +325,7 @@ Proof.
   intros.
   pose proof (p := @Fix_F { t : _ & { t0 : _ & { qt : Q 0 t & eval Σ t t0 }}}).
   specialize (p (MR lt (fun x => eval_depth x.π2.π2.π2))).
-  set(foo := existT _ t (existT _ t0 (existT _ X16 H)) :  { t : _ & { t0 : _ & { qt : Q 0 t & eval Σ t t0 }}}).
+  set(foo := existT _ t (existT _ t0 (existT _ X17 H)) :  { t : _ & { t0 : _ & { qt : Q 0 t & eval Σ t t0 }}}).
   change t with (projT1 foo).
   change t0 with (projT1 (projT2 foo)).
   revert foo.
@@ -330,8 +335,8 @@ Proof.
   forward p.
   2:{ apply p. apply measure_wf, lt_wf. }
   clear p.
-  rename X16 into qt. rename X13 into Xcappexp.
-  rename X14 into Qprim, X15 into Qatom.
+  rename X17 into qt. rename X13 into Xcappexp.
+  rename X14 into Qprim, X15 into Qforce, X16 into Qatom.
   clear t t0 qt H.
   intros (t & t0 & qt & ev).
   intros IH.
@@ -354,7 +359,7 @@ Proof.
   Ltac myt hyp anda P'Q := eapply hyp; tea; (apply and_assum; [ih|hp' P'Q]).
 
   destruct ev.
-  1-18:eapply qpres in qt as qt'; depelim qt' => //.
+  1-19:eapply qpres in qt as qt'; depelim qt' => //.
   all:try congruence.
   - eapply X; tea; (apply and_assum; [ih|hp' P'Q]).
   - assert (ql : Q 0 (tLambda na b)).
@@ -467,6 +472,15 @@ Proof.
       + depelim p0. destruct p.
         eapply and_assum. unshelve eapply IH; tea. cbn; lia.
         intros; split => //; eapply P'Q; tea.
+  - eapply qpres in qt; depelim qt => //.
+    assert (Q 0 (tLazy v)).
+    { eapply P'Q; tea. eapply (IH _ _ q ev1); tea. now cbn; lia. }
+    eapply qpres in X13. depelim X13 => //.
+    eapply Qforce; tea.
+    + eapply and_assum. eapply (IH _ _ q ev1); eauto; cbn; lia.
+      intros hp'. split => //. eapply P'Q; tea.
+    + eapply and_assum. eapply (IH _ _ q0 ev2); eauto; cbn; lia.
+      intros hp'. split => //. eapply P'Q; tea.
   - eapply Qatom; tea.
 Qed.
 
@@ -502,6 +516,7 @@ Proof.
     split; intros; rtoProp; intuition auto; solve_all.
   - red.
     move=> hascase n ci discr brs. simpl.
+    rewrite /wf_brs.
     destruct lookup_inductive eqn:hl => /= //.
     intros; rtoProp; intuition auto; solve_all.
   - red. simpl. move=> hasproj n p discr wf discr' wf'.
diff --git a/erasure/theories/EWcbvEvalEtaInd.v b/erasure/theories/EWcbvEvalEtaInd.v
index d048beb4d..691d64c78 100644
--- a/erasure/theories/EWcbvEvalEtaInd.v
+++ b/erasure/theories/EWcbvEvalEtaInd.v
@@ -306,7 +306,7 @@ Lemma eval_preserve_mkApps_ind :
      P f11 f' ->
      (forall t u (ev' : eval Σ t u), eval_depth ev' <= eval_depth ev -> Q 0 t -> isEtaExp Σ t -> P t u) →
      ~~ (isLambda f' || (if with_guarded_fix then isFixApp f' else isFix f') || isBox f' || isConstructApp f' ||
-      isPrimApp f') →
+      isPrimApp f' || isLazyApp f') →
      eval Σ a a' → P a a' →
      isEtaExp Σ (tApp f' a') ->
      P' (tApp f11 a) (tApp f' a')) →
@@ -324,11 +324,10 @@ Lemma eval_preserve_mkApps_ind :
     eval_primitive_ind _ (fun x y _ => P x y) _ _ ev ->
     P' (tPrim p) (tPrim p')) ->
 
-  (* (forall t t', eval Σ t t' -> Q 0 t -> Q 0 t' -> P t t' ->
-    P' (tLazy t) (tLazy t')) ->
-
-  (forall t t', eval Σ t t' -> Q 0 t -> Q 0 t' -> P t t' ->
-    P' (tForce t) (tForce t')) -> *)
+  (forall t t' v, eval Σ t (tLazy t') -> eval Σ t' v ->
+    P t (tLazy t') ->
+    P t' v ->
+    P' (tForce t) v) ->
 
   (∀ t : term, atom Σ t → Q 0 t -> isEtaExp Σ t -> P' t t) ->
   ∀ (t t0 : term), Q 0 t -> isEtaExp Σ t -> eval Σ t t0 → P' t t0.
@@ -337,10 +336,10 @@ Proof.
   assert (qfixs: Qfixs Q) by tc.
   assert (qcofixs: Qcofixs Q) by tc.
   intros.
-  enough (P' t t0 × isEtaExp Σ t0). apply X17.
+  enough (P' t t0 × isEtaExp Σ t0). apply X18.
   pose proof (p := @Fix_F { t : _ & { t0 : _ & { qt : Q 0 t & eval Σ t t0 }}}).
   specialize (p (MR lt (fun x => eval_depth x.π2.π2.π2))).
-  set(foo := existT _ t (existT _ t0 (existT _ X16 H0)) :  { t : _ & { t0 : _ & { qt : Q 0 t & eval Σ t t0 }}}).
+  set(foo := existT _ t (existT _ t0 (existT _ X17 H0)) :  { t : _ & { t0 : _ & { qt : Q 0 t & eval Σ t t0 }}}).
   move: H.
   change t with (projT1 foo).
   change t0 with (projT1 (projT2 foo)).
@@ -352,8 +351,9 @@ Proof.
   forward p.
   2:{ apply p. apply measure_wf, lt_wf. }
   clear p.
-  rename X16 into qt. rename X13 into Xcappexp.
-  rename X14 into Qprim. rename X15 into Qatom.
+  rename X17 into qt. rename X13 into Xcappexp.
+  rename X14 into Qprim. rename X15 into Qforce.
+  rename X16 into Qatom.
   clear t t0 qt H0.
   intros (t & t0 & qt & ev).
   intros IH.
@@ -379,7 +379,7 @@ Proof.
       eapply H; tea; (apply and_assum; [ih|hp' P'Q])
     end.
   destruct ev.
-  1-18:eapply qpres in qt as qt'; depelim qt' => //.
+  1-19:eapply qpres in qt as qt'; depelim qt' => //.
   - move/isEtaExp_tApp.
     destruct decompose_app as [hd args] eqn:da.
     destruct (construct_viewc hd) eqn:cv.
@@ -697,29 +697,44 @@ Proof.
       split; simp_eta. unshelve eapply Qprim. constructor; eauto. constructor.
       + apply All2_over_undep. cbn in IH.
         ELiftSubst.solve_all.
-        depelim H. destruct p as [[] ?].
+        depelim H0. destruct p as [[] a0].
         clear -ev IH a0 P'Q and_assum. cbn in a0. subst a; cbn in *.
         induction ev; constructor; eauto.
-        ** depelim a0. destruct p as [].
+        ** depelim a0. destruct p as [? []].
            eapply and_assum. unshelve eapply IH; tea. cbn. lia.
            intros []. split => //. split => //. eapply P'Q; tea.
         ** depelim a0. intuition eauto. eapply IHev; intros. 2:eauto.
            unshelve eapply IH; tea. cbn; lia.
-      + ELiftSubst.solve_all. depelim H; destruct p as [[] ?].
+      + ELiftSubst.solve_all. depelim H0. destruct p as [[? []] ?].
         eapply and_assum. unshelve eapply IH; tea. cbn; lia.
         intros []; split => //; split => //. eapply P'Q; tea.
       + ELiftSubst.solve_all. subst a a'; cbn in *.
-        depelim H; constructor; cbn in *; intuition eauto.
+        depelim H0; constructor; cbn in *; intuition eauto.
         unshelve eapply IH. 2:tea. all:eauto. cbn; lia.
         clear -ev IH b P'Q and_assum. cbn in b.
         induction ev; constructor; eauto.
-        ** depelim b. destruct p. unshelve eapply IH. 2:tea. all:eauto. cbn. lia.
+        ** depelim b. destruct p as [? []]. unshelve eapply IH. 2:tea. all:eauto. cbn. lia.
         ** depelim b. intuition eauto. eapply IHev; intros. 2:eauto.
            unshelve eapply IH; tea. cbn; lia.
- - intros ise. split => //. eapply Qatom; tea.
+  - simp_eta => ise.
+    eapply Qpres in qt. depelim qt => //.
+    assert (Q 0 (tLazy v)).
+    { eapply P'Q; tea. eapply (IH _ _ q ev1); tea. now cbn; lia. }
+    eapply qpres in X13. depelim X13 => //.
+    assert (isEtaExp Σ (tLazy v)) as etav.
+    { eapply (IH _ _ q ev1); tea. now cbn; lia. }
+    simp_eta in etav.
+    split.
+    + unshelve eapply Qforce. 2:tea. auto.
+      eapply and_assum. eapply (IH _ _ q ev1); tea. now cbn; lia.
+      intros []. split => //. split => //. eapply P'Q; tea.
+      pose proof (IH _ _ q ev1). forward X13. cbn; lia. specialize (X13 ise) as [].
+      eapply and_assum. eapply (IH _ _ q0 ev2); tea. now cbn; lia.
+      now simp_eta in i1.
+    + eapply (IH _ _ q0 ev2) => //. now cbn; lia.
+  - intros ise. split => //. eapply Qatom; tea.
 Qed.
 
-
 From MetaCoq.Erasure Require Import ELiftSubst.
 Lemma Qpreserves_wellformed (efl : EEnvFlags) Σ :
   cstr_as_blocks = false ->
diff --git a/erasure/theories/EWcbvEvalInd.v b/erasure/theories/EWcbvEvalInd.v
index 05328f1ef..8e0f365b2 100644
--- a/erasure/theories/EWcbvEvalInd.v
+++ b/erasure/theories/EWcbvEvalInd.v
@@ -238,7 +238,7 @@ Section eval_mkApps_rect.
                  then isFixApp f'
                  else isFix f') ||
                 isBox f' ||
-                isConstructApp f' || isPrimApp f'))
+                isConstructApp f' || isPrimApp f' || isLazyApp f'))
           (e0 : eval Σ a a'),
           P a a'
           → P (tApp f15 a)
@@ -246,12 +246,15 @@ Section eval_mkApps_rect.
 
    (forall p p' (ev : eval_primitive (eval Σ) p p'),
       eval_primitive_ind _ (fun x y _ => P x y) _ _ ev ->
-      P (tPrim p) (tPrim p'))
+      P (tPrim p) (tPrim p')) ->
 
+   (forall t t' v (ev1 : eval Σ t (tLazy t')) (ev2 : eval Σ t' v),
+      P t (tLazy t') -> P t' v ->
+      P (tForce t) v)
     → (∀ t : term, atom Σ t → P t t)
     → ∀ t t0 : term, eval Σ t t0 → P t t0.
 Proof using Type.
-  intros ?????????????????????? H.
+  intros ??????????????????????? H.
   pose proof (p := @Fix_F { t : _ & { t0 : _ & eval Σ t t0 }}).
   specialize (p (MR lt (fun x => eval_depth x.π2.π2))).
   set(foo := existT _ t (existT _ t0 H) :  { t : _ & { t0 : _ & eval Σ t t0 }}).
diff --git a/erasure/theories/EWcbvEvalNamed.v b/erasure/theories/EWcbvEvalNamed.v
index b495a1aae..0cb96358b 100644
--- a/erasure/theories/EWcbvEvalNamed.v
+++ b/erasure/theories/EWcbvEvalNamed.v
@@ -36,7 +36,8 @@ Inductive value : Set :=
 | vClos (na : ident) (b : term) (env : list (ident * value))
 | vConstruct (ind : inductive) (c : nat) (args : list (value))
 | vRecClos (b : list (ident * term)) (idx : nat) (env : list (ident * value))
-| vPrim (p : EPrimitive.prim_val value).
+| vPrim (p : EPrimitive.prim_val value)
+| vLazy (p : term) (env : list (ident * value)).
 
 Definition environment := list (ident * value).
 Definition add : ident -> value -> environment -> environment := fun (x : ident) (v : value) env =>
@@ -148,7 +149,14 @@ Section Wcbv.
 
   | eval_prim p p' :
     eval_primitive (eval Γ) p p' ->
-    eval Γ (tPrim p) (vPrim p').
+    eval Γ (tPrim p) (vPrim p')
+
+  | eval_lazy t : eval Γ (tLazy t) (vLazy t Γ)
+  | eval_force Γ' t t' v :
+    eval Γ t (vLazy t' Γ') ->
+    eval Γ' t' v ->
+    eval Γ (tForce t) v
+  .
 
   Program Definition eval_ind :=
     λ (P : ∀ (Γ : environment) (t : term) (v : value), eval Γ t v → Type) (f : ∀ (Γ : environment) (na : string) (v : value) (e : lookup Γ na = Some v),
@@ -247,7 +255,11 @@ Section Wcbv.
           P Γ (tConstruct ind c []) (vConstruct ind c []) (eval_construct_block_empty Γ ind c mdecl idecl cdecl e))
       (f10 : ∀ (Γ : environment) (p : prim_val term) (p' : prim_val value) (ev : eval_primitive (eval Γ) p p')
         (evih : eval_primitive_ind (eval Γ) (P Γ) _ _ ev),
-        P Γ (tPrim p) (vPrim p') (eval_prim _ _ _ ev)),
+        P Γ (tPrim p) (vPrim p') (eval_prim _ _ _ ev))
+      (f11 :∀ (Γ : environment) t, P Γ (tLazy t) (vLazy t Γ) (eval_lazy _ _))
+      (f12 : ∀ Γ Γ' t t' v (ev0 : eval Γ t (vLazy t' Γ')) (ev1 : eval Γ' t' v),
+        P _ _ _ ev0 -> P _ _ _ ev1 ->
+        P _ _ _ (eval_force _ _ _ _ _ ev0 ev1)),
       fix F (Γ : environment) (t : term) (v : value) (e : eval Γ t v) {struct e} : P Γ t v e :=
       match e as e0 in (eval _ t0 v0) return (P Γ t0 v0 e0) with
       | @eval_var _ na v0 e0 => f Γ na v0 e0
@@ -263,6 +275,8 @@ Section Wcbv.
       | @eval_construct_block _ ind c mdecl idecl cdecl args args' e0 l a => f8 Γ ind c mdecl idecl cdecl args args' e0 l a (map_All2_dep _ (F Γ) a)
       | @eval_construct_block_empty _ ind c mdecl idecl cdecl e0 => f9 Γ ind c mdecl idecl cdecl e0
       | @eval_prim _ p p' ev => f10 Γ p p' ev (map_eval_primitive (P := P Γ) (F Γ) ev)
+      | @eval_lazy _ t => f11 Γ t
+      | @eval_force _ Γ' t t' v ev ev' => f12 _ _ _ _ _ ev ev' (F Γ _ _ ev) (F Γ' _ _ ev')
       end.
 
 End Wcbv.
@@ -307,6 +321,7 @@ with represents_value : value -> term -> Set :=
 | represents_value_tFix vfix i E mfix :
   All2_Set (fun v d => isLambda (snd v) × (List.rev (map fst vfix) ;;; E ⊩ snd v ~ d.(dbody))) vfix mfix -> represents_value (vRecClos vfix i E) (tFix mfix i)
 | represents_value_tPrim p p' : onPrims represents_value p p' -> represents_value (vPrim p) (tPrim p')
+| represents_value_tLazy E t t' : [] ;;; E ⊩ t ~ t' -> represents_value (vLazy t E) (tLazy t')
 where "Γ ;;; E ⊩ s ~ t" := (represents Γ E s t).
 Derive Signature for represents represents_value.
 
@@ -413,7 +428,9 @@ Program Definition represents_ind :=
          P0 (vRecClos vfix i E) (tFix mfix i)
            (represents_value_tFix vfix i E mfix a))
      (f13 : forall p p' (o : onPrims represents_value p p'), onPrims_dep _ P0 _ _ o ->
-        P0 (vPrim p) (tPrim p') (represents_value_tPrim p p' o)),
+        P0 (vPrim p) (tPrim p') (represents_value_tPrim p p' o))
+    (f14 : forall E t t' (r : represents [] E t t'), P [] E t t' r ->
+      P0 (vLazy t E) (tLazy t') (represents_value_tLazy E t t' r)),
     fix F
       (l : list ident) (e : environment) (t t0 : term)
       (r : l;;; e ⊩ t ~ t0) {struct r} : P l e t t0 r :=
@@ -450,6 +467,7 @@ Program Definition represents_ind :=
           | represents_value_tConstruct vs ts ind c a => f11 vs ts ind c a _
           | represents_value_tFix vfix i E mfix a => f12 vfix i E mfix a _
           | represents_value_tPrim p p' r => f13 p p' r (map_onPrims F0 r)
+          | represents_value_tLazy E t t' r => f14 E t t' r (F [] E t t' r)
           end
             for
             F).
@@ -578,7 +596,9 @@ Program Definition represents_value_ind :=
          P0 (vRecClos vfix i E) (tFix mfix i)
            (represents_value_tFix vfix i E mfix a))
     (f13 : forall p p' (o : onPrims represents_value p p'), onPrims_dep _ P0 _ _ o ->
-           P0 (vPrim p) (tPrim p') (represents_value_tPrim p p' o)),
+           P0 (vPrim p) (tPrim p') (represents_value_tPrim p p' o))
+    (f14 : forall E t t' (r : represents [] E t t'), P [] E t t' r ->
+        P0 (vLazy t E) (tLazy t') (represents_value_tLazy E t t' r)),
 
     fix F
       (l : list ident) (e : environment) (t t0 : term)
@@ -617,6 +637,7 @@ Program Definition represents_value_ind :=
           | represents_value_tConstruct vs ts ind c a => f11 vs ts ind c a _
           | represents_value_tFix vfix i E mfix a => f12 vfix i E mfix a _
           | represents_value_tPrim p p' r => f13 p p' r (map_onPrims F0 r)
+          | represents_value_tLazy E t t' r => f14 E t t' r (F [] E t t' r)
           end
             for
             F0).
@@ -746,9 +767,10 @@ Definition rep_ind :=
            (represents_value_tFix vfix i E mfix a))
       (f13 : forall p p' (o : onPrims represents_value p p'), onPrims_dep _ P0 _ _ o ->
            P0 (vPrim p) (tPrim p') (represents_value_tPrim p p' o))
+      f14
            ,
-    (represents_ind P P0 f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 flazy fforce f10 f11 f12 f13,
-      represents_value_ind P P0 f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 flazy fforce f10 f11 f12 f13)).
+    (represents_ind P P0 f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 flazy fforce f10 f11 f12 f13 f14,
+      represents_value_ind P P0 f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 flazy fforce f10 f11 f12 f13 f14)).
 
 Local Notation "'⊩' v ~ s" := (represents_value v s) (at level 50).
 Local Hint Constructors represents : core.
@@ -1096,13 +1118,12 @@ Proof.
     repeat split. len. solve_all.
     destruct cstr_as_blocks; eauto.
     rtoProp; intuition eauto. solve_all. destruct args => //.
-  - destruct lookup_env as [ [] | ] eqn:E; cbn in *; eauto.
+  - move: H0; rewrite /wf_brs; cbn; destruct lookup_env as [ [] | ] eqn:E; cbn in *; eauto.
     erewrite lookup_annotate_env; eauto. cbn.
-    destruct nth_error as [ [] | ]; cbn in *; eauto.
-  - destruct lookup_env as [ [] | ] eqn:E; cbn in *; eauto.
-    destruct nth_error as [ [] | ]; cbn in *; eauto.
-    repeat split. eauto.
-    solve_all. rewrite length_map. rewrite <- length_app.
+    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.
     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.
@@ -1118,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 length_map.
+    rewrite map2_length gen_many_fresh_length map_length.
     { 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 ? [[] ].
@@ -1128,25 +1149,25 @@ Proof.
       }
       revert H2.
       generalize ((List.rev (gen_many_fresh Γ (map dname m)) ++ Γ)).
-      intros. rewrite map2_length gen_many_fresh_length length_map Nat.min_id.
+      intros. rewrite map2_length gen_many_fresh_length map_length 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 length_map.
+    rewrite map2_length gen_many_fresh_length map_length.
     { 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.length_rev length_app ?List.length_rev gen_many_fresh_length ?List.length_rev length_map. intros r.
+      revert i. rewrite ?List.rev_length app_length ?List.rev_length gen_many_fresh_length ?List.rev_length map_length. 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 length_map Nat.min_id.
+    intros. rewrite map2_length gen_many_fresh_length map_length Nat.min_id.
     revert H1. generalize (#|m| + #|Γ|).
     intros.
     induction m in Γ, n, n0, l, H1 |- *.
@@ -1226,7 +1247,7 @@ Lemma unfolds_bound :
   (forall Γ E s t, Γ ;;; E ⊩ s ~ t -> closedn #|Γ| t) ×
     (forall v s, ⊩ v ~ s -> closedn 0 s).
 Proof.
-  refine (rep_ind _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); intros; cbn; rtoProp; eauto.
+  refine (rep_ind _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); intros; cbn; rtoProp; eauto.
   - eapply Nat.ltb_lt, nth_error_Some. congruence.
   - eapply closed_upwards; eauto. lia.
   - solve_all. induction a; cbn in *; econstructor; firstorder.
@@ -1515,7 +1536,8 @@ Inductive wf : value -> Type :=
   All (fun t => sunny (map fst vfix ++ map fst E) (snd t)) vfix ->
   All (fun v => wf (snd v)) E ->
   wf (vRecClos vfix idx E)
-| wf_vPrim p : primProp wf p -> wf (vPrim p).
+| wf_vPrim p : primProp wf p -> wf (vPrim p)
+| wf_vLazy E t : sunny (map fst E) t -> All (fun v => wf (snd v)) E -> wf (vLazy t E).
 
 Lemma declared_constant_Forall P Σ c decl :
   Forall (P ∘ snd) Σ ->
@@ -1609,6 +1631,8 @@ Proof.
   - rtoProp; solve_all.
 Qed.
 
+Derive NoConfusion for value.
+
 Lemma eval_wf Σ E s v :
   Forall (fun d => match d.2 with ConstantDecl (Build_constant_body (Some d)) => sunny [] d | _ => true end) Σ ->
   All (fun x => wf (snd x)) E ->
@@ -1723,6 +1747,8 @@ Proof.
   - cbn. econstructor. econstructor.
   - econstructor. solve_all. depelim evih; depelim Hsunny; try subst a0 a'; cbn; constructor; cbn in *; intuition solve_all.
     eapply All2_over_undep in a. solve_all.
+  - econstructor; eauto.
+  - eapply X in HE; eauto. depelim HE. eapply X0; eauto.
 Qed.
 
 Lemma eval_construct_All2 Σ E ind c args vs mdecl idecl cdecl :
@@ -2154,6 +2180,12 @@ Proof.
         { clear -Hvs; induction Hvs; constructor; intuition eauto. }
       + constructor; eauto. eapply All2_All2_Set.
         { clear -Hvs; induction Hvs; constructor; intuition eauto. }
+  - invs Hrep; cbn in *; rtoProp. depelim H2.
+    apply s0 in H5 as [v' [reprev t1v]]; eauto.
+    depelim reprev.
+    eapply eval_wf in HΣ; tea. depelim HΣ.
+    eapply s1 in r as [v2 [reprv2 evv2]]; eauto.
+    exists v2. split => //. econstructor; eauto.
   - invs Hrep; cbn in *; try congruence; rtoProp.
     + econstructor. split; eauto. econstructor. eauto.
     + econstructor. split; eauto. econstructor.
@@ -2170,8 +2202,8 @@ Proof.
       intros.
       cbn in *. destruct H5 as (([? []] & ?) & ?).
       rewrite app_nil_r in r. all: eauto.
-
-      Unshelve. all: repeat econstructor.
+    + exists (vLazy t1 E). now split; econstructor.
+  Unshelve. all: repeat econstructor.
 Qed.
 
 Lemma concat_sing {X} l :
diff --git a/erasure/theories/EWellformed.v b/erasure/theories/EWellformed.v
index 0ad7268a3..1285b158d 100644
--- a/erasure/theories/EWellformed.v
+++ b/erasure/theories/EWellformed.v
@@ -110,7 +110,8 @@ Section wf.
     - all occuring constructors are defined,
     - all occuring constants are defined, and
     - all occuring fixpoints have lambdas as bodies
-    - if has_axioms is false, all occuring constants have bodies *)
+    - if has_axioms is false, all occuring constants have bodies
+    - all cases are exhaustive w.r.t the global declaration *)
 
   Definition wf_fix_gen (wf : nat -> term -> bool) k mfix idx :=
     let k' := List.length mfix + k in
@@ -118,6 +119,12 @@ Section wf.
 
   Definition is_nil {A} (l : list A) := match l with [] => true | _ => false end.
 
+  Definition wf_brs ind brsl :=
+    match lookup_inductive Σ ind with
+    | Some (mib, oib) => #|oib.(ind_ctors)| == brsl
+    | None => false
+    end.
+
   Fixpoint wellformed k (t : term) : bool :=
     match t with
     | tRel i => has_tRel && Nat.ltb i k
@@ -127,7 +134,7 @@ Section wf.
     | tLetIn na b b' => has_tLetIn && wellformed k b && wellformed (S k) b'
     | tCase ind c brs => has_tCase &&
       let brs' := List.forallb (fun br => wellformed (#|br.1| + k) br.2) brs in
-      isSome (lookup_inductive Σ ind.1) && wellformed k c && brs'
+      wf_brs ind.1 #|brs| && wellformed k c && brs'
     | tProj p c => has_tProj && isSome (lookup_projection Σ p) && wellformed k c
     | tFix mfix idx => has_tFix && List.forallb (isLambda ∘ dbody) mfix && wf_fix_gen wellformed k mfix idx
     | tCoFix mfix idx => has_tCoFix && wf_fix_gen wellformed k mfix idx
@@ -443,6 +450,19 @@ Proof.
   intros wfΣ' Hl; apply Hl.
 Qed.
 
+
+Lemma extends_lookup_inductive {efl} {Σ Σ'} :
+  wf_glob Σ' -> extends Σ Σ' ->
+  forall ind b, lookup_inductive Σ ind = Some b ->
+    lookup_inductive Σ' ind = Some b.
+Proof.
+  intros wf ex ind b.
+  rewrite /lookup_inductive /lookup_minductive.
+  destruct lookup_env eqn:lookup => //=.
+  now rewrite (extends_lookup wf ex lookup).
+Qed.
+
+
 Lemma extends_lookup_constructor {efl} {Σ Σ'} :
   wf_glob Σ' -> extends Σ Σ' ->
   forall ind c b, lookup_constructor Σ ind c = Some b ->
@@ -485,6 +505,8 @@ Proof.
   all:try destruct g => //.
   - destruct cstr_as_blocks; eauto; solve_all.
     destruct lookup_constructor_pars_args as [ [] | ]; rtoProp; repeat solve_all.
+  - move: H0. rewrite /wf_brs. destruct lookup_inductive eqn:hl => //.
+    now rewrite (extends_lookup_inductive wf ex _ _ hl).
   - move/andP: H0 => [] hn hf. unfold wf_fix. rewrite hn /=. solve_all.
   - move/andP: H0 => [] hn hf. unfold wf_fix. rewrite hn /=. solve_all.
 Qed.
diff --git a/erasure/theories/ErasureCorrectness.v b/erasure/theories/ErasureCorrectness.v
index db6bc66a7..a53593a34 100644
--- a/erasure/theories/ErasureCorrectness.v
+++ b/erasure/theories/ErasureCorrectness.v
@@ -40,6 +40,14 @@ Notation "Σ ⊢ s ⇓ t" := (EWcbvEval.eval Σ s t) (at level 50, s, t at next
 
 Import ssrbool.
 
+Lemma erases_lazy Σ Γ t t' : Σ ;;; Γ |- t ⇝ℇ t' -> EAstUtils.isLazyApp t' -> False.
+Proof.
+  rewrite /EAstUtils.isLazyApp /EAstUtils.head /EAstUtils.decompose_app.
+  generalize (@nil EAst.term) as l; intros l.
+  induction 1 in l |- *; cbn => //=.
+  eapply IHerases1.
+Qed.
+
 Lemma erases_correct (wfl := default_wcbv_flags) Σ t t' v Σ' :
   wf_ext Σ ->
   welltyped Σ [] t ->
@@ -187,9 +195,10 @@ Proof.
   eapply Construct_Ind_ind_eq in X0; tea. 2:{ eapply declared_constructor_from_gen; tea. }
   destruct X0 as (((([_ Ru] & cu) & cpu) & ?) & (parsubst & argsubst & parsubst' & argsubst' & [])).
   invs He.
-  + depelim Hed.
+  + depelim Hed. rename H5 into Hlen.
     rename H1 into decli. rename H2 into decli'.
     rename H3 into em. rename Hed into er.
+    rename H6 into H5. rename H7 into H6. rename H8 into H7.
     edestruct (IHeval1 _ scrut_ty) as (v' & Hv' & [He_v']); eauto.
     pose proof e0 as Hnth.
     assert (lenppars : ind_npars mdecl = #|pparams p|).
@@ -830,7 +839,9 @@ Proof.
     2:{ now eapply nth_error_all in a; tea. }
     invs He.
     * edestruct IHeval1 as (? & ? & ?); eauto. now depelim Hed.
-      depelim Hed.
+      depelim Hed. rename H5 into Hlen.
+      rename H6 into H5. rename H7 into H6. rename H8 into H7.
+      rename H9 into H8. rename H10 into H9.
       unshelve eapply declared_inductive_to_gen in H1, decli; eauto.
       destruct (declared_inductive_inj H1 decli). subst mdecl0 idecl0.
       rename H0 into decli'. rename H1 into decli''. rename H2 into er. rename H3 into H0.
@@ -1150,6 +1161,10 @@ Proof.
         -- rewrite !negb_or in i. rtoProp; intuition auto.
            eapply is_PrimApp_erases in H8; tea.
            now move/negbTE: H8.
+        -- rewrite !negb_or in i.
+           rtoProp; intuition auto.
+           apply/negbTE. apply PCUICNormal.negb_is_true => isl.
+           eapply erases_lazy in H1; tea.
     + exists EAst.tBox. split. 2: now constructor; econstructor.
       econstructor.
       eapply inversion_App in Hty as [na [A [B [Hf [Ha _]]]]]; auto.
@@ -1358,7 +1373,7 @@ Proof.
     depelim etaΣ.
     eauto.
     depelim etaΣ.
-    solve_all. rewrite -b2. len. eapply H7 => //.
+    solve_all. rewrite -b2. len. eapply H8 => //.
     exact a0.
   - intros Γ0 v etaΣ.
     move=> /erases_mkApps_inv; intros [(?&?&?&?&_&?&?&?)|(?&?&?&?&?)]; subst.
diff --git a/erasure/theories/ErasureFunction.v b/erasure/theories/ErasureFunction.v
index 89edfe784..6a1658d13 100644
--- a/erasure/theories/ErasureFunction.v
+++ b/erasure/theories/ErasureFunction.v
@@ -169,6 +169,7 @@ Proof.
   - destruct p. rewrite KernameSet.union_spec knset_in_fold_left in H0.
     destruct H0.
     apply KernameSet.singleton_spec in H0. subst kn. cbn in *.
+    move: H1; rewrite /EWellformed.wf_brs; cbn.
     destruct (EGlobalEnv.lookup_env Σ _) eqn:E.
     destruct g => //.
     now eapply lookup_env_In in E. easy. clear H1.
diff --git a/erasure/theories/ErasureFunctionProperties.v b/erasure/theories/ErasureFunctionProperties.v
index 596d44a31..534663095 100644
--- a/erasure/theories/ErasureFunctionProperties.v
+++ b/erasure/theories/ErasureFunctionProperties.v
@@ -245,6 +245,9 @@ Proof.
     eapply erases_deps_tCase; eauto.
     apply declared_inductive_from_gen; auto.
     split; eauto. split; eauto.
+    apply All2_length in X. rewrite -X.
+    destruct H5. apply Forall2_length in H5. rewrite -H5.
+    now apply Forall2_length in wf_brs.
     destruct H1.
     eapply In_Forall in H3.
     eapply All_Forall. eapply Forall_All in H3.
@@ -350,6 +353,7 @@ Proof.
     eapply extends_decls_extends, strictly_extends_decls_extends_decls. econstructor; try reflexivity. eexists [(_, _)]; reflexivity.
   - econstructor; eauto.
     eapply declared_inductive_from_gen.
+    rename H3 into Hlen, H4 into H3, H5 into H4.
     inv wfΣ. inv X.
     assert (wf Σ) by (inversion H5;econstructor; eauto).
     unshelve eapply declared_inductive_to_gen in H; eauto.
@@ -1451,11 +1455,11 @@ Proof.
   - cbn. red in H0. rewrite H0 //.
   - cbn -[lookup_constructor].
     cbn. now destruct H0 as [[-> ->] ->].
-  - cbn in *. move/andP: H5 => [] cld clbrs.
+  - cbn in *. move/andP: H6 => [] cld clbrs.
     cbn. apply/andP; split. apply/andP; split.
-    * now destruct H0 as [-> ->].
-    * now move/andP: H6.
-    * move/andP: H6; PCUICAstUtils.solve_all.
+    * rewrite /wf_brs. cbn. destruct H0 as [-> ->]. now apply Nat.eqb_eq.
+    * now move/andP: H7.
+    * move/andP: H7; PCUICAstUtils.solve_all.
   - cbn -[lookup_projection] in *. apply/andP; split; eauto.
     now rewrite (declared_projection_lookup H0).
   - cbn in H, H0 |- *. rtoProp; intuition eauto. solve_all_k 7.
diff --git a/erasure/theories/ErasureProperties.v b/erasure/theories/ErasureProperties.v
index ca1bc5910..d1a385c1d 100644
--- a/erasure/theories/ErasureProperties.v
+++ b/erasure/theories/ErasureProperties.v
@@ -475,6 +475,12 @@ Section wellscoped.
   Context (Σ : global_env).
   Import ssrbool.
 
+  Definition wf_brs ind brsl :=
+    match lookup_inductive Σ ind with
+    | Some (mib, oib) => #|oib.(ind_ctors)| == brsl
+    | None => false
+    end.
+
   Fixpoint wellformed (t : term) : bool :=
   match t with
   | tRel i => true
@@ -485,7 +491,7 @@ Section wellscoped.
   | tLetIn na b ty b' => wellformed b && wellformed ty && wellformed b'
   | tCase ind p c brs =>
     let brs' := forallb (wellformed ∘ bbody) brs in
-    isSome (lookup_inductive Σ ind.(ci_ind)) && wellformed c && brs'
+    wf_brs ind.(ci_ind) #|brs| && wellformed c && brs'
   | tProj p c => isSome (lookup_projection Σ p) && wellformed c
   | tFix mfix idx =>
     (idx <? #|mfix|) &&
@@ -518,7 +524,9 @@ Section wellscoped.
     - unshelve eapply declared_constructor_to_gen in isdecl; eauto.
       unfold lookup_constructor. rewrite (declared_constructor_lookup_gen isdecl) //.
     - unshelve eapply declared_inductive_to_gen in isdecl; eauto.
-      unfold lookup_inductive. now rewrite (declared_inductive_lookup_gen isdecl).
+      rewrite /wf_brs.
+      unfold lookup_inductive. rewrite (declared_inductive_lookup_gen isdecl).
+      red in H8. apply Forall2_length in H8. now apply Nat.eqb_eq.
     - red in H8. eapply Forall2_All2 in H8.
       eapply All2i_All2_mix_left in X4; tea. clear H8.
       solve_all.
@@ -557,14 +565,19 @@ Section trans_lookups.
     erewrite EGlobalEnv.declared_constant_lookup; eauto.
   Qed.
 
-  Lemma trans_lookup_inductive kn : isSome (lookup_inductive Σ kn) -> isSome (EGlobalEnv.lookup_inductive Σ' kn).
-  Proof using g.
-    destruct g.
-    destruct (lookup_inductive Σ kn) as [[]|] eqn:hl => /= // _.
+  Lemma trans_lookup_inductive kn mib oib :
+    lookup_inductive Σ kn = Some (mib, oib) ->
+    exists mib' oib', EGlobalEnv.lookup_inductive Σ' kn = Some (mib', oib') /\ #|oib.(ind_ctors)| = #|oib'.(EAst.ind_ctors)|.
+  Proof. destruct g.
+    destruct (lookup_inductive Σ kn) as [[]|] eqn:hl => /= // [=]. intros -> ->.
     eapply lookup_inductive_declared in hl.
     eapply declared_inductive_from_gen in hl.
-    specialize (H0 kn m o hl) as [? [? [d _]]].
-    now rewrite (EGlobalEnv.declared_inductive_lookup d).
+    specialize (H0 kn mib oib hl) as [? [? [d er]]].
+    exists x, x0.
+    split. now rewrite (EGlobalEnv.declared_inductive_lookup d).
+    depelim er. depelim hl. depelim d.
+    eapply Forall2_nth_error_left in H4 as [x' []]; tea.
+    rewrite H3 in H4. noconf H4. depelim H6. now apply Forall2_length in H4.
   Qed.
 
   Lemma trans_lookup_constructor kn c : isSome (lookup_constructor Σ kn c) -> isSome (EGlobalEnv.lookup_constructor Σ' kn c).
@@ -636,7 +649,11 @@ Proof.
   - eapply trans_lookup_constructor in wfa; tea. now rewrite wfa.
   - move/andP: wfa => [] /andP[] lookup wfc wfbrs.
     apply/andP. split. apply/andP. split; eauto.
-    eapply trans_lookup_inductive; tea.
+    { rewrite /wf_brs.
+      move: lookup. rewrite /ErasureProperties.wf_brs.
+      destruct lookup_inductive as [[mib oib]|] eqn:hli => //.
+      eapply trans_lookup_inductive in hli as [mib' [oib' [-> <-]]]; tea.
+      move/Nat.eqb_eq ->. apply All2_length in X1. now apply Nat.eqb_eq. }
     eapply All_forallb. unfold tCaseBrsProp_k in X0.
     eapply All2_All_mix_left in X1; eauto.
     eapply forallb_All in wfbrs.
diff --git a/erasure/theories/Extract.v b/erasure/theories/Extract.v
index c5ca0ec26..3cb455005 100644
--- a/erasure/theories/Extract.v
+++ b/erasure/theories/Extract.v
@@ -339,6 +339,7 @@ Inductive erases_deps (Σ : global_env) (Σ' : E.global_declarations) : E.term -
     erases_mutual_inductive_body mdecl mdecl' ->
     erases_one_inductive_body idecl idecl' ->
     erases_deps Σ Σ' discr ->
+    #|EAst.ind_ctors idecl'| = #|brs| ->
     Forall (fun br => erases_deps Σ Σ' br.2) brs ->
     erases_deps Σ Σ' (E.tCase p discr brs)
 | erases_deps_tProj p mdecl idecl cdecl pdecl mdecl' idecl' cdecl' pdecl' t :
diff --git a/erasure/theories/Typed/OptimizeCorrectness.v b/erasure/theories/Typed/OptimizeCorrectness.v
index b650b78b6..c4a58f8ac 100644
--- a/erasure/theories/Typed/OptimizeCorrectness.v
+++ b/erasure/theories/Typed/OptimizeCorrectness.v
@@ -2017,6 +2017,8 @@ Proof.
   - depelim X; auto.
     eapply All2_over_undep in a. eapply All2_Set_All2 in ev. solve_all. subst a0 a'; cbn in *.
     depelim exp_t; constructor; cbn in *; intuition eauto. solve_all.
+  - eapply IHev1 in exp_t. eapply IHev2 in exp_t.
+    eapply is_expanded_aux_upwards; tea. lia.
 Qed.
 
 Lemma valid_case_masks_lift ind c brs n k :
@@ -2823,6 +2825,7 @@ Proof with auto with dearg.
   - depelim X; auto.
     eapply All2_over_undep in a. eapply All2_Set_All2 in ev. subst a0 a'; cbn -[test_prim] in *.
     solve_all. depelim H0; constructor; cbn; intuition eauto. solve_all.
+  - eapply IHev2. eapply eval_closed in ev1; tea. eapply IHev1; eauto.
 Qed.
 
 Lemma declared_constant_dearg Σ k cst :
@@ -3452,22 +3455,22 @@ Section dearg.
           cbn in *; propify.
           rewrite dearg_single_masked by (now rewrite length_map).
           rewrite isLambda_mkApps, isFixApp_mkApps, isBox_mkApps, isConstructApp_mkApps;cbn in *.
-          rewrite isPrimApp_mkApps.
-          destruct with_guarded_fix;cbn;auto.
+          rewrite isPrimApp_mkApps, isLazyApp_mkApps in *.
+          destruct with_guarded_fix;cbn;intuition auto.
           now rewrite EOptimizePropDiscr.isFix_mkApps;cbn.
         * rewrite isLambda_mkApps, isFixApp_mkApps, isBox_mkApps, isConstructApp_mkApps in *;cbn in *.
           propify.
           destruct with_guarded_fix;cbn in *; intuition.
         * unfold dearg_case.
           destruct with_guarded_fix;cbn.
-          now rewrite isLambda_mkApps, isFixApp_mkApps, isBox_mkApps, isConstructApp_mkApps, isPrimApp_mkApps;cbn.
-          now rewrite isLambda_mkApps, isBox_mkApps, isConstructApp_mkApps, EOptimizePropDiscr.isFix_mkApps, isPrimApp_mkApps;cbn.
+          now rewrite isLambda_mkApps, isFixApp_mkApps, isBox_mkApps, isConstructApp_mkApps, isPrimApp_mkApps, isLazyApp_mkApps;cbn.
+          now rewrite isLambda_mkApps, isBox_mkApps, isConstructApp_mkApps, EOptimizePropDiscr.isFix_mkApps, isPrimApp_mkApps, isLazyApp_mkApps;cbn.
         * unfold dearg_proj.
           unfold dearg_case.
           destruct with_guarded_fix;cbn.
-          ** now rewrite isLambda_mkApps, isFixApp_mkApps, isBox_mkApps, isConstructApp_mkApps, isPrimApp_mkApps;cbn.
-          ** now rewrite isLambda_mkApps, isBox_mkApps, isConstructApp_mkApps, EOptimizePropDiscr.isFix_mkApps, isPrimApp_mkApps;cbn.
-        * rewrite !isLambda_mkApps, !isFixApp_mkApps, !EOptimizePropDiscr.isFix_mkApps, !isBox_mkApps, isConstructApp_mkApps, isPrimApp_mkApps in *
+          ** now rewrite isLambda_mkApps, isFixApp_mkApps, isBox_mkApps, isConstructApp_mkApps, isPrimApp_mkApps, isLazyApp_mkApps;cbn.
+          ** now rewrite isLambda_mkApps, isBox_mkApps, isConstructApp_mkApps, EOptimizePropDiscr.isFix_mkApps, isPrimApp_mkApps, isLazyApp_mkApps;cbn.
+        * rewrite !isLambda_mkApps, !isFixApp_mkApps, !EOptimizePropDiscr.isFix_mkApps, !isBox_mkApps, isConstructApp_mkApps, isPrimApp_mkApps, isLazyApp_mkApps in *
             by now destruct hd.
           rewrite length_map.
           destruct with_guarded_fix;cbn;auto;
@@ -3608,6 +3611,7 @@ Section dearg.
       erewrite lookup_ctor_trans_env_inv; tea.
     - destruct p. rewrite wellformed_mkApps; try easy.
       unfold dearg_case.
+      rewrite /wf_brs in H.
       destruct (EGlobalEnv.lookup_inductive _ _) as [[mib oib]|] eqn:hl => //.
       assert (decl_ind :declared_inductive (trans_env Σ) i mib oib).
       { move: hl. unfold EGlobalEnv.lookup_inductive. cbn.
@@ -3616,15 +3620,18 @@ Section dearg.
       specialize (valid_ind_mask_inductive _ _ _ _ valid_Σ decl_ind) as [mask [Hmask Hparams]].
       rewrite Hmask.
       rtoProp; intuition eauto; solve_all.
-      cbn [wellformed]. rtoProp; intuition eauto.
+      cbn [wellformed]. rtoProp; intuition eauto. len.
+      rewrite mapi_length map_length. rewrite /wf_brs.
       { unfold EGlobalEnv.lookup_inductive. cbn.
         move: hl. cbn.
         rewrite !lookup_env_trans_env lookup_env_dearg_env.
         destruct lookup_env => //=. destruct g => //=.
         rewrite !nth_error_map. unfold dearg_mib. rewrite Hmask. cbn.
-        rewrite nth_error_mapi. destruct nth_error => //. }
+        rewrite nth_error_mapi. destruct nth_error => //=.
+        intros [= <- <-].
+        move: H; cbn. now rewrite /trans_ctors !map_length !mapi_length. }
       cbn.
-      unfold mapi. clear clos_args IHt.
+      unfold mapi. clear clos_args IHt H.
       unfold valid_case_masks in H3. rewrite Hmask in H3.
       move/andP: H3 => [] _ hbrs.
       eapply alli_Alli in hbrs.
@@ -4970,6 +4977,9 @@ Proof.
       unshelve eapply IHb0; tea. cbn in deriv_len. lia.
       cbn in *; unfold test_array_model in *; subst a a'; cbn in *.
       unshelve eapply IH; tea; rtoProp; intuition eauto. lia.
+    + facts. econstructor. specialize (IH _ _ clos_t valid_t exp_t ev1).
+      cbn in IH. apply IH. lia.
+      now forward (IH v _ H2 H4 H6 ev2).
     + destruct t; cbn in *; try destruct y; try congruence; now constructor.
 Qed.
 End dearg_correct.
diff --git a/erasure/theories/Typed/WcbvEvalAux.v b/erasure/theories/Typed/WcbvEvalAux.v
index 616729500..4ab082134 100644
--- a/erasure/theories/Typed/WcbvEvalAux.v
+++ b/erasure/theories/Typed/WcbvEvalAux.v
@@ -307,6 +307,7 @@ Fixpoint deriv_length {Σ t v} (ev : Σ e⊢ t ⇓ v) : nat :=
       S (deriv_length ev1 + deriv_length ev2 + deriv_length ev3)
   | eval_construct_block _ _ _ _ _ args _ _ _ _ _ => S #|args|
   | eval_prim _ _ ev => S (eval_prim_length (@deriv_length _) ev)
+  | eval_force _ _ _ ev ev' => S (deriv_length ev + deriv_length ev')
   end.
 
 Lemma deriv_length_min {Σ t v} (ev : Σ e⊢ t ⇓ v) :
diff --git a/examples/metacoq_tour.v b/examples/metacoq_tour.v
index 3830aa3de..5b5ba9c1c 100644
--- a/examples/metacoq_tour.v
+++ b/examples/metacoq_tour.v
@@ -99,7 +99,7 @@ From MetaCoq.ErasurePlugin Require Import Erasure Loader.
 
 (** Running erasure live in Coq *)
 Definition test (p : Ast.Env.program) : string :=
-  erase_and_print_template_program default_erasure_config p.
+  erase_and_print_template_program default_erasure_config [] p.
 
 MetaCoq Quote Recursively Definition zero := 0.
 
diff --git a/make-opam-files.sh b/make-opam-files.sh
index f448ac508..38bbba529 100755
--- a/make-opam-files.sh
+++ b/make-opam-files.sh
@@ -33,15 +33,20 @@ gh release upload $tag $archive
 
 release=https://github.com/MetaCoq/metacoq/releases/download/$tag/$archive
 
+skipline=""
+
 for f in *.opam;
 do
     opamf=${f/.opam/};
     target=$1/$opamf/$opamf.$2/opam;
     echo $opamf;
     mkdir -p $1/$opamf/$opamf.$2
+    skipline="$skipline $opamf.$2"
     gsed -e "/^version:.*/d" $f > $target
     echo url { >> $target
     echo "  src:" \"$release\" >> $target
     echo "  checksum:" \"sha512=$hash\" >> $target
     echo } >> $target
-done
\ No newline at end of file
+done
+
+echo "ci-skip:" $skipline
\ No newline at end of file
diff --git a/test-suite/erasure_live_test.v b/test-suite/erasure_live_test.v
index d9796c1f1..97c5c67e3 100644
--- a/test-suite/erasure_live_test.v
+++ b/test-suite/erasure_live_test.v
@@ -18,14 +18,11 @@ Unset MetaCoq Debug.
 #[local] Existing Instance config.extraction_checker_flags.
 
 Definition test (p : Ast.Env.program) : string :=
-  erase_and_print_template_program default_erasure_config p.
+  erase_and_print_template_program default_erasure_config [] p.
 
 Definition testty (p : Ast.Env.program) : string :=
   typed_erase_and_print_template_program p.
 
-Definition test_fast (p : Ast.Env.program) : string :=
-  erase_fast_and_print_template_program p.
-
 MetaCoq Quote Recursively Definition zero := 0.
 
 Definition zerocst := Eval lazy in test zero.
@@ -53,12 +50,7 @@ Definition singlelim := ((fun (X : Set) (x : X) (e : x = x) =>
 
 Definition erase {A} (a : A) : TemplateMonad unit :=
   aq <- tmQuoteRec a ;;
-  s <- tmEval lazy (erase_and_print_template_program default_erasure_config aq) ;;
-  tmMsg s.
-
-Definition erase_fast {A} (a : A) : TemplateMonad unit :=
-  aq <- tmQuoteRec a ;;
-  s <- tmEval lazy (erase_fast_and_print_template_program aq) ;;
+  s <- tmEval lazy (erase_and_print_template_program default_erasure_config [] aq) ;;
   tmMsg s.
 
 MetaCoq Run (erase 0).
@@ -80,7 +72,13 @@ Definition vplus0123 := (vplus v01 v23).
 Set MetaCoq Timing.
 
 Time MetaCoq Run (tmEval hnf vplus0123 >>= erase).
-Time MetaCoq Run (tmEval hnf vplus0123 >>= erase_fast).
+
+(** Cofix *)
+From Coq Require Import StreamMemo.
+
+MetaCoq Quote Recursively Definition memo := memo_make.
+
+Definition testmemo := Eval lazy in test memo.
 
 (** Cofix *)
 From Coq Require Import StreamMemo.
@@ -352,7 +350,7 @@ MetaCoq Quote Recursively Definition cbv_provedCopyx :=
 Definition ans_provedCopyx :=
   Eval lazy in (test cbv_provedCopyx).
 MetaCoq Quote Recursively Definition p_provedCopyx := provedCopyx. (* program *)
-Time Definition P_provedCopyx := Eval lazy in (test_fast cbv_provedCopyx).
+Time Definition P_provedCopyx := Eval lazy in (test cbv_provedCopyx).
 (* We don't run this one every time as it is really expensive *)
 (*Time Definition P_provedCopyxvm := Eval vm_compute in (test p_provedCopyx).*)