diff --git a/README.md b/README.md
index 5a0f256d..6e675075 100644
--- a/README.md
+++ b/README.md
@@ -17,7 +17,7 @@ opam switch create . 4.07.1
 eval $(opam env)
 opam repo add coq-released https://coq.inria.fr/opam/released
 opam install -j 4 coq.8.11.2 coq-bignums coq-stdpp coq-quickchick
-opam pin -j 4 add https://github.com/MetaCoq/metacoq.git#abc736f20020156e520e7ca4ef0557ce5f8b7db0
+opam pin -j 4 add https://github.com/MetaCoq/metacoq.git#77adb13585d2f357b78642c16b6c4da817f35eff
 ```
 
 After completing the procedures above, run `make` to build the development, and
diff --git a/embedding/examples/Demo.v b/embedding/examples/Demo.v
index e410137f..002ac427 100644
--- a/embedding/examples/Demo.v
+++ b/embedding/examples/Demo.v
@@ -33,7 +33,7 @@ Print id_nat_syn.
 
 (* Unquote *)
 MetaCoq Unquote Definition plus_one :=
-  (MC.tLambda (nNamed "x")
+  (MC.tLambda (aRelevant (nNamed "x"))
               (MC.tInd (mkInd (MPfile ["Datatypes"; "Init"; "Coq"], "nat") 0) nil)
               (MC.tApp (MC.tConstruct (mkInd (MPfile ["Datatypes"; "Init"; "Coq"], "nat") 0) 1 nil)
                        (MC.tRel 0 :: nil))).
diff --git a/embedding/theories/pcuic/PCUICCorrectnessAux.v b/embedding/theories/pcuic/PCUICCorrectnessAux.v
index b2e5720c..aae13546 100644
--- a/embedding/theories/pcuic/PCUICCorrectnessAux.v
+++ b/embedding/theories/pcuic/PCUICCorrectnessAux.v
@@ -488,7 +488,7 @@ Definition lpat_to_lam : term -> list term -> list (BasicTC.ident * term) -> ter
          lambda introduces a binder, we need also to lift free
          variables in [ty_params] *)
          let lam_type := subst (map (lift0 #|tys'|) ty_params) 0 ty in
-         rec (tLambda (BasicTC.nNamed n) lam_type body) ty_params tys'
+         rec (tLambda (aRelevant (nNamed n)) lam_type body) ty_params tys'
        end.
 
 
@@ -508,7 +508,7 @@ Qed.
 
 Lemma pat_to_lam_unfold b tys n ty params :
   lpat_to_lam b params (tys ++ [(n,ty)]) =
-  tLambda (BasicTC.nNamed n) (subst0 params ty) (lpat_to_lam b (map (lift0 1) params) tys).
+  tLambda (aRelevant (nNamed n)) (subst0 params ty) (lpat_to_lam b (map (lift0 1) params) tys).
 Proof.
   revert b params.
   induction tys;intros.
@@ -1766,7 +1766,7 @@ Qed.
 
 
 Lemma from_vConstr_not_lambda :
-  forall (Σ : global_env) (i : Ast.inductive) (n0 : ename) (na : BasicAst.name) (t0 b : term) l,
+  forall (Σ : global_env) (i : Ast.inductive) (n0 : ename) (na : aname) (t0 b : term) l,
     tLambda na t0 b = t⟦ of_val_i (vConstr i n0 l) ⟧ Σ -> False.
 Proof.
   intros Σ i n0 na t0 b l H.
diff --git a/embedding/theories/pcuic/PCUICTranslate.v b/embedding/theories/pcuic/PCUICTranslate.v
index a747c74b..8aeabd27 100644
--- a/embedding/theories/pcuic/PCUICTranslate.v
+++ b/embedding/theories/pcuic/PCUICTranslate.v
@@ -64,17 +64,20 @@ Fixpoint string_of_modpath (mp : modpath) : string :=
 Definition string_of_kername (kn : kername) :=
   (string_of_modpath kn.1 ++ "@" ++ kn.2)%string.
 
+Definition aRelevant (n : name) :=
+  {| binder_name := n; binder_relevance := Relevant |}.
+
 (** Translation of types to PCUIC terms. Universal types become Pi-types with the first argument being of type [Set]. Keeping them in [Set] is crucial, since we don't have to deal with universe levels *)
 Fixpoint type_to_term (ty : type) : term :=
   match ty with
   | tyInd i => tInd (mkInd (kername_of_string i) 0) []
-  | tyForall nm ty => tProd (nNamed nm) (tSort Universe.type0) T⟦ty⟧
+  | tyForall nm ty => tProd (aRelevant (nNamed nm)) (tSort Universe.type0) T⟦ty⟧
   | tyVar nm => tVar nm
   | tyApp ty1 ty2 => tApp T⟦ty1⟧ T⟦ty2⟧
   | tyArr ty1 ty2 =>
     (* NOTE: we have to lift indices for the codomain,
        since in Coq arrows are Pi types and introduce an binder *)
-    tProd nAnon T⟦ty1⟧ (lift0 1 T⟦ty2⟧)
+    tProd (aRelevant nAnon) T⟦ty1⟧ (lift0 1 T⟦ty2⟧)
   | tyRel i => tRel i
   end
 where "T⟦ ty ⟧ " := (type_to_term ty).
@@ -91,7 +94,7 @@ Definition pat_to_lam (body : term)
       introduces a binder, we need also to lift free variables in
       [ty_params] *)
       let lam_type := subst ty_params 0 ty in
-      tLambda (BasicTC.nNamed n) lam_type (rec (map (lift0 1) ty_params) tys')
+      tLambda (aRelevant (nNamed n)) lam_type (rec (map (lift0 1) ty_params) tys')
     end).
 
 (** Translating branches of the [eCase] construct. Note that MetaCoq uses indices to represent constructors. Indices are corresponding positions in the list of constructors for a particular inductive type *)
@@ -121,9 +124,9 @@ Fixpoint expr_to_term (Σ : global_env) (e : expr) : term :=
   match e with
   | eRel i => tRel i
   | eVar nm => tVar nm
-  | eLambda nm ty b => tLambda (nNamed nm) T⟦ty⟧ t⟦b⟧Σ
-  | eTyLam nm b => tLambda (nNamed nm) (tSort Universe.type0) t⟦b⟧Σ
-  | eLetIn nm e1 ty e2 => tLetIn (nNamed nm) t⟦e1⟧Σ T⟦ty⟧ t⟦e2⟧Σ
+  | eLambda nm ty b => tLambda (aRelevant (nNamed nm)) T⟦ty⟧ t⟦b⟧Σ
+  | eTyLam nm b => tLambda (aRelevant (nNamed nm)) (tSort Universe.type0) t⟦b⟧Σ
+  | eLetIn nm e1 ty e2 => tLetIn (aRelevant (nNamed nm)) t⟦e1⟧Σ T⟦ty⟧ t⟦e2⟧Σ
   | eApp e1 e2 => tApp t⟦e1⟧Σ t⟦e2⟧Σ
   | eConstr i t =>
     match (resolve_constr Σ i t) with
@@ -133,8 +136,9 @@ Fixpoint expr_to_term (Σ : global_env) (e : expr) : term :=
   | eConst nm => tConst (kername_of_string nm) []
   | eCase nm_i ty2 e bs =>
     let (nm, params) := nm_i in
-    let typeInfo := tLambda nAnon (mkApps (tInd (mkInd (kername_of_string nm) 0) [])
-                                          (map type_to_term params))
+    let typeInfo := tLambda (aRelevant nAnon)
+                            (mkApps (tInd (mkInd (kername_of_string nm) 0) [])
+                                    (map type_to_term params))
                             (lift0 1 (type_to_term ty2)) in
     match (resolve_inductive Σ nm) with
     | Some v =>
@@ -149,11 +153,11 @@ Fixpoint expr_to_term (Σ : global_env) (e : expr) : term :=
   | eFix nm nv ty1 ty2 b =>
     let tty1 := T⟦ty1⟧ in
     let tty2 := T⟦ty2⟧ in
-    let ty := tProd nAnon tty1 (lift0 1 tty2) in
+    let ty := tProd (aRelevant nAnon) tty1 (lift0 1 tty2) in
     (* NOTE: we have to lift the indices in [tty1] because [tRel 0]
              corresponds to the recursive call *)
-    let body := tLambda (nNamed nv) (lift0 1 tty1) t⟦b⟧Σ in
-    tFix [(mkdef _ (nNamed nm) ty body 0)] 0
+    let body := tLambda (aRelevant (nNamed nv)) (lift0 1 tty1) t⟦b⟧Σ in
+    tFix [(mkdef _ (aRelevant (nNamed nm)) ty body 0)] 0
   | eTy ty => T⟦ty⟧
   end
 where "t⟦ e ⟧ Σ":= (expr_to_term Σ e).
@@ -163,12 +167,12 @@ where "t⟦ e ⟧ Σ":= (expr_to_term Σ e).
 
 Import Basics.
 
-Definition of_ename (e : option ename) : BasicTC.name :=
+Definition of_ename (e : option ename) : aname :=
   match e with
   | Some e' =>
     let (mp,unqualified_nm) := kername_of_string e' in
-    BasicTC.nNamed unqualified_nm
-  | None => BasicTC.nAnon
+    aRelevant (nNamed unqualified_nm)
+  | None => aRelevant nAnon
   end.
 
 (** Translation of constructors of parameterised inductive types requires
diff --git a/embedding/theories/pcuic/PCUICtoTemplate.v b/embedding/theories/pcuic/PCUICtoTemplate.v
index d047af41..386807da 100644
--- a/embedding/theories/pcuic/PCUICtoTemplate.v
+++ b/embedding/theories/pcuic/PCUICtoTemplate.v
@@ -3,6 +3,7 @@ From Coq Require Import Bool String List Program BinPos Compare_dec Omega.
 From MetaCoq.Template Require Import All.
      (* config utils AstUtils BasicAst Ast. *)
 From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICInduction PCUICLiftSubst PCUICUnivSubst PCUICTyping PCUICGeneration.
+From MetaCoq.PCUIC Require Export PCUICToTemplate.
 Require Import String.
 Local Open Scope string_scope.
 Set Asymmetric Patterns.
@@ -10,45 +11,9 @@ Set Asymmetric Patterns.
 Module TC := Ast.
 Module P := PCUICAst.
 
-Fixpoint trans (t : P.term) : TC.term :=
-  match t with
-  | P.tRel n => TC.tRel n
-  | P.tVar n => TC.tVar n
-  | P.tEvar ev args => TC.tEvar ev (List.map trans args)
-  | P.tSort u => TC.tSort u
-  | P.tConst c u => TC.tConst c u
-  | P.tInd c u => TC.tInd c u
-  | P.tConstruct c k u => TC.tConstruct c k u
-  | P.tLambda na T M => TC.tLambda na (trans T) (trans M)
-  | P.tApp u v => TC.mkApps (trans u) [trans v]
-  | P.tProd na A B => TC.tProd na (trans A) (trans B)
-  | P.tLetIn na b t b' => TC.tLetIn na (trans b) (trans t) (trans b')
-  | P.tCase ind p c brs =>
-    let brs' := List.map (on_snd trans) brs in
-    TC.tCase ind (trans p) (trans c) brs'
-  | P.tProj p c => TC.tProj p (trans c)
-  | P.tFix mfix idx =>
-    let mfix' := List.map (map_def trans trans) mfix in
-    TC.tFix mfix' idx
-  | P.tCoFix mfix idx =>
-    let mfix' := List.map (map_def trans trans) mfix in
-    TC.tCoFix mfix' idx
-  end.
-
-Definition trans_decl (d : P.context_decl) :=
-  let 'P.mkdecl na b t := d in
-  {| TC.decl_name := na;
-     TC.decl_body := option_map trans b;
-     TC.decl_type := trans t |}.
-
-Definition trans_local Γ := List.map trans_decl Γ.
-
-Definition trans_one_ind_body (d : P.one_inductive_body) :=
-  {| TC.ind_name := d.(P.ind_name);
-     TC.ind_type := trans d.(P.ind_type);
-     TC.ind_kelim := d.(P.ind_kelim);
-     TC.ind_ctors := List.map (fun '(x, y, z) => (x, trans y, z)) d.(P.ind_ctors);
-     TC.ind_projs := List.map (fun '(x, y) => (x, trans y)) d.(P.ind_projs) |}.
+Definition aRelevant (n : name) : aname :=
+  {| binder_name := n;
+     binder_relevance := Relevant |}.
 
 Definition trans_local_entry (nle : ident * P.local_entry) : TC.context_decl :=
   let (nm, le) := nle in
@@ -58,9 +23,9 @@ Definition trans_local_entry (nle : ident * P.local_entry) : TC.context_decl :=
        bodies as parameters, so we produce a dummy value here.
        To produce an actual decalaration with a body we need its type,
        and it's not available it this point*)
-    TC.mkdecl (nNamed nm) None (TC.tVar "not supported")
+    TC.mkdecl (aRelevant (nNamed nm)) None (TC.tVar "not supported")
   | P.LocalAssum la =>
-    TC.mkdecl (nNamed nm) None (trans la)
+    TC.mkdecl (aRelevant (nNamed nm)) None (trans la)
   end.
 
 Definition trans_one_ind_entry (d : P.one_inductive_entry) : TC.one_inductive_entry :=
@@ -84,28 +49,3 @@ Definition trans_minductive_entry (e : P.mutual_inductive_entry) :  TC.mutual_in
      TC.mind_entry_universes := trans_universes_decl e.(P.mind_entry_universes);
      TC.mind_entry_variance := None;
      TC.mind_entry_private := e.(P.mind_entry_private) |}.
-
-Definition trans_constant_body (bd : P.constant_body) : TC.constant_body :=
-  {| TC.cst_type := trans bd.(P.cst_type);
-     TC.cst_body := option_map trans bd.(P.cst_body);
-     TC.cst_universes := bd.(P.cst_universes) |}.
-
-Definition trans_minductive_body md :=
-  {| TC.ind_finite := md.(P.ind_finite);
-     TC.ind_npars := md.(P.ind_npars);
-     TC.ind_params := trans_local md.(P.ind_params);
-     TC.ind_bodies := map trans_one_ind_body md.(P.ind_bodies);
-     TC.ind_variance := md.(ind_variance);
-     TC.ind_universes := md.(P.ind_universes) |}.
-
-Definition trans_global_decl (d : P.global_decl) : TC.global_decl :=
-  match d with
-  | P.ConstantDecl bd => TC.ConstantDecl (trans_constant_body bd)
-  | P.InductiveDecl bd => TC.InductiveDecl (trans_minductive_body bd)
-  end.
-
-Definition trans_global_env (d : P.global_env) :=
-  List.map (on_snd trans_global_decl) d.
-
-Definition trans_global (Σ : P.global_env_ext) : TC.global_env_ext :=
-  (trans_global_env (fst Σ), snd Σ).
\ No newline at end of file
diff --git a/extra/docker/ConCert-8.11/Dockerfile b/extra/docker/ConCert-8.11/Dockerfile
index 01b7e767..7d645f96 100644
--- a/extra/docker/ConCert-8.11/Dockerfile
+++ b/extra/docker/ConCert-8.11/Dockerfile
@@ -9,7 +9,7 @@ RUN ["/bin/bash", "--login", "-c", "set -x \
   && opam install -y -v -j ${NJOBS} coq-equations.1.2.1+8.11 coq-stdpp coq-quickchick \
   && git clone https://github.com/MetaCoq/metacoq.git \
   && cd metacoq \
-  && git checkout coq-8.11 \
+  && git checkout 77adb13585d2f357b78642c16b6c4da817f35eff \
   && opam install -y -v -j ${NJOBS} . \
   && opam clean -a -c -s --logs \
   && opam config list \
diff --git a/extraction/examples/ErasureTests.v b/extraction/examples/ErasureTests.v
index e1253d66..6696b8bb 100644
--- a/extraction/examples/ErasureTests.v
+++ b/extraction/examples/ErasureTests.v
@@ -7,7 +7,6 @@ From Coq Require Import Ascii.
 From Coq Require Import Bool.
 From Coq Require Import List.
 From Coq Require Import String.
-From MetaCoq.Erasure Require Import SafeTemplateErasure.
 From MetaCoq.PCUIC Require Import PCUICAst.
 From MetaCoq.PCUIC Require Import PCUICTyping.
 From MetaCoq.PCUIC Require Import TemplateToPCUIC.
@@ -24,6 +23,8 @@ Import ListNotations.
 Import MonadNotation.
 Set Equations Transparent.
 
+Local Existing Instance extraction_checker_flags.
+
 Module flag_of_type_tests.
 Record type_flag_squashed :=
   { is_logical : bool;
diff --git a/extraction/examples/ForPaper.v b/extraction/examples/ForPaper.v
index 39cd4b7e..48b44222 100644
--- a/extraction/examples/ForPaper.v
+++ b/extraction/examples/ForPaper.v
@@ -11,9 +11,8 @@ From ConCert.Extraction Require Import Erasure.
 
 From MetaCoq.Template Require Import Kernames.
 From MetaCoq.Template Require Import Loader.
-From MetaCoq.Erasure Require Import SafeTemplateErasure Loader.
+From MetaCoq.Erasure Require Import Loader.
 From MetaCoq.Erasure Require ErasureFunction.
-From MetaCoq.Erasure Require SafeErasureFunction.
 From MetaCoq.Template Require Import config.
 From MetaCoq.SafeChecker Require Import PCUICSafeReduce PCUICSafeChecker
      SafeTemplateChecker.
diff --git a/extraction/plugin/_CoqProject b/extraction/plugin/_CoqProject
index acf764ec..66351708 100644
--- a/extraction/plugin/_CoqProject
+++ b/extraction/plugin/_CoqProject
@@ -93,8 +93,8 @@ src/resultMonad.ml
 src/resultMonad.mli
 src/rustExtract.ml
 src/rustExtract.mli
-src/safeErasureFunction.ml
-src/safeErasureFunction.mli
+src/erasureFunction.ml
+src/erasureFunction.mli
 src/safeTemplateChecker.ml
 src/safeTemplateChecker.mli
 src/ssrbool.ml
diff --git a/extraction/plugin/src/.gitignore b/extraction/plugin/src/.gitignore
index ee817814..ac9f1976 100644
--- a/extraction/plugin/src/.gitignore
+++ b/extraction/plugin/src/.gitignore
@@ -82,8 +82,8 @@ resultMonad.ml
 resultMonad.mli
 rustExtract.ml
 rustExtract.mli
-safeErasureFunction.ml
-safeErasureFunction.mli
+erasureFunction.ml
+erasureFunction.mli
 safeTemplateChecker.ml
 safeTemplateChecker.mli
 ssrbool.ml
diff --git a/extraction/plugin/src/concert_extraction_plugin.mlpack b/extraction/plugin/src/concert_extraction_plugin.mlpack
index cb378318..9a3f9ee7 100644
--- a/extraction/plugin/src/concert_extraction_plugin.mlpack
+++ b/extraction/plugin/src/concert_extraction_plugin.mlpack
@@ -40,7 +40,7 @@ ETyping
 EPretty
 Extract
 EOptimizePropDiscr
-SafeErasureFunction
+ErasureFunction
 Typing0
 SafeTemplateChecker
 
diff --git a/extraction/process_extraction.sh b/extraction/process_extraction.sh
index e76ad042..fa678f1d 100755
--- a/extraction/process_extraction.sh
+++ b/extraction/process_extraction.sh
@@ -21,10 +21,6 @@ then
   files=`cat ../template-coq-files.txt`
   echo "Removing files linked in template-coq:" $files
   rm -f $files
-
-  echo "Fixing extraction bugs"
-  sed -i "s/Coq__2/Coq__1/g" common1.mli
-  sed -i "s/Coq__3/Coq__1/g" common1.mli
 else
   echo "Extraction up to date"
 fi
diff --git a/extraction/theories/CameLIGOExtract.v b/extraction/theories/CameLIGOExtract.v
index d48f00c2..fd66ce35 100644
--- a/extraction/theories/CameLIGOExtract.v
+++ b/extraction/theories/CameLIGOExtract.v
@@ -1,9 +1,8 @@
 From Coq Require Import PeanoNat ZArith.
 
 From MetaCoq.Template Require Import Loader.
-From MetaCoq.Erasure Require Import SafeTemplateErasure.
+From MetaCoq.Erasure Require Import Erasure.
 From MetaCoq.Erasure Require ErasureFunction.
-From MetaCoq.Erasure Require SafeErasureFunction.
 From MetaCoq.Template Require Import Kernames config.
 From MetaCoq.SafeChecker Require Import PCUICSafeReduce PCUICSafeChecker
      SafeTemplateChecker.
@@ -25,13 +24,6 @@ Local Open Scope string_scope.
 From MetaCoq.Template Require Import All.
 From MetaCoq.PCUIC Require PCUICAst PCUICTyping.
 
-Definition to_constant_decl (gd : option T.global_decl) :=
-  match gd with
-  | Some (ConstantDecl cst_body) => ret cst_body
-  | Some (InductiveDecl cst_body) => tmFail "Error (constant expected, given inductive)"
-  | None => tmFail "Error (expected constant with a body)"
-  end.
-
 Record CameLIGOMod {Base : ChainBase} (msg ctx setup storage operation : Type) :=
   { lmd_module_name : string ;
     lmd_prelude : string ;
@@ -61,7 +53,7 @@ Definition cameligo_args :=
 
 Import PCUICAst PCUICTyping.
 Definition annot_extract_env_cameligo
-           (Σ : PCUICAst.global_env) 
+           (Σ : PCUICAst.global_env)
            (wfΣ : ∥wf Σ∥)
            (include : KernameSet.t)
            (ignore : kername -> bool) : option (∑ Σ, env_annots box_type Σ).
@@ -79,13 +71,13 @@ Definition annot_extract_template_env_specalize
            (seeds : KernameSet.t)
            (ignore : kername -> bool) : result (∑ e, env_annots box_type e) string :=
   let e := SafeTemplateChecker.fix_global_env_universes e in
-  let e := T2P.trans_global_decls e in
+  let e := TemplateToPCUIC.trans_global_decls e in
   e <- specialize_ChainBase_env e ;;
   wfe <-check_wf_env_func extract_within_coq e;;
   match annot_extract_env_cameligo e wfe seeds ignore with
   | Some s => Ok s
   | None => Err "failed internally in annot_extract_template_env_specalize"
-  end. 
+  end.
 
 Definition printCameLIGODefs (prefix : string) (Σ : TemplateEnvironment.global_env)
            (TT : MyEnv.env string)
@@ -98,17 +90,17 @@ Definition printCameLIGODefs (prefix : string) (Σ : TemplateEnvironment.global_
   : string + string :=
   let seeds := KernameSet.union (KernameSet.singleton init) (KernameSet.singleton receive) in
   match annot_extract_template_env_specalize Σ seeds (fun k => List.existsb (eq_kername k) ignore) with
-  | Ok (eΣ; annots) => 
+  | Ok (eΣ; annots) =>
     (* dependencies should be printed before the dependent definitions *)
     let ldef_list := List.rev (print_global_env prefix TT eΣ annots) in
     (* filtering empty strings corresponding to the ignored definitions *)
     let not_empty_str := (negb ∘ (String.eqb "") ∘ snd) in
-    
-    let ldef_ty_list := ldef_list 
+
+    let ldef_ty_list := ldef_list
                           |> filter (fun d => match d with TyDecl _ => true | _ => false end)
                           |> map (fun d => match d with ConstDecl d' => d' | TyDecl d' => d' end)
                           |> filter not_empty_str in
-    let ldef_const_list := ldef_list 
+    let ldef_const_list := ldef_list
                             |> filter (fun d => match d with ConstDecl _ => true | _ => false end)
                             |> map (fun d => match d with ConstDecl d' => d' | TyDecl d' => d' end)
                             |> filter not_empty_str in
@@ -162,7 +154,7 @@ Definition CameLIGO_ignore_default {Base : ChainBase} :=
   ].
 
 Definition TT_remap_default : list (kername * string) :=
-  [  
+  [
     (* types *)
     remap <%% Z %%> "tez"
   ; remap <%% N %%> "nat"
@@ -207,8 +199,8 @@ Definition TT_remap_default : list (kername * string) :=
   ; remap <%% @address_eqdec %%> ""
   ; remap <%% @address_countable %%> ""
   ].
-  
-Definition CameLIGO_rename_default := 
+
+Definition CameLIGO_rename_default :=
   [
       ("to", "to_")
     ; ("amount", "amount_")
diff --git a/extraction/theories/Common.v b/extraction/theories/Common.v
index 08e324d8..c3f07769 100644
--- a/extraction/theories/Common.v
+++ b/extraction/theories/Common.v
@@ -1,47 +1,13 @@
-From Coq Require Import Arith.
-From Coq Require Import Ascii.
-From Coq Require Import List.
-From Coq Require Import NArith.
-From Coq Require Import String.
-
-From MetaCoq Require Import monad_utils.
-From MetaCoq Require Import MCPrelude.
-From MetaCoq Require Import MCProd.
-From MetaCoq Require Import MCString.
-From MetaCoq Require Import MCSquash.
-From MetaCoq.Erasure Require Import EAst.
-From MetaCoq.Erasure Require Import SafeErasureFunction.
-From MetaCoq.Erasure Require Import SafeTemplateErasure.
-From MetaCoq.PCUIC Require Import PCUICAst PCUICTyping PCUICValidity TemplateToPCUIC.
-From MetaCoq.SafeChecker Require Import PCUICSafeChecker.
-From MetaCoq.SafeChecker Require Import SafeTemplateChecker.
+From ConCert.Extraction Require Import ResultMonad.
 From MetaCoq.Template Require Import Ast.
+From MetaCoq.Template Require Import AstUtils.
 From MetaCoq.Template Require Import BasicAst.
 From MetaCoq.Template Require Import Loader.
 From MetaCoq.Template Require Import TemplateMonad.
-
-From ConCert.Extraction Require Import ClosedAux.
-From ConCert.Extraction Require Import Erasure.
-From ConCert.Extraction Require Import ResultMonad.
-From ConCert.Extraction Require Import Optimize.
-From ConCert.Extraction Require Import OptimizeCorrectness.
-From ConCert.Utils Require Import StringExtra.
-
-Module T := MetaCoq.Template.Ast.
-Module P := MetaCoq.PCUIC.PCUICAst.
-Module E := MetaCoq.Erasure.EAst.
-Module TUtil := MetaCoq.Template.AstUtils.
-Module PUtil := MetaCoq.PCUIC.PCUICAstUtils.
-Module PT := MetaCoq.PCUIC.PCUICTyping.
-Module EF := MetaCoq.Erasure.SafeErasureFunction.
-Module T2P := MetaCoq.PCUIC.TemplateToPCUIC.
-
-Local Open Scope string.
-Import ListNotations.
-Import MonadNotation.
-
-Local Open Scope bool.
-Import E.
+From MetaCoq.Template Require Import monad_utils.
+From MetaCoq.Template Require Import utils.
+From MetaCoq.PCUIC Require PCUICAst.
+From MetaCoq.SafeChecker Require Import PCUICSafeChecker.
 
 (** Extracts a constant name, inductive name or returns None *)
 Definition to_kername (t : Ast.term) : option kername :=
@@ -61,7 +27,7 @@ Notation "<%% t %%>" :=
              
 Definition result_of_typing_result
            {A}
-           (Σ : P.global_env_ext)
+           (Σ : PCUICAst.global_env_ext)
            (tr : typing_result A) : result A string :=
   match tr with
   | Checked a => ret a
@@ -96,10 +62,10 @@ Definition to_string_name (t : Ast.term) : string :=
 Definition extract_def_name {A : Type} (a : A) : TemplateMonad kername :=
   a <- tmEval cbn a;;
   quoted <- tmQuote a;;
-  let (head, args) := TUtil.decompose_app quoted in
+  let (head, args) := decompose_app quoted in
   match head with
-  | T.tConst name _ => ret name
-  | _ => tmFail ("Expected constant at head, got " ++ TUtil.string_of_term head)
+  | tConst name _ => ret name
+  | _ => tmFail ("Expected constant at head, got " ++ string_of_term head)
   end.
 
 Notation "'unfolded' d" :=
@@ -114,25 +80,25 @@ Definition EnvCheck_to_template {A } (ec : EnvCheck A) : TemplateMonad A :=
   | EnvError Σ e => tmFail (string_of_env_error Σ e)
   end.
 
-Definition quote_recursively_body {A : Type} (def : A) : TemplateMonad T.program :=
+Definition quote_recursively_body {A : Type} (def : A) : TemplateMonad program :=
   p <- tmQuoteRecTransp def false ;;
   kn <- match p.2 with
-       | T.tConst name _ => ret name
+       | tConst name _ => ret name
        | _ => tmFail ("Expected constant, got "  ++
-                       TUtil.string_of_term p.2)
+                       string_of_term p.2)
        end;;
-  match T.lookup_env p.1 kn with
-  | Some (T.ConstantDecl cb) =>
-    match cb.(T.cst_body) with
+  match lookup_env p.1 kn with
+  | Some (ConstantDecl cb) =>
+    match cb.(cst_body) with
     | Some b => ret (p.1, b)
     | None => tmFail ("The constant doesn't have a body: " ++ kn.2)
     end
   | _ => tmFail ("Not found: " ++ kn.2)
   end.
 
-Fixpoint update_global_env (Σ :T.global_env) (Σup : T.global_env) : T.global_env :=
+Fixpoint update_global_env (Σ : global_env) (Σup : global_env) : global_env :=
   match Σ with
-  | (kn, gd) :: Σ' => match T.lookup_env Σup kn with
+  | (kn, gd) :: Σ' => match lookup_env Σup kn with
                     | Some v => (kn,v) :: update_global_env Σ' Σup
                     | None => (kn, gd) :: update_global_env Σ' Σup
                     end
diff --git a/extraction/theories/Erasure.v b/extraction/theories/Erasure.v
index 621246ec..4f5994c1 100644
--- a/extraction/theories/Erasure.v
+++ b/extraction/theories/Erasure.v
@@ -13,7 +13,7 @@ From MetaCoq.Erasure Require Import EArities.
 From MetaCoq.Erasure Require Import EAstUtils.
 From MetaCoq.Erasure Require Import Extract.
 From MetaCoq.Erasure Require Import Prelim.
-From MetaCoq.Erasure Require SafeErasureFunction.
+From MetaCoq.Erasure Require ErasureFunction.
 From MetaCoq.PCUIC Require Import PCUICArities.
 From MetaCoq.PCUIC Require Import PCUICAst.
 From MetaCoq.PCUIC Require Import PCUICAstUtils.
@@ -66,12 +66,12 @@ Context (Σ : global_env_ext).
 Context (wfextΣ : ∥wf_ext Σ∥).
 Let wfΣ : ∥wf Σ∥ := ltac:(now sq).
 
-Opaque SafeErasureFunction.wf_reduction.
+Opaque ErasureFunction.wf_reduction.
 Opaque reduce_term.
 
-Notation term_rel := (SafeErasureFunction.term_rel Σ).
+Notation term_rel := (ErasureFunction.term_rel Σ).
 Instance WellFounded_term_rel : WellFounded term_rel :=
-  (SafeErasureFunction.wf_reduction Σ wfΣ).
+  (ErasureFunction.wf_reduction Σ wfΣ).
 
 Lemma sq_red_transitivity {Γ A} B {C} :
   ∥red Σ Γ A B∥ ->
@@ -93,7 +93,7 @@ Proof.
   eapply isArity_red1; eassumption.
 Qed.
 
-Lemma isType_red Γ t t' :
+Lemma isType_red_sq Γ t t' :
   ∥isType Σ Γ t∥ ->
   ∥red Σ Γ t t'∥ ->
   ∥isType Σ Γ t'∥.
@@ -106,7 +106,7 @@ Proof.
   eapply subject_reduction; eauto.
 Qed.
 
-Hint Resolve isType_red : erase.
+Hint Resolve isType_red_sq : erase.
 
 Lemma isType_prod_dom Γ na A B :
   ∥isType Σ Γ (tProd na A B)∥ ->
@@ -134,59 +134,6 @@ Qed.
 
 Hint Resolve isType_prod_cod : erase.
 
-Lemma isType_isWfArity_or_Type Γ t :
-  ∥isType Σ Γ t∥ ->
-  ∥isWfArity_or_Type Σ Γ t∥.
-Proof.
-  intros [isT].
-  now constructor; right.
-Qed.
-
-Hint Resolve isType_isWfArity_or_Type : erase.
-
-Lemma isWfArity_or_Type_red Γ t t' :
-  ∥isWfArity_or_Type Σ Γ t∥ ->
-  ∥red Σ Γ t t'∥ ->
-  ∥isWfArity_or_Type Σ Γ t'∥.
-Proof.
-  intros.
-  sq.
-  eapply isWfArity_or_Type_red; eauto.
-Qed.
-
-Hint Resolve isWfArity_or_Type_red : erase.
-
-Lemma isWfArity_or_Type_prod_dom Γ na A B :
-  ∥ isWfArity_or_Type Σ Γ (tProd na A B) ∥ ->
-  ∥ isType Σ Γ A ∥.
-Proof.
-  destruct wfΣ as [wfΣu].
-  intros [[ar|isT]].
-  - constructor.
-    apply isWfArity_prod_inv in ar as ((s & ?) & _).
-    now exists s.
-  - pose proof (isType_prod_dom _ _ _ _ (sq isT)).
-    now sq.
-Qed.
-
-Hint Resolve isWfArity_or_Type_prod_dom : erase.
-
-Lemma isWfArity_or_Type_prod_cod Γ na A B :
-  ∥ isWfArity_or_Type Σ Γ (tProd na A B) ∥ ->
-  ∥ isWfArity_or_Type Σ (Γ,, vass na A) B ∥.
-Proof.
-  destruct wfΣ as [wfΣu].
-  intros [[ar|isT]].
-  - constructor; left.
-    apply isWfArity_prod_inv in ar.
-    now destruct ar as ((s & typ) & ar).
-  - pose proof (isType_prod_cod _ _ _ _ (sq isT)).
-    sq.
-    now right.
-Qed.
-
-Hint Resolve isWfArity_or_Type_prod_cod : erase.
-
 Lemma Is_conv_to_Arity_red Γ T T' :
   Is_conv_to_Arity Σ Γ T ->
   ∥ red Σ Γ T T' ∥ ->
@@ -225,13 +172,17 @@ Proof.
   apply Is_conv_to_Arity_inv in car as [(?&?&?&[r'])|(?&[r'])]; auto.
   - eapply red_confluence in r' as (?&r1&r2); eauto.
     apply invert_red_prod in r2 as (?&?&(->&?)&?); auto.
-    apply whnf_red_prod in r1 as (?&?&?); auto.
+    destruct wh as [wh].
+    eapply whnf_red_inv in wh; eauto.
+    depelim wh.
     rewrite H in nar.
     now cbn in nar.
   - eapply red_confluence in r' as (?&r1&r2); eauto.
     apply invert_red_sort in r2 as ->; auto.
-    apply whnf_red_sort in r1; auto.
-    rewrite r1 in nar.
+    destruct wh as [wh].
+    eapply whnf_red_inv in wh; eauto.
+    depelim wh.
+    rewrite H in nar.
     now cbn in nar.
 Qed.
 
@@ -276,7 +227,7 @@ Proof.
     now rewrite decompose_app_rec_mkApps, atom_decompose_app by easy.
 Qed.
 
-Definition erase_rel : Relation_Definitions.relation (∑ Γ t, wellformed Σ Γ t) :=
+Definition erase_rel : Relation_Definitions.relation (∑ Γ t, welltyped Σ Γ t) :=
   fun '(Γs; ts; wfs) '(Γl; tl; wfl) =>
     ∥∑m, red Σ Γl tl m × term_sub_ctx (Γs, ts) (Γl, m)∥.
 
@@ -312,7 +263,7 @@ Lemma well_founded_erase_rel : well_founded erase_rel.
 Proof.
   intros (Γl & l & wfl).
   destruct wfΣ as [wfΣu].
-  induction (normalisation' Σ Γl l wfΣu wfl) as [l _ IH].
+  induction (normalisation Σ Γl l wfl) as [l _ IH].
   remember (Γl, l) as p.
   revert wfl IH.
   replace Γl with (fst p) by (now subst).
@@ -333,7 +284,7 @@ Proof.
       cbn in *.
       unshelve eapply (IH (tProd na y B)).
       3: now repeat econstructor.
-      1: { eapply red_wellformed in wfl; eauto.
+      1: { eapply red_welltyped in wfl; eauto.
            eapply cored_red in cor as [cor].
            constructor.
            now apply red_prod_l. }
@@ -341,7 +292,7 @@ Proof.
     + apply Relation_Properties.clos_rtn1_rt in X0.
       unshelve eapply (IH (tProd na s B)).
       3: now repeat econstructor.
-      1: { eapply red_wellformed in wfl; eauto.
+      1: { eapply red_welltyped in wfl; eauto.
            constructor.
            etransitivity; [exact X0|].
            now apply red1_red. }
@@ -351,8 +302,8 @@ Proof.
       intros eq.
       rewrite eq in *.
       eapply cored_red_trans in X0; eauto.
-      eapply SafeErasureFunction.Acc_no_loop in X0; [easy|].
-      eapply @normalisation'; eauto.
+      eapply ErasureFunction.Acc_no_loop in X0; [easy|].
+      eapply @normalisation; eauto.
   - eapply Relation_Properties.clos_rt_rtn1 in mred; inversion mred; subst.
     + apply (IH' (p.1,, vass na A, s)).
       { replace p with (p.1, tProd na A s) by (destruct p; cbn in *; congruence).
@@ -365,7 +316,7 @@ Proof.
            eexists.
            split; try easy.
            constructor. }
-      1: { eapply red_wellformed; eauto.
+      1: { eapply red_welltyped; eauto.
            eapply cored_red in cor as [cored].
            constructor.
            rewrite H0.
@@ -378,7 +329,7 @@ Proof.
            eexists.
            split; try easy.
            constructor. }
-      1: { eapply red_wellformed; eauto.
+      1: { eapply red_welltyped; eauto.
            constructor.
            etransitivity; [exact X0|].
            now apply red1_red. }
@@ -388,8 +339,8 @@ Proof.
       intros eq.
       rewrite eq in *.
       eapply cored_red_trans in X0; eauto.
-      eapply SafeErasureFunction.Acc_no_loop in X0; [easy|].
-      eapply @normalisation'; eauto.
+      eapply ErasureFunction.Acc_no_loop in X0; [easy|].
+      eapply @normalisation; eauto.
   - eapply Relation_Properties.clos_rt_rtn1 in mred; inversion mred; subst.
     + apply (IH' (p.1, s)).
       { replace p with (p.1, tApp hd arg1) by (destruct p; cbn in *; congruence).
@@ -424,7 +375,7 @@ Proof.
              apply in_or_app; left.
              apply in_or_app; left.
              now apply in_or_app; right; left. }
-      1: { eapply red_wellformed in wfl; eauto.
+      1: { eapply red_welltyped in wfl; eauto.
            eapply cored_red in cor as [cor].
            constructor.
            rewrite H1.
@@ -454,7 +405,7 @@ Proof.
            eexists.
            split; try easy.
            now constructor. }
-      1: { eapply red_wellformed in wfl; eauto.
+      1: { eapply red_welltyped in wfl; eauto.
            constructor.
            etransitivity; [exact X0|].
            now apply red1_red. }
@@ -464,8 +415,8 @@ Proof.
       intros eq.
       rewrite eq in *.
       eapply cored_red_trans in X0; eauto.
-      eapply SafeErasureFunction.Acc_no_loop in X0; [easy|].
-      eapply @normalisation'; eauto.
+      eapply ErasureFunction.Acc_no_loop in X0; [easy|].
+      eapply @normalisation; eauto.
 Qed.
 
 Instance WellFounded_erase_rel : WellFounded erase_rel :=
@@ -484,11 +435,11 @@ fot_viewc (tProd na A B) := fot_view_prod na A B;
 fot_viewc (tSort univ) := fot_view_sort univ;
 fot_viewc t := fot_view_other t _.
 
-Lemma watwf {Γ T} (wat : ∥isWfArity_or_Type Σ Γ T∥) : wellformed Σ Γ T.
-Proof. now apply wat_wellformed. Qed.
+Lemma tywt {Γ T} (isT : ∥isType Σ Γ T∥) : welltyped Σ Γ T.
+Proof. destruct isT. now apply isType_welltyped. Qed.
 
 (* Definition of normalized arities *)
-Definition arity_ass := name * term.
+Definition arity_ass := aname * term.
 
 Fixpoint mkNormalArity (l : list arity_ass) (s : Universe.t) : term :=
   match l with
@@ -632,10 +583,10 @@ Record type_flag {Γ T} :=
 
 Global Arguments type_flag : clear implicits.
 
-Equations(noeqns) flag_of_type (Γ : context) (T : term) (wat : ∥isWfArity_or_Type Σ Γ T∥)
+Equations(noeqns) flag_of_type (Γ : context) (T : term) (isT : ∥isType Σ Γ T∥)
   : type_flag Γ T
-  by wf ((Γ;T; (watwf wat)) : (∑ Γ t, wellformed Σ Γ t)) erase_rel :=
-flag_of_type Γ T wat with inspect (hnf wfΣ Γ T (watwf wat)) :=
+  by wf ((Γ;T; (tywt isT)) : (∑ Γ t, welltyped Σ Γ t)) erase_rel :=
+flag_of_type Γ T isT with inspect (hnf wfΣ Γ T (tywt isT)) :=
   | exist T is_hnf with fot_viewc T := {
     | fot_view_prod na A B with flag_of_type (Γ,, vass na A) B _ := {
       | flag_cod := {| is_logical := is_logical flag_cod;
@@ -700,18 +651,14 @@ Next Obligation.
   now intros [].
 Qed.
 Next Obligation.
-  destruct wat as [[ar|isT]].
-  - apply not_prod_or_sort_hnf in discr.
-    now apply nIs_conv_to_Arity_isWfArity_elim in discr.
-  - destruct isT as [[]].
-    now econstructor.
+  apply tywt; auto.
 Qed.
 Next Obligation.
   destruct princK as [(typK & princK)].
-  apply wat_wellformed; [easy|].
+  destruct isT as [isT].
   destruct wfΣ.
-  sq.
-  eapply validity; [easy|exact typK].
+  eapply isType_welltyped.
+  eapply validity_term; eauto.
 Qed.
 Next Obligation.
   clear eq.
@@ -723,24 +670,13 @@ Next Obligation.
   pose proof (PCUICSafeChecker.reduce_to_sort_complete _ _ (eq_sym eq)).
   clear eq.
   apply not_prod_or_sort_hnf in discr.
-  destruct wat as [[|]].
-  - now apply nIs_conv_to_Arity_isWfArity_elim in discr.
-  - destruct i.
-    red in t0.
-    destruct princK as [(typK & princK)].
-    specialize (princK _ t0).
-    eapply invert_cumul_sort_r in princK as (? & ? & ?).
-    eauto.
+  destruct isT as [(u&typ)].
+  destruct princK as [(typK & princK)].
+  specialize (princK _ typ).
+  eapply invert_cumul_sort_r in princK as (? & ? & ?).
+  eauto.
 Qed.
 
-Definition redβιζ : RedFlags.t :=
-  {| RedFlags.beta := true;
-     RedFlags.iota := true;
-     RedFlags.zeta := true;
-     RedFlags.delta := false;
-     RedFlags.fix_ := true;
-     RedFlags.cofix_ := true |}.
-
 Equations erase_type_discr (t : term) : Prop := {
   | tRel _ := False;
   | tSort _ := False;
@@ -778,13 +714,6 @@ Inductive tRel_kind :=
 (* tRel refers to something else, for example something logical or a value *)
 | RelOther.
 
-Lemma isTwf {Γ t} (isT: ∥isType Σ Γ t∥) :
-  wellformed Σ Γ t.
-Proof.
-  destruct isT.
-  now apply isType_wellformed.
-Qed.
-
 Equations(noeqns) erase_type_aux
           (Γ : context)
           (erΓ : Vector.t tRel_kind #|Γ|)
@@ -797,9 +726,9 @@ Equations(noeqns) erase_type_aux
              while in (Type -> nat) -> nat we should erase to (TBox ->
              nat) -> nat with no type vars. *)
           (next_tvar : option nat) : list name × box_type
-  by wf ((Γ; t; (isTwf isT)) : (∑ Γ t, wellformed Σ Γ t)) erase_rel :=
+  by wf ((Γ; t; (tywt isT)) : (∑ Γ t, welltyped Σ Γ t)) erase_rel :=
 erase_type_aux Γ erΓ t isT next_tvar
-  with inspect (reduce_term redβιζ Σ wfΣ Γ t (isTwf isT)) :=
+  with inspect (reduce_term RedFlags.nodelta Σ wfΣ Γ t (tywt isT)) :=
 
   | exist t eq_hnf with is_logical (flag_of_type Γ t _) := {
 
@@ -850,7 +779,7 @@ erase_type_aux Γ erΓ t isT next_tvar
                 (Γ,, vass na A) (var :: erΓ)%vector
                 B _
                 (option_map S next_tvar) in
-          (if next_tvar then na :: tvars else tvars, TArr TBox cod)
+          (if next_tvar then binder_name na :: tvars else tvars, TArr TBox cod)
         };
 
       | et_view_app orig_hd orig_arg with inspect (decompose_app (tApp orig_hd orig_arg)) := {
@@ -971,13 +900,12 @@ Qed.
 Definition erase_type (t : term) (isT : ∥isType Σ [] t∥) : list name × box_type :=
   erase_type_aux [] []%vector t isT (Some 0).
 
-Lemma typwf {Γ t T} :
+Lemma typwt {Γ t T} :
   ∥Σ;;; Γ |- t : T∥ ->
-  wellformed Σ Γ t.
+  welltyped Σ Γ t.
 Proof.
   intros [typ].
-  left.
-  now econstructor.
+  econstructor; eauto.
 Qed.
 
 Inductive erase_type_scheme_view : term -> Type :=
@@ -988,8 +916,8 @@ Equations erase_type_scheme_viewc (t : term) : erase_type_scheme_view t :=
 erase_type_scheme_viewc (tLambda na A B) := erase_type_scheme_view_lam na A B;
 erase_type_scheme_viewc t := erase_type_scheme_view_other t _.
 
-Definition type_var_info_of_flag (na : name) {Γ t} (f : type_flag Γ t) : type_var_info :=
-  {| tvar_name := na;
+Definition type_var_info_of_flag (na : aname) {Γ t} (f : type_flag Γ t) : type_var_info :=
+  {| tvar_name := binder_name na;
      tvar_is_logical := is_logical f;
      tvar_is_arity := if is_arity (conv_ar f) then true else false;
      tvar_is_sort := if is_sort (conv_ar f) then true else false; |}.
@@ -1029,17 +957,16 @@ Proof.
     destruct wfΣ.
     assert (wf_local Σ Γ) by (eapply typing_wf_local; eauto).
     apply validity in typ; auto.
-    apply isWAT_tProd in typ; auto.
-    constructor.
-    now right.
+    apply isType_tProd in typ; auto.
+    now constructor.
   - clear inf.
     destruct wfΣ.
     destruct typ as [typ].
     apply typing_wf_local in typ as wfl.
     assert (wflext: wf_local Σ (Γ,, vass na A)).
     { apply validity in typ; auto.
-      apply isWAT_tProd in typ as (_ & typ); auto.
-      eapply isWAT_wf_local; eauto. }
+      apply isType_tProd in typ as (_ & typ); auto.
+      eapply isType_wf_local; eauto. }
     constructor.
     rewrite <- (PCUICSpine.subst_rel0_lift_id 0 (mkNormalArity ar_ctx univ)).
     eapply type_App.
@@ -1058,7 +985,7 @@ Equations? (noeqns) erase_type_scheme
           (next_tvar : nat) : list type_var_info × box_type :=
 erase_type_scheme Γ erΓ t [] univ typ next_tvar => ([], (erase_type_aux Γ erΓ t _ None).2);
 erase_type_scheme Γ erΓ t ((na', A') :: ar_ctx) univ typ next_tvar
-  with inspect (reduce_term redβιζ Σ wfΣ Γ t (typwf typ)) := {
+  with inspect (reduce_term RedFlags.nodelta Σ wfΣ Γ t (typwt typ)) := {
   | exist thnf eq_hnf with erase_type_scheme_viewc thnf := {
     | erase_type_scheme_view_lam na A body =>
       let inf := type_var_info_of_flag na (flag_of_type Γ A _) in
@@ -1084,7 +1011,6 @@ Proof.
     eapply subject_reduction in r; eauto.
     apply inversion_Lambda in r as (?&?&?&?&?); auto.
     constructor.
-    right.
     eexists; eassumption.
   - clear inf.
     destruct typ as [typ].
@@ -1093,11 +1019,11 @@ Proof.
     eapply subject_reduction in r; eauto.
     apply inversion_Lambda in r as (?&?&?&?&?); auto.
     assert (wf_local Σ Γ) by (eapply typing_wf_local; eauto).
-    apply cumul_Prod_inv_l in c as (?&?); auto.
+    apply cumul_Prod_inv_l in c as ((?&?)&?); auto.
     constructor.
     clear eq_hnf.
-    eapply validity in typ; auto.
-    apply isWAT_tProd in typ as (_ & typ); auto.
+    eapply validity in typ as typ; auto.
+    apply isType_tProd in typ as (_ & (u&?)); auto.
     assert (conv_context Σ (Γ,, vass na A) (Γ,, vass na' A')).
     { constructor; [reflexivity|].
       constructor; assumption. }
@@ -1106,7 +1032,7 @@ Proof.
     2: now apply conv_context_sym; eauto.
     eapply type_Cumul.
     + eapply context_conversion; eauto.
-      eapply isWAT_wf_local; eassumption.
+      eapply typing_wf_local; eassumption.
     + eassumption.
     + now eapply cumul_conv_ctx; eauto.
 Qed.
@@ -1126,7 +1052,7 @@ erase_constant_decl cst wt with flag_of_type [] (P.cst_type cst) _ := {
     inl {| cst_type := erase_type (P.cst_type cst) _; cst_body := erased_body |}
     where erased_body : option term := {
     erased_body with inspect (P.cst_body cst) := {
-      | exist (Some body) body_eq => Some (SafeErasureFunction.erase Σ wfextΣ [] body _);
+      | exist (Some body) body_eq => Some (ErasureFunction.erase Σ wfextΣ [] body _);
       | exist None _ => None
       }
     }
@@ -1134,13 +1060,10 @@ erase_constant_decl cst wt with flag_of_type [] (P.cst_type cst) _ := {
 Proof.
   - sq.
     unfold on_constant_decl in wt.
-    destruct (P.cst_body cst).
-    + cbn in wt.
-      eapply validity_term; [easy|exact wt].
-    + cbn in wt.
-      destruct wt as (s & ?).
-      right.
-      now exists s.
+    destruct (P.cst_body cst); cbn in *.
+    + eapply validity_term; [easy|exact wt].
+    + destruct wt.
+      eexists; eassumption.
   - unfold on_constant_decl in wt.
     rewrite <- body_eq in wt.
     cbn in *.
@@ -1160,13 +1083,7 @@ Proof.
     destruct wfΣ.
     unfold on_constant_decl in wt.
     destruct (P.cst_body cst).
-    + eapply validity_term in wt; [|now eauto].
-      destruct wt.
-      * apply nIs_conv_to_Arity_isWfArity_elim in i; [easy|].
-        intros conv.
-        apply Is_conv_to_Arity_conv_arity in conv.
-        tauto.
-      * now constructor.
+    + now eapply validity_term in wt; [|now eauto].
     + cbn in wt.
       destruct wt as (s & ?).
       constructor.
@@ -1178,9 +1095,9 @@ Import P.
 Equations? (noeqns) erase_ind_arity
           (Γ : context)
           (t : term)
-          (wat : ∥isWfArity_or_Type Σ Γ t∥) : list type_var_info
-  by wf ((Γ; t; watwf wat) : (∑ Γ t, wellformed Σ Γ t)) erase_rel :=
-erase_ind_arity Γ t wat with inspect (hnf wfΣ Γ t (watwf wat)) := {
+          (isT : ∥isType Σ Γ t∥) : list type_var_info
+  by wf ((Γ; t; tywt isT) : (∑ Γ t, welltyped Σ Γ t)) erase_rel :=
+erase_ind_arity Γ t isT with inspect (hnf wfΣ Γ t (tywt isT)) := {
   | exist (tProd na A B) hnf_eq =>
     let hd := type_var_info_of_flag na (flag_of_type Γ A _) in
     let tl := erase_ind_arity (Γ,, vass na A) B _ in
@@ -1191,6 +1108,10 @@ Proof.
   all: reduce_term_sound; eauto with erase.
 Qed.
 
+Definition ind_aname (oib : P.one_inductive_body) :=
+  {| binder_name := nNamed (P.ind_name oib);
+     binder_relevance := P.ind_relevance oib |}.
+
 Definition arities_contexts
          (mind : kername)
          (oibs : list P.one_inductive_body) : ∑Γ, Vector.t tRel_kind #|Γ| :=
@@ -1202,14 +1123,14 @@ Definition arities_contexts
     | oib :: oibs =>
       f oibs
         (S i)
-        (Γ,, vass (nNamed (P.ind_name oib)) (P.ind_type oib))
+        (Γ,, vass (ind_aname oib) (P.ind_type oib))
         (RelInductive {| inductive_mind := mind;
                          inductive_ind := i |} :: erΓ)%vector
     end) oibs 0 [] []%vector.
 
 Lemma arities_contexts_cons_1 mind oib oibs :
   (arities_contexts mind (oib :: oibs)).π1 =
-  (arities_contexts mind oibs).π1 ++ [vass (nNamed (P.ind_name oib)) (P.ind_type oib)].
+  (arities_contexts mind oibs).π1 ++ [vass (ind_aname oib) (P.ind_type oib)].
 Proof.
   unfold arities_contexts.
   match goal with
@@ -1258,7 +1179,7 @@ Equations? (noeqns) erase_ind_ctor
 erase_ind_ctor Γ erΓ t isT next_par [] := (erase_type_aux Γ erΓ t isT None).2;
 
 erase_ind_ctor Γ erΓ t isT next_par (tvar :: tvars)
-  with inspect (reduce_term redβιζ Σ wfΣ Γ t (isTwf isT)) :=
+  with inspect (reduce_term RedFlags.nodelta Σ wfΣ Γ t (tywt isT)) :=
   | exist t eq_red with view_prodc t := {
     | view_prod_prod na A B =>
       let rel_kind := if tvar_is_arity tvar then RelTypeVar next_par else RelOther in
@@ -1279,7 +1200,7 @@ Proof.
   unshelve refine (
   let is_propositional :=
       match destArity [] (ind_type oib) with
-      | Some (_, u) => Universe.is_prop u
+      | Some (_, u) => is_propositional u
       | None => false
       end in
   let oib_tvars := erase_ind_arity [] (P.ind_type oib) _ in
@@ -1310,7 +1231,6 @@ Proof.
   - abstract (
         destruct wt as [wt];
         sq;
-        right;
         exact (onArity wt.π2)).
   - abstract (
         destruct p as ((?&?)&?);
diff --git a/extraction/theories/ErasureCorrectness.v b/extraction/theories/ErasureCorrectness.v
index e238182c..c34a987e 100644
--- a/extraction/theories/ErasureCorrectness.v
+++ b/extraction/theories/ErasureCorrectness.v
@@ -15,7 +15,7 @@ From MetaCoq.Erasure Require Import ErasureFunction.
 From MetaCoq.Erasure Require Import ESubstitution.
 From MetaCoq.Erasure Require Import EWcbvEval.
 From MetaCoq.Erasure Require Import Extract.
-From MetaCoq.Erasure Require Import SafeErasureFunction.
+From MetaCoq.Erasure Require Import ErasureFunction.
 From MetaCoq.PCUIC Require Import PCUICAstUtils.
 From MetaCoq.PCUIC Require Import PCUICInduction.
 From MetaCoq.PCUIC Require Import PCUICInversion.
@@ -96,7 +96,7 @@ Proof.
   apply erase_ind_body_correct.
 Qed.
 
-Opaque erase_type flag_of_type SafeErasureFunction.wf_reduction.
+Opaque erase_type flag_of_type ErasureFunction.wf_reduction.
 Lemma erase_global_decls_deps_recursive_correct Σ wfΣ include ignore_deps :
   (forall k, ignore_deps k = false) ->
   (forall k, KernameSet.In k include -> PCUICAst.lookup_env Σ k <> None) ->
diff --git a/extraction/theories/ExtractExtraction.v b/extraction/theories/ExtractExtraction.v
index 0f8cc41b..a9d74eed 100644
--- a/extraction/theories/ExtractExtraction.v
+++ b/extraction/theories/ExtractExtraction.v
@@ -29,7 +29,7 @@ Extraction Inline Equations.Init.pr2.
 Extraction Inline Equations.Init.hidebody.
 Extraction Inline Equations.Prop.DepElim.solution_left.
 
-Extract Inductive Equations.Init.sigma => "(*)" ["(,)"].
+Extract Inductive Equations.Init.sigma => "( * )" ["(,)"].
 Extract Constant PCUICTyping.fix_guard => "(fun x -> true)".
 Extract Constant PCUICTyping.cofix_guard => "(fun x -> true)".
 Extract Constant PCUICTyping.ind_guard => "(fun x -> true)".
@@ -42,10 +42,8 @@ Extract Constant timed =>
    Feedback.msg_debug (Pp.str (Printf.sprintf ""%s executed in: %fs"" ((fun s-> (String.concat """" (List.map (String.make 1) s))) c) time));
               temp)".
 
-
-
 Cd "plugin/src".
 Separate Extraction RustExtract.extract
          (* The following directives ensure separate extraction does not produce name clashes *)
-         Coq.Strings.String Common utils ELiftSubst ETyping.
+         Bool Nat Coq.Strings.String Common utils ELiftSubst ETyping.
 Cd "../..".
diff --git a/extraction/theories/Extraction.v b/extraction/theories/Extraction.v
index ad286131..a99d0871 100644
--- a/extraction/theories/Extraction.v
+++ b/extraction/theories/Extraction.v
@@ -13,21 +13,26 @@ From ConCert.Extraction Require Import Utils.
 From Coq Require Import List.
 From Coq Require Import String.
 From MetaCoq.Erasure Require Import ELiftSubst.
-From MetaCoq.Erasure Require Import SafeErasureFunction.
+From MetaCoq.Erasure Require Import ErasureFunction.
 From MetaCoq.Template Require Import BasicAst.
 From MetaCoq.Template Require Import Kernames.
 From MetaCoq.Template Require Import Loader.
+From MetaCoq.Template Require Import config.
 From MetaCoq.Template Require Import monad_utils.
 From MetaCoq.Template Require Import utils.
 From MetaCoq.PCUIC Require Import PCUICAst.
 From MetaCoq.PCUIC Require Import PCUICSafeLemmata.
 From MetaCoq.PCUIC Require Import PCUICTyping.
+From MetaCoq.PCUIC Require Import TemplateToPCUIC.
 From MetaCoq.SafeChecker Require Import PCUICSafeChecker.
+From MetaCoq.SafeChecker Require Import SafeTemplateChecker.
 
 Local Open Scope bool.
 Local Open Scope string.
 Import MonadNotation.
 
+Existing Instance extraction_checker_flags.
+
 Record extract_pcuic_params :=
   { (* Whether to remove discrimination (matches and projections) on things in Prop.
      Necessary to run the transforms. *)
@@ -37,7 +42,7 @@ Record extract_pcuic_params :=
 
 Definition extract_pcuic_env
            (params : extract_pcuic_params)
-           (Σ : P.global_env) (wfΣ : ∥PT.wf Σ∥)
+           (Σ : P.global_env) (wfΣ : ∥wf Σ∥)
            (seeds : KernameSet.t)
            (ignore : kername -> bool) : result ExAst.global_env string :=
 
@@ -51,16 +56,16 @@ Definition extract_pcuic_env
 
 Record extract_template_env_params :=
   { (* Function to use to check wellformedness of the environment *)
-    check_wf_env_func : forall Σ, result (∥PT.wf Σ∥) string;
+    check_wf_env_func : forall Σ, result (∥wf Σ∥) string;
     pcuic_args : extract_pcuic_params }.
 
 Definition extract_template_env
            (params : extract_template_env_params)
-           (Σ : T.global_env)
+           (Σ : Ast.global_env)
            (seeds : KernameSet.t)
            (ignore : kername -> bool) : result ExAst.global_env string :=
   let Σ := SafeTemplateChecker.fix_global_env_universes Σ in
-  let Σ := T2P.trans_global_decls Σ in
+  let Σ := trans_global_decls Σ in
   wfΣ <- check_wf_env_func params Σ;;
   extract_pcuic_env (pcuic_args params) Σ wfΣ seeds ignore.
 
@@ -68,7 +73,7 @@ Definition extract_template_env
    To work around this we assume environments are well formed when extracting
    from within Coq. This is justified since our environments are produced by quoting
    and thus come directly from Coq, where they have already been type checked. *)
-Axiom assume_env_wellformed : forall Σ, ∥PT.wf Σ∥.
+Axiom assume_env_wellformed : forall Σ, ∥wf Σ∥.
 
 (* Extract an environment with some minimal checks. This assumes the environment
    is well-formed (to make it computable from within Coq) but furthermore checks that the
diff --git a/extraction/theories/ExtractionCorrectness.v b/extraction/theories/ExtractionCorrectness.v
index bf06a035..d65d7d4b 100644
--- a/extraction/theories/ExtractionCorrectness.v
+++ b/extraction/theories/ExtractionCorrectness.v
@@ -14,7 +14,7 @@ From Coq Require Import List.
 From Coq Require Import String.
 From Equations Require Import Equations.
 From MetaCoq.Erasure Require Import ErasureCorrectness.
-From MetaCoq.Erasure Require Import SafeErasureFunction.
+From MetaCoq.Erasure Require Import ErasureFunction.
 From MetaCoq.Erasure Require Import EWcbvEval.
 From MetaCoq.Erasure Require Import Extract.
 From MetaCoq.Erasure Require Import Prelim.
diff --git a/extraction/theories/LiquidityExtract.v b/extraction/theories/LiquidityExtract.v
index 183a26f6..d38b273d 100644
--- a/extraction/theories/LiquidityExtract.v
+++ b/extraction/theories/LiquidityExtract.v
@@ -1,9 +1,7 @@
 From Coq Require Import PeanoNat ZArith.
 
 From MetaCoq.Template Require Import Loader.
-From MetaCoq.Erasure Require Import SafeTemplateErasure.
 From MetaCoq.Erasure Require ErasureFunction.
-From MetaCoq.Erasure Require SafeErasureFunction.
 From MetaCoq.Template Require Import Kernames config.
 From MetaCoq.SafeChecker Require Import PCUICSafeReduce PCUICSafeChecker
      SafeTemplateChecker.
@@ -31,7 +29,7 @@ Import AcornBlockchain.
 Import MonadNotation.
 Import ResultMonad.
 
-Definition to_constant_decl (gd : option T.global_decl) :=
+Definition to_constant_decl (gd : option Ast.global_decl) :=
   match gd with
   | Some (ConstantDecl cst_body) => ret cst_body
   | Some (InductiveDecl cst_body) => tmFail "Error (constant expected, given inductive)"
diff --git a/extraction/theories/MidlangExtract.v b/extraction/theories/MidlangExtract.v
index ec1bb4ef..95fe66d9 100644
--- a/extraction/theories/MidlangExtract.v
+++ b/extraction/theories/MidlangExtract.v
@@ -20,7 +20,7 @@ From Coq Require Import ZArith.
 
 From MetaCoq.SafeChecker Require Import PCUICSafeChecker SafeTemplateChecker.
 From MetaCoq.Template Require Import All.
-From MetaCoq.Erasure Require Import Loader SafeTemplateErasure EAst EAstUtils ETyping.
+From MetaCoq.Erasure Require Import Loader EAst EAstUtils ETyping.
 
 Import StringExtra.
 Import String.
@@ -31,7 +31,7 @@ Module T2P := MetaCoq.PCUIC.TemplateToPCUIC.
 Module E := MetaCoq.Erasure.EAst.
 Module T := MetaCoq.Template.Ast.
 Module TUtil := MetaCoq.Template.AstUtils.
-Module EF := MetaCoq.Erasure.SafeErasureFunction.
+Module EF := MetaCoq.Erasure.ErasureFunction.
 Module Ex := ConCert.Extraction.ExAst.
 
 Import PrettyPrinterMonad.
diff --git a/extraction/theories/Optimize.v b/extraction/theories/Optimize.v
index ff3ed437..905c2694 100644
--- a/extraction/theories/Optimize.v
+++ b/extraction/theories/Optimize.v
@@ -21,7 +21,7 @@ From MetaCoq.Erasure Require Import ELiftSubst.
 From MetaCoq.Erasure Require Import Extract.
 From MetaCoq.Erasure Require Import EWcbvEval.
 From MetaCoq.Erasure Require Import Prelim.
-From MetaCoq.Erasure Require SafeErasureFunction.
+From MetaCoq.Erasure Require ErasureFunction.
 From MetaCoq.Template Require Import config.
 From MetaCoq.Template Require Import monad_utils.
 From MetaCoq.Template Require Import utils.
diff --git a/extraction/theories/OptimizeCorrectness.v b/extraction/theories/OptimizeCorrectness.v
index aa996077..ae4f0382 100644
--- a/extraction/theories/OptimizeCorrectness.v
+++ b/extraction/theories/OptimizeCorrectness.v
@@ -2784,11 +2784,11 @@ Proof.
         apply filter_length.
 Qed.
 
-Lemma is_propositional_trans_env_dearg_env Σ ind :
-  is_propositional (trans_env (dearg_env Σ)) ind =
-  is_propositional (trans_env Σ) ind.
+Lemma is_propositional_ind_trans_env_dearg_env Σ ind :
+  is_propositional_ind (trans_env (dearg_env Σ)) ind =
+  is_propositional_ind (trans_env Σ) ind.
 Proof.
-  unfold is_propositional.
+  unfold is_propositional_ind.
   rewrite !lookup_env_trans_env, lookup_env_dearg_env.
   destruct lookup_env; cbn in *; [|reflexivity].
   destruct g; cbn in *; auto.
@@ -2933,7 +2933,7 @@ Proof.
         rewrite dearg_mkApps in *.
         cbn in *.
         now rewrite dearg_single_masked in * by (now rewrite map_length).
-      * rewrite is_propositional_trans_env_dearg_env; eauto.
+      * rewrite is_propositional_ind_trans_env_dearg_env; eauto.
       * destruct (get_mib_masks _) eqn:mm; cycle 1.
         { cbn in *.
           unfold get_ctor_mask.
@@ -3038,7 +3038,7 @@ Proof.
       * eauto.
       * unshelve eapply (IH _ tBox); eauto.
         lia.
-      * rewrite is_propositional_trans_env_dearg_env; eauto.
+      * rewrite is_propositional_ind_trans_env_dearg_env; eauto.
       * destruct (get_mib_masks _); cbn in *; [easy|].
         now rewrite dearg_lambdas_nil, Nat.sub_0_r.
       * replace (repeat tBox _) with (masked branch_mask (repeat tBox n)); cycle 1.
@@ -3164,7 +3164,7 @@ Proof.
         rewrite dearg_mkApps in *.
         cbn in *.
         now rewrite dearg_single_masked in * by (now rewrite map_length).
-      * rewrite is_propositional_trans_env_dearg_env; eauto.
+      * rewrite is_propositional_ind_trans_env_dearg_env; eauto.
       * clear clos_constr valid_constr.
         unfold get_ctor_mask in *.
         revert ev2 deriv_len.
@@ -3211,7 +3211,7 @@ Proof.
       * eauto.
       * unshelve eapply (IH _ _ _ _ _ ev _); auto.
         lia.
-      * rewrite is_propositional_trans_env_dearg_env; eauto.
+      * rewrite is_propositional_ind_trans_env_dearg_env; eauto.
     + congruence.
 
   - facts.
@@ -3256,11 +3256,11 @@ Proof.
   apply IH.
 Qed.
 
-Lemma is_propositional_trans_env_debox_env_types Σ ind :
-  is_propositional (trans_env (debox_env_types Σ)) ind =
-  is_propositional (trans_env Σ) ind.
+Lemma is_propositional_ind_trans_env_debox_env_types Σ ind :
+  is_propositional_ind (trans_env (debox_env_types Σ)) ind =
+  is_propositional_ind (trans_env Σ) ind.
 Proof.
-  unfold is_propositional.
+  unfold is_propositional_ind.
   rewrite !lookup_env_trans_env, lookup_env_debox_env_types.
   destruct lookup_env; cbn in *; [|reflexivity].
   destruct g; cbn in *; auto.
@@ -3274,9 +3274,9 @@ Lemma eval_debox_env_types {wfl:WcbvFlags} Σ t v :
 Proof.
   induction 1; try solve [econstructor; eauto].
   - eapply eval_iota; eauto.
-    now rewrite is_propositional_trans_env_debox_env_types.
+    now rewrite is_propositional_ind_trans_env_debox_env_types.
   - eapply eval_iota_sing; eauto.
-    now rewrite is_propositional_trans_env_debox_env_types.
+    now rewrite is_propositional_ind_trans_env_debox_env_types.
   - eapply eval_delta; eauto.
     unfold declared_constant in *.
     rewrite !lookup_env_trans_env, lookup_env_debox_env_types in *.
@@ -3284,9 +3284,9 @@ Proof.
     destruct g; cbn in *; auto.
     congruence.
   - eapply eval_proj; eauto.
-    now rewrite is_propositional_trans_env_debox_env_types.
+    now rewrite is_propositional_ind_trans_env_debox_env_types.
   - eapply eval_proj_prop; eauto.
-    now rewrite is_propositional_trans_env_debox_env_types.
+    now rewrite is_propositional_ind_trans_env_debox_env_types.
 Qed.
 
 Lemma eval_const_construct_expanded {wfl:WcbvFlags} Σ kn ind c im cm :
diff --git a/extraction/theories/RustExtract.v b/extraction/theories/RustExtract.v
index 5f06157d..e844839a 100644
--- a/extraction/theories/RustExtract.v
+++ b/extraction/theories/RustExtract.v
@@ -23,7 +23,7 @@ From Coq Require Import ZArith.
 
 From MetaCoq.SafeChecker Require Import PCUICSafeChecker SafeTemplateChecker.
 From MetaCoq.Template Require Import Kernames All.
-From MetaCoq.Erasure Require Import Loader SafeTemplateErasure EAst EAstUtils ELiftSubst ETyping.
+From MetaCoq.Erasure Require Import Loader EAst EAstUtils ELiftSubst ETyping.
 
 Import StringExtra.
 Import String.
@@ -35,7 +35,7 @@ Module T2P := MetaCoq.PCUIC.TemplateToPCUIC.
 Module E := MetaCoq.Erasure.EAst.
 Module T := MetaCoq.Template.Ast.
 Module TUtil := MetaCoq.Template.AstUtils.
-Module EF := MetaCoq.Erasure.SafeErasureFunction.
+Module EF := MetaCoq.Erasure.ErasureFunction.
 Module Ex := ConCert.Extraction.ExAst.
 
 Import PrettyPrinterMonad.
diff --git a/extraction/theories/SpecializeChainBase.v b/extraction/theories/SpecializeChainBase.v
index 9e5fcb26..014db60a 100644
--- a/extraction/theories/SpecializeChainBase.v
+++ b/extraction/theories/SpecializeChainBase.v
@@ -21,11 +21,11 @@ From ConCert.Extraction Require Import Common.
 From ConCert.Extraction Require Import ResultMonad.
 From Coq Require Import List.
 From Coq Require Import String.
+From MetaCoq.PCUIC Require Import PCUICAst.
+From MetaCoq.PCUIC Require Import PCUICAstUtils.
 From MetaCoq.Template Require Import BasicAst.
-From MetaCoq.Template Require Import Loader.
 From MetaCoq.Template Require Import monad_utils.
 From MetaCoq.Template Require Import utils.
-From MetaCoq.PCUIC Require Import PCUICAst.
 
 Import MonadNotation.
 Local Open Scope string.
@@ -148,7 +148,7 @@ Section ChainBaseSpecialization.
       map_error (fun s => "While specializing body in " ++ string_of_kername name ++ ": " ++ s)
                 (specialize_term specialized (replace :: Γ) body)
 
-    | true, _ => Err ("Expected lambda in " ++ string_of_kername name ++ ", got" ++ nl ++ PUtil.string_of_term t)
+    | true, _ => Err ("Expected lambda in " ++ string_of_kername name ++ ", got" ++ nl ++ string_of_term t)
     | false, _ => specialize_term specialized Γ t
     end.
 
@@ -163,7 +163,7 @@ Section ChainBaseSpecialization.
       map_error (fun s => "While specializing type in " ++ string_of_kername name ++ ": " ++ s)
                 (specialize_term specialized (replace :: Γ) body)
 
-    | true, _ => Err ("Expected product in " ++ string_of_kername name ++ ", got" ++ nl ++ PUtil.string_of_term t)
+    | true, _ => Err ("Expected product in " ++ string_of_kername name ++ ", got" ++ nl ++ string_of_term t)
     | false, _ => specialize_term specialized Γ t
     end.
 
@@ -246,10 +246,11 @@ Section ChainBaseSpecialization.
                       (ind_projs oib);;
           ret
             {| ind_name := ind_name oib;
-                ind_type := type;
-                ind_kelim := ind_kelim oib;
-                ind_ctors := ctors;
-                ind_projs := projs; |} in
+               ind_type := type;
+               ind_kelim := ind_kelim oib;
+               ind_ctors := ctors;
+               ind_projs := projs;
+               ind_relevance := ind_relevance oib |} in
       bodies <- monad_map go (ind_bodies mib);;
       ret (if remove then kn :: specialized else specialized,
             InductiveDecl
diff --git a/extraction/theories/TypeAnnotations.v b/extraction/theories/TypeAnnotations.v
index bbbbd727..24d01eb1 100644
--- a/extraction/theories/TypeAnnotations.v
+++ b/extraction/theories/TypeAnnotations.v
@@ -12,7 +12,7 @@ From Coq Require Import VectorDef.
 From Equations Require Import Equations.
 From MetaCoq.Erasure Require Import EArities.
 From MetaCoq.Erasure Require Import Extract.
-From MetaCoq.Erasure Require SafeErasureFunction.
+From MetaCoq.Erasure Require ErasureFunction.
 From MetaCoq.PCUIC Require Import PCUICAst.
 From MetaCoq.PCUIC Require Import PCUICInversion.
 From MetaCoq.PCUIC Require Import PCUICLiftSubst.
@@ -98,12 +98,7 @@ Next Obligation.
   destruct infer as (ty & [(typ & ?)]).
   cbn in *.
   destruct wfΣ.
-  eapply validity_term in typ; eauto.
-  destruct typ.
-  - apply nIs_conv_to_Arity_isWfArity_elim in i; [easy|].
-    intros conv.
-    now apply Is_conv_to_Arity_conv_arity in conv.
-  - now constructor.
+  eapply validity_term in typ; eauto using sq.
 Qed.
 
 Equations? (noeqns) annotate_types
@@ -215,7 +210,7 @@ Proof.
   - destruct cst; cbn.
     destruct cst_body; [|exact tt].
     cbn.
-    apply (annotate_types [] t); [|apply SafeErasureFunction.erases_erase].
+    apply (annotate_types [] t); [|apply ErasureFunction.erases_erase].
     cbn in *.
     destruct wt.
     econstructor; eauto.
@@ -482,7 +477,7 @@ Module AnnotOptimizePropDiscr.
     - assert (br_annots : bigprod (fun br => annots box_type br.2) (map (on_snd (optimize Σ)) l)).
       { refine (bigprod_map _ a.2.2).
         intros ? a'; apply (f _ a'). }
-      destruct ETyping.is_propositional as [[]|]; cbn.
+      destruct ETyping.is_propositional_ind as [[]|]; cbn.
       2-3: exact (a.1, (f _ a.2.1, br_annots)).
       destruct map as [|(?&?) []]; cbn in *.
       1,3: exact (a.1, (f _ a.2.1, br_annots)).
@@ -506,7 +501,7 @@ Module AnnotOptimizePropDiscr.
             | TArr dom cod => (cod, (hda, cod))
             | t => (t, (hda, t))
             end).
-    - destruct ETyping.is_propositional as [[]|].
+    - destruct ETyping.is_propositional_ind as [[]|].
       2-3: exact (a.1, f _ a.2).
       exact a.1.
     - refine (a.1, bigprod_map _ a.2).