diff --git a/.vscode/metacoq.code-workspace b/.vscode/metacoq.code-workspace
index d6ac88a4c..0c15d9de8 100644
--- a/.vscode/metacoq.code-workspace
+++ b/.vscode/metacoq.code-workspace
@@ -11,27 +11,28 @@
 
 
 
-			"-R", "safechecker-plugin/theories,MetaCoq.SafeCheckerPlugin",
 
-			"-R", "utils/theories,MetaCoq.Utils",
-			"-R", "common/theories,MetaCoq.Common",
-			"-R", "template-pcuic/theories,MetaCoq.TemplatePCUIC",
+			"-R", "safechecker-plugin/theories","MetaCoq.SafeCheckerPlugin",
 
-		"-I template-coq",
+			"-R", "utils/theories","MetaCoq.Utils",
+			"-R", "common/theories","MetaCoq.Common",
+			"-R", "template-pcuic/theories","MetaCoq.TemplatePCUIC",
+
+		"-I", "template-coq",
     	//	"-bt", get backtraces from Coq on errors
-		"-I template-coq/build",
-		"-R", "template-coq/theories,MetaCoq.Template",
-		"-R", "examples,MetaCoq.Examples",
-		"-R", "checker/theories,MetaCoq.Checker",
-		"-R", "pcuic/theories,MetaCoq.PCUIC",
-		"-I safechecker/src",
-		"-R", "safechecker/theories,MetaCoq.SafeChecker",
-		"-I erasure/src",
-		"-R", "erasure/theories,MetaCoq.Erasure",
-		"-R", "erasure-plugin/theories,MetaCoq.ErasurePlugin",
-		"-R", "translations,MetaCoq.Translations",
-		"-R", "test-suite/plugin-demo/theories,MetaCoq.ExtractedPluginDemo",
-		"-R", "test-suite,MetaCoq.TestSuite"
+		"-I", "template-coq/build",
+		"-R", "template-coq/theories", "MetaCoq.Template",
+		"-R", "examples", "MetaCoq.Examples",
+		"-R", "checker/theories" "MetaCoq.Checker",
+		"-R", "pcuic/theories","MetaCoq.PCUIC",
+		"-I", "safechecker/src",
+		"-R", "safechecker/theories","MetaCoq.SafeChecker",
+		"-I", "erasure/src",
+		"-R", "erasure/theories","MetaCoq.Erasure",
+		"-R", "erasure-plugin/theories","MetaCoq.ErasurePlugin",
+		"-R", "translations","MetaCoq.Translations",
+		"-R", "test-suite/plugin-demo/theories","MetaCoq.ExtractedPluginDemo",
+		"-R", "test-suite","MetaCoq.TestSuite"
 	    ],
 
 	 // When enabled, will trim trailing whitespace when saving a file.
diff --git a/erasure-plugin/_PluginProject.in b/erasure-plugin/_PluginProject.in
index dc5b48e22..217e83bb3 100644
--- a/erasure-plugin/_PluginProject.in
+++ b/erasure-plugin/_PluginProject.in
@@ -50,6 +50,8 @@ src/pCUICSafeReduce.ml
 src/pCUICSafeRetyping.ml
 src/pCUICSafeRetyping.mli
 
+src/ePrimitive.mli
+src/ePrimitive.ml
 src/eAst.ml
 src/eAst.mli
 src/eAstUtils.ml
diff --git a/erasure-plugin/src/metacoq_erasure_plugin.mlpack b/erasure-plugin/src/metacoq_erasure_plugin.mlpack
index 29a6ec0d0..8bd95c56b 100644
--- a/erasure-plugin/src/metacoq_erasure_plugin.mlpack
+++ b/erasure-plugin/src/metacoq_erasure_plugin.mlpack
@@ -39,6 +39,7 @@ PCUICUnivSubst
 PCUICSafeReduce
 PCUICSafeRetyping
 
+EPrimitive
 EAst
 EAstUtils
 ELiftSubst
diff --git a/erasure/theories/EAstUtils.v b/erasure/theories/EAstUtils.v
index ec168e08e..ec9068a60 100644
--- a/erasure/theories/EAstUtils.v
+++ b/erasure/theories/EAstUtils.v
@@ -2,7 +2,7 @@
 From Equations Require Import Equations.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import BasicAst Kernames.
-From MetaCoq.Erasure Require Import EAst.
+From MetaCoq.Erasure Require Import EPrimitive EAst.
 Require Import ssreflect ssrbool.
 
 Global Hint Resolve app_tip_nil : core.
@@ -378,24 +378,36 @@ Fixpoint string_of_term (t : term) : string :=
 
 (** Compute all the global environment dependencies of the term *)
 
-Fixpoint term_global_deps (t : EAst.term) :=
+Section PrimDeps.
+  Context (deps : term -> KernameSet.t).
+
+  Equations prim_global_deps (p : prim_val term) : KernameSet.t :=
+   | (primInt; primIntModel i) => KernameSet.empty
+   | (primFloat; primFloatModel f) => KernameSet.empty
+   | (primArray; primArrayModel a) =>
+      List.fold_left (fun acc x => KernameSet.union (deps x) acc) a.(array_value) (deps a.(array_default)).
+
+End PrimDeps.
+
+Fixpoint term_global_deps (t : term) :=
   match t with
-  | EAst.tConst kn => KernameSet.singleton kn
-  | EAst.tConstruct {| inductive_mind := kn |} _ args =>
+  | tConst kn => KernameSet.singleton kn
+  | tConstruct {| inductive_mind := kn |} _ args =>
      List.fold_left (fun acc x => KernameSet.union (term_global_deps x) acc) args
           (KernameSet.singleton kn)
-  | EAst.tLambda _ x => term_global_deps x
-  | EAst.tApp x y
-  | EAst.tLetIn _ x y => KernameSet.union (term_global_deps x) (term_global_deps y)
-  | EAst.tCase (ind, _) x brs =>
+  | tLambda _ x => term_global_deps x
+  | tApp x y
+  | tLetIn _ x y => KernameSet.union (term_global_deps x) (term_global_deps y)
+  | tCase (ind, _) x brs =>
     KernameSet.union (KernameSet.singleton (inductive_mind ind))
       (List.fold_left (fun acc x => KernameSet.union (term_global_deps (snd x)) acc) brs
         (term_global_deps x))
-   | EAst.tFix mfix _ | EAst.tCoFix mfix _ =>
-     List.fold_left (fun acc x => KernameSet.union (term_global_deps (EAst.dbody x)) acc) mfix
+   | tFix mfix _ | tCoFix mfix _ =>
+     List.fold_left (fun acc x => KernameSet.union (term_global_deps (dbody x)) acc) mfix
       KernameSet.empty
-  | EAst.tProj p c =>
+  | tProj p c =>
     KernameSet.union (KernameSet.singleton (inductive_mind p.(proj_ind)))
       (term_global_deps c)
+  | tPrim p => prim_global_deps term_global_deps p
   | _ => KernameSet.empty
   end.
\ No newline at end of file
diff --git a/erasure/theories/EConstructorsAsBlocks.v b/erasure/theories/EConstructorsAsBlocks.v
index 78dab5e91..58fe52125 100644
--- a/erasure/theories/EConstructorsAsBlocks.v
+++ b/erasure/theories/EConstructorsAsBlocks.v
@@ -2,7 +2,7 @@
 From Coq Require Import Utf8 Program.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import config Kernames BasicAst EnvMap.
-From MetaCoq.Erasure Require Import EAst EAstUtils EInduction EArities
+From MetaCoq.Erasure Require Import EPrimitive EAst EAstUtils EInduction EArities
     ELiftSubst ESpineView EGlobalEnv EWellformed EEnvMap
     EWcbvEval EEtaExpanded ECSubst EWcbvEvalEtaInd EProgram.
 
@@ -62,7 +62,7 @@ Section transform_blocks.
     | tVar n => EAst.tVar n
     | tConst n => EAst.tConst n
     | tConstruct ind i block_args => EAst.tConstruct ind i []
-    | tPrim p => EAst.tPrim p }.
+    | tPrim p => EAst.tPrim (map_primIn p (fun x H => transform_blocks x)) }.
   Proof.
     all:try lia.
     all:try apply (In_size); tea.
@@ -82,6 +82,7 @@ Section transform_blocks.
       change (fun x => size x) with size in H.
       pose proof (size_mkApps_l napp nnil). lia.
     - eapply (In_size snd size) in H. cbn in *. lia.
+    - now eapply InPrim_size in H.
   Qed.
 
   End Def.
@@ -116,6 +117,7 @@ Section transform_blocks.
     unfold test_def in *;
     simpl closed in *;
     try solve [simpl; subst; simpl closed; f_equal; auto; rtoProp; solve_all; solve_all]; try easy.
+    - solve_all_k 6.
     - rewrite !closedn_mkApps in H1 *.
       rtoProp; intuition auto. solve_all.
     - destruct (chop nargs v) eqn:E.
@@ -714,6 +716,7 @@ Proof.
     cbn -[transform_blocks isEtaExp] in *. rtoProp. eauto.
   - unfold wf_fix in *. len. solve_all. rtoProp; intuition auto.
     solve_all.
+  - solve_all_k 7.
   - rewrite !wellformed_mkApps in Hw |- * => //. rtoProp.
     eapply isEtaExp_mkApps in H1. rewrite decompose_app_mkApps in H1; eauto.
     destruct construct_viewc; eauto. cbn in d. eauto.
diff --git a/erasure/theories/EDeps.v b/erasure/theories/EDeps.v
index 8189ffdfe..dd272ca21 100644
--- a/erasure/theories/EDeps.v
+++ b/erasure/theories/EDeps.v
@@ -1,9 +1,9 @@
 From Coq Require Import Arith List.
 From Equations Require Import Equations.
 From MetaCoq.PCUIC Require Import
-     PCUICAst PCUICAstUtils PCUICTyping PCUICInversion PCUICWeakeningEnv PCUICWeakeningEnvTyp.
+     PCUICPrimitive PCUICAst PCUICAstUtils PCUICTyping PCUICInversion PCUICWeakeningEnv PCUICWeakeningEnvTyp.
 Set Warnings "-notation-overridden".
-From MetaCoq.Erasure Require Import EAst EAstUtils ECSubst EInduction
+From MetaCoq.Erasure Require Import EPrimitive EAst EAstUtils ECSubst EInduction
   ELiftSubst EGlobalEnv EWcbvEval Extract ESubstitution.
 From MetaCoq.Erasure Require EExtends.
 Set Warnings "+notation-overridden".
@@ -84,6 +84,8 @@ Proof.
     depelim X.
     constructor; [|easy].
     now apply e.
+  - depelim X; depelim er; constructor; cbn. solve_all.
+    destruct p. solve_all.
 Qed.
 
 Lemma erases_deps_subst Σ Σ' s k t :
@@ -134,6 +136,7 @@ Proof.
     depelim X.
     constructor; [|easy].
     now apply e.
+  - depelim X; depelim er; constructor; cbn; intuition auto; solve_all.
 Qed.
 
 Lemma erases_deps_subst1 Σ Σ' t k u :
@@ -191,6 +194,7 @@ Proof.
     depelim X.
     constructor; [|easy].
     now apply e.
+  - depelim X; depelim er; constructor; cbn; intuition auto; solve_all.
 Qed.
 
 Lemma erases_deps_substl Σ Σ' s t :
@@ -402,7 +406,7 @@ Lemma erases_deps_forall_ind Σ Σ'
          Forall (fun d : Extract.E.def Extract.E.term => erases_deps Σ Σ' (Extract.E.dbody d)) defs ->
          Forall (fun d => P (E.dbody d)) defs ->
          P (Extract.E.tCoFix defs i))
-  (Hprim : forall p, P (Extract.E.tPrim p)):
+  (Hprim : forall p, primProp (erases_deps Σ Σ') p -> primProp P p -> P (Extract.E.tPrim p)):
   forall t, erases_deps Σ Σ' t -> P t.
 Proof.
   fix f 2.
@@ -441,6 +445,15 @@ Proof.
     fix f' 2.
     intros defs []; [now constructor|].
     constructor; [now apply f|now apply f'].
+  - eapply Hprim; tea; constructor.
+  - eapply Hprim; tea; constructor.
+  - eapply Hprim; tea; constructor.
+    intuition auto; solve_all.
+    split. auto. destruct a as [d v]. cbn in *.
+    eapply Forall_All.
+    revert v H.
+    fix aux 2.
+    intros ? [];constructor; auto.
 Defined.
 
 (* Lemma fresh_global_erase {cf : checker_flags} Σ Σ' kn :
@@ -559,6 +572,7 @@ Proof.
     rewrite H in declm.
     eapply PCUICWeakeningEnv.lookup_env_Some_fresh in kn_fresh.
     eauto. eauto.
+  - depelim X0; intuition auto; constructor; auto.
 Qed.
 
 Derive Signature for erases_global_decls.
@@ -681,6 +695,8 @@ Proof.
     depelim all_deps.
     destruct p as (?&?&?).
     now constructor; eauto.
+  - eapply inversion_Prim in wt as [prim_ty [decl []]]; eauto.
+    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' ->
diff --git a/erasure/theories/EEtaExpanded.v b/erasure/theories/EEtaExpanded.v
index 18cccf6e2..96377e3bd 100644
--- a/erasure/theories/EEtaExpanded.v
+++ b/erasure/theories/EEtaExpanded.v
@@ -5,7 +5,7 @@
 From Coq Require Import Utf8 Program.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import config Kernames EnvMap BasicAst.
-From MetaCoq.Erasure Require Import EAst EAstUtils EInduction EGlobalEnv EExtends EWellformed ELiftSubst ESpineView ECSubst EWcbvEval EWcbvEvalInd EProgram.
+From MetaCoq.Erasure Require Import EPrimitive EAst EAstUtils EInduction EGlobalEnv EExtends EWellformed ELiftSubst ESpineView ECSubst EWcbvEval EWcbvEvalInd EProgram.
 
 Local Open Scope string_scope.
 Set Asymmetric Patterns.
@@ -75,7 +75,7 @@ Section isEtaExp.
     | tBox => true
     | tVar _ => true
     | tConst _ => true
-    | tPrim _ => true
+    | tPrim p => test_primIn p (fun x H => isEtaExp x)
     | tConstruct ind i block_args => isEtaExp_app ind i 0 && is_nil block_args }.
   Proof.
     all:try lia.
@@ -92,11 +92,15 @@ Section isEtaExp.
       change (fun x => size x) with size in H.
       pose proof (size_mkApps_l napp nnil). lia.
     - eapply (In_size snd size) in H. cbn in H; lia.
+    - destruct p as [? []]; cbn in *; intuition eauto.
+      subst. lia.
+      eapply (In_size id size) in H0. unfold id in H0.
+      change (fun x => size x) with size in H0. lia.
   Qed.
 
 End isEtaExp.
 
-Global Hint Rewrite @forallb_InP_spec : isEtaExp.
+Global Hint Rewrite @test_primIn_spec @forallb_InP_spec : isEtaExp.
 Tactic Notation "simp_eta" "in" hyp(H) := simp isEtaExp in H; rewrite -?isEtaExp_equation_1 in H.
 Ltac simp_eta := simp isEtaExp; rewrite -?isEtaExp_equation_1.
 
@@ -276,8 +280,8 @@ Section WeakEtaExp.
       eapply a0 => //.
     - move/andP: H0 => [] etaexp h.
       rewrite csubst_mkApps /=.
-      rewrite isEtaExp_Constructor. solve_all.
-      rewrite map_length. rtoProp; solve_all. solve_all.
+      rewrite isEtaExp_Constructor; solve_all.
+      rtoProp; solve_all. solve_all.
       now destruct block_args.
     - rewrite csubst_mkApps /=.
       move/andP: H1 => [] eu ev.
@@ -417,6 +421,7 @@ Proof.
   - eapply In_All in H; solve_all.
     move/andP: b => [] -> /=. eauto.
   - eapply In_All in H; solve_all.
+  - solve_all.
   - eapply In_All in H; solve_all.
     rewrite isEtaExp_Constructor //. rtoProp; intuition auto.
     eapply isEtaExp_app_extends; tea.
@@ -471,7 +476,7 @@ Inductive expanded : term -> Prop :=
     #|args| >= cstr_arity mind cdecl ->
     Forall expanded args ->
     expanded (mkApps (tConstruct ind idx []) args)
-| expanded_tPrim p : expanded (tPrim p)
+| expanded_tPrim p : primProp expanded p -> expanded (tPrim p)
 | expanded_tBox : expanded tBox.
 
 End expanded.
@@ -510,7 +515,7 @@ forall (Σ : global_declarations) (P : term -> Prop),
    (args : list term),
  declared_constructor Σ (ind, idx) mind idecl cdecl ->
  #|args| >= cstr_arity mind cdecl -> Forall (expanded Σ) args -> Forall P args -> P (mkApps (tConstruct ind idx []) args)) ->
-(forall p, P (tPrim p)) ->
+(forall p, primProp (expanded Σ) p -> primProp P p -> P (tPrim p)) ->
 (P tBox) ->
 forall t : term, expanded Σ t -> P t.
 Proof.
@@ -523,6 +528,9 @@ Proof.
   - eapply H8; eauto. induction H13; econstructor; cbn in *; intuition eauto.
   - eapply H9; eauto. induction H13; econstructor; cbn in *; eauto.
   - eapply H10; eauto. clear - H15 f. induction H15; econstructor; cbn in *; eauto.
+  - eapply H11; eauto.
+    depelim X; constructor. destruct p; split; eauto.
+    eapply (make_All_All f a0).
 Qed.
 
 Local Hint Constructors expanded : core.
@@ -595,6 +603,7 @@ Proof.
     intuition auto.
   - econstructor. rewrite forallb_InP_spec in H0. eapply forallb_Forall in H0.
     eapply In_All in H. solve_all.
+  - econstructor. rewrite test_primIn_spec in H0. solve_all.
   - rtoProp. eapply In_All in H.
     rewrite forallb_InP_spec in H2. eapply forallb_Forall in H2.
     eapply isEtaExp_app_expanded in H0 as (? & ? & ? & ? & ?).
@@ -621,6 +630,7 @@ Proof.
   - rewrite isEtaExp_Constructor. rtoProp; repeat split.
     2: eapply forallb_Forall.
     2: solve_all. eapply expanded_isEtaExp_app_; eauto.
+  - solve_all.
 Qed.
 
 Lemma expanded_global_env_isEtaExp_env {Σ} : expanded_global_env Σ -> isEtaExp_env Σ.
@@ -695,6 +705,7 @@ Proof.
   - simp_eta. rtoProp; intuition auto.
     eapply In_All in H0; solve_all.
   - eapply In_All in H. simp_eta; rtoProp; intuition auto. solve_all.
+  - simp_eta. solve_all_k 7. primProp. solve_all.
   - eapply In_All in H. simp_eta; rtoProp; intuition auto.
     rewrite EEtaExpanded.isEtaExp_Constructor. rtoProp; repeat split. eauto.
     solve_all. destruct block_args; cbn in *; eauto.
diff --git a/erasure/theories/EEtaExpandedFix.v b/erasure/theories/EEtaExpandedFix.v
index 257deaee4..3d50dab63 100644
--- a/erasure/theories/EEtaExpandedFix.v
+++ b/erasure/theories/EEtaExpandedFix.v
@@ -65,23 +65,6 @@ Inductive expanded (Γ : list nat): term -> Prop :=
 
 End expanded.
 
-Section make_All.
-  Context {A} {B : A -> Type} (f : forall x : A, B x).
-
-  Equations make_All (l : list A) : All B l :=
-  | [] := All_nil
-  | hd :: tl := All_cons (f hd) (make_All tl).
-End make_All.
-
-Section make_All_All.
-  Context {A} {B : A -> Type} {C : A -> Type} (f : forall x : A, B x -> C x).
-
-  Equations make_All_All {l : list A} (a : All B l) : All C l :=
-  | All_nil := All_nil
-  | All_cons bhd btl := All_cons (f _ bhd) (make_All_All btl).
-
-End make_All_All.
-
 Lemma expanded_ind :
   ∀ (Σ : global_declarations) (P : list nat → term → Prop),
      (∀ (Γ : list nat) (n : nat) (args : list term) (m : nat),
@@ -287,40 +270,6 @@ Section isEtaExp.
     | None => false
     end.
 
-  Section PrimIn.
-    Context {term : Set}.
-
-    Equations InPrim (x : term) (p : prim_val term) : Prop :=
-      | x | (primInt; primIntModel i) := False
-      | x | (primFloat; primFloatModel _) := False
-      | x | (primArray; primArrayModel a) :=
-        x = a.(array_default) \/ In x a.(array_value).
-
-    Lemma InPrim_primProp p P : (forall x, InPrim x p -> P x) -> primProp P p.
-    Proof.
-      intros hin.
-      destruct p as [? []]; constructor.
-      split. eapply hin; eauto. now left.
-      cbn in hin.
-      induction (array_value a); constructor.
-      eapply hin. now right; left. eapply IHl.
-      intros. eapply hin. intuition eauto. now right; right.
-    Qed.
-
-    Equations test_primIn (p : prim_val term) (f : forall x : term, InPrim x p -> bool) : bool :=
-      | (primInt; primIntModel i) | _ := true
-      | (primFloat; primFloatModel _) | _ := true
-      | (primArray; primArrayModel a) | f :=
-        f a.(array_default) (or_introl eq_refl) && forallb_InP a.(array_value) (fun x H => f x (or_intror H)).
-
-    Lemma test_primIn_spec p (f : term -> bool) :
-      test_primIn p (fun x H => f x) = test_prim f p.
-    Proof.
-      funelim (test_primIn p (fun x H => f x)); cbn => //.
-      rewrite forallb_InP_spec //.
-    Qed.
-  End PrimIn.
-
   Import TermSpineView.
 
   Definition is_nil {A} (l : list A) := match l with nil => true | _ => false end.
@@ -489,7 +438,6 @@ Section isEtaExp.
     - destruct nth_error eqn:E; try easy. erewrite nth_error_app_left; eauto.
     - rewrite app_assoc. eapply a, b. reflexivity.
     - rewrite app_assoc. eapply a, b. reflexivity.
-    - eapply InPrim_primProp in H. solve_all.
     - rewrite isEtaExp_mkApps => //. cbn [expanded_head_viewc]. rtoProp; repeat solve_all.
     - rewrite isEtaExp_mkApps => //. cbn [expanded_head_viewc]. rtoProp; repeat solve_all.
       rewrite app_assoc. rtoProp; intuition auto.
@@ -508,7 +456,6 @@ Section isEtaExp.
     - destruct block_args; cbn in *; eauto.
     - eapply a in b. 2: f_equal. revert b. now len.
     - eapply a in b. 2: f_equal. revert b. now len.
-    - eapply InPrim_primProp in H; solve_all.
     - cbn. destruct block_args; cbn in *; eauto.
     - cbn. solve_all. rtoProp; intuition auto. eapply a in H0. 2: reflexivity. revert H0. now len.
     - destruct nth_error eqn:Hn; cbn in H1; try easy.
@@ -541,12 +488,14 @@ Section isEtaExp.
       solve_all. rewrite app_assoc. eapply a0; cbn; eauto. now len. cbn.
       now rewrite app_assoc.
     - rewrite app_assoc. eapply a0; len; eauto. now rewrite app_assoc.
-    - eapply InPrim_primProp in H. solve_all.
-      eapply primProp_map. solve_all.
+    - solve_all_k 6.
     - fold csubst. move/andP: H1 => [] etaexp h.
       rewrite csubst_mkApps /=.
       rewrite isEtaExp_Constructor. solve_all.
-      rewrite map_length. rtoProp; solve_all. solve_all. destruct block_args; cbn in *; eauto.
+      rtoProp; solve_all. destruct block_args.
+      2:{ cbn in *; eauto. }
+      solve_all.
+      destruct block_args; cbn in *; eauto.
     - rewrite csubst_mkApps /=.
       move/andP : H2 => [] /andP [] eu ef ev.
       rewrite isEtaExp_mkApps //.
@@ -600,9 +549,7 @@ Section isEtaExp.
         erewrite option_default_ext; eauto. f_equal.
         destruct i; cbn; lia.
       + now rewrite !nth_error_app1 in H0 |- *; try lia.
-    - intros. eapply forallb_All in H1; eapply All_mix in H; tea.
-      eapply All_forallb, All_map, All_impl; tea; cbv beta.
-      intros x Hx. eapply Hx; eauto. apply Hx.
+    - solve_all. eapply a; trea. solve_all.
     - eapply H with (Γ := 0 :: Γ0); cbn -[isEtaExp]; eauto.
     - solve_all. move/andP: H2 => [] etab etab'. simp_eta.
       apply/andP. split; eauto.
@@ -617,14 +564,11 @@ Section isEtaExp.
       { cbn in Hcl. solve_all. rewrite Nat.add_0_r in a0. eauto. }
       now rewrite app_assoc.
       solve_all.
-    - eapply InPrim_primProp in H. solve_all.
-      eapply primProp_map. eapply primProp_impl; tea. intuition eauto.
+    - solve_all. eapply primProp_impl; tea. intuition eauto.
       destruct H. eapply i; eauto. solve_all.
     - solve_all. fold csubst. move/andP: H1 => [] etaexp h.
       rewrite csubst_mkApps /=.
-      rewrite isEtaExp_Constructor. solve_all.
-      rewrite map_length. rtoProp; solve_all.
-      rewrite forallb_map.
+      rewrite isEtaExp_Constructor. solve_all. rtoProp; solve_all.
       eapply All_forallb. clear Heq0 Heq.
       eapply All_impl; tea; cbv beta.
       intros x Hx.
@@ -874,7 +818,7 @@ Proof.
     eapply In_All in H0. solve_all.
   - econstructor. rewrite forallb_InP_spec in H0. eapply forallb_Forall in H0.
     eapply In_All in H. solve_all.
-  - econstructor. eapply InPrim_primProp in H. rewrite test_primIn_spec in H0.
+  - econstructor. rewrite test_primIn_spec in H0.
     solve_all.
   - rtoProp. eapply In_All in H.
     rewrite forallb_InP_spec in H2. eapply forallb_Forall in H2.
diff --git a/erasure/theories/EImplementBox.v b/erasure/theories/EImplementBox.v
index 001c2dc9c..132539142 100644
--- a/erasure/theories/EImplementBox.v
+++ b/erasure/theories/EImplementBox.v
@@ -2,7 +2,7 @@
 From Coq Require Import Utf8 Program.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import config Kernames BasicAst EnvMap.
-From MetaCoq.Erasure Require Import EAst EAstUtils EInduction EArities
+From MetaCoq.Erasure Require Import EPrimitive EAst EAstUtils EInduction EArities
     ELiftSubst ESpineView EGlobalEnv EWellformed EEnvMap
     EWcbvEval EEtaExpanded ECSubst EWcbvEvalEtaInd EProgram.
 
@@ -54,7 +54,7 @@ Section implement_box.
     | tVar n => EAst.tVar n
     | tConst n => EAst.tConst n
     | tConstruct ind i block_args => EAst.tConstruct ind i (map_InP block_args (fun d H => implement_box d))
-    | tPrim p => EAst.tPrim p.
+    | tPrim p => EAst.tPrim (map_primIn p (fun x H => implement_box x)).
   Proof.
     all:try lia.
     all:try apply (In_size); tea.
@@ -62,6 +62,7 @@ Section implement_box.
     - now apply (In_size id size).
     - now eapply (In_size id size).
     - eapply (In_size snd size) in H. cbn in *. lia.
+    - now eapply InPrim_size in H.
   Qed.
 
   End Def.
@@ -93,11 +94,12 @@ Section implement_box.
     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.
+    (*try solve [simpl; subst; simpl closed; f_equal; auto; rtoProp; solve_all; solve_all]; try easy.
     rtoProp. split. eauto.
     solve_all.
     replace (#|x.1| + S k) with (#|x.1| + k + 1) by lia.
-    eapply closedn_lift. eauto.
+    eapply closedn_lift. eauto.*)
+    try solve [simpl; subst; simpl closed; f_equal; auto; rtoProp; solve_all; solve_all_k 6]; try easy.
   Qed.
 
   Hint Rewrite @forallb_InP_spec : isEtaExp.
@@ -175,7 +177,7 @@ Section implement_box.
     - cbn. do 2 f_equal. 1: eauto.
       rewrite !map_map. solve_all.
       eapply In_All. intros ? ?. unfold map_def. cbn. f_equal.
-      setoid_rewrite -> closed_subst at 2.  
+      setoid_rewrite -> closed_subst at 2.
       replace (#|x.1| + S k) with ((#|x.1| + k) + 1) by lia.
       rewrite <- commut_lift_subst_rec. 2: lia.
       rewrite <- closed_subst.
@@ -183,11 +185,10 @@ Section implement_box.
       f_equal.
       eapply H; eauto.
     - cbn. f_equal. rewrite !map_map. solve_all.
-      eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. erewrite H; eauto.
-      f_equal. now rewrite map_length.
+      eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. rewrite H; eauto.
     - cbn. f_equal. rewrite !map_map. solve_all.
-      eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. erewrite H; eauto.
-      f_equal. now rewrite map_length.
+      eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. rewrite H; eauto.
+    - cbn. solve_all.
   Qed.
 
   Lemma implement_box_substl s t :
@@ -252,7 +253,7 @@ Section implement_box.
     unfold cunfold_cofix.
     rewrite nth_error_map.
     destruct nth_error eqn:heq.
-    intros [= <- <-] => /=. f_equal. 
+    intros [= <- <-] => /=. f_equal.
     rewrite implement_box_substl //. 2:congruence.
     f_equal. f_equal. apply implement_box_cofix_subst.
   Qed.
@@ -468,11 +469,10 @@ Proof.
     eapply wellformed_lift. eauto.
   - rewrite lookup_constructor_implement_box. intuition auto.
   - unfold wf_fix in *. rtoProp. solve_all. solve_all. now eapply isLambda_implement_box.
-  - unfold wf_fix in *. rtoProp. solve_all.
-    len. solve_all. len. destruct x.
-    cbn -[implement_box isEtaExp] in *. rtoProp. eauto.
+  - unfold wf_fix in *. rtoProp. solve_all. len. solve_all.
   - unfold wf_fix in *. len. solve_all. rtoProp; intuition auto.
     solve_all.
+  - solve_all_k 6.
 Qed.
 
 Lemma transform_wellformed_decl' {efl : EEnvFlags} {Σ : global_declarations} d :
diff --git a/erasure/theories/EInduction.v b/erasure/theories/EInduction.v
index 19f8929ad..208332ffc 100644
--- a/erasure/theories/EInduction.v
+++ b/erasure/theories/EInduction.v
@@ -124,6 +124,14 @@ Proof.
   rewrite IHl. simpl. lia.
 Qed.
 
+Lemma InPrim_size x p : InPrim x p -> size x < S (prim_size size p).
+Proof.
+  destruct p as [? []]; cbn => //.
+  intros [->|H]; try lia.
+  eapply (In_size id size) in H; unfold id in H.
+  change (fun x => size x) with size in H. lia.
+Qed.
+
 Lemma decompose_app_rec_size t l :
   let da := decompose_app_rec t l in
   size da.1 + list_size size da.2 = size t + list_size size l.
diff --git a/erasure/theories/EInlineProjections.v b/erasure/theories/EInlineProjections.v
index 0eaa0b364..e9cee9812 100644
--- a/erasure/theories/EInlineProjections.v
+++ b/erasure/theories/EInlineProjections.v
@@ -2,7 +2,7 @@
 From Coq Require Import Utf8 Program.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import config Kernames BasicAst.
-From MetaCoq.Erasure Require Import EAst EAstUtils EExtends
+From MetaCoq.Erasure Require Import EPrimitive EAst EAstUtils EExtends
     ELiftSubst ECSubst EGlobalEnv EWellformed EWcbvEval Extract
     EEnvMap EArities EProgram.
 
@@ -123,7 +123,7 @@ Section optimize.
     | tVar _ => t
     | tConst _ => t
     | tConstruct ind n args => tConstruct ind n (map optimize args)
-    | tPrim _ => t
+    | tPrim p => tPrim (map_prim optimize p)
     end.
 
   Lemma optimize_mkApps f l : optimize (mkApps f l) = mkApps (optimize f) (map optimize l).
@@ -163,9 +163,10 @@ Section optimize.
       rewrite hl /= andb_true_r.
       rewrite IHt //=; len. apply Nat.ltb_lt.
       lia.
-    - len. rtoProp; solve_all. rewrite forallb_map; solve_all.
+    - len. rtoProp; solve_all. solve_all.
       now eapply isLambda_optimize. solve_all.
-    - len. rtoProp; solve_all. rewrite forallb_map; solve_all.
+    - len. rtoProp; repeat solve_all.
+    - rewrite test_prim_map. solve_all.
   Qed.
 
   Lemma optimize_csubst {a k b} n :
@@ -787,10 +788,9 @@ Proof.
     rewrite hrel IHt //= andb_true_r.
     have hargs' := wellformed_projection_args wfΣ hl'.
     apply Nat.ltb_lt. len.
-  - cbn. unfold wf_fix; rtoProp; intuition auto; solve_all. now eapply isLambda_optimize. 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.
+  - cbn. unfold wf_fix; rtoProp; intuition auto; solve_all. now eapply isLambda_optimize.
+  - cbn. unfold wf_fix; rtoProp; intuition auto; solve_all.
+  - cbn. rtoProp; intuition eauto; solve_all_k 6.
 Qed.
 
 Import EWellformed.
diff --git a/erasure/theories/ELiftSubst.v b/erasure/theories/ELiftSubst.v
index 83ad52ef7..a03c221eb 100644
--- a/erasure/theories/ELiftSubst.v
+++ b/erasure/theories/ELiftSubst.v
@@ -213,6 +213,7 @@ Ltac change_Sk :=
 
 Ltac primProp :=
   repeat match goal with
+    | [ H : (forall x, InPrim x _ -> _) |- _ ] => eapply InPrim_primProp in H
     | [ H : is_true (test_prim _ _) |- _ ] => eapply test_prim_impl_primProp in H
     | [ H : test_prim _ _ = true |- _ ] => eapply test_prim_impl_primProp in H
     | [ |- is_true (test_prim _ _) ] => eapply primProp_impl_test_prim
@@ -223,7 +224,7 @@ Ltac primProp :=
 
 Tactic Notation "solve_all_k" int(k) :=
   unfold tFixProp in *;
-  primProp;
+  primProp; autorewrite with map;
   repeat toAll; try All_map; try close_Forall;
   change_Sk; auto with all;
   intuition eauto k with all.
diff --git a/erasure/theories/EOptimizePropDiscr.v b/erasure/theories/EOptimizePropDiscr.v
index 38cc0bbf5..c713427bd 100644
--- a/erasure/theories/EOptimizePropDiscr.v
+++ b/erasure/theories/EOptimizePropDiscr.v
@@ -7,7 +7,7 @@ From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils
      PCUICTyping PCUICInversion
      PCUICSafeLemmata. (* for welltyped *)
 From MetaCoq.SafeChecker Require Import PCUICWfEnvImpl.
-From MetaCoq.Erasure Require Import EAst EAstUtils EDeps EExtends
+From MetaCoq.Erasure Require Import EPrimitive EAst EAstUtils EDeps EExtends
     ELiftSubst ECSubst EGlobalEnv EWellformed EWcbvEval Extract Prelim
     EEnvMap EArities EProgram.
 
@@ -68,7 +68,7 @@ Section remove_match_on_box.
     | tVar _ => t
     | tConst _ => t
     | tConstruct ind i args => tConstruct ind i (map remove_match_on_box args)
-    | tPrim _ => t
+    | tPrim p => tPrim (map_prim remove_match_on_box p)
     end.
 
   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).
@@ -103,7 +103,6 @@ Section remove_match_on_box.
     - move/andP => []. intros. f_equal; solve_all; eauto.
     - move/andP => []. intros. f_equal; solve_all; eauto.
     - move/andP => []. intros. f_equal; solve_all; eauto.
-      destruct x0; cbn in *. f_equal; auto.
   Qed.
 
   Lemma closed_remove_match_on_box t k : closedn k t -> closedn k (remove_match_on_box t).
@@ -128,6 +127,7 @@ Section remove_match_on_box.
       rtoProp; solve_all. solve_all.
       rtoProp; solve_all. solve_all.
     - destruct GlobalContextMap.inductive_isprop_and_pars as [[[|] _]|]; cbn; auto.
+    - solve_all_k 6.
   Qed.
 
   Lemma subst_csubst_comm l t k b :
@@ -818,10 +818,9 @@ 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_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.
+  - cbn. unfold wf_fix; rtoProp; intuition auto; solve_all. now eapply isLambda_remove_match_on_box.
+  - cbn. unfold wf_fix; rtoProp; intuition auto; solve_all.
+  - cbn. rtoProp; intuition auto; solve_all_k 6.
 Qed.
 
 Import EWellformed.
diff --git a/erasure/theories/EPrimitive.v b/erasure/theories/EPrimitive.v
index 866b3c414..736744df1 100644
--- a/erasure/theories/EPrimitive.v
+++ b/erasure/theories/EPrimitive.v
@@ -32,7 +32,7 @@ Arguments primIntModel {term}.
 Arguments primFloatModel {term}.
 Arguments primArrayModel {term}.
 
-Derive Signature NoConfusion for prim_model.
+Derive Signature NoConfusion NoConfusionHom for prim_model.
 
 Definition prim_model_of (term : Set) (p : prim_tag) : Set :=
   match p with
@@ -165,6 +165,13 @@ Inductive primProp {term} P : prim_val term -> Type :=
       primProp P (primArray; primArrayModel a).
 Derive Signature NoConfusion for primProp.
 
+Definition fold_prim {A term} (f : A -> term -> A) (p : prim_val term) (acc : A) : A :=
+  match p.π2 return A with
+  | primIntModel f => acc
+  | primFloatModel f => acc
+  | primArrayModel a => fold_left f a.(array_value) (f acc a.(array_default))
+  end.
+
 Section primtheory.
   Context {term term' term''} (g : term' -> term'') (f : term -> term') (p : prim_val term).
 
@@ -175,7 +182,7 @@ Section primtheory.
     do 2 f_equal. destruct a; rewrite /map_array_model //= map_map_compose //.
   Qed.
 End primtheory.
-#[global] Hint Rewrite @map_prim_compose : all.
+#[global] Hint Rewrite @map_prim_compose : map all.
 
 Lemma reflectT_forallb {A} {P : A -> Type} {p l} :
   (forall x, reflectT (P x) (p x)) ->
@@ -312,3 +319,58 @@ End primtheory.
 #[global] Hint Resolve map_prim_eq map_prim_eq_prop : all.
 #[global] Hint Resolve primProp_impl primProp_map : all.
 #[global] Hint Resolve test_prim_eq_prop : all.
+
+Set Equations Transparent.
+
+Section PrimIn.
+  Context {term : Set}.
+
+  Equations InPrim (x : term) (p : prim_val term) : Prop :=
+    | x | (primInt; primIntModel i) := False
+    | x | (primFloat; primFloatModel _) := False
+    | x | (primArray; primArrayModel a) :=
+      x = a.(array_default) \/ In x a.(array_value).
+
+  Lemma InPrim_primProp p P : (forall x, InPrim x p -> P x) -> primProp P p.
+  Proof.
+    intros hin.
+    destruct p as [? []]; constructor.
+    split. eapply hin; eauto. now left.
+    cbn in hin.
+    induction (array_value a); constructor.
+    eapply hin. now right; left. eapply IHl.
+    intros. eapply hin. intuition eauto. now right; right.
+  Qed.
+
+  Equations test_primIn (p : prim_val term) (f : forall x : term, InPrim x p -> bool) : bool :=
+    | (primInt; primIntModel i) | _ := true
+    | (primFloat; primFloatModel _) | _ := true
+    | (primArray; primArrayModel a) | f :=
+      f a.(array_default) (or_introl eq_refl) && forallb_InP a.(array_value) (fun x H => f x (or_intror H)).
+
+  Lemma test_primIn_spec p (f : term -> bool) :
+    test_primIn p (fun x H => f x) = test_prim f p.
+  Proof.
+    funelim (test_primIn p (fun x H => f x)); cbn => //.
+    rewrite forallb_InP_spec //.
+  Qed.
+
+  Equations map_primIn (p : prim_val term) (f : forall x : term, InPrim x p -> term) : prim_val term :=
+    | (primInt; primIntModel i) | _ := (primInt; primIntModel i)
+    | (primFloat; primFloatModel f) | _ := (primFloat; primFloatModel f)
+    | (primArray; primArrayModel a) | f :=
+      (primArray; primArrayModel
+        {| array_default := f a.(array_default) (or_introl eq_refl);
+           array_value := map_InP a.(array_value) (fun x H => f x (or_intror H)) |}).
+
+  Lemma map_primIn_spec p f :
+    map_primIn p (fun x _ => f x) = map_prim f p.
+  Proof.
+    funelim (map_primIn p _); cbn => //.
+    do 2 f_equal. unfold map_array_model; destruct a => //.
+    rewrite map_InP_spec //.
+  Qed.
+
+End PrimIn.
+
+#[global] Hint Rewrite @map_primIn_spec : map.
\ No newline at end of file
diff --git a/erasure/theories/ERemoveParams.v b/erasure/theories/ERemoveParams.v
index bf4d33e52..42e43f62b 100644
--- a/erasure/theories/ERemoveParams.v
+++ b/erasure/theories/ERemoveParams.v
@@ -1,8 +1,8 @@
 (* Distributed under the terms of the MIT license. *)
 From Coq Require Import Utf8 Program.
 From MetaCoq.Utils Require Import utils.
-From MetaCoq.Common Require Import config Kernames BasicAst EnvMap.
-From MetaCoq.Erasure Require Import EAst EAstUtils EInduction EArities
+From MetaCoq.Common Require Import config Kernames Primitive BasicAst EnvMap.
+From MetaCoq.Erasure Require Import EPrimitive EAst EAstUtils EInduction EArities
     ELiftSubst ESpineView EGlobalEnv EWellformed EEnvMap
     EWcbvEval EEtaExpanded ECSubst EWcbvEvalEtaInd EProgram.
 
@@ -59,7 +59,7 @@ Section strip.
     | tVar n => EAst.tVar n
     | tConst n => EAst.tConst n
     | tConstruct ind i block_args => EAst.tConstruct ind i block_args
-    | tPrim p => EAst.tPrim p }.
+    | tPrim p => EAst.tPrim (map_primIn p (fun x H => strip x)) }.
   Proof.
     all:try lia.
     all:try apply (In_size); tea.
@@ -72,10 +72,14 @@ Section strip.
     - pose proof (size_mkApps_l napp nnil).
       eapply (In_size id size) in H. change (fun x => size (id x)) with size in H. unfold id in H. lia.
     - eapply (In_size snd size) in H. cbn in H; lia.
+    - destruct p as [? []]; cbn in H; eauto.
+      intuition auto; subst; cbn; try lia.
+      eapply (In_size id size) in H0. unfold id in H0.
+      change (fun x => size x) with size in H0. lia.
   Qed.
   End Def.
 
-  Hint Rewrite @map_InP_spec : strip.
+  Hint Rewrite @map_primIn_spec @map_InP_spec : strip.
 
   Lemma map_repeat {A B} (f : A -> B) x n : map f (repeat x n) = repeat (f x) n.
   Proof using Type.
@@ -107,6 +111,7 @@ Section strip.
     unfold test_def in *;
     simpl closed in *;
     try solve [simpl; subst; simpl closed; f_equal; auto; rtoProp; solve_all; solve_all]; try easy.
+    - solve_all_k 6.
     - rewrite !closedn_mkApps in H1 *.
       rtoProp; intuition auto.
       solve_all.
@@ -557,6 +562,10 @@ Module Fast.
     | app, tConstruct kn c block_args with GlobalContextMap.lookup_inductive_pars Σ (inductive_mind kn) := {
         | Some npars => mkApps (EAst.tConstruct kn c block_args) (List.skipn npars app)
         | None => mkApps (EAst.tConstruct kn c block_args) app }
+    | app, tPrim (primInt; primIntModel i) => mkApps (tPrim (primInt; primIntModel i)) app
+    | app, tPrim (primFloat; primFloatModel f) => mkApps (tPrim (primFloat; primFloatModel f)) app
+    | app, tPrim (primArray; primArrayModel a) =>
+      mkApps (tPrim (primArray; primArrayModel {| array_default := strip [] a.(array_default); array_value := strip_args a.(array_value) |})) app
     | app, x => mkApps x app }
 
     where strip_args (t : list term) : list term :=
@@ -597,6 +606,11 @@ Module Fast.
         specialize (IHv [] eq_refl). simpl in IHv.
         intros args ->. specialize (IHu (v :: args)).
         forward IHu. now rewrite -IHv. exact IHu.
+      - intros Hl hargs args ->.
+        rewrite strip_mkApps //=. simp_strip.
+        rewrite map_primIn_spec. f_equal. f_equal. cbn.
+        do 2 f_equal. rewrite /map_array_model.
+        specialize (Hl [] eq_refl). f_equal; eauto.
       - intros Hl args ->.
         rewrite strip_mkApps // /=.
         rewrite GlobalContextMap.lookup_inductive_pars_spec in Hl. now rewrite Hl.
@@ -1072,7 +1086,7 @@ Proof.
     all: eapply H; auto.
   - unfold wf_fix_gen in *. rewrite map_length. rtoProp; intuition auto. toAll; solve_all.
     now rewrite -strip_isLambda. toAll; solve_all.
-  - unfold wf_fix in *. rewrite map_length; rtoProp; intuition auto. toAll; solve_all.
+  - rewrite map_primIn_spec. primProp. rtoProp; intuition eauto; solve_all_k 6.
   - move:H1; rewrite !wellformed_mkApps //. rtoProp; intuition auto.
     toAll; solve_all. toAll; solve_all.
   - move:H0; rewrite !wellformed_mkApps //. rtoProp; intuition auto.
diff --git a/erasure/theories/ESubstitution.v b/erasure/theories/ESubstitution.v
index af58c8a04..fb17df33d 100644
--- a/erasure/theories/ESubstitution.v
+++ b/erasure/theories/ESubstitution.v
@@ -113,10 +113,10 @@ Proof.
     split; eauto.
   - econstructor.
     induction H2; constructor.
-    induction H; constructor; depelim X2; eauto.
+    induction X3; constructor; depelim X2; eauto.
     depelim X1.
-    eapply All2_All_mix_left in X3; eauto.
-    eapply All2_impl. exact X3.
+    eapply All2_All_mix_left in a0; eauto.
+    eapply All2_impl. exact a0.
     cbn. intros ? ? [? ?]. eauto.
 Qed.
 
@@ -315,6 +315,12 @@ Proof.
     unfold app_context in IH. rewrite <- !app_assoc in IH.
     rewrite (All2_length X3) in IH |- *.
     apply IH. apply IH'.
+
+  - econstructor. depelim H3.
+    depelim X4; repeat constructor.
+    depelim X2; cbn. now eapply hdef.
+    depelim X2. cbn. eapply All2_map.
+    ELiftSubst.solve_all.
 Qed.
 
 Lemma erases_weakening (Σ : global_env_ext) (Γ Γ' : context) (t T : PCUICAst.term) t' :
@@ -581,10 +587,10 @@ Proof.
       eapply is_type_subst; eauto.
   - cbn. depelim H1.
     * cbn; constructor.
-      depelim H1. depelim H1; repeat constructor.
-      depelim X2.
-      + eapply (@substitution _ Σ _ Γ Γ' s Δ) in H1.
+      depelim H1. depelim X5; depelim X2; repeat constructor; cbn; eauto.
+      ELiftSubst.solve_all.
     * constructor. eapply is_type_subst in X3; tea.
+      now cbn in X3.
   - eapply H; eauto.
 Qed.
 
diff --git a/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v b/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v
index 1ac8603df..d9a4ac6d7 100644
--- a/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v
+++ b/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v
@@ -2,7 +2,7 @@
 From Coq Require Import Utf8 Program ssreflect ssrbool.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import config Kernames BasicAst EnvMap.
-From MetaCoq.Erasure Require Import EAst EAstUtils EInduction ELiftSubst EWcbvEval EGlobalEnv
+From MetaCoq.Erasure Require Import EPrimitive EAst EAstUtils EInduction ELiftSubst EWcbvEval EGlobalEnv
   EWellformed ECSubst EInduction EWcbvEvalInd EEtaExpanded.
 
 Set Asymmetric Patterns.
@@ -42,7 +42,8 @@ Section OnSubterm.
     All (fun br => Q (#|br.1| + n) br.2) brs -> on_subterms Q n (tCase ci discr brs)
   | on_proj p c : has_tProj -> Q n c -> on_subterms Q n (tProj p c)
   | on_fix mfix idx : has_tFix -> All (fun d => Q (#|mfix| + n) d.(dbody)) mfix -> on_subterms Q n (tFix mfix idx)
-  | on_cofix mfix idx : has_tCoFix -> All (fun d => Q (#|mfix| + n) d.(dbody)) mfix -> on_subterms Q n (tCoFix mfix idx).
+  | on_cofix mfix idx : has_tCoFix -> All (fun d => Q (#|mfix| + n) d.(dbody)) mfix -> on_subterms Q n (tCoFix mfix idx)
+  | on_prim p : has_tPrim -> primProp (Q n) p -> on_subterms Q n (tPrim p).
   Derive Signature for on_subterms.
 End OnSubterm.
 
@@ -551,7 +552,7 @@ Proof.
   - eapply Qatom; cbn; auto.
   - eapply Qatom; cbn; auto.
   - eapply Qatom; cbn; auto.
-  Unshelve. all: repeat econstructor.
+  - eapply Qatom; cbn; eauto.
 Qed.
 
 Lemma Qpreserves_wellformed (efl : EEnvFlags) Σ : wf_glob Σ -> Qpreserves (fun n x => wellformed Σ n x) Σ.
@@ -576,7 +577,8 @@ Proof.
     eapply on_fix => //. move/andP: H0 => [] _ ha. solve_all.
     rtoProp; intuition auto.
     eapply on_cofix => //. move/andP: H0 => [] _ ha. solve_all.
-  - red. intros kn decl.
+    move/andP: H => [] hp ha. eapply on_prim => //. solve_all.
+ - red. intros kn decl.
     move/(lookup_env_wellformed clΣ).
     unfold wf_global_decl. destruct cst_body => //.
   - red. move=> hasapp n t args. rewrite wellformed_mkApps //.
diff --git a/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v b/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v
index f7b7d4325..4aa2b1de7 100644
--- a/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v
+++ b/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v
@@ -2,7 +2,7 @@
 From Coq Require Import Utf8 Program ssreflect ssrbool.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import config Kernames BasicAst EnvMap.
-From MetaCoq.Erasure Require Import EAst EAstUtils EInduction ELiftSubst EWcbvEval EGlobalEnv
+From MetaCoq.Erasure Require Import EPrimitive EAst EAstUtils EInduction ELiftSubst EWcbvEval EGlobalEnv
   EWellformed ECSubst EInduction EWcbvEvalInd EEtaExpanded.
 
 Set Asymmetric Patterns.
@@ -42,7 +42,8 @@ Section OnSubterm.
     All (fun br => Q (#|br.1| + n) br.2) brs -> on_subterms Q n (tCase ci discr brs)
   | on_proj p c : has_tProj -> Q n c -> on_subterms Q n (tProj p c)
   | on_fix mfix idx : has_tFix -> All (fun d => Q (#|mfix| + n) d.(dbody)) mfix -> on_subterms Q n (tFix mfix idx)
-  | on_cofix mfix idx : has_tCoFix -> All (fun d => Q (#|mfix| + n) d.(dbody)) mfix -> on_subterms Q n (tCoFix mfix idx).
+  | on_cofix mfix idx : has_tCoFix -> All (fun d => Q (#|mfix| + n) d.(dbody)) mfix -> on_subterms Q n (tCoFix mfix idx)
+  | on_prim p : has_tPrim -> primProp (Q n) p -> on_subterms Q n (tPrim p).
   Derive Signature for on_subterms.
 End OnSubterm.
 
@@ -470,6 +471,7 @@ Proof.
     eapply on_fix => //. move/andP: H0 => [] _ ha. solve_all.
     rtoProp; intuition auto.
     eapply on_cofix => //. move/andP: H0 => [] _ ha. solve_all.
+    move/andP: H => [] hasp ht. eapply on_prim => //. solve_all.
   - red. intros kn decl.
     move/(lookup_env_wellformed clΣ).
     unfold wf_global_decl. destruct cst_body => //.
diff --git a/erasure/theories/EWcbvEvalEtaInd.v b/erasure/theories/EWcbvEvalEtaInd.v
index e30f2baf9..3dbd3814f 100644
--- a/erasure/theories/EWcbvEvalEtaInd.v
+++ b/erasure/theories/EWcbvEvalEtaInd.v
@@ -2,7 +2,7 @@
 From Coq Require Import Utf8 Program ssreflect ssrbool.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import config Kernames BasicAst EnvMap.
-From MetaCoq.Erasure Require Import EAst EAstUtils EInduction EWcbvEval EGlobalEnv
+From MetaCoq.Erasure Require Import EPrimitive EAst EAstUtils EInduction EWcbvEval EGlobalEnv
   EWellformed ECSubst EInduction EWcbvEvalInd EEtaExpanded.
 
 Set Asymmetric Patterns.
@@ -42,7 +42,8 @@ Section OnSubterm.
     All (fun br => Q (#|br.1| + n) br.2) brs -> on_subterms Q n (tCase ci discr brs)
   | on_proj p c : has_tProj -> Q n c -> on_subterms Q n (tProj p c)
   | on_fix mfix idx : has_tFix -> All (fun d => Q (#|mfix| + n) d.(dbody)) mfix -> on_subterms Q n (tFix mfix idx)
-  | on_cofix mfix idx : has_tCoFix -> All (fun d => Q (#|mfix| + n) d.(dbody)) mfix -> on_subterms Q n (tCoFix mfix idx).
+  | on_cofix mfix idx : has_tCoFix -> All (fun d => Q (#|mfix| + n) d.(dbody)) mfix -> on_subterms Q n (tCoFix mfix idx)
+  | on_prim p : has_tPrim -> primProp (Q n) p -> on_subterms Q n (tPrim p).
   Derive Signature for on_subterms.
 End OnSubterm.
 
@@ -727,6 +728,7 @@ Proof.
     eapply on_proj; auto.
     eapply on_fix; eauto. move/andP: H0 => [] _ wf. solve_all.
     eapply on_cofix; eauto. move/andP: H0 => [] _ wf. solve_all.
+    eapply on_prim; eauto. solve_all.
   - red. intros kn decl.
     move/(lookup_env_wellformed clΣ).
     unfold wf_global_decl. destruct cst_body => //.
diff --git a/erasure/theories/EWellformed.v b/erasure/theories/EWellformed.v
index 034bd6334..6383c28ae 100644
--- a/erasure/theories/EWellformed.v
+++ b/erasure/theories/EWellformed.v
@@ -221,11 +221,6 @@ Section EEnvFlags.
       apply Nat.ltb_lt in H1. lia.
     - destruct cstr_as_blocks; eauto. destruct lookup_constructor_pars_args as [ [] | ]; rtoProp; repeat solve_all.
       destruct args; firstorder.
-    - solve_all. rewrite Nat.add_assoc. eauto.
-    - len. move/andP: H1 => [] -> ha. cbn. solve_all.
-      rewrite Nat.add_assoc; eauto.
-    - len. move/andP: H1 => [] -> ha. cbn. solve_all.
-      rewrite Nat.add_assoc; eauto.
   Qed.
 
   Lemma wellformed_subst_eq {s k k' t} :
@@ -265,10 +260,8 @@ Section EEnvFlags.
       rewrite !Nat.add_assoc. eapply a => //.
       now rewrite !Nat.add_assoc in b.
     - destruct (dbody x) => //.
-    - intros. now len.
     - specialize (a (#|m| + k')).
       len. now rewrite !Nat.add_assoc !(Nat.add_comm k) in a, b0 |- *.
-    - intros. now len.
     - specialize (a (#|m| + k')); len.
       now rewrite !Nat.add_assoc !(Nat.add_comm k) in a, b |- *.
   Qed.
diff --git a/erasure/theories/ErasureCorrectness.v b/erasure/theories/ErasureCorrectness.v
index 8a3c835ba..df3a996f9 100644
--- a/erasure/theories/ErasureCorrectness.v
+++ b/erasure/theories/ErasureCorrectness.v
@@ -1379,4 +1379,11 @@ Proof.
         + constructor => //.
           eapply erases_deps_mkApps_inv in etaΣ as [].
           solve_all.
+  - intros Γ0 v etaΣ er.
+    depelim er; eauto. depelim H1.
+    depelim H0. 1-2:depelim X; repeat constructor.
+    depelim X0. eapply expanded_tPrim. constructor; split => //; cbn.
+    eapply H0; tea. now depelim etaΣ; cbn in *.
+    eapply Forall_All. depelim etaΣ. cbn in *.
+    solve_all.
 Qed.
diff --git a/erasure/theories/ErasureFunction.v b/erasure/theories/ErasureFunction.v
index 75ca06fa8..e579925c5 100644
--- a/erasure/theories/ErasureFunction.v
+++ b/erasure/theories/ErasureFunction.v
@@ -11,7 +11,7 @@ From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICPrimitive
   PCUICValidity PCUICPrincipality PCUICElimination PCUICOnFreeVars PCUICWellScopedCumulativity PCUICSN PCUICEtaExpand.
 
 From MetaCoq.SafeChecker Require Import PCUICErrors PCUICWfEnv PCUICSafeReduce PCUICSafeRetyping PCUICRetypingEnvIrrelevance.
-From MetaCoq.Erasure Require Import EAstUtils EArities Extract Prelim EDeps ErasureProperties ErasureCorrectness.
+From MetaCoq.Erasure Require Import EPrimitive EAstUtils ELiftSubst EArities Extract Prelim EDeps ErasureProperties ErasureCorrectness.
 
 Local Open Scope string_scope.
 Set Asymmetric Patterns.
@@ -112,6 +112,18 @@ Proof.
     eapply All_In in X as [X]; tea. specialize (X _ _ H0). intuition auto; try knset.
     cbn in H0. apply KernameSet.union_spec in X as []; [knset|].
     right; right. now exists cs.
+  - intros kn.
+    funelim (prim_global_deps term_global_deps p); cbn; simp prim_global_deps; try knset.
+    rewrite !knset_in_fold_left !KernameSet.union_spec; cbn.
+    dependent elimination X as [EPrimitive.primPropArray (pair s al)].
+    rewrite knset_in_fold_left.
+    intuition eauto.
+    * eapply s in H0. rewrite KernameSet.union_spec in H0. intuition eauto.
+    * destruct H0 as [a [ha hkn]].
+      eapply in_map_iff in ha as [x [heq hx]]. subst a.
+      eapply All_In in al as [al]; tea.
+      eapply al in hkn.
+      rewrite KernameSet.union_spec in hkn. destruct hkn; eauto.
 Qed.
 
 
@@ -178,6 +190,10 @@ Proof.
     unfold EWellformed.wf_fix_gen in H1. move/andP: H1 => [_ hm]. solve_all.
     eapply All_In in hm as [hm]; tea. intuition auto.
     eapply (a0 (#|m| + k)) => //.
+  - primProp.
+    move: H0; funelim (prim_global_deps term_global_deps p); try knset.
+    rewrite knset_in_fold_left. depelim H2. intuition eauto.
+    destruct H1 as [ar []]. eapply All_In in b as [[]]; tea. eauto.
 Qed.
 
 Lemma knset_mem_spec kn s : reflect (KernameSet.In kn s) (KernameSet.mem kn s).
@@ -998,8 +1014,15 @@ Section Erase.
         let Γ' := (fix_context mfix ++ Γ)%list in
         let mfix' := erase_cofix Γ' mfix _ in
         E.tCoFix mfix' n
-      | tPrim p := E.tPrim (erase_prim_val p) }
+      | tPrim (primInt; PCUICPrimitive.primIntModel i) := E.tPrim (primInt; EPrimitive.primIntModel i) ;
+      | tPrim (primFloat; PCUICPrimitive.primFloatModel f) := E.tPrim (primFloat; EPrimitive.primFloatModel f) ;
+      | tPrim (primArray; PCUICPrimitive.primArrayModel a) :=
+        E.tPrim (primArray; EPrimitive.primArrayModel
+          {| EPrimitive.array_default := erase Γ a.(PCUICPrimitive.array_default) _;
+             EPrimitive.array_value := erase_terms Γ a.(PCUICPrimitive.array_value) _ |})
+    }
     } }
+
   where erase_terms (Γ : context) (l : list term) (Hl : forall Σ : global_env_ext, abstract_env_ext_rel X Σ -> ∥ All (welltyped Σ Γ) l ∥) : list E.term :=
   { erase_terms Γ [] _ := [];
     erase_terms Γ (t :: ts) _ :=
@@ -1084,6 +1107,10 @@ Section Erase.
       solve_all. now eexists.
     - eapply inversion_CoFix in Ht as (? & ? & ? & ? & ? & ?); auto.
       sq. eapply All_impl; tea. cbn. intros d Ht; now eexists.
+    - eapply inversion_Prim in Ht as [prim_ty [decl []]]; eauto.
+      depelim p0. now eexists.
+    - eapply inversion_Prim in Ht as [prim_ty [decl []]]; eauto.
+      depelim p0. sq. solve_all. now eexists.
     - sq. now depelim Hl.
     - sq. now depelim Hl.
     - sq. now depelim Hbrs.
@@ -1137,9 +1164,9 @@ Proof.
 Qed.
 
 Lemma erase_terms_eq X_type X {normalization_in : forall Σ, wf_ext Σ -> Σ ∼_ext X -> NormalizationIn Σ} Γ ts wt :
-  erase_terms X_type X Γ ts wt = map_All (erase X_type X Γ) ts wt.
+  erase_terms X_type X Γ ts wt = All_Forall.map_All (erase X_type X Γ) ts wt.
 Proof.
-  funelim (map_All (erase X_type X Γ) ts wt); cbn; auto.
+  funelim (All_Forall.map_All (erase X_type X Γ) ts wt); cbn; auto.
   f_equal => //. apply erase_irrel.
   rewrite -H. eapply erase_irrel.
 Qed.
@@ -1238,6 +1265,9 @@ Proof.
     intros isp. eapply isErasable_Proof in isp.
     eapply H'; intros. now rewrite (abstract_env_ext_irr _ H0 H).
 
+  - repeat constructor.
+  - repeat constructor.
+  - repeat constructor; eauto.
   - cbn. pose proof (abstract_env_ext_wf _ H) as [wf].
     pose proof Hmfix as Hmfix'.
     specialize (Hmfix' _ H). destruct Hmfix'.
@@ -1380,23 +1410,6 @@ Ltac iserasableb_irrel_env :=
     generalize dependent H; rewrite (@is_erasableb_irrel_global_env _ _ _ _ _ _ _ _ wt wt') //; intros; rewrite Heq
   end.
 
-  (*
-    (forall Σ Σ' : global_env_ext, abstract_env_ext_rel X Σ ->
-      abstract_env_ext_rel X' Σ' -> ∥ extends_decls Σ' Σ ∥ /\ (Σ.2 = Σ'.2)) ->
-
-  assert (hl : Hlookup X_type X X_type' X').
-  { red. intros Σ H Σ' H0. specialize (ext _ _ H H0) as [[X0] H1].
-    split. intros kn decl decl' H2 H3.
-    rewrite -(abstract_env_lookup_correct' _ _ H).
-    rewrite -(abstract_env_lookup_correct' _ _ H0).
-    rewrite H2 H3.
-    red in X0. specialize (proj1 X0 kn decl' H3). congruence.
-    destruct X0. intros tag.
-    rewrite (abstract_primitive_constant_correct _ _ _ H).
-    rewrite (abstract_primitive_constant_correct _ _ _ H0).
-    now symmetry. }
-*)
-
 Lemma erase_irrel_global_env {X_type X} {normalization_in : forall Σ, wf_ext Σ -> Σ ∼_ext X -> NormalizationIn Σ} {X_type' X'} {normalization_in' : forall Σ, wf_ext Σ -> Σ ∼_ext X' -> NormalizationIn Σ} {Γ t wt wt'} :
   forall (hl : Hlookup X_type X X_type' X'),
   erase X_type X Γ t wt = erase X_type' X' Γ t wt'.
diff --git a/erasure/theories/ErasureFunctionProperties.v b/erasure/theories/ErasureFunctionProperties.v
index 533e5104a..e617fc6fd 100644
--- a/erasure/theories/ErasureFunctionProperties.v
+++ b/erasure/theories/ErasureFunctionProperties.v
@@ -12,7 +12,7 @@ From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICPrimitive
   PCUICFirstorder.
 
 From MetaCoq.SafeChecker Require Import PCUICErrors PCUICWfEnv PCUICSafeReduce PCUICSafeRetyping PCUICRetypingEnvIrrelevance.
-From MetaCoq.Erasure Require Import EAstUtils EArities Extract Prelim EDeps ErasureProperties ErasureCorrectness ErasureFunction.
+From MetaCoq.Erasure Require Import EPrimitive EAstUtils ELiftSubst EArities Extract Prelim EDeps ErasureProperties ErasureCorrectness ErasureFunction.
 
 Local Open Scope string_scope.
 Set Asymmetric Patterns.
@@ -152,6 +152,16 @@ Proof.
     eapply All2_In_right in H; eauto.
     destruct H as [[def [Hty Hdef]]].
     eapply Hdef; eauto.
+
+  - eapply inversion_Prim in wt as [prim_ty [decl []]]; eauto.
+    move: hin.
+    funelim (prim_global_deps _ _); try knset.
+    rewrite knset_in_fold_left. depelim H0; cbn in *.
+    depelim X. depelim p1. depelim H. depelim X.
+    intuition eauto.
+    destruct H as [a [hin inkn]]. cbn in hin.
+    eapply All2_All_mix_left in a2; tea.
+    eapply All2_In_right in a2 as [[x []]]; tea. eapply d1; tea.
 Qed.
 
 Global Remove Hints erases_deps_eval : core.
@@ -289,7 +299,18 @@ Proof.
     eapply In_Forall in Σer.
     eapply Forall_All in Σer.
     eapply Forall2_All2 in H.
-    ELiftSubst.solve_all. Unshelve.
+    ELiftSubst.solve_all.
+  - eapply inversion_Prim in wt as [prim_ty [decl []]]; eauto.
+    depelim H; depelim H0. depelim X; depelim X0; depelim p1; constructor;
+    noconf H; cbn; simp prim_global_deps in Σer; simpl in *.
+    eapply e0; eauto.
+    red in Σer. intros kn; specialize (Σer kn).
+    rewrite knset_in_fold_left in Σer. intuition eauto. cbn.
+    eapply All_Forall.
+    eapply includes_deps_fold in Σer as [? Σer].
+    eapply In_Forall in Σer.
+    eapply Forall_All in Σer.
+    solve_all.
 Qed.
 
 Lemma erases_deps_weaken kn d (Σ : global_env) (Σ' : EAst.global_declarations) t :
@@ -343,6 +364,8 @@ Proof.
     red in H |- *.
     rewrite -H. simpl. unfold lookup_env; simpl; destruct (eqb_spec (inductive_mind p.(proj_ind)) kn); try congruence.
     eapply lookup_env_Some_fresh in H. subst kn. destruct X1. contradiction.
+  - solve_all. depelim H; econstructor; intuition eauto.
+    solve_all.
 Qed.
 
 Lemma lookup_env_ext {Σ kn kn' d d'} :
@@ -1216,15 +1239,15 @@ From MetaCoq.Erasure Require Import EEtaExpandedFix.
 
 Lemma erase_brs_eq X_type X {normalization_in : forall Σ, wf_ext Σ -> Σ ∼_ext X -> NormalizationIn Σ} Γ p ts wt :
   erase_brs X_type X Γ p ts wt =
-  map_All (fun br wt => (erase_context (bcontext br), erase X_type X _ (bbody br) wt)) ts wt.
+  All_Forall.map_All (fun br wt => (erase_context (bcontext br), erase X_type X _ (bbody br) wt)) ts wt.
 Proof.
-  funelim (map_All _ ts wt); cbn; auto.
+  funelim (All_Forall.map_All _ ts wt); cbn; auto.
   f_equal => //. f_equal => //. apply erase_irrel.
   rewrite -H. eapply erase_irrel.
 Qed.
 
 Lemma erase_fix_eq X_type X {normalization_in : forall Σ, wf_ext Σ -> Σ ∼_ext X -> NormalizationIn Σ} Γ ts wt :
-  erase_fix X_type X Γ ts wt = map_All (fun d wt =>
+  erase_fix X_type X Γ ts wt = All_Forall.map_All (fun d wt =>
     let dbody' := erase X_type X _ (dbody d) (fun Σ abs => proj2 (wt Σ abs)) in
     let dbody' := if isBox dbody' then
         match d.(dbody) with
@@ -1234,7 +1257,7 @@ Lemma erase_fix_eq X_type X {normalization_in : forall Σ, wf_ext Σ -> Σ ∼_e
     in
     {| E.dname := d.(dname).(binder_name); E.rarg := d.(rarg); E.dbody := dbody' |}) ts wt.
 Proof.
-  funelim (map_All _ ts wt); cbn; auto.
+  funelim (All_Forall.map_All _ ts wt); cbn; auto.
   f_equal => //. f_equal => //.
   rewrite (fst (erase_irrel _ _) _ _ _ _ (fun (Σ : global_env_ext) (abs : abstract_env_ext_rel X Σ) =>
     (map_All_obligation_1 x xs h Σ abs).p2)).
@@ -1243,11 +1266,11 @@ Proof.
 Qed.
 
 Lemma erase_cofix_eq X_type X {normalization_in : forall Σ, wf_ext Σ -> Σ ∼_ext X -> NormalizationIn Σ} Γ ts wt :
-  erase_cofix X_type X Γ ts wt = map_All (fun d wt =>
+  erase_cofix X_type X Γ ts wt = All_Forall.map_All (fun d wt =>
     let dbody' := erase X_type X _ (dbody d) wt in
     {| E.dname := d.(dname).(binder_name); E.rarg := d.(rarg); E.dbody := dbody' |}) ts wt.
 Proof.
-  funelim (map_All _ ts wt); cbn; auto.
+  funelim (All_Forall.map_All _ ts wt); cbn; auto.
   f_equal => //. f_equal => //.
   apply erase_irrel.
   rewrite -H. eapply erase_irrel.
@@ -1407,7 +1430,7 @@ Section wffix.
     | tConstruct ind c _ => true
     | tVar _ => true
     | tBox => true
-    | tPrim _ => true
+    | tPrim p => test_prim wf_fixpoints p
     end.
 
 End wffix.
@@ -1420,7 +1443,7 @@ Lemma erases_deps_wellformed (cf := config.extraction_checker_flags) (efl := all
 Proof.
   intros ed.
   induction ed using erases_deps_forall_ind; intros => //;
-   try solve [cbn in *; unfold wf_fix in *; rtoProp; intuition eauto; solve_all].
+   try solve [cbn in *; unfold wf_fix in *; rtoProp; intuition eauto; PCUICAstUtils.solve_all].
   - cbn. red in H0. rewrite H0 //.
   - cbn -[lookup_constructor].
     cbn. now destruct H0 as [[-> ->] ->].
@@ -1428,21 +1451,24 @@ Proof.
     cbn. apply/andP; split. apply/andP; split.
     * now destruct H0 as [-> ->].
     * now move/andP: H6.
-    * move/andP: H6; solve_all.
+    * move/andP: H6; PCUICAstUtils.solve_all.
   - cbn -[lookup_projection] in *. apply/andP; split; eauto.
     now rewrite (declared_projection_lookup H0).
+  - cbn in H, H0 |- *. solve_all_k 7.
 Qed.
 
 Lemma erases_wf_fixpoints Σ Γ t t' : Σ;;; Γ |- t ⇝ℇ t' ->
   ErasureProperties.wellformed Σ t -> wf_fixpoints t'.
 Proof.
-  induction 1 using erases_forall_list_ind; cbn; auto; try solve [rtoProp; repeat solve_all].
+  induction 1 using erases_forall_list_ind; cbn; auto; try solve [rtoProp; repeat PCUICAstUtils.solve_all].
   - move/andP => []. rewrite (All2_length X) => -> /=. unfold test_def in *.
     eapply Forall2_All2 in H.
-    eapply All2_All2_mix in X; tea. solve_all.
+    eapply All2_All2_mix in X; tea. PCUICAstUtils.solve_all.
     destruct b0; eapply erases_isLambda in H1; tea.
   - move/andP => []. rewrite (All2_length X) => -> /=.
-    unfold test_def in *. solve_all.
+    unfold test_def in *. PCUICAstUtils.solve_all.
+  - depelim H; depelim H0; depelim X; depelim X0; solve_all. noconf H.
+    solve_all_k 7. cbn in H0. constructor; cbn; rtoProp; intuition eauto. solve_all.
 Qed.
 
 Lemma erase_wf_fixpoints (efl := all_env_flags) {X_type X} univs wfΣ {Γ t} wt
@@ -2117,7 +2143,7 @@ Lemma In_map_All {A B C : Type} {Q : C -> Type} {P : C -> A -> Prop}
   (fn : forall x : A, (forall y : C, Q y -> P y x) -> B) (l : list A) (Hl : forall y : C, Q y -> ∥ All (P y) l ∥) :
   forall x, In x l ->
     exists D : forall y : C, Q y -> P y x,
-      In (fn x D) (map_All fn l Hl).
+      In (fn x D) (All_Forall.map_All fn l Hl).
 Proof.
   induction l; cbn => //.
   intros x [].
@@ -2849,8 +2875,7 @@ Proof.
   apply: (PCUICFirstorder.firstorder_value_inds Σ Γ).
   intros i n ui u args pandi hty hfo ih isp.
   assert (Forall2 (erases Σ Γ) args (map (flip compile_value_erase []) args)).
-  { solve_all. eapply All_All2; tea.
-    cbn. intros x [fo hx]. exact hx. }
+  { PCUICAstUtils.solve_all. }
   unshelve epose proof (erases_mkApps Σ Γ (tConstruct i n ui) (EAst.tConstruct i n []) args _ _ H).
   now constructor.
   now rewrite compile_value_erase_mkApps app_nil_r.
diff --git a/erasure/theories/ErasureProperties.v b/erasure/theories/ErasureProperties.v
index 12df078fd..a2af130af 100644
--- a/erasure/theories/ErasureProperties.v
+++ b/erasure/theories/ErasureProperties.v
@@ -2,7 +2,7 @@
 From Coq Require Import Program ssreflect ssrbool.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import config.
-From MetaCoq.Erasure Require Import ELiftSubst EGlobalEnv EWcbvEval Extract Prelim
+From MetaCoq.Erasure Require Import EPrimitive ELiftSubst EGlobalEnv EWcbvEval Extract Prelim
      ESubstitution EArities EDeps.
 From MetaCoq.PCUIC Require Import PCUICTyping PCUICGlobalEnv PCUICAst
   PCUICAstUtils PCUICConversion PCUICSigmaCalculus
@@ -252,6 +252,8 @@ Proof.
     + subst types. eapply conv_context_app_same; auto.
     + subst types. eapply conv_context_wf_local_app; eauto.
     + assumption.
+  - econstructor. depelim H2; constructor. depelim X5; depelim X2; constructor; eauto.
+    solve_all.
 Qed.
 
 
@@ -408,6 +410,10 @@ Proof.
   eapply erases_ctx_ext. eassumption. unfold app_context.
   f_equal.
   eapply fix_context_subst_instance. all: eauto.
+
+  - cbn; constructor. depelim H4.
+    depelim X2; depelim X5; repeat constructor; cbn; eauto.
+    solve_all.
 Qed.
 
 Lemma erases_subst_instance :
@@ -484,6 +490,9 @@ Proof.
     unfold EAst.test_def; simpl; eauto.
     rewrite <-H. rewrite fix_context_length in b0.
     eapply b0. eauto. now rewrite app_length fix_context_length.
+  - depelim H. depelim X0; solve_all.
+    depelim X; solve_all. eapply primProp_impl_test_prim.
+    constructor; intuition eauto. solve_all.
 Qed.
 
 (** Auxilliary notion of wellformedness on PCUIC to prove that erased terms are wellformed *)
@@ -505,7 +514,7 @@ Section wellscoped.
   Fixpoint wellformed (t : term) : bool :=
   match t with
   | tRel i => true
-  | tPrim p => true
+  | tPrim p => test_prim wellformed p
   | tEvar ev args => List.forallb (wellformed) args
   | tLambda _ N M => wellformed N && wellformed M
   | tApp u v => wellformed u && wellformed v
@@ -557,6 +566,7 @@ Section wellscoped.
     - now eapply nth_error_Some_length, Nat.ltb_lt in H0.
     - solve_all. destruct a as [s []], b.
       unfold test_def. len in i0. now rewrite i i0.
+    - depelim X1; solve_all; constructor; eauto.
   Qed.
 
   Lemma welltyped_wellformed {Σ : global_env_ext} {wfΣ : wf Σ} {Γ a} : welltyped Σ Γ a -> wellformed Σ a.
@@ -692,6 +702,8 @@ Proof.
     unfold EAst.test_def; simpl; eauto.
     rewrite fix_context_length in b.
     eapply b. now move: b0 => /andP[]. eauto. now rewrite app_length fix_context_length. tea.
+  - depelim H. solve_all. primProp.
+    depelim X0; depelim X1; repeat constructor; cbn; intuition eauto. solve_all.
 Qed.
 
 
diff --git a/erasure/theories/Extract.v b/erasure/theories/Extract.v
index 67b4c5ff7..bf09291c7 100644
--- a/erasure/theories/Extract.v
+++ b/erasure/theories/Extract.v
@@ -68,7 +68,7 @@ Definition erase_context (Γ : context) : list name :=
   map (fun d => d.(decl_name).(binder_name)) Γ.
 
 Inductive erase_prim_model (erase : term -> E.term -> Prop) : forall {t : prim_tag},
-  @PCUICPrimitive.prim_model term t -> @prim_model E.term t -> Prop :=
+  @PCUICPrimitive.prim_model term t -> @prim_model E.term t -> Type :=
 | erase_primInt i : @erase_prim_model erase primInt (PCUICPrimitive.primIntModel i) (primIntModel i)
 | erase_primFloat f : @erase_prim_model erase primFloat (PCUICPrimitive.primFloatModel f) (primFloatModel f)
 | erase_primArray a ed ev :
@@ -76,11 +76,13 @@ Inductive erase_prim_model (erase : term -> E.term -> Prop) : forall {t : prim_t
     All2 erase a.(PCUICPrimitive.array_value) ev ->
     @erase_prim_model erase primArray
       (PCUICPrimitive.primArrayModel a) (primArrayModel {| array_default := ed; array_value := ev |}).
+Derive Signature NoConfusion for erase_prim_model.
 
 Inductive erase_prim_val (erase : term -> E.term -> Prop) :
   PCUICPrimitive.prim_val term -> prim_val E.term -> Prop :=
 | erase_prim t m m' : @erase_prim_model erase t m m' ->
   erase_prim_val erase (t; m) (t; m').
+Derive Signature for erase_prim_val.
 
 Inductive erases (Σ : global_env_ext) (Γ : context) : term -> E.term -> Prop :=
     erases_tRel : forall i : nat, Σ;;; Γ |- tRel i ⇝ℇ E.tRel i
@@ -250,10 +252,10 @@ Proof.
     constructor; [now apply f|now apply f'].
   - eapply Hprim; tea.
     induction H. constructor.
-    induction H; constructor.
+    induction X; constructor.
     * now eapply f.
     * destruct a; cbn in *.
-      revert array_value ev X.
+      revert array_value ev a0.
       fix f' 3; intros mfix mfix' []; [now constructor|].
       constructor; [now apply f|now apply f'].
 Defined.
diff --git a/erasure/theories/Typed/Optimize.v b/erasure/theories/Typed/Optimize.v
index dbd61b4ea..7d52b6110 100644
--- a/erasure/theories/Typed/Optimize.v
+++ b/erasure/theories/Typed/Optimize.v
@@ -4,7 +4,7 @@ From MetaCoq.Erasure.Typed Require Import ExAst.
 From MetaCoq.Erasure.Typed Require Import Transform.
 From MetaCoq.Erasure.Typed Require Import ResultMonad.
 From MetaCoq.Erasure.Typed Require Import Utils.
-From MetaCoq.Erasure Require Import ELiftSubst.
+From MetaCoq.Erasure Require Import EPrimitive ELiftSubst.
 From MetaCoq.Utils Require Import utils.
 
 Import Kernames.
@@ -20,6 +20,7 @@ Definition map_subterms (f : term -> term) (t : term) : term :=
   | tProj p t => tProj p (f t)
   | tFix def i => tFix (map (map_def f) def) i
   | tCoFix def i => tCoFix (map (map_def f) def) i
+  | tPrim p => tPrim (map_prim f p)
   | t => t
   end.
 
@@ -309,6 +310,7 @@ Fixpoint is_dead (rel : nat) (t : term) : bool :=
   | tFix defs _
   | tCoFix defs _ => forallb (is_dead (#|defs| + rel) ∘ EAst.dbody) defs
   | tConstruct _ _ args => forallb (is_dead rel) args
+  | tPrim p => test_prim (is_dead rel) p
   | _ => true
   end.
 
@@ -366,6 +368,7 @@ Fixpoint valid_cases (t : term) : bool :=
   | tFix defs _
   | tCoFix defs _ => forallb (valid_cases ∘ EAst.dbody) defs
   | tConstruct _ _ (_ :: _) => false (* check whether constructors are not blocks*)
+  | tPrim p => test_prim valid_cases p
   | _ => true
   end.
 
@@ -407,7 +410,7 @@ Fixpoint is_expanded_aux (nargs : nat) (t : term) : bool :=
   | tProj _ t => is_expanded_aux 0 t
   | tFix defs _
   | tCoFix defs _ => forallb (is_expanded_aux 0 ∘ EAst.dbody) defs
-  | tPrim _ => true
+  | tPrim p => test_prim (is_expanded_aux 0) p
   end.
 
 (** Check if all applications are applied enough to be deboxed without eta expansion *)
@@ -644,7 +647,7 @@ Fixpoint analyze (state : analyze_state) (t : term) {struct t} : analyze_state :
     let state := new_vars state #|defs| in
     let state := fold_left (fun state d => analyze state (dbody d)) defs state in
     remove_vars state #|defs|
-  | tPrim _ => state
+  | tPrim p => fold_prim analyze p state
   end.
 
 Fixpoint decompose_TArr (bt : box_type) : list box_type × box_type :=
diff --git a/erasure/theories/Typed/OptimizeCorrectness.v b/erasure/theories/Typed/OptimizeCorrectness.v
index 8c08f5441..741357b87 100644
--- a/erasure/theories/Typed/OptimizeCorrectness.v
+++ b/erasure/theories/Typed/OptimizeCorrectness.v
@@ -9,7 +9,7 @@ From Coq Require Import List.
 From Coq Require Import ssrbool.
 From Coq Require Import PeanoNat.
 From Equations Require Import Equations.
-From MetaCoq.Erasure Require Import EAstUtils.
+From MetaCoq.Erasure Require Import EPrimitive EAstUtils.
 From MetaCoq.Erasure Require Import ECSubst.
 From MetaCoq.Erasure Require Import EInduction.
 From MetaCoq.Erasure Require Import ELiftSubst.
@@ -220,6 +220,7 @@ Proof.
     split; [easy|].
     rewrite <- Nat.add_succ_r in *.
     now eapply IHX.
+  - solve_all.
 Qed.
 
 Lemma is_dead_csubst k t u k' :
@@ -285,6 +286,7 @@ Proof.
     + rewrite <- !Nat.add_succ_r in *.
       apply IHX; [easy|easy|].
       now eapply closed_upwards.
+  - solve_all_k 6.
 Qed.
 
 Lemma valid_dearg_mask_nil t : valid_dearg_mask [] t.
@@ -453,7 +455,7 @@ Proof.
       now f_equal.
     + rewrite <- !Nat.add_succ_r in *.
       now apply IHX.
-  - reflexivity.
+  - f_equal; solve_all.
 Qed.
 
 Lemma masked_nil {X} mask :
@@ -802,7 +804,7 @@ Proof.
     cbn.
     f_equal.
     now rewrite p.
-  - now rewrite lift_mkApps.
+  - rewrite lift_mkApps. f_equal. simpl lift. f_equal. solve_all.
 Qed.
 
 Lemma lift_dearg n k t :
@@ -853,7 +855,7 @@ Proof.
     f_equal.
     rewrite <- !Nat.add_succ_r.
     now apply IHX.
-  - reflexivity.
+  - solve_all.
 Qed.
 
 Lemma is_dead_lift_all k k' n t :
@@ -894,6 +896,7 @@ Proof.
     cbn.
     rewrite <- !Nat.add_succ_r.
     now apply IHX.
+  - solve_all.
 Qed.
 
 Lemma is_dead_subst_other k k' s t :
@@ -944,6 +947,7 @@ Proof.
     f_equal.
     rewrite <- !Nat.add_succ_r.
     now apply IHX.
+  - solve_all.
 Qed.
 
 Lemma valid_dearg_mask_lift mask n k t :
@@ -1128,6 +1132,7 @@ Proof.
     cbn.
     rewrite <- Nat.add_succ_r.
     now rewrite p, IHX.
+  - solve_all.
 Qed.
 
 Lemma is_expanded_lift n k t :
@@ -1190,6 +1195,7 @@ Proof.
     rewrite <- !Nat.add_succ_r.
     rewrite IHX by easy.
     now replace (S (k - n)) with (S k - n) by lia.
+  - solve_all.
 Qed.
 
 Lemma is_dead_dearg_single k mask t args :
@@ -1288,6 +1294,19 @@ Proof.
      rewrite <- !Nat.add_succ_r.
      rewrite IHX.
      bia.
+    - solve_all. rtoProp; intuition eauto.
+      depelim X; cbn; eauto.
+      destruct a; unfold test_array_model; cbn.
+      destruct p. cbn in *. rewrite e; eauto.
+      rewrite <- !andb_assoc. f_equal.
+      rewrite andb_comm.
+      induction a; cbn. rewrite andb_true_r; auto.
+      rewrite <- !andb_assoc.
+      rewrite IHa. rewrite p;eauto.
+      rewrite <- !andb_assoc. f_equal.
+      rewrite andb_comm.
+      rewrite <- !andb_assoc. f_equal.
+      bia. now rewrite andb_true_r.
 Qed.
 
 Lemma is_dead_dearg_lambdas k mask t :
@@ -1400,7 +1419,7 @@ Proof.
     rewrite p by easy.
     split; [easy|].
     now apply IHX.
-  - now apply forallb_Forall.
+  - solve_all. rtoProp; intuition solve_all.
 Qed.
 
 Lemma valid_dearg_mask_dearg mask t :
@@ -1557,7 +1576,9 @@ Proof.
     unfold map_def; cbn.
     f_equal.
     now apply (p _ _ []).
-  - now rewrite subst_mkApps, map_map.
+  - rewrite subst_mkApps, map_map; cbn; f_equal. f_equal.
+    solve_all. eapply map_prim_eq_prop; tea; cbn; intuition eauto.
+    specialize (a s k []). eauto.
 Qed.
 
 Lemma dearg_subst s k t :
@@ -1673,7 +1694,7 @@ Proof.
     propify.
     rewrite <- !Nat.add_succ_r.
     now rewrite p, IHX.
-  - assumption.
+  - solve_all_k 6.
 Qed.
 
 Lemma is_expanded_aux_subst s n t k :
@@ -1717,7 +1738,7 @@ Proof.
     propify.
     rewrite <- !Nat.add_succ_r.
     now rewrite p, IHX.
-  - assumption.
+  - solve_all_k 6.
 Qed.
 
 Lemma is_expanded_substl s n t :
@@ -2001,6 +2022,7 @@ Proof.
     cbn in *.
     propify.
     now rewrite <- !Nat.add_succ_r.
+  - solve_all_k 6.
 Qed.
 
 Lemma valid_cases_subst s k t :
@@ -2036,6 +2058,7 @@ Proof.
   - induction X in X, k, valid_t |- *; [easy|].
     cbn in *; propify.
     now rewrite <- !Nat.add_succ_r.
+  - solve_all_k 6.
 Qed.
 
 Lemma closedn_dearg_single k t args mask :
@@ -2113,6 +2136,7 @@ Proof.
   - rtoProp; solve_all. rewrite -> !Nat.add_assoc in *.
     specialize (a (#|m| + k')). unfold is_true. rewrite <- a. f_equal. lia.
     unfold is_true. rewrite <- b. f_equal. lia.
+  - solve_all_k 6.
 Qed.
 
 Lemma closedn_dearg_case_branch_body_rec i k mask t :
@@ -2212,6 +2236,7 @@ Proof.
     split; [easy|].
     rewrite <- !Nat.add_succ_r in *.
     now apply IHX.
+  - rewrite closedn_mkApps; cbn; rtoProp; intuition solve_all. solve_all_k 6.
 Qed.
 
 Hint Resolve
diff --git a/erasure/theories/Typed/TypeAnnotations.v b/erasure/theories/Typed/TypeAnnotations.v
index f37c98f9e..a59888cda 100644
--- a/erasure/theories/Typed/TypeAnnotations.v
+++ b/erasure/theories/Typed/TypeAnnotations.v
@@ -583,7 +583,7 @@ Proof.
     apply bigprod_map; [|exact ta.2].
     intros.
     exact (f _ All_nil _ X).
-  - exact (annot_mkApps ta argsa).
+  - refine (annot_mkApps _ argsa). cbn. cbn in ta. exact ta.
 Defined.
 
 Definition annot_dearg im cm {t : term} (ta : annots box_type t) : annots box_type (dearg im cm t) :=
diff --git a/pcuic/theories/utils/PCUICPrimitive.v b/pcuic/theories/utils/PCUICPrimitive.v
index ac205a86e..10d9a633b 100644
--- a/pcuic/theories/utils/PCUICPrimitive.v
+++ b/pcuic/theories/utils/PCUICPrimitive.v
@@ -31,7 +31,7 @@ Arguments primIntModel {term}.
 Arguments primFloatModel {term}.
 Arguments primArrayModel {term}.
 
-Derive Signature NoConfusion for prim_model.
+Derive Signature NoConfusion NoConfusionHom for prim_model.
 
 Definition prim_model_of (term : Type) (p : prim_tag) : Type :=
   match p with
diff --git a/utils/theories/All_Forall.v b/utils/theories/All_Forall.v
index ad2966a7e..6c82bc714 100644
--- a/utils/theories/All_Forall.v
+++ b/utils/theories/All_Forall.v
@@ -3760,6 +3760,22 @@ Section map_All.
   Qed.
 End map_All.
 
+Section make_All.
+  Context {A} {B : A -> Type} (f : forall x : A, B x).
+
+  Equations make_All (l : list A) : All B l :=
+  | [] := All_nil
+  | hd :: tl := All_cons (f hd) (make_All tl).
+End make_All.
+
+Section make_All_All.
+  Context {A} {B : A -> Type} {C : A -> Type} (f : forall x : A, B x -> C x).
+
+  Equations make_All_All {l : list A} (a : All B l) : All C l :=
+  | All_nil := All_nil
+  | All_cons bhd btl := All_cons (f _ bhd) (make_All_All btl).
+End make_All_All.
+
 Lemma All_map_All {A B C} {Q : C -> Type} {P : C -> A -> Prop}
   {Q' : B -> Type} {R : C -> A -> Prop}
   f args (ha: forall y : C, Q y -> ∥ All (R y) args ∥) :