From 4d7bc44c7888f296b3b5b46267b21bc11f3faa99 Mon Sep 17 00:00:00 2001
From: Yannick Forster <yannick.forster@inria.fr>
Date: Thu, 6 Jul 2023 08:06:27 +0200
Subject: [PATCH] split out verified erasure pipeline

---
 Makefile                                   |   3 +-
 erasure-plugin/theories/ETransform.v       |  12 +-
 erasure-plugin/theories/Erasure.v          |  58 +++-
 erasure/theories/EOptimizePropDiscr.v      | 334 ++++++++++-----------
 erasure/theories/EWcbvEvalNamed.v          | 160 +++++++++-
 erasure/theories/Typed/Extraction.v        |   2 +-
 erasure/theories/Typed/OptimizePropDiscr.v |  34 +--
 erasure/theories/Typed/TypeAnnotations.v   |  30 +-
 8 files changed, 403 insertions(+), 230 deletions(-)

diff --git a/Makefile b/Makefile
index a99854e73..e16daadc8 100644
--- a/Makefile
+++ b/Makefile
@@ -1,5 +1,5 @@
 
-all: printconf template-coq pcuic safechecker erasure examples test-suite translations quotation
+all: printconf template-coq pcuic safechecker erasure 
 
 -include Makefile.conf
 
@@ -37,7 +37,6 @@ install: all translations
 	$(MAKE) -C safechecker-plugin install
 	$(MAKE) -C erasure install
 	$(MAKE) -C erasure-plugin install
-	$(MAKE) -C translations install
 
 uninstall:
 	$(MAKE) -C utils uninstall
diff --git a/erasure-plugin/theories/ETransform.v b/erasure-plugin/theories/ETransform.v
index 822730bdd..521481293 100644
--- a/erasure-plugin/theories/ETransform.v
+++ b/erasure-plugin/theories/ETransform.v
@@ -358,23 +358,23 @@ Qed.
 
 Import EOptimizePropDiscr EWcbvEval.
 
-Program Definition optimize_prop_discr_optimization {fl : WcbvFlags} {wcon : with_constructor_as_block = false} {efl : EEnvFlags} {hastrel : has_tRel} {hastbox : has_tBox} :
+Program Definition remove_match_on_box_trans {fl : WcbvFlags} {wcon : with_constructor_as_block = false} {efl : EEnvFlags} {hastrel : has_tRel} {hastbox : has_tBox} :
   Transform.t eprogram_env eprogram EAst.term EAst.term (eval_eprogram_env fl) (eval_eprogram (disable_prop_cases fl)) :=
   {| name := "optimize_prop_discr";
-    transform p _ := optimize_program p ;
+    transform p _ := remove_match_on_box_program p ;
     pre p := wf_eprogram_env efl p /\ EEtaExpanded.expanded_eprogram_env_cstrs p;
     post p := wf_eprogram efl p /\ EEtaExpanded.expanded_eprogram_cstrs p;
-    obseq g g' v v' := v' = EOptimizePropDiscr.optimize g.1 v |}.
+    obseq g g' v v' := v' = EOptimizePropDiscr.remove_match_on_box g.1 v |}.
 
 Next Obligation.
   move=> fl wcon efl hastrel hastbox [Σ t] [wfp etap].
   cbn in *. split.
-  - now eapply optimize_program_wf.
-  - now eapply optimize_program_expanded.
+  - now eapply remove_match_on_box_program_wf.
+  - now eapply remove_match_on_box_program_expanded.
 Qed.
 Next Obligation.
   red. move=> fl wcon efl hastrel hastbox [Σ t] /= v [wfe wft] [ev].
-  eapply EOptimizePropDiscr.optimize_correct in ev; eauto.
+  eapply EOptimizePropDiscr.remove_match_on_box_correct in ev; eauto.
   eexists; split => //. red. sq; auto. cbn. apply wfe.
   eapply wellformed_closed_env, wfe.
   eapply wellformed_closed, wfe.
diff --git a/erasure-plugin/theories/Erasure.v b/erasure-plugin/theories/Erasure.v
index 05789e1c6..567ca5f4f 100644
--- a/erasure-plugin/theories/Erasure.v
+++ b/erasure-plugin/theories/Erasure.v
@@ -57,10 +57,10 @@ Next Obligation.
   apply assume_preservation_template_program_env_expansion in ev as [ev']; eauto.
 Qed.
 
-Program Definition erasure_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) :
- Transform.t TemplateProgram.template_program EProgram.eprogram
-  Ast.term EAst.term
-  TemplateProgram.eval_template_program
+Program Definition verified_erasure_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) :
+ Transform.t pcuic_program EProgram.eprogram
+  PCUICAst.term EAst.term
+  PCUICTransform.eval_pcuic_program
   (EProgram.eval_eprogram {| with_prop_case := false; with_guarded_fix := false; with_constructor_as_block := true |}) :=
   (* a bunch of nonsense for normalization preconditions *)
   let K ty (T : ty -> _) p
@@ -68,15 +68,6 @@ Program Definition erasure_pipeline {guard : abstract_guard_impl} (efl := EWellf
        (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 an efficient lookup map for the following eta-expansion phase *)
-  build_template_program_env (K _ T4) ▷
-  (* Eta-expand constructors and fixpoint *)
-  eta_expand (K _ T3) ▷
-  (* Casts are removed, application is binary, case annotations are inferred from the global environment *)
-  template_to_pcuic_transform (K _ T2) ▷
   (* Branches of cases are expanded to bind only variables, constructor types are expanded accordingly *)
   pcuic_expand_lets_transform (K _ T1) ▷
   (* Erasure of proofs terms in Prop and types *)
@@ -90,7 +81,7 @@ Program Definition erasure_pipeline {guard : abstract_guard_impl} (efl := EWellf
   (* Rebuild the efficient lookup table *)
   rebuild_wf_env_transform (efl := ERemoveParams.switch_no_params EWellformed.all_env_flags) true ▷
   (* Remove all cases / projections on propositional content *)
-  optimize_prop_discr_optimization (efl := ERemoveParams.switch_no_params EWellformed.all_env_flags) (wcon := eq_refl) (hastrel := eq_refl) (hastbox := eq_refl) ▷
+  remove_match_on_box_trans (efl := ERemoveParams.switch_no_params EWellformed.all_env_flags) (wcon := eq_refl) (hastrel := eq_refl) (hastbox := eq_refl) ▷
   (* Rebuild the efficient lookup table *)
   rebuild_wf_env_transform (efl := ERemoveParams.switch_no_params EWellformed.all_env_flags) true  ▷
   (* Inline projections to cases *)
@@ -114,6 +105,43 @@ Next Obligation.
   now eapply ETransform.expanded_eprogram_env_expanded_eprogram_cstrs.
 Qed.
 
+Program Definition pre_erasure_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) :
+ Transform.t TemplateProgram.template_program pcuic_program
+  Ast.term PCUICAst.term
+  TemplateProgram.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
+       (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 an efficient lookup map for the following eta-expansion phase *)
+  build_template_program_env (K _ T4) ▷
+  (* Eta-expand constructors and fixpoint *)
+  eta_expand (K _ T3) ▷
+  (* Casts are removed, application is binary, case annotations are inferred from the global environment *)
+  template_to_pcuic_transform (K _ T2).
+
+Program Definition erasure_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) :
+ Transform.t TemplateProgram.template_program EProgram.eprogram
+  Ast.term EAst.term
+  TemplateProgram.eval_template_program
+  (EProgram.eval_eprogram {| with_prop_case := false; with_guarded_fix := false; with_constructor_as_block := true |}) :=
+  pre_erasure_pipeline ▷
+  verified_erasure_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 run_erase_program {guard : abstract_guard_impl} := run erasure_pipeline.
 
 Program Definition erasure_pipeline_fast {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) :=
@@ -134,7 +162,7 @@ Program Definition erasure_pipeline_fast {guard : abstract_guard_impl} (efl := E
   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 ▷
-  optimize_prop_discr_optimization (efl := ERemoveParams.switch_no_params EWellformed.all_env_flags) (wcon := eq_refl) (hastrel := eq_refl) (hastbox := eq_refl) ▷
+  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 ▷
   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
diff --git a/erasure/theories/EOptimizePropDiscr.v b/erasure/theories/EOptimizePropDiscr.v
index bbf48f9af..70ad8701c 100644
--- a/erasure/theories/EOptimizePropDiscr.v
+++ b/erasure/theories/EOptimizePropDiscr.v
@@ -28,7 +28,7 @@ Ltac introdep := let H := fresh in intros H; depelim H.
 #[global]
 Hint Constructors eval : core.
 
-Section optimize.
+Section remove_match_on_box.
   Context (Σ : GlobalContextMap.t).
 
   Definition isprop_ind Σ (ind:inductive × nat)
@@ -37,41 +37,41 @@ Section optimize.
         | _ => false
     end.
 
-  Fixpoint optimize (t : term) : term :=
+  Fixpoint remove_match_on_box (t : term) : term :=
     match t with
     | tRel i => tRel i
-    | tEvar ev args => tEvar ev (List.map optimize args)
-    | tLambda na M => tLambda na (optimize M)
-    | tApp u v => tApp (optimize u) (optimize v)
-    | tLetIn na b b' => tLetIn na (optimize b) (optimize b')
+    | tEvar ev args => tEvar ev (List.map remove_match_on_box args)
+    | tLambda na M => tLambda na (remove_match_on_box M)
+    | tApp u v => tApp (remove_match_on_box u) (remove_match_on_box v)
+    | tLetIn na b b' => tLetIn na (remove_match_on_box b) (remove_match_on_box b')
     | tCase ind c brs =>
-      let brs' := List.map (on_snd optimize) brs in
+      let brs' := List.map (on_snd remove_match_on_box) brs in
       if isprop_ind Σ ind
       then
         match brs' with
         | [(a, b)] => ECSubst.substl (repeat tBox #|a|) b
-        | _ => tCase ind (optimize c) brs'
+        | _ => tCase ind (remove_match_on_box c) brs'
         end
-      else tCase ind (optimize c) brs'
+      else tCase ind (remove_match_on_box c) brs'
     | tProj p c =>
       match GlobalContextMap.inductive_isprop_and_pars Σ p.(proj_ind) with
       | Some (true, _) => tBox
-      | _ => tProj p (optimize c)
+      | _ => tProj p (remove_match_on_box c)
       end
     | tFix mfix idx =>
-      let mfix' := List.map (map_def optimize) mfix in
+      let mfix' := List.map (map_def remove_match_on_box) mfix in
       tFix mfix' idx
     | tCoFix mfix idx =>
-      let mfix' := List.map (map_def optimize) mfix in
+      let mfix' := List.map (map_def remove_match_on_box) mfix in
       tCoFix mfix' idx
     | tBox => t
     | tVar _ => t
     | tConst _ => t
-    | tConstruct ind i args => tConstruct ind i (map optimize args)
+    | tConstruct ind i args => tConstruct ind i (map remove_match_on_box args)
     | tPrim _ => t
     end.
 
-  Lemma optimize_mkApps f l : optimize (mkApps f l) = mkApps (optimize f) (map optimize l).
+  Lemma remove_match_on_box_mkApps f l : remove_match_on_box (mkApps f l) = mkApps (remove_match_on_box f) (map remove_match_on_box l).
   Proof using Type.
     induction l using rev_ind; simpl; auto.
     now rewrite mkApps_app /= IHl map_app /= mkApps_app /=.
@@ -82,7 +82,7 @@ Section optimize.
     now induction n; simpl; auto; rewrite IHn.
   Qed.
 
-  Lemma map_optimize_repeat_box n : map optimize (repeat tBox n) = repeat tBox n.
+  Lemma map_remove_match_on_box_repeat_box n : map remove_match_on_box (repeat tBox n) = repeat tBox n.
   Proof using Type. by rewrite map_repeat. Qed.
 
   Import ECSubst.
@@ -106,7 +106,7 @@ Section optimize.
       destruct x0; cbn in *. f_equal; auto.
   Qed.
 
-  Lemma closed_optimize t k : closedn k t -> closedn k (optimize t).
+  Lemma closed_remove_match_on_box t k : closedn k t -> closedn k (remove_match_on_box t).
   Proof using Type.
     induction t in k |- * using EInduction.term_forall_list_ind; simpl; auto;
     intros; try easy;
@@ -166,9 +166,9 @@ Section optimize.
     apply subst_csubst_comm => //.
   Qed.
 
-  Lemma optimize_csubst a k b :
+  Lemma remove_match_on_box_csubst a k b :
     closed a ->
-    optimize (ECSubst.csubst a k b) = ECSubst.csubst (optimize a) k (optimize b).
+    remove_match_on_box (ECSubst.csubst a k b) = ECSubst.csubst (remove_match_on_box a) k (remove_match_on_box b).
   Proof using Type.
     induction b in k |- * using EInduction.term_forall_list_ind; simpl; auto;
     intros cl; try easy;
@@ -186,7 +186,7 @@ Section optimize.
         rewrite {2}H.
         rewrite substl_csubst_comm //.
         solve_all. eapply All_repeat => //.
-        now eapply closed_optimize.
+        now eapply closed_remove_match_on_box.
       * depelim X. depelim X.
         f_equal; eauto.
         unfold on_snd; cbn. f_equal; eauto.
@@ -199,28 +199,28 @@ Section optimize.
       now rewrite IHb.
   Qed.
 
-  Lemma optimize_substl s t :
+  Lemma remove_match_on_box_substl s t :
     forallb (closedn 0) s ->
-    optimize (substl s t) = substl (map optimize s) (optimize t).
+    remove_match_on_box (substl s t) = substl (map remove_match_on_box s) (remove_match_on_box t).
   Proof using Type.
     induction s in t |- *; simpl; auto.
     move/andP => [] cla cls.
     rewrite IHs //. f_equal.
-    now rewrite optimize_csubst.
+    now rewrite remove_match_on_box_csubst.
   Qed.
 
-  Lemma optimize_iota_red pars args br :
+  Lemma remove_match_on_box_iota_red pars args br :
     forallb (closedn 0) args ->
-    optimize (EGlobalEnv.iota_red pars args br) = EGlobalEnv.iota_red pars (map optimize args) (on_snd optimize br).
+    remove_match_on_box (EGlobalEnv.iota_red pars args br) = EGlobalEnv.iota_red pars (map remove_match_on_box args) (on_snd remove_match_on_box br).
   Proof using Type.
     intros cl.
     unfold EGlobalEnv.iota_red.
-    rewrite optimize_substl //.
+    rewrite remove_match_on_box_substl //.
     rewrite forallb_rev forallb_skipn //.
     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).
+  Lemma remove_match_on_box_fix_subst mfix : EGlobalEnv.fix_subst (map (map_def remove_match_on_box) mfix) = map remove_match_on_box (EGlobalEnv.fix_subst mfix).
   Proof using Type.
     unfold EGlobalEnv.fix_subst.
     rewrite map_length.
@@ -229,7 +229,7 @@ Section optimize.
     f_equal; auto.
   Qed.
 
-  Lemma optimize_cofix_subst mfix : EGlobalEnv.cofix_subst (map (map_def optimize) mfix) = map optimize (EGlobalEnv.cofix_subst mfix).
+  Lemma remove_match_on_box_cofix_subst mfix : EGlobalEnv.cofix_subst (map (map_def remove_match_on_box) mfix) = map remove_match_on_box (EGlobalEnv.cofix_subst mfix).
   Proof using Type.
     unfold EGlobalEnv.cofix_subst.
     rewrite map_length.
@@ -238,41 +238,41 @@ Section optimize.
     f_equal; auto.
   Qed.
 
-  Lemma optimize_cunfold_fix mfix idx n f :
+  Lemma remove_match_on_box_cunfold_fix mfix idx n f :
     forallb (closedn 0) (EGlobalEnv.fix_subst mfix) ->
     cunfold_fix mfix idx = Some (n, f) ->
-    cunfold_fix (map (map_def optimize) mfix) idx = Some (n, optimize f).
+    cunfold_fix (map (map_def remove_match_on_box) mfix) idx = Some (n, remove_match_on_box f).
   Proof using Type.
     intros hfix.
     unfold cunfold_fix.
     rewrite nth_error_map.
     destruct nth_error.
     intros [= <- <-] => /=. f_equal.
-    now rewrite optimize_substl // optimize_fix_subst.
+    now rewrite remove_match_on_box_substl // remove_match_on_box_fix_subst.
     discriminate.
   Qed.
 
-  Lemma optimize_cunfold_cofix mfix idx n f :
+  Lemma remove_match_on_box_cunfold_cofix mfix idx n f :
     forallb (closedn 0) (EGlobalEnv.cofix_subst mfix) ->
     cunfold_cofix mfix idx = Some (n, f) ->
-    cunfold_cofix (map (map_def optimize) mfix) idx = Some (n, optimize f).
+    cunfold_cofix (map (map_def remove_match_on_box) mfix) idx = Some (n, remove_match_on_box f).
   Proof using Type.
     intros hcofix.
     unfold cunfold_cofix.
     rewrite nth_error_map.
     destruct nth_error.
     intros [= <- <-] => /=. f_equal.
-    now rewrite optimize_substl // optimize_cofix_subst.
+    now rewrite remove_match_on_box_substl // remove_match_on_box_cofix_subst.
     discriminate.
   Qed.
 
-  Lemma optimize_nth {n l d} :
-    optimize (nth n l d) = nth n (map optimize l) (optimize d).
+  Lemma remove_match_on_box_nth {n l d} :
+    remove_match_on_box (nth n l d) = nth n (map remove_match_on_box l) (remove_match_on_box d).
   Proof using Type.
     induction l in n |- *; destruct n; simpl; auto.
   Qed.
 
-End optimize.
+End remove_match_on_box.
 
 Lemma is_box_inv b : is_box b -> ∑ args, b = mkApps tBox args.
 Proof.
@@ -313,26 +313,26 @@ Proof.
   eexists; econstructor; eauto.
 Qed.
 
-Definition optimize_constant_decl Σ cb :=
-  {| cst_body := option_map (optimize Σ) cb.(cst_body) |}.
+Definition remove_match_on_box_constant_decl Σ cb :=
+  {| cst_body := option_map (remove_match_on_box Σ) cb.(cst_body) |}.
 
-Definition optimize_decl Σ d :=
+Definition remove_match_on_box_decl Σ d :=
   match d with
-  | ConstantDecl cb => ConstantDecl (optimize_constant_decl Σ cb)
+  | ConstantDecl cb => ConstantDecl (remove_match_on_box_constant_decl Σ cb)
   | InductiveDecl idecl => d
   end.
 
-Definition optimize_env Σ :=
-  map (on_snd (optimize_decl Σ)) Σ.(GlobalContextMap.global_decls).
+Definition remove_match_on_box_env Σ :=
+  map (on_snd (remove_match_on_box_decl Σ)) Σ.(GlobalContextMap.global_decls).
 
 Import EnvMap.
 
-Program Fixpoint optimize_env' Σ : EnvMap.fresh_globals Σ -> global_context :=
+Program Fixpoint remove_match_on_box_env' Σ : EnvMap.fresh_globals Σ -> global_context :=
   match Σ with
   | [] => fun _ => []
   | hd :: tl => fun HΣ =>
     let Σg := GlobalContextMap.make tl (fresh_globals_cons_inv HΣ) in
-    on_snd (optimize_decl Σg) hd :: optimize_env' tl (fresh_globals_cons_inv HΣ)
+    on_snd (remove_match_on_box_decl Σg) hd :: remove_match_on_box_env' tl (fresh_globals_cons_inv HΣ)
   end.
 
 Import EGlobalEnv EExtends.
@@ -363,10 +363,10 @@ Proof.
   destruct nth_error => //.
 Qed.
 
-Lemma wellformed_optimize_extends {wfl: EEnvFlags} {Σ : GlobalContextMap.t} t :
+Lemma wellformed_remove_match_on_box_extends {wfl: EEnvFlags} {Σ : GlobalContextMap.t} t :
   forall n, EWellformed.wellformed Σ n t ->
   forall {Σ' : GlobalContextMap.t}, extends Σ Σ' -> wf_glob Σ' ->
-  optimize Σ t = optimize Σ' t.
+  remove_match_on_box Σ t = remove_match_on_box Σ' t.
 Proof.
   induction t using EInduction.term_forall_list_ind; cbn -[lookup_constant lookup_inductive
     lookup_projection
@@ -375,7 +375,7 @@ Proof.
   all:try now f_equal; eauto; solve_all.
   - 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 (optimize Σ)) l = map (on_snd (optimize Σ')) l) as -> by solve_all.
+    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).
     destruct inductive_isprop_and_pars as [[[]]|].
     destruct map => //. f_equal; eauto.
@@ -390,23 +390,23 @@ Proof.
     all:f_equal; eauto.
 Qed.
 
-Lemma wellformed_optimize_decl_extends {wfl: EEnvFlags} {Σ : GlobalContextMap.t} t :
+Lemma wellformed_remove_match_on_box_decl_extends {wfl: EEnvFlags} {Σ : GlobalContextMap.t} t :
   wf_global_decl Σ t ->
   forall {Σ' : GlobalContextMap.t}, extends Σ Σ' -> wf_glob Σ' ->
-  optimize_decl Σ t = optimize_decl Σ' t.
+  remove_match_on_box_decl Σ t = remove_match_on_box_decl Σ' t.
 Proof.
   destruct t => /= //.
-  intros wf Σ' ext wf'. f_equal. unfold optimize_constant_decl. f_equal.
+  intros wf Σ' ext wf'. f_equal. unfold remove_match_on_box_constant_decl. f_equal.
   destruct (cst_body c) => /= //. f_equal.
-  now eapply wellformed_optimize_extends.
+  now eapply wellformed_remove_match_on_box_extends.
 Qed.
 
-Lemma lookup_env_optimize_env_Some {efl : EEnvFlags} {Σ : GlobalContextMap.t} kn d :
+Lemma lookup_env_remove_match_on_box_env_Some {efl : EEnvFlags} {Σ : GlobalContextMap.t} kn d :
   wf_glob Σ ->
   GlobalContextMap.lookup_env Σ kn = Some d ->
   ∑ Σ' : GlobalContextMap.t,
     [× extends Σ' Σ, wf_global_decl Σ' d &
-      lookup_env (optimize_env Σ) kn = Some (optimize_decl Σ' d)].
+      lookup_env (remove_match_on_box_env Σ) kn = Some (remove_match_on_box_decl Σ' d)].
 Proof.
   rewrite GlobalContextMap.lookup_env_spec.
   destruct Σ as [Σ map repr wf].
@@ -417,7 +417,7 @@ Proof.
     exists (GlobalContextMap.make Σ (fresh_globals_cons_inv wf)). split.
     now eexists [_].
     cbn. now depelim wfg.
-    f_equal. symmetry. eapply wellformed_optimize_decl_extends. cbn. now depelim wfg.
+    f_equal. symmetry. eapply wellformed_remove_match_on_box_decl_extends. cbn. now depelim wfg.
     cbn. now exists [a]. now cbn.
   - intros _.
     set (Σ' := GlobalContextMap.make Σ (fresh_globals_cons_inv wf)).
@@ -430,7 +430,7 @@ Proof.
     * rewrite -hl'. f_equal.
       clear -wfg.
       eapply map_ext_in => kn hin. unfold on_snd. f_equal.
-      symmetry. eapply wellformed_optimize_decl_extends => //. cbn.
+      symmetry. eapply wellformed_remove_match_on_box_decl_extends => //. cbn.
       eapply lookup_env_In in hin. 2:now depelim wfg.
       depelim wfg. eapply lookup_env_wellformed; tea.
       cbn. now exists [a].
@@ -442,48 +442,48 @@ Proof.
   case: eqb_spec => //.
 Qed.
 
-Lemma lookup_env_optimize_env_None {efl : EEnvFlags} {Σ : GlobalContextMap.t} kn :
+Lemma lookup_env_remove_match_on_box_env_None {efl : EEnvFlags} {Σ : GlobalContextMap.t} kn :
   GlobalContextMap.lookup_env Σ kn = None ->
-  lookup_env (optimize_env Σ) kn = None.
+  lookup_env (remove_match_on_box_env Σ) kn = None.
 Proof.
   rewrite GlobalContextMap.lookup_env_spec.
   destruct Σ as [Σ map repr wf].
   cbn. intros hl. rewrite lookup_env_map_snd hl //.
 Qed.
 
-Lemma lookup_env_optimize {efl : EEnvFlags} {Σ : GlobalContextMap.t} kn :
+Lemma lookup_env_remove_match_on_box {efl : EEnvFlags} {Σ : GlobalContextMap.t} kn :
   wf_glob Σ ->
-  lookup_env (optimize_env Σ) kn = option_map (optimize_decl Σ) (lookup_env Σ kn).
+  lookup_env (remove_match_on_box_env Σ) kn = option_map (remove_match_on_box_decl Σ) (lookup_env Σ kn).
 Proof.
   intros wf.
   rewrite -GlobalContextMap.lookup_env_spec.
   destruct (GlobalContextMap.lookup_env Σ kn) eqn:hl.
-  - eapply lookup_env_optimize_env_Some in hl as [Σ' [ext wf' hl']] => /=.
+  - eapply lookup_env_remove_match_on_box_env_Some in hl as [Σ' [ext wf' hl']] => /=.
     rewrite hl'. f_equal.
-    eapply wellformed_optimize_decl_extends; eauto. auto.
+    eapply wellformed_remove_match_on_box_decl_extends; eauto. auto.
 
-  - cbn. now eapply lookup_env_optimize_env_None in hl.
+  - cbn. now eapply lookup_env_remove_match_on_box_env_None in hl.
 Qed.
 
-Lemma is_propositional_optimize {efl : EEnvFlags} {Σ : GlobalContextMap.t} ind :
+Lemma is_propositional_remove_match_on_box {efl : EEnvFlags} {Σ : GlobalContextMap.t} ind :
   wf_glob Σ ->
-  inductive_isprop_and_pars Σ ind = inductive_isprop_and_pars (optimize_env Σ) ind.
+  inductive_isprop_and_pars Σ ind = inductive_isprop_and_pars (remove_match_on_box_env Σ) ind.
 Proof.
   rewrite /inductive_isprop_and_pars => wf.
   rewrite /lookup_inductive /lookup_minductive.
-  rewrite (lookup_env_optimize (inductive_mind ind) wf).
+  rewrite (lookup_env_remove_match_on_box (inductive_mind ind) wf).
   rewrite /GlobalContextMap.inductive_isprop_and_pars /GlobalContextMap.lookup_inductive
     /GlobalContextMap.lookup_minductive.
   destruct lookup_env as [[decl|]|] => //.
 Qed.
 
-Lemma is_propositional_cstr_optimize {efl : EEnvFlags} {Σ : GlobalContextMap.t} ind c :
+Lemma is_propositional_cstr_remove_match_on_box {efl : EEnvFlags} {Σ : GlobalContextMap.t} ind c :
   wf_glob Σ ->
-  constructor_isprop_pars_decl Σ ind c = constructor_isprop_pars_decl (optimize_env Σ) ind c.
+  constructor_isprop_pars_decl Σ ind c = constructor_isprop_pars_decl (remove_match_on_box_env Σ) ind c.
 Proof.
   rewrite /constructor_isprop_pars_decl => wf.
   rewrite /lookup_constructor /lookup_inductive /lookup_minductive.
-  rewrite (lookup_env_optimize (inductive_mind ind) wf).
+  rewrite (lookup_env_remove_match_on_box (inductive_mind ind) wf).
   rewrite /GlobalContextMap.inductive_isprop_and_pars /GlobalContextMap.lookup_inductive
     /GlobalContextMap.lookup_minductive.
   destruct lookup_env as [[decl|]|] => //.
@@ -511,12 +511,12 @@ Proof.
   - rewrite mkApps_app /=. now destruct l => /= //; rewrite andb_false_r.
 Qed.
 
-Lemma lookup_constructor_optimize {efl : EEnvFlags} {Σ : GlobalContextMap.t} {ind c} :
+Lemma lookup_constructor_remove_match_on_box {efl : EEnvFlags} {Σ : GlobalContextMap.t} {ind c} :
   wf_glob Σ ->
-  lookup_constructor Σ ind c = lookup_constructor (optimize_env Σ) ind c.
+  lookup_constructor Σ ind c = lookup_constructor (remove_match_on_box_env Σ) ind c.
 Proof.
   intros wfΣ. rewrite /lookup_constructor /lookup_inductive /lookup_minductive.
-  rewrite lookup_env_optimize // /=. destruct lookup_env => // /=.
+  rewrite lookup_env_remove_match_on_box // /=. destruct lookup_env => // /=.
   destruct g => //.
 Qed.
 
@@ -529,12 +529,12 @@ Proof.
   destruct nth_error => //. congruence.
 Qed.
 
-Lemma optimize_correct {efl : EEnvFlags} {fl}{wcon : with_constructor_as_block = false} {Σ : GlobalContextMap.t} t v :
+Lemma remove_match_on_box_correct {efl : EEnvFlags} {fl}{wcon : with_constructor_as_block = false} {Σ : GlobalContextMap.t} t v :
   wf_glob Σ ->
   closed_env Σ ->
   @Ee.eval fl Σ t v ->
   closed t ->
-  @Ee.eval (disable_prop_cases fl) (optimize_env Σ) (optimize Σ t) (optimize Σ v).
+  @Ee.eval (disable_prop_cases fl) (remove_match_on_box_env Σ) (remove_match_on_box Σ t) (remove_match_on_box Σ v).
 Proof.
   intros wfΣ clΣ ev.
   induction ev; simpl in *.
@@ -544,23 +544,23 @@ Proof.
     eapply eval_closed in ev2; tea.
     eapply eval_closed in ev1; tea.
     econstructor; eauto.
-    rewrite optimize_csubst // in IHev3.
+    rewrite remove_match_on_box_csubst // in IHev3.
     apply IHev3. eapply closed_csubst => //.
 
-  - move/andP => [] clb0 clb1. rewrite optimize_csubst in IHev2.
+  - move/andP => [] clb0 clb1. rewrite remove_match_on_box_csubst in IHev2.
     now eapply eval_closed in ev1.
     econstructor; eauto. eapply IHev2, closed_csubst => //.
     now eapply eval_closed in ev1.
 
-  - move/andP => [] cld clbrs. rewrite optimize_mkApps in IHev1.
+  - move/andP => [] cld clbrs. rewrite remove_match_on_box_mkApps in IHev1.
     have := (eval_closed _ clΣ _ _ cld ev1); rewrite closedn_mkApps => /andP[] _ clargs.
-    rewrite optimize_iota_red in IHev2.
+    rewrite remove_match_on_box_iota_red in IHev2.
     eapply eval_closed in ev1 => //.
     unfold isprop_ind.
     rewrite GlobalContextMap.inductive_isprop_and_pars_spec.
     rewrite (constructor_isprop_pars_decl_inductive e1).
     eapply eval_iota; eauto.
-    now rewrite -is_propositional_cstr_optimize.
+    now rewrite -is_propositional_cstr_remove_match_on_box.
     rewrite nth_error_map e2 //. now len. cbn.
     rewrite -e4. rewrite !skipn_length map_length //.
     eapply IHev2.
@@ -574,24 +574,24 @@ Proof.
     rewrite GlobalContextMap.inductive_isprop_and_pars_spec.
     rewrite e0 e1 /=.
     subst brs. cbn in clbrs. rewrite Nat.add_0_r andb_true_r in clbrs.
-    rewrite optimize_substl in IHev2.
+    rewrite remove_match_on_box_substl in IHev2.
     eapply All_forallb, All_repeat => //.
-    rewrite map_optimize_repeat_box in IHev2.
+    rewrite map_remove_match_on_box_repeat_box in IHev2.
     apply IHev2.
     eapply closed_substl.
     eapply All_forallb, All_repeat => //.
     now rewrite repeat_length Nat.add_0_r.
 
-  - move/andP => [] clf cla. rewrite optimize_mkApps in IHev1.
+  - move/andP => [] clf cla. rewrite remove_match_on_box_mkApps in IHev1.
     simpl in *.
     eapply eval_closed in ev1 => //.
     rewrite closedn_mkApps in ev1.
     move: ev1 => /andP [] clfix clargs.
     eapply Ee.eval_fix; eauto.
     rewrite map_length.
-    eapply optimize_cunfold_fix; tea.
+    eapply remove_match_on_box_cunfold_fix; tea.
     eapply closed_fix_subst. tea.
-    rewrite optimize_mkApps in IHev3. apply IHev3.
+    rewrite remove_match_on_box_mkApps in IHev3. apply IHev3.
     rewrite closedn_mkApps clargs.
     eapply eval_closed in ev2; tas. rewrite ev2 /= !andb_true_r.
     eapply closed_cunfold_fix; tea.
@@ -601,9 +601,9 @@ Proof.
     rewrite closedn_mkApps in ev1.
     move: ev1 => /andP [] clfix clargs.
     eapply eval_closed in ev2; tas.
-    rewrite optimize_mkApps in IHev1 |- *.
+    rewrite remove_match_on_box_mkApps in IHev1 |- *.
     simpl in *. eapply Ee.eval_fix_value. auto. auto. auto.
-    eapply optimize_cunfold_fix; eauto.
+    eapply remove_match_on_box_cunfold_fix; eauto.
     eapply closed_fix_subst => //.
     now rewrite map_length.
 
@@ -611,7 +611,7 @@ Proof.
     eapply eval_closed in ev1 => //.
     eapply eval_closed in ev2; tas.
     simpl in *. eapply Ee.eval_fix'. auto. auto.
-    eapply optimize_cunfold_fix; eauto.
+    eapply remove_match_on_box_cunfold_fix; eauto.
     eapply closed_fix_subst => //.
     eapply IHev2; tea. eapply IHev3.
     apply/andP; split => //.
@@ -625,21 +625,21 @@ Proof.
     forward IHev2.
     { rewrite clargs clbrs !andb_true_r.
       eapply closed_cunfold_cofix; tea. }
-    rewrite -> optimize_mkApps in IHev1, IHev2. simpl. unfold isprop_ind in *.
+    rewrite -> remove_match_on_box_mkApps in IHev1, IHev2. simpl. unfold isprop_ind in *.
     rewrite GlobalContextMap.inductive_isprop_and_pars_spec in IHev2 |- *.
     destruct EGlobalEnv.inductive_isprop_and_pars as [[[] pars]|] eqn:isp => //.
     destruct brs as [|[a b] []]; simpl in *; auto.
     simpl in IHev1.
     eapply Ee.eval_cofix_case. tea.
-    apply optimize_cunfold_cofix; tea. eapply closed_cofix_subst; tea.
+    apply remove_match_on_box_cunfold_cofix; tea. eapply closed_cofix_subst; tea.
     apply IHev2.
     eapply Ee.eval_cofix_case; tea.
-    apply optimize_cunfold_cofix; tea. eapply closed_cofix_subst; tea.
+    apply remove_match_on_box_cunfold_cofix; tea. eapply closed_cofix_subst; tea.
     simpl in *.
     eapply Ee.eval_cofix_case; tea.
-    apply optimize_cunfold_cofix; tea. eapply closed_cofix_subst; tea.
+    apply remove_match_on_box_cunfold_cofix; tea. eapply closed_cofix_subst; tea.
     eapply Ee.eval_cofix_case; tea.
-    apply optimize_cunfold_cofix; tea. eapply closed_cofix_subst; tea.
+    apply remove_match_on_box_cunfold_cofix; tea. eapply closed_cofix_subst; tea.
 
   - intros cd. specialize (IHev1 cd).
     move: (eval_closed _ clΣ _ _ cd ev1).
@@ -647,15 +647,15 @@ Proof.
     { rewrite closedn_mkApps clargs andb_true_r. eapply closed_cunfold_cofix; tea. }
     rewrite GlobalContextMap.inductive_isprop_and_pars_spec in IHev2 |- *.
     destruct EGlobalEnv.inductive_isprop_and_pars as [[[] pars]|] eqn:isp; auto.
-    rewrite -> optimize_mkApps in IHev1, IHev2. simpl in *.
+    rewrite -> remove_match_on_box_mkApps in IHev1, IHev2. simpl in *.
     econstructor; eauto.
-    apply optimize_cunfold_cofix; tea. eapply closed_cofix_subst; tea.
-    rewrite -> optimize_mkApps in IHev1, IHev2. simpl in *.
+    apply remove_match_on_box_cunfold_cofix; tea. eapply closed_cofix_subst; tea.
+    rewrite -> remove_match_on_box_mkApps in IHev1, IHev2. simpl in *.
     econstructor; eauto.
-    apply optimize_cunfold_cofix; tea. eapply closed_cofix_subst; tea.
+    apply remove_match_on_box_cunfold_cofix; tea. eapply closed_cofix_subst; tea.
 
   - rewrite /declared_constant in isdecl.
-    move: (lookup_env_optimize c wfΣ).
+    move: (lookup_env_remove_match_on_box c wfΣ).
     rewrite isdecl /= //.
     intros hl.
     econstructor; tea. cbn. rewrite e //.
@@ -668,10 +668,10 @@ Proof.
     move: ev1; rewrite closedn_mkApps /= => clargs.
     rewrite GlobalContextMap.inductive_isprop_and_pars_spec.
     rewrite (constructor_isprop_pars_decl_inductive e1).
-    rewrite optimize_mkApps in IHev1.
+    rewrite remove_match_on_box_mkApps in IHev1.
     specialize (IHev1 cld).
     eapply Ee.eval_proj; tea.
-    now rewrite -is_propositional_cstr_optimize.
+    now rewrite -is_propositional_cstr_remove_match_on_box.
     now len. rewrite nth_error_map e3 //.
     eapply IHev2.
     eapply nth_error_forallb in e3; tea.
@@ -682,10 +682,10 @@ Proof.
     now rewrite e0.
 
   - move/andP=> [] clf cla.
-    rewrite optimize_mkApps.
+    rewrite remove_match_on_box_mkApps.
     eapply eval_construct; tea.
-    rewrite -lookup_constructor_optimize //. exact e0.
-    rewrite optimize_mkApps in IHev1. now eapply IHev1.
+    rewrite -lookup_constructor_remove_match_on_box //. exact e0.
+    rewrite remove_match_on_box_mkApps in IHev1. now eapply IHev1.
     now len.
     now eapply IHev2.
 
@@ -696,11 +696,11 @@ Proof.
     eapply Ee.eval_app_cong; eauto.
     eapply Ee.eval_to_value in ev1.
     destruct ev1; simpl in *; eauto.
-    * destruct t => //; rewrite optimize_mkApps /=.
+    * destruct t => //; rewrite remove_match_on_box_mkApps /=.
     * destruct with_guarded_fix.
       + move: i.
         rewrite !negb_or.
-        rewrite optimize_mkApps !isFixApp_mkApps !isConstructApp_mkApps !isPrimApp_mkApps.
+        rewrite remove_match_on_box_mkApps !isFixApp_mkApps !isConstructApp_mkApps !isPrimApp_mkApps.
         destruct args using rev_case => // /=. rewrite map_app !mkApps_app /= //.
         rewrite !andb_true_r.
         rtoProp; intuition auto.
@@ -709,26 +709,26 @@ Proof.
         destruct v => /= //.
       + move: i.
         rewrite !negb_or.
-        rewrite optimize_mkApps !isConstructApp_mkApps !isPrimApp_mkApps.
+        rewrite remove_match_on_box_mkApps !isConstructApp_mkApps !isPrimApp_mkApps.
         destruct args using rev_case => // /=. rewrite map_app !mkApps_app /= //.
         destruct v => /= //.
   - destruct t => //.
-    all:constructor; eauto. cbn [atom optimize] in i |- *.
-    rewrite -lookup_constructor_optimize //. destruct l => //.
+    all:constructor; eauto. cbn [atom remove_match_on_box] in i |- *.
+    rewrite -lookup_constructor_remove_match_on_box //. destruct l => //.
 Qed.
 
 From MetaCoq.Erasure Require Import EEtaExpanded.
 
-Lemma isLambda_optimize Σ t : isLambda t -> isLambda (optimize Σ t).
+Lemma isLambda_remove_match_on_box Σ t : isLambda t -> isLambda (remove_match_on_box Σ t).
 Proof. destruct t => //. Qed.
-Lemma isBox_optimize Σ t : isBox t -> isBox (optimize Σ t).
+Lemma isBox_remove_match_on_box Σ t : isBox t -> isBox (remove_match_on_box Σ t).
 Proof. destruct t => //. Qed.
 
-Lemma optimize_expanded {Σ : GlobalContextMap.t} t : expanded Σ t -> expanded Σ (optimize Σ t).
+Lemma remove_match_on_box_expanded {Σ : GlobalContextMap.t} t : expanded Σ t -> expanded Σ (remove_match_on_box Σ t).
 Proof.
   induction 1 using expanded_ind.
   all:try solve[constructor; eauto; solve_all].
-  all:rewrite ?optimize_mkApps.
+  all:rewrite ?remove_match_on_box_mkApps.
   - eapply expanded_mkApps_expanded => //. solve_all.
   - cbn -[GlobalContextMap.inductive_isprop_and_pars]. unfold isprop_ind.
     rewrite GlobalContextMap.inductive_isprop_and_pars_spec.
@@ -750,40 +750,40 @@ Proof.
     destruct inductive_isprop_and_pars as [[[|] _]|] => /= //.
     constructor. all:constructor; auto.
   - cbn. eapply expanded_tFix. solve_all.
-    rewrite isLambda_optimize //.
+    rewrite isLambda_remove_match_on_box //.
   - eapply expanded_tConstruct_app; tea.
     now len. solve_all.
 Qed.
 
-Lemma optimize_expanded_irrel {efl : EEnvFlags} {Σ : GlobalContextMap.t} t : wf_glob Σ -> expanded Σ t -> expanded (optimize_env Σ) t.
+Lemma remove_match_on_box_expanded_irrel {efl : EEnvFlags} {Σ : GlobalContextMap.t} t : wf_glob Σ -> expanded Σ t -> expanded (remove_match_on_box_env Σ) t.
 Proof.
   intros wf; induction 1 using expanded_ind.
   all:try solve[constructor; eauto; solve_all].
   eapply expanded_tConstruct_app.
   destruct H as [[H ?] ?].
   split => //. split => //. red.
-  red in H. rewrite lookup_env_optimize // /= H //. 1-2:eauto. auto. solve_all.
+  red in H. rewrite lookup_env_remove_match_on_box // /= H //. 1-2:eauto. auto. solve_all.
 Qed.
 
-Lemma optimize_expanded_decl {Σ : GlobalContextMap.t} t : expanded_decl Σ t -> expanded_decl Σ (optimize_decl Σ t).
+Lemma remove_match_on_box_expanded_decl {Σ : GlobalContextMap.t} t : expanded_decl Σ t -> expanded_decl Σ (remove_match_on_box_decl Σ t).
 Proof.
   destruct t as [[[]]|] => /= //.
   unfold expanded_constant_decl => /=.
-  apply optimize_expanded.
+  apply remove_match_on_box_expanded.
 Qed.
 
-Lemma optimize_expanded_decl_irrel {efl : EEnvFlags} {Σ : GlobalContextMap.t} t : wf_glob Σ -> expanded_decl Σ t -> expanded_decl (optimize_env Σ) t.
+Lemma remove_match_on_box_expanded_decl_irrel {efl : EEnvFlags} {Σ : GlobalContextMap.t} t : wf_glob Σ -> expanded_decl Σ t -> expanded_decl (remove_match_on_box_env Σ) t.
 Proof.
   destruct t as [[[]]|] => /= //.
   unfold expanded_constant_decl => /=.
-  apply optimize_expanded_irrel.
+  apply remove_match_on_box_expanded_irrel.
 Qed.
 
-Lemma optimize_env_extends' {efl : EEnvFlags} {Σ Σ' : GlobalContextMap.t} :
+Lemma remove_match_on_box_env_extends' {efl : EEnvFlags} {Σ Σ' : GlobalContextMap.t} :
   extends Σ Σ' ->
   wf_glob Σ' ->
-  List.map (on_snd (optimize_decl Σ)) Σ.(GlobalContextMap.global_decls) =
-  List.map (on_snd (optimize_decl Σ')) Σ.(GlobalContextMap.global_decls).
+  List.map (on_snd (remove_match_on_box_decl Σ)) Σ.(GlobalContextMap.global_decls) =
+  List.map (on_snd (remove_match_on_box_decl Σ')) Σ.(GlobalContextMap.global_decls).
 Proof.
   intros ext.
   destruct Σ as [Σ map repr wf]; cbn in *.
@@ -798,48 +798,48 @@ Proof.
   f_equal.
   2:{ eapply IHΣ'' => //. destruct hin. exists (x ++ [(kn, d)]). rewrite -app_assoc /= //. }
   unfold on_snd. cbn. f_equal.
-  eapply wellformed_optimize_decl_extends => //. cbn.
+  eapply wellformed_remove_match_on_box_decl_extends => //. cbn.
   eapply extends_wf_global_decl. 3:tea.
   eapply extends_wf_glob; tea.
   destruct hin. exists (x ++ [(kn, d)]). rewrite -app_assoc /= //.
 Qed.
 
-Lemma optimize_env_eq {efl : EEnvFlags} (Σ : GlobalContextMap.t) : wf_glob Σ -> optimize_env Σ = optimize_env' Σ.(GlobalContextMap.global_decls) Σ.(GlobalContextMap.wf).
+Lemma remove_match_on_box_env_eq {efl : EEnvFlags} (Σ : GlobalContextMap.t) : wf_glob Σ -> remove_match_on_box_env Σ = remove_match_on_box_env' Σ.(GlobalContextMap.global_decls) Σ.(GlobalContextMap.wf).
 Proof.
   intros wf.
-  unfold optimize_env.
+  unfold remove_match_on_box_env.
   destruct Σ; cbn. cbn in wf.
   induction global_decls in map, repr, wf0, wf |- * => //.
   cbn. f_equal.
   destruct a as [kn d]; unfold on_snd; cbn. f_equal. symmetry.
-  eapply wellformed_optimize_decl_extends => //. cbn. now depelim wf. cbn. now exists [(kn, d)]. cbn.
+  eapply wellformed_remove_match_on_box_decl_extends => //. cbn. now depelim wf. cbn. now exists [(kn, d)]. cbn.
   set (Σg' := GlobalContextMap.make global_decls (fresh_globals_cons_inv wf0)).
   erewrite <- (IHglobal_decls (GlobalContextMap.map Σg') (GlobalContextMap.repr Σg')).
   2:now depelim wf.
   set (Σg := {| GlobalContextMap.global_decls := _ :: _ |}).
-  symmetry. eapply (optimize_env_extends' (Σ := Σg') (Σ' := Σg)) => //.
+  symmetry. eapply (remove_match_on_box_env_extends' (Σ := Σg') (Σ' := Σg)) => //.
   cbn. now exists [a].
 Qed.
 
-Lemma optimize_env_expanded {efl : EEnvFlags} {Σ : GlobalContextMap.t} :
-  wf_glob Σ -> expanded_global_env Σ -> expanded_global_env (optimize_env Σ).
+Lemma remove_match_on_box_env_expanded {efl : EEnvFlags} {Σ : GlobalContextMap.t} :
+  wf_glob Σ -> expanded_global_env Σ -> expanded_global_env (remove_match_on_box_env Σ).
 Proof.
   unfold expanded_global_env; move=> wfg.
-  rewrite optimize_env_eq //.
+  rewrite remove_match_on_box_env_eq //.
   destruct Σ as [Σ map repr wf]. cbn in *.
   clear map repr.
   induction 1; cbn; constructor; auto.
   cbn in IHexpanded_global_declarations.
   unshelve eapply IHexpanded_global_declarations. now depelim wfg. cbn.
   set (Σ' := GlobalContextMap.make _ _).
-  rewrite -(optimize_env_eq Σ'). cbn. now depelim wfg.
-  eapply (optimize_expanded_decl_irrel (Σ := Σ')). now depelim wfg.
-  now unshelve eapply (optimize_expanded_decl (Σ:=Σ')).
+  rewrite -(remove_match_on_box_env_eq Σ'). cbn. now depelim wfg.
+  eapply (remove_match_on_box_expanded_decl_irrel (Σ := Σ')). now depelim wfg.
+  now unshelve eapply (remove_match_on_box_expanded_decl (Σ:=Σ')).
 Qed.
 
-Lemma optimize_wellformed {efl : EEnvFlags} {Σ : GlobalContextMap.t} n t :
+Lemma remove_match_on_box_wellformed {efl : EEnvFlags} {Σ : GlobalContextMap.t} n t :
   has_tBox -> has_tRel ->
-  wf_glob Σ -> EWellformed.wellformed Σ n t -> EWellformed.wellformed Σ n (optimize Σ t).
+  wf_glob Σ -> EWellformed.wellformed Σ n t -> EWellformed.wellformed Σ n (remove_match_on_box Σ t).
 Proof.
   intros wfΣ hbox hrel.
   induction t in n |- * using EInduction.term_forall_list_ind => //.
@@ -865,7 +865,7 @@ Proof.
   - cbn -[GlobalContextMap.inductive_isprop_and_pars lookup_inductive]. move/andP => [] /andP[]hasc hs ht.
     destruct GlobalContextMap.inductive_isprop_and_pars as [[[|] _]|] => /= //.
     all:rewrite hasc hs /=; eauto.
-  - cbn. unfold wf_fix; rtoProp; intuition auto; solve_all. now eapply isLambda_optimize. now len.
+  - cbn. unfold wf_fix; rtoProp; intuition auto; solve_all. now eapply isLambda_remove_match_on_box. now len.
     unfold test_def in *. len. eauto.
   - cbn. unfold wf_fix; rtoProp; intuition auto; solve_all. now len.
     unfold test_def in *. len. eauto.
@@ -873,26 +873,26 @@ Qed.
 
 Import EWellformed.
 
-Lemma optimize_wellformed_irrel {efl : EEnvFlags} {Σ : GlobalContextMap.t} t :
+Lemma remove_match_on_box_wellformed_irrel {efl : EEnvFlags} {Σ : GlobalContextMap.t} t :
   wf_glob Σ ->
-  forall n, wellformed Σ n t -> wellformed (optimize_env Σ) n t.
+  forall n, wellformed Σ n t -> wellformed (remove_match_on_box_env Σ) n t.
 Proof.
   intros wfΣ. induction t using EInduction.term_forall_list_ind; cbn => //.
   all:try solve [intros; unfold wf_fix_gen in *; rtoProp; intuition eauto; solve_all].
-  - rewrite lookup_env_optimize //.
+  - rewrite lookup_env_remove_match_on_box //.
     destruct lookup_env eqn:hl => // /=.
     destruct g eqn:hg => /= //. subst g.
     destruct (cst_body c) => //.
-  - rewrite lookup_env_optimize //.
+  - rewrite lookup_env_remove_match_on_box //.
     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_optimize //.
+  - rewrite lookup_env_remove_match_on_box //.
     destruct lookup_env eqn:hl => // /=.
     destruct g eqn:hg => /= //. subst g.
     destruct nth_error => /= //.
     intros; rtoProp; intuition auto; solve_all.
-  - rewrite lookup_env_optimize //.
+  - rewrite lookup_env_remove_match_on_box //.
     destruct lookup_env eqn:hl => // /=.
     destruct g eqn:hg => /= //.
     rewrite andb_false_r => //.
@@ -900,73 +900,73 @@ Proof.
     all:intros; rtoProp; intuition auto; solve_all.
 Qed.
 
-Lemma optimize_wellformed_decl_irrel {efl : EEnvFlags} {Σ : GlobalContextMap.t} d :
+Lemma remove_match_on_box_wellformed_decl_irrel {efl : EEnvFlags} {Σ : GlobalContextMap.t} d :
   wf_glob Σ ->
-  wf_global_decl Σ d -> wf_global_decl (optimize_env Σ) d.
+  wf_global_decl Σ d -> wf_global_decl (remove_match_on_box_env Σ) d.
 Proof.
   intros wf; destruct d => /= //.
   destruct (cst_body c) => /= //.
-  now eapply optimize_wellformed_irrel.
+  now eapply remove_match_on_box_wellformed_irrel.
 Qed.
 
-Lemma optimize_decl_wf {efl : EEnvFlags} {Σ : GlobalContextMap.t} :
+Lemma remove_match_on_box_decl_wf {efl : EEnvFlags} {Σ : GlobalContextMap.t} :
   has_tBox -> has_tRel -> wf_glob Σ ->
-  forall d, wf_global_decl Σ d -> wf_global_decl (optimize_env Σ) (optimize_decl Σ d).
+  forall d, wf_global_decl Σ d -> wf_global_decl (remove_match_on_box_env Σ) (remove_match_on_box_decl Σ d).
 Proof.
   intros hasb hasr wf d.
   intros hd.
-  eapply optimize_wellformed_decl_irrel; tea.
+  eapply remove_match_on_box_wellformed_decl_irrel; tea.
   move: hd.
   destruct d => /= //.
   destruct (cst_body c) => /= //.
-  now eapply optimize_wellformed => //.
+  now eapply remove_match_on_box_wellformed => //.
 Qed.
 
-Lemma fresh_global_optimize_env {Σ : GlobalContextMap.t} kn :
+Lemma fresh_global_remove_match_on_box_env {Σ : GlobalContextMap.t} kn :
   fresh_global kn Σ ->
-  fresh_global kn (optimize_env Σ).
+  fresh_global kn (remove_match_on_box_env Σ).
 Proof.
   destruct Σ as [Σ map repr wf]; cbn in *.
   induction 1; cbn; constructor; auto.
   now eapply Forall_map; cbn.
 Qed.
 
-Lemma optimize_env_wf {efl : EEnvFlags} {Σ : GlobalContextMap.t} :
+Lemma remove_match_on_box_env_wf {efl : EEnvFlags} {Σ : GlobalContextMap.t} :
   has_tBox -> has_tRel ->
-  wf_glob Σ -> wf_glob (optimize_env Σ).
+  wf_glob Σ -> wf_glob (remove_match_on_box_env Σ).
 Proof.
   intros hasb hasrel.
-  intros wfg. rewrite optimize_env_eq //.
+  intros wfg. rewrite remove_match_on_box_env_eq //.
   destruct Σ as [Σ map repr wf]; cbn in *.
   clear map repr.
   induction wfg; cbn; constructor; auto.
-  - rewrite /= -(optimize_env_eq (GlobalContextMap.make Σ (fresh_globals_cons_inv wf))) //.
-    eapply optimize_decl_wf => //.
-  - rewrite /= -(optimize_env_eq (GlobalContextMap.make Σ (fresh_globals_cons_inv wf))) //.
-    now eapply fresh_global_optimize_env.
+  - rewrite /= -(remove_match_on_box_env_eq (GlobalContextMap.make Σ (fresh_globals_cons_inv wf))) //.
+    eapply remove_match_on_box_decl_wf => //.
+  - rewrite /= -(remove_match_on_box_env_eq (GlobalContextMap.make Σ (fresh_globals_cons_inv wf))) //.
+    now eapply fresh_global_remove_match_on_box_env.
 Qed.
 
-Definition optimize_program (p : eprogram_env) :=
-  (EOptimizePropDiscr.optimize_env p.1, EOptimizePropDiscr.optimize p.1 p.2).
+Definition remove_match_on_box_program (p : eprogram_env) :=
+(remove_match_on_box_env p.1, remove_match_on_box p.1 p.2).
 
-Definition optimize_program_wf {efl} (p : eprogram_env) {hastbox : has_tBox} {hastrel : has_tRel} :
-  wf_eprogram_env efl p -> wf_eprogram efl (optimize_program p).
+Definition remove_match_on_box_program_wf {efl} (p : eprogram_env) {hastbox : has_tBox} {hastrel : has_tRel} :
+  wf_eprogram_env efl p -> wf_eprogram efl (remove_match_on_box_program p).
 Proof.
   intros []; split.
-  now eapply optimize_env_wf.
-  cbn. eapply optimize_wellformed_irrel => //. now eapply optimize_wellformed.
+  now eapply remove_match_on_box_env_wf.
+  cbn. eapply remove_match_on_box_wellformed_irrel => //. now eapply remove_match_on_box_wellformed.
 Qed.
 
-Definition optimize_program_expanded {efl} (p : eprogram_env) :
+Definition remove_match_on_box_program_expanded {efl} (p : eprogram_env) :
   wf_eprogram_env efl p ->
-  expanded_eprogram_env_cstrs p -> expanded_eprogram_cstrs (optimize_program p).
+  expanded_eprogram_env_cstrs p -> expanded_eprogram_cstrs (remove_match_on_box_program p).
 Proof.
   unfold expanded_eprogram_env_cstrs.
   move=> [wfe wft] /andP[] etae etat.
   apply/andP; split.
-  cbn. eapply expanded_global_env_isEtaExp_env, optimize_env_expanded => //.
+  cbn. eapply expanded_global_env_isEtaExp_env, remove_match_on_box_env_expanded => //.
   now eapply isEtaExp_env_expanded_global_env.
   eapply expanded_isEtaExp.
-  eapply optimize_expanded_irrel => //.
-  now apply optimize_expanded, isEtaExp_expanded.
+  eapply remove_match_on_box_expanded_irrel => //.
+  now apply remove_match_on_box_expanded, isEtaExp_expanded.
 Qed.
diff --git a/erasure/theories/EWcbvEvalNamed.v b/erasure/theories/EWcbvEvalNamed.v
index 08e77b7d4..c3578d341 100644
--- a/erasure/theories/EWcbvEvalNamed.v
+++ b/erasure/theories/EWcbvEvalNamed.v
@@ -78,6 +78,8 @@ Section Wcbv.
     lookup Γ na = Some v ->
     eval Γ (tVar na) v
 
+  | eval_vbox : eval Γ tBox vBox
+
   | eval_box a t t' :
     eval Γ a vBox ->
     eval Γ t t' ->
@@ -148,7 +150,10 @@ Section Wcbv.
 
   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),
-          P Γ (tVar na) v (eval_var Γ na v e)) (f0 : ∀ (Γ : environment) (a t : term)
+          P Γ (tVar na) v (eval_var Γ na v e))
+
+      (f_vbox : ∀ (Γ : environment) (e : eval Γ tBox vBox), P Γ tBox vBox e)
+      (f0 : ∀ (Γ : environment) (a t : term)
                                                        (t' : value) (e : eval Γ a vBox),
           P Γ a vBox e
           → ∀ e0 : eval Γ t t',
@@ -249,6 +254,7 @@ Section Wcbv.
       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
+      | @eval_vbox _ => f_vbox Γ _
       | @eval_box _ a t0 t' e0 e1 => f0 Γ a t0 t' e0 (F Γ a vBox e0) e1 (F Γ t0 t' e1)
       | @eval_beta _ f10 na b a a' res Γ' e0 e1 e2 => f1 Γ f10 na b a a' res Γ' e0 (F Γ f10 (vClos na b Γ') e0) e1 (F Γ a a' e1) e2 (F (add na a' Γ') b res e2)
       | @eval_lambda _ na b => f2 Γ na b
@@ -963,7 +969,7 @@ Proof.
     { clear.  generalize ((List.rev (gen_many_fresh Γ ( (map dname m))) ++ Γ)).
       induction m in Γ |- *; cbn.
       - econstructor.
-      - intros. destruct a; cbn. destruct dname; cbn; try econstructor; eauto.  
+      - intros. destruct a; cbn. destruct dname; cbn; try econstructor; eauto.
     }
     { solve_all. unfold wf_fix in *. rtoProp. solve_all. clear H0. unfold test_def in *. cbn in *.
       eapply All_impl in H1. 2:{ intros ? [[] ].
@@ -974,7 +980,7 @@ Proof.
       generalize ((List.rev (gen_many_fresh Γ (map dname m)) ++ Γ)).
       intros. induction H1 in Γ |- *.
       - econstructor.
-      - cbn. destruct x; cbn. destruct dname; cbn; econstructor; eauto. 
+      - cbn. destruct x; cbn. destruct dname; cbn; econstructor; eauto.
     }
 Qed.
 
@@ -1226,7 +1232,9 @@ Definition dupfree (Γ : list ident) :=
 
 Fixpoint sunny Γ (t : term) : bool :=
   match t with
-  | tRel i => true
+  | tBox => true
+  | tRel _ => true
+  | tVar na => true
   | tEvar ev args => List.forallb (sunny Γ) args
   | tLambda (nNamed na) M => fresh na Γ && sunny (na :: Γ) M
   | tApp u v => sunny Γ u && sunny Γ v
@@ -1244,8 +1252,7 @@ Fixpoint sunny Γ (t : term) : bool :=
          dupfree names &&
            forallb (test_def (sunny (names ++ Γ))) mfix
   | tConstruct _ _ args => forallb (sunny Γ) args
-  | tConst _ => true
-  | _ => false
+  | _ => true
   end.
 
 Inductive wf : value -> Type :=
@@ -1363,6 +1370,13 @@ Proof.
   revert HE Hsunny. pattern E, s, v, Heval.
   revert E s v Heval.
   eapply eval_ind; intros; eauto; cbn in *; rtoProp; eauto using Forall.
+  - induction HE.
+    + cbn in *. congruence.
+    + unfold lookup in e. cbn in e. destruct x.
+      destruct eqb eqn:E.
+      * invs e. cbn in *; eauto.
+      * eapply IHHE. exact e.
+  - econstructor.
   - let X := match reverse goal with H : All _ _ -> _ -> _ |- _ => H end in
     do 2 forward X; eauto; inv X.
     let X1 := multimatch goal with H : _ |- _ => H end in
@@ -1514,6 +1528,8 @@ Proof.
 Qed.
  *)
 
+(*)
+
 Lemma represents_add_fresh nms Γ E vs s t :
   Γ ;;; E ⊩ s ~ t ->
   sunny nms s ->
@@ -1523,6 +1539,7 @@ Proof.
   revert Γ E s t.
   refine (@represents_ind _ (fun _ _ _ => True) _ _ _ _ _ _ _ _ _ _ _ _ _ _).
   all: intros; cbn in *; rtoProp; eauto.
+  - econstructor; eauto.
   - econstructor; eauto. eapply H; eauto.
     eapply sunny_subset; eauto. firstorder.
   - econstructor; eauto. eapply H0; eauto.
@@ -1549,6 +1566,8 @@ Proof.
       eapply incl_appr, incl_refl.
 Qed.
 
+*)
+
 Lemma NoDup_In_1 {A} (l1 l2 : list A) a :
     NoDup (l1 ++ l2) -> In a l1 -> ~ In a l2.
 Proof.
@@ -1853,6 +1872,8 @@ Proof.
        unfold cstr_arity in *.  invs H. lia.
        clear - Hvs; induction Hvs; econstructor; eauto. eapply r.
   - invs Hrep; cbn in *; try congruence; rtoProp.
+    + econstructor. split; eauto. eapply eval_vbox.
+    + econstructor. split; eauto. econstructor. eauto.
     + econstructor. split; eauto. econstructor.
     + destruct args'; congruence.
     + solve_all. eexists. split. 2: econstructor; eauto. 4: solve_all.
@@ -1868,5 +1889,130 @@ Proof.
       cbn in *. destruct H1 as (([? []] & ?) & ?).
       rewrite app_nil_r in r. all: eauto.
 
-      Unshelve. all: repeat econstructor. 
+      Unshelve. all: repeat econstructor.
 Qed.
+
+Lemma concat_sing {X} l :
+  List.concat (map (fun x :X  => [x]) l) = l.
+Proof.
+  induction l; cbn in *; try congruence.
+Qed.
+
+Lemma sunny_annotate Γ s :
+  sunny Γ (annotate Γ s).
+Proof.
+  induction s in Γ |- * using EInduction.term_forall_list_ind; cbn; eauto; rtoProp.
+  - destruct nth_error; cbn; eauto.
+  - solve_all.
+  - split; eauto. destruct n; eauto.
+    unfold fresh. destruct in_dec; cbn; eauto.
+    eapply gen_fresh_fresh in i; eauto.
+    destruct in_dec; cbn; eauto.
+    unfold fresh. destruct in_dec; cbn; eauto.
+    eapply gen_fresh_fresh in i1; eauto.
+    unfold fresh. destruct in_dec; cbn; eauto. exfalso; eauto.
+  - split; eauto. destruct n; eauto.
+    unfold fresh. destruct in_dec; cbn; eauto.
+    eapply gen_fresh_fresh in i; eauto.
+    destruct in_dec; cbn; eauto.
+    unfold fresh. destruct in_dec; cbn; eauto.
+    eapply gen_fresh_fresh in i1; eauto.
+    unfold fresh. destruct in_dec; cbn; eauto. exfalso; eauto.
+  - split; eauto.
+  - solve_all.
+  - split; eauto. solve_all. rtoProp. repeat split; eauto.
+    + solve_all. eapply In_All. intros.
+      unfold fresh. destruct in_dec; cbn; eauto.
+      exfalso. eapply NoDup_gen_many_fresh; eauto.
+    + unfold dupfree. destruct dupfree_dec_ident; eauto.
+      exfalso. eapply n.
+      rewrite flat_map_concat_map. rewrite map_map.
+      rewrite concat_sing.
+      eapply NoDup_gen_many_fresh; eauto.
+    + rewrite flat_map_concat_map map_map concat_sing.
+      eapply sunny_subset. eapply H.
+      intros ? ? %in_app_iff. eapply in_app_iff. rewrite <- in_rev in H0.
+      eauto.
+  - repeat split; eauto.
+    1:{ unfold map_def_name.  generalize (annotate (List.rev (gen_many_fresh Γ (map dname m)) ++ Γ)).
+        cbn. intros. solve_all.
+        clear. induction m in Γ |- *.
+        - cbn. econstructor.
+        - cbn. destruct a; cbn. destruct dname; cbn.
+          + econstructor; cbn.
+            unfold fresh. destruct in_dec; eauto; cbn. exfalso.
+            eapply gen_fresh_fresh; eauto.
+            specialize (IHm (gen_fresh "wildcard" Γ :: Γ)).
+            solve_all. destruct x, dname; cbn in *; try congruence.
+            unfold fresh in *. repeat (destruct in_dec; cbn in *; try congruence).
+            exfalso. eapply n. eauto.
+          + econstructor; cbn.
+            { destruct in_dec; cbn.
+              + unfold fresh. destruct in_dec; eauto; cbn. exfalso.
+                eapply gen_fresh_fresh; eauto.
+              + unfold fresh. destruct in_dec; eauto; cbn. exfalso. eauto. }
+            specialize (IHm ((if is_left (in_dec (ReflectEq_EqDec IdentOT.reflect_eq_string) i Γ) then gen_fresh i Γ else i) :: Γ)).
+            solve_all. destruct x, dname; cbn in *; try congruence.
+            destruct in_dec; cbn in *.
+            * unfold fresh in *.
+              repeat (destruct in_dec; cbn in *; try congruence).
+              exfalso. eapply n. eauto.
+            * unfold fresh in *.
+              repeat (destruct in_dec; cbn in *; try congruence).
+              exfalso. eapply n0. eauto.
+    }
+    { unfold map_def_name. generalize (annotate (List.rev (gen_many_fresh Γ (map dname m)) ++ Γ)).
+      intros t0.
+      assert ((flat_map (λ d : def term, match dname d with
+      | nAnon => []
+      | nNamed i => [i]
+      end)
+(map2 (λ (d : def term) (na : ident), {| dname := nNamed na; dbody := t0 (dbody d); rarg := rarg d |}) m (gen_many_fresh Γ (map dname m)))) = (gen_many_fresh Γ (map dname m))) as ->.
+      { pose proof (gen_many_fresh_length Γ (map dname m)). rewrite map_length in H. revert H.
+        generalize (gen_many_fresh Γ (map dname m)). clear. induction m; destruct l; cbn; try congruence.
+        intros. f_equal. eapply IHm. lia. }
+
+      unfold dupfree. intros. destruct dupfree_dec_ident; cbn; eauto.
+      exfalso. apply n0.
+      eapply NoDup_gen_many_fresh.
+    }
+    {
+      unfold map_def_name.
+      assert ((flat_map (λ d : def term, match dname d with
+      | nAnon => []
+      | nNamed i => [i]
+      end)
+(map2 (λ (d : def term) (na : ident), {| dname := nNamed na; dbody := annotate (List.rev (gen_many_fresh Γ (map dname m)) ++ Γ) (dbody d); rarg := rarg d |}) m (gen_many_fresh Γ (map dname m)))) = (gen_many_fresh Γ (map dname m))) as ->.
+      { generalize (annotate (List.rev (gen_many_fresh Γ (map dname m)) ++ Γ)).
+         pose proof (gen_many_fresh_length Γ (map dname m)). rewrite map_length in H. revert H.
+        generalize (gen_many_fresh Γ (map dname m)). clear. induction m; destruct l; cbn; try congruence.
+        intros. f_equal. eapply IHm. lia. }
+
+      solve_all.
+      eapply (All_impl(P := (λ x : def term, test_def (sunny (List.rev (gen_many_fresh Γ (map dname m)) ++ Γ)) x))).
+      2:{ intros x H. unfold test_def. eapply sunny_subset. eassumption.
+          intros ? ? % in_app_iff. eapply in_app_iff. rewrite <- in_rev. eauto. }
+
+      generalize (List.rev (gen_many_fresh Γ (map dname m))).
+      pose proof (gen_many_fresh_length Γ (map dname m)). rewrite map_length in H. revert H.
+      generalize (gen_many_fresh Γ (map dname m)). clear - X. induction X.
+      + intros l. destruct l; cbn in *; try congruence. econstructor.
+      + intros []; cbn in *; try congruence. intros. econstructor; eauto.
+    }
+Qed.
+
+Lemma eval_to_eval_named_full (Σ Σ' : global_context) s t :
+  wf_glob Σ ->
+  Forall (fun d => match d.2 with ConstantDecl (Build_constant_body (Some d)) => sunny [] d | _ => true end) Σ' ->
+  All2 (fun d d' => d.1 = d'.1 × match d.2 with ConstantDecl (Build_constant_body (Some body)) =>
+    ∑ body', d'.2 = ConstantDecl (Build_constant_body (Some body')) × [] ;;; [] ⊩ body' ~ body
+  | decl => d'.2 = decl
+  end) Σ Σ' ->
+  EWcbvEval.eval Σ s t ->
+  wellformed Σ 0 s ->
+  ∑ v, ⊩ v ~ t × eval Σ' [] (annotate [] s) v.
+Proof.
+  intros. eapply eval_to_eval_named; eauto.
+  eapply sunny_annotate.
+  eapply nclosed_represents. eauto.
+Qed.
\ No newline at end of file
diff --git a/erasure/theories/Typed/Extraction.v b/erasure/theories/Typed/Extraction.v
index 07d2524ff..2e7c75a9d 100644
--- a/erasure/theories/Typed/Extraction.v
+++ b/erasure/theories/Typed/Extraction.v
@@ -89,7 +89,7 @@ Program Definition extract_pcuic_env
            (ignore : kername -> bool) : result ExAst.global_env _ :=
   let Σ := timed "Erasure" (fun _ => erase_global_decls_deps_recursive (declarations Σ) (universes Σ) (retroknowledge Σ) wfΣ seeds ignore) in
   if optimize_prop_discr params then
-    let Σ := timed "Removal of prop discrimination" (fun _ => OptimizePropDiscr.optimize_env Σ _) in
+    let Σ := timed "Removal of prop discrimination" (fun _ => OptimizePropDiscr.remove_match_on_box_env Σ _) in
     compose_transforms (extract_transforms params) Σ
   else
     Ok Σ.
diff --git a/erasure/theories/Typed/OptimizePropDiscr.v b/erasure/theories/Typed/OptimizePropDiscr.v
index a2fd1965c..b5036ae65 100644
--- a/erasure/theories/Typed/OptimizePropDiscr.v
+++ b/erasure/theories/Typed/OptimizePropDiscr.v
@@ -3,13 +3,13 @@
 From MetaCoq.Erasure.Typed Require Import ExAst.
 From MetaCoq.Erasure Require Import EOptimizePropDiscr.
 
-Definition optimize_constant_body Σ cst :=
+Definition remove_match_on_box_constant_body Σ cst :=
   {| cst_type := cst_type cst;
-     cst_body := option_map (optimize Σ) (cst_body cst) |}.
+     cst_body := option_map (remove_match_on_box Σ) (cst_body cst) |}.
 
-Definition optimize_decl Σ d :=
+Definition remove_match_on_box_decl Σ d :=
   match d with
-  | ConstantDecl cst => ConstantDecl (optimize_constant_body Σ cst)
+  | ConstantDecl cst => ConstantDecl (remove_match_on_box_constant_body Σ cst)
   | _ => d
   end.
 
@@ -36,21 +36,21 @@ Proof.
     now apply trans_env_fresh_global.
 Qed.
 
-Program Definition optimize_env (Σ : global_env) (fgΣ : fresh_globals Σ) : global_env :=
-  List.map (MCProd.on_snd (optimize_decl (EEnvMap.GlobalContextMap.make (trans_env Σ) _))) Σ.
+Program Definition remove_match_on_box_env (Σ : global_env) (fgΣ : fresh_globals Σ) : global_env :=
+  List.map (MCProd.on_snd (remove_match_on_box_decl (EEnvMap.GlobalContextMap.make (trans_env Σ) _))) Σ.
 Next Obligation.
   now apply trans_env_fresh_globals.
 Qed.
 
 Module Ee := EWcbvEval.
 
-Lemma trans_env_optimize_env Σ fgΣ :
-  trans_env (optimize_env Σ fgΣ) =
-  EOptimizePropDiscr.optimize_env (EEnvMap.GlobalContextMap.make (trans_env Σ) (trans_env_fresh_globals _ fgΣ)).
+Lemma trans_env_remove_match_on_box_env Σ fgΣ :
+  trans_env (remove_match_on_box_env Σ fgΣ) =
+  EOptimizePropDiscr.remove_match_on_box_env (EEnvMap.GlobalContextMap.make (trans_env Σ) (trans_env_fresh_globals _ fgΣ)).
 Proof.
   unfold trans_env.
-  unfold EOptimizePropDiscr.optimize_env.
-  unfold optimize_env.
+  unfold EOptimizePropDiscr.remove_match_on_box_env.
+  unfold remove_match_on_box_env.
   unfold MCProd.on_snd. cbn.
   rewrite !List.map_map.
   apply List.map_ext.
@@ -62,7 +62,7 @@ Proof.
   now destruct o.
 Qed.
 
-Lemma optimize_correct `{EWellformed.EEnvFlags} `{Ee.WcbvFlags} Σ fgΣ t v :
+Lemma remove_match_on_box_correct `{EWellformed.EEnvFlags} `{Ee.WcbvFlags} Σ fgΣ t v :
   EWcbvEval.with_constructor_as_block = false ->
   ELiftSubst.closed t = true ->
   EGlobalEnv.closed_env (trans_env Σ) = true ->
@@ -70,12 +70,12 @@ Lemma optimize_correct `{EWellformed.EEnvFlags} `{Ee.WcbvFlags} Σ fgΣ t v :
   @Prelim.Ee.eval _ (trans_env Σ) t v ->
   @Prelim.Ee.eval
       (EWcbvEval.disable_prop_cases _)
-      (trans_env (optimize_env Σ fgΣ))
-      (optimize (EEnvMap.GlobalContextMap.make (trans_env Σ) (trans_env_fresh_globals _ fgΣ)) t)
-      (optimize (EEnvMap.GlobalContextMap.make (trans_env Σ) (trans_env_fresh_globals _ fgΣ)) v).
+      (trans_env (remove_match_on_box_env Σ fgΣ))
+      (remove_match_on_box (EEnvMap.GlobalContextMap.make (trans_env Σ) (trans_env_fresh_globals _ fgΣ)) t)
+      (remove_match_on_box (EEnvMap.GlobalContextMap.make (trans_env Σ) (trans_env_fresh_globals _ fgΣ)) v).
 Proof.
   intros ? cl_t cl_env wfg ev.
-  rewrite trans_env_optimize_env.
+  rewrite trans_env_remove_match_on_box_env.
   remember (EEnvMap.GlobalContextMap.make _ _) as Σ0.
-  unshelve eapply EOptimizePropDiscr.optimize_correct;subst;cbn;eauto.
+  unshelve eapply EOptimizePropDiscr.remove_match_on_box_correct;subst;cbn;eauto.
 Qed.
diff --git a/erasure/theories/Typed/TypeAnnotations.v b/erasure/theories/Typed/TypeAnnotations.v
index 3815a4a8e..e6b195cd1 100644
--- a/erasure/theories/Typed/TypeAnnotations.v
+++ b/erasure/theories/Typed/TypeAnnotations.v
@@ -699,7 +699,7 @@ Module AnnotOptimizePropDiscr.
       intros ? a'; exact (f _ _ a').
   Defined.
 
-  Definition annot_optimize Σ {t} (a : annots box_type t) : annots box_type (optimize Σ t).
+  Definition annot_remove_match_on_box Σ {t} (a : annots box_type t) : annots box_type (remove_match_on_box Σ t).
   Proof.
     revert t a.
     fix f 1.
@@ -708,7 +708,7 @@ Module AnnotOptimizePropDiscr.
     - exact (a.1, f _ a.2).
     - exact (a.1, (f _ a.2.1, f _ a.2.2)).
     - exact (a.1, (f _ a.2.1, f _ a.2.2)).
-    - assert (br_annots : bigprod (fun br => annots box_type br.2) (map (on_snd (optimize Σ)) l)).
+    - assert (br_annots : bigprod (fun br => annots box_type br.2) (map (on_snd (remove_match_on_box Σ)) l)).
       { refine (bigprod_map _ a.2.2).
         intros ? a'; apply (f _ a'). }
       unfold isprop_ind.
@@ -743,32 +743,32 @@ Module AnnotOptimizePropDiscr.
       intros ? a'; exact (f _ a').
   Defined.
 
-  Definition annot_optimize_constant_body Σ {cst} (a : constant_body_annots box_type cst) :
-    constant_body_annots box_type (optimize_constant_body Σ cst).
+  Definition annot_remove_match_on_box_constant_body Σ {cst} (a : constant_body_annots box_type cst) :
+    constant_body_annots box_type (remove_match_on_box_constant_body Σ cst).
   Proof.
-    unfold constant_body_annots, optimize_constant_body in *.
+    unfold constant_body_annots, remove_match_on_box_constant_body in *.
     cbn.
     destruct ExAst.cst_body; cbn; [|exact tt].
-    apply annot_optimize.
+    apply annot_remove_match_on_box.
     exact a.
   Defined.
 
-  Definition annot_optimize_decl Σ {decl} (a : global_decl_annots box_type decl) :
-    global_decl_annots box_type (optimize_decl Σ decl).
+  Definition annot_remove_match_on_box_decl Σ {decl} (a : global_decl_annots box_type decl) :
+    global_decl_annots box_type (remove_match_on_box_decl Σ decl).
   Proof.
-    unfold global_decl_annots, optimize_decl in *.
+    unfold global_decl_annots, remove_match_on_box_decl in *.
     destruct decl; [|exact tt|exact tt].
-    apply annot_optimize_constant_body.
+    apply annot_remove_match_on_box_constant_body.
     exact a.
   Defined.
 
-  Definition annot_optimize_env Σ fgΣ (a : env_annots box_type Σ) :
-    env_annots box_type (optimize_env Σ fgΣ).
+  Definition annot_remove_match_on_box_env Σ fgΣ (a : env_annots box_type Σ) :
+    env_annots box_type (remove_match_on_box_env Σ fgΣ).
   Proof.
-    unfold env_annots, optimize_env.
+    unfold env_annots, remove_match_on_box_env.
     apply bigprod_map.
     - intros.
-      apply annot_optimize_decl.
+      apply annot_remove_match_on_box_decl.
       exact X.
     - exact a.
   Defined.
@@ -803,7 +803,7 @@ Proof.
   unfold extract_pcuic_env.
   destruct optimize_prop_discr.
   + apply annot_compose_transforms; [|exact all].
-    apply AnnotOptimizePropDiscr.annot_optimize_env.
+    apply AnnotOptimizePropDiscr.annot_remove_match_on_box_env.
     apply annotate_types_erase_global_decls_deps_recursive.
   + apply annotate_types_erase_global_decls_deps_recursive.
 Defined.