diff --git a/erasure/theories/ErasureFunction.v b/erasure/theories/ErasureFunction.v
index 7d8ceae05..69e7e365f 100644
--- a/erasure/theories/ErasureFunction.v
+++ b/erasure/theories/ErasureFunction.v
@@ -793,8 +793,8 @@ Proof.
   assert (hl : Hlookup X_type X X_type' X').
   { red. intros. specialize (ext _ _ H H0) as [[?] ?].
     split. intros.
-    rewrite -(abstract_env_lookup_correct _ _ H).
-    rewrite -(abstract_env_lookup_correct _ _ H0).
+    rewrite -(abstract_env_lookup_correct' _ _ H).
+    rewrite -(abstract_env_lookup_correct' _ _ H0).
     rewrite H2 H3. pose proof (abstract_env_ext_wf _ H) as [?].
     eapply extends_lookup_env in H3; try apply e; eauto. clear -H2 H3. congruence.
     destruct X0. intros tag.
diff --git a/safechecker/theories/PCUICSafeConversion.v b/safechecker/theories/PCUICSafeConversion.v
index cc1327a3b..6dd6d3e67 100644
--- a/safechecker/theories/PCUICSafeConversion.v
+++ b/safechecker/theories/PCUICSafeConversion.v
@@ -1537,8 +1537,8 @@ Qed.
   exfalso;
   Tactics.program_simplify;
   CoreTactics.equations_simpl;
-  try erewrite <- abstract_env_lookup_correct in eq1; eauto ;
-  try erewrite <- abstract_env_lookup_correct in eq2; eauto ;
+  try erewrite <- abstract_env_lookup_correct' in eq1; eauto ;
+  try erewrite <- abstract_env_lookup_correct' in eq2; eauto ;
   try clear aux; specialize_Σ wfΣ;
   try solve
       [match goal with
@@ -1554,8 +1554,8 @@ Qed.
   exfalso;
   Tactics.program_simplify;
   CoreTactics.equations_simpl;
-  try erewrite <- abstract_env_lookup_correct in eq1; eauto ;
-  try erewrite <- abstract_env_lookup_correct in eq2; eauto ;
+  try erewrite <- abstract_env_lookup_correct' in eq1; eauto ;
+  try erewrite <- abstract_env_lookup_correct' in eq2; eauto ;
   try clear aux; specialize_Σ wfΣ;
   solve
       [match goal with
@@ -1573,13 +1573,13 @@ Qed.
     sq.
     eapply red_welltyped; try eapply h2; eauto.
     eapply red_zipc.
-    eapply red_const. erewrite abstract_env_lookup_correct; eauto.
+    eapply red_const. erewrite abstract_env_lookup_correct'; eauto.
   Qed.
   Next Obligation.
     unshelve eapply R_cored2.
     all: try reflexivity.
     simpl. intros. eapply cored_zipc.
-    eapply cored_const. erewrite abstract_env_lookup_correct; eassumption.
+    eapply cored_const. erewrite abstract_env_lookup_correct'; eassumption.
   Qed.
   Next Obligation.
     rename H into wfΣ; destruct (hΣ _ wfΣ).
@@ -1591,7 +1591,7 @@ Qed.
       eapply welltyped_is_open_term in h2.
       sq. now rewrite (All2_fold_length hx).
     * eapply into_closed_red; fvs.
-      + eapply red_const. erewrite abstract_env_lookup_correct; eauto.
+      + eapply red_const. erewrite abstract_env_lookup_correct'; eauto.
       + red in h. sq. fvs.
    Unshelve. eauto.
   Qed.
@@ -1606,7 +1606,7 @@ Qed.
     * clear aux; eapply welltyped_zipc_zipp in h2; eauto.
       eapply welltyped_is_open_term in h2. sq. now rewrite (All2_fold_length hx).
     * eapply into_closed_red; fvs.
-      + eapply red_const. erewrite abstract_env_lookup_correct; eauto.
+      + eapply red_const. erewrite abstract_env_lookup_correct'; eauto.
       + sq. fvs.
   Unshelve. eauto.
   Qed.
@@ -1614,11 +1614,11 @@ Qed.
     pose proof (hΣ _ wfΣ). sq.
     eapply red_welltyped ; [eauto|exact (h1 _ wfΣ)|..].
     eapply red_zipc.
-    eapply red_const. erewrite abstract_env_lookup_correct; eauto.
+    eapply red_const. erewrite abstract_env_lookup_correct'; eauto.
   Qed.
   Next Obligation.
     eapply R_cored. simpl. intros. eapply cored_zipc.
-    eapply cored_const. erewrite abstract_env_lookup_correct; eauto.
+    eapply cored_const. erewrite abstract_env_lookup_correct'; eauto.
   Qed.
   Next Obligation.
     rename H into wfΣ. destruct (heΣ _ wfΣ) as [wΣ].
@@ -1627,7 +1627,7 @@ Qed.
     eapply closed_red_zipp.
     { eapply welltyped_zipc_zipp in h1; auto; fvs. }
     eapply into_closed_red; fvs.
-    + eapply red_const. erewrite abstract_env_lookup_correct; eauto.
+    + eapply red_const. erewrite abstract_env_lookup_correct'; eauto.
     + specialize (hx _ wfΣ). clear -hx wΣ. sq.  fvs.
     Unshelve. all : eauto.
   Qed.
@@ -1640,7 +1640,7 @@ Qed.
     eapply closed_red_zipp.
     { eapply welltyped_zipc_zipp in h1; auto; fvs. }
     eapply into_closed_red; fvs.
-    + eapply red_const. erewrite abstract_env_lookup_correct; eauto.
+    + eapply red_const. erewrite abstract_env_lookup_correct'; eauto.
     + specialize (hx _ wfΣ). sq; fvs.
     Unshelve. eauto.
   Qed.
@@ -1652,7 +1652,7 @@ Qed.
       apply conv_cum_alt in H as [(?&?&[r1 r2 eq])]; auto.
     2: pose proof (hΣ _ wfΣ); sq ; eauto.
     rewrite zipp_as_mkApps in r1, r2.
-    erewrite <- abstract_env_lookup_correct in eq1, eq2; eauto.
+    erewrite <- abstract_env_lookup_correct' in eq1, eq2; eauto.
     symmetry in eq1, eq2.
     generalize hΣ. intros []; eauto.
     unshelve eapply closed_red_mkApps_tConst_axiom in r1 as (?&->&?); eauto.
@@ -2685,7 +2685,7 @@ Qed.
     - intros ? ? Hu Hu'; apply iff_reflect; apply (abstract_env_compare_universe_correct _ wfΣ Conv).
       + revert Hu. apply reflect_iff. apply wf_universe_reflect.
       + revert Hu'. apply reflect_iff. apply wf_universe_reflect.
-    - intros; now eapply abstract_env_lookup_correct.
+    - intros; now eapply abstract_env_lookup_correct'.
     - revert hl. apply reflect_iff, wf_universe_instanceP.
     - revert hl'. apply reflect_iff, wf_universe_instanceP.
   Qed.
@@ -3497,20 +3497,20 @@ Qed.
     eapply red_welltyped ; [auto|..].
     - exact h1.
     - eapply red_zipc.
-      eapply red_const. erewrite abstract_env_lookup_correct; eauto.
+      eapply red_const. erewrite abstract_env_lookup_correct'; eauto.
   Qed.
   Next Obligation.
     pose (heΣ _ wfΣ). clear aux. specialize_Σ wfΣ. sq.
     eapply red_welltyped ; [auto|..].
     - exact h2.
     - eapply red_zipc.
-      eapply red_const. erewrite abstract_env_lookup_correct; eauto.
+      eapply red_const. erewrite abstract_env_lookup_correct'; eauto.
   Qed.
   Next Obligation.
     eapply R_cored. simpl. intros.
     eapply cored_zipc.
     eapply cored_const.
-    erewrite abstract_env_lookup_correct; eauto.
+    erewrite abstract_env_lookup_correct'; eauto.
   Qed.
   Next Obligation.
     rename H into wfΣ. destruct (hΣ _ wfΣ).
@@ -3519,14 +3519,14 @@ Qed.
     - eapply red_conv_cum_l ; try assumption.
       eapply closed_red_zipp. 1:eapply welltyped_zipc_zipp in h1; fvs.
       eapply into_closed_red.
-      * eapply red_const. erewrite abstract_env_lookup_correct; eauto.
+      * eapply red_const. erewrite abstract_env_lookup_correct'; eauto.
       * eapply welltyped_zipc_zipp in h1; fvs.
       * eapply welltyped_zipc_zipp in h1; fvs.
     - etransitivity ; try eassumption.
       eapply red_conv_cum_r ; try assumption.
       eapply closed_red_zipp; auto.
       2:{ eapply into_closed_red; auto.
-        * eapply red_const. erewrite abstract_env_lookup_correct; eauto.
+        * eapply red_const. erewrite abstract_env_lookup_correct'; eauto.
         * eapply welltyped_zipc_zipp in h1; fvs. }
       clear aux. eapply welltyped_zipc_zipp in h2; eauto.
       destruct hx as [hx]. rewrite (All2_fold_length hx); fvs.
@@ -3538,9 +3538,9 @@ Qed.
     eapply conv_cum_red_inv.
     - eauto.
     - apply red_zipp.
-      eapply red_const. erewrite abstract_env_lookup_correct; eauto.
+      eapply red_const. erewrite abstract_env_lookup_correct'; eauto.
     - apply red_zipp.
-      eapply red_const. erewrite abstract_env_lookup_correct; eauto.
+      eapply red_const. erewrite abstract_env_lookup_correct'; eauto.
     - now eapply H.
   Qed.
   Next Obligation.
@@ -3550,24 +3550,24 @@ Qed.
     eapply conv_cum_mkApps_inv in H as [(?&?)]; eauto.
     - apply whnf_mkApps.
       eapply whne_const.
-      + erewrite abstract_env_lookup_correct; eauto.
+      + erewrite abstract_env_lookup_correct'; eauto.
       + eauto.
     - apply whnf_mkApps.
       eapply whne_const.
-      + erewrite abstract_env_lookup_correct; eauto.
+      + erewrite abstract_env_lookup_correct'; eauto.
       + eauto.
   Qed.
   Next Obligation.
     destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
     eapply welltyped_zipc_tConst_inv in h1 as (?&?&?); eauto.
     unfold declared_constant, declared_constant_gen in *.
-    erewrite abstract_env_lookup_correct in d; eauto. congruence.
+    erewrite abstract_env_lookup_correct' in d; eauto. congruence.
   Qed.
   Next Obligation.
   destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
   eapply welltyped_zipc_tConst_inv in h1 as (?&?&?); eauto.
   unfold declared_constant, declared_constant_gen in *.
-  erewrite abstract_env_lookup_correct in d; eauto. congruence.
+  erewrite abstract_env_lookup_correct' in d; eauto. congruence.
 Qed.
   Next Obligation.
     destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
@@ -5089,7 +5089,7 @@ Qed.
       + reflexivity.
       + eapply red_delta.
       * unfold declared_constant, declared_constant_gen.
-        erewrite abstract_env_lookup_correct; eauto.
+        erewrite abstract_env_lookup_correct'; eauto.
         * reflexivity.
     - eapply unfold_one_case_cored in eq as r; eauto.
       apply cored_red in r.
@@ -5122,7 +5122,7 @@ Qed.
       + reflexivity.
       + eapply red_delta.
         * unfold declared_constant, declared_constant_gen.
-          erewrite abstract_env_lookup_correct;  eauto.
+          erewrite abstract_env_lookup_correct';  eauto.
         * reflexivity.
     - eapply unfold_one_case_cored in eq as r; eauto. apply cored_red in r.
       destruct r as [r].
@@ -5153,7 +5153,7 @@ Qed.
     - repeat zip fold. eapply cored_context.
       constructor. eapply red_delta.
       + unfold declared_constant, declared_constant_gen.
-        erewrite abstract_env_lookup_correct; eauto.
+        erewrite abstract_env_lookup_correct'; eauto.
       + reflexivity.
     - repeat zip fold. eapply cored_context.
       eapply unfold_one_case_cored; eauto.
@@ -5256,7 +5256,7 @@ Qed.
       constructor; eexists _, [].
       eauto using whnf_red with pcuic.
     - constructor; eexists _, (decompose_stack π).1.
-      clear H. erewrite <- abstract_env_lookup_correct in e; eauto.
+      clear H. erewrite <- abstract_env_lookup_correct' in e; eauto.
       split; [econstructor|]; eauto.
       split; [eauto with pcuic|].
       apply whnf_mkApps.
@@ -5267,7 +5267,7 @@ Qed.
       destruct h as (?&typ); auto.
       apply inversion_Const in typ as (?&?&?&?); auto.
       unfold declared_constant in d.
-      clear H. erewrite <- abstract_env_lookup_correct in e; eauto.
+      clear H. erewrite <- abstract_env_lookup_correct' in e; eauto.
       congruence.
     - zip fold in h.
       destruct (hΣ _ wfΣ).
@@ -5275,7 +5275,7 @@ Qed.
       destruct h as (?&typ); auto.
       apply inversion_Const in typ as (?&?&?&?); auto.
       unfold declared_constant in d.
-      clear H. erewrite <- abstract_env_lookup_correct in e; eauto.
+      clear H. erewrite <- abstract_env_lookup_correct' in e; eauto.
       congruence.
     - clear H.
       eapply unfold_one_case_None in e as [(c'&r&whcase)]; eauto.
diff --git a/safechecker/theories/PCUICSafeReduce.v b/safechecker/theories/PCUICSafeReduce.v
index c3060f7ea..ba34674c3 100644
--- a/safechecker/theories/PCUICSafeReduce.v
+++ b/safechecker/theories/PCUICSafeReduce.v
@@ -593,7 +593,7 @@ Corollary R_Acc_aux :
     left. econstructor. eapply red1_context.
     econstructor.
     - unfold declared_constant, declared_constant_gen.
-      rewrite (abstract_env_lookup_correct _ _ wfΣ). rewrite <- eq. reflexivity.
+      rewrite (abstract_env_lookup_correct' _ _ wfΣ). rewrite <- eq. reflexivity.
     - cbn. reflexivity.
   Qed.
 
@@ -605,7 +605,7 @@ Corollary R_Acc_aux :
     destruct h as [T h].
     apply inversion_Const in h as [decl [? [d [? ?]]]] ; auto.
     unfold declared_constant, declared_constant_gen in d.
-    rewrite (abstract_env_lookup_correct _ _ wfΣ), <- eq in d.
+    rewrite (abstract_env_lookup_correct' _ _ wfΣ), <- eq in d.
     discriminate.
   Qed.
   Next Obligation.
@@ -616,7 +616,7 @@ Corollary R_Acc_aux :
     destruct h as [T h].
     apply inversion_Const in h as [decl [? [d [? ?]]]] ; auto.
     unfold declared_constant, declared_constant_gen in d.
-    rewrite (abstract_env_lookup_correct _ _ wfΣ), <- eq in d.
+    rewrite (abstract_env_lookup_correct' _ _ wfΣ), <- eq in d.
     discriminate.
   Qed.
 
@@ -1567,7 +1567,7 @@ Corollary R_Acc_aux :
       assumption.
     - unfold zipp. case_eq (decompose_stack π). intros.
       constructor. constructor. eapply whne_mkApps. econstructor.
-      + symmetry. erewrite abstract_env_lookup_correct; eauto.
+      + symmetry. erewrite abstract_env_lookup_correct'; eauto.
       + reflexivity.
     - match goal with
       | |- context [ reduce ?x ?y ?z ] =>
diff --git a/safechecker/theories/PCUICSafeRetyping.v b/safechecker/theories/PCUICSafeRetyping.v
index 7ca7bfc40..b0ba7d6ea 100644
--- a/safechecker/theories/PCUICSafeRetyping.v
+++ b/safechecker/theories/PCUICSafeRetyping.v
@@ -260,7 +260,7 @@ Qed.
   Next Obligation.
     split.
     - symmetry in look.
-      etransitivity. erewrite (abstract_env_lookup_correct X); eauto.
+      etransitivity. erewrite (abstract_env_lookup_correct' X); eauto.
       reflexivity.
     - now symmetry.
   Defined.
@@ -271,10 +271,10 @@ Qed.
     cbn.
     apply_funelim (lookup_ind_decl ind).
     1-2: intros * _ her [mdecl [idecl [declm decli]]];
-      red in declm; erewrite <- abstract_env_lookup_correct, declm in e0; eauto;
+      red in declm; erewrite <- abstract_env_lookup_correct', declm in e0; eauto;
       congruence.
     1-2:intros * _ _ => // => _ [mdecl [idecl [declm /= decli]]].
-    red in declm. erewrite <- abstract_env_lookup_correct, declm in look; eauto.
+    red in declm. erewrite <- abstract_env_lookup_correct', declm in look; eauto.
     noconf look.
     congruence.
   Qed.
@@ -486,7 +486,7 @@ Qed.
     cbn in *; intros. pose (hΣ _ wfΣ). specialize_Σ wfΣ.
     inversion wt. sq.
     inversion X0; subst.
-    erewrite <- abstract_env_lookup_correct in e; eauto.
+    erewrite <- abstract_env_lookup_correct' in e; eauto.
     rewrite isdecl in e. inversion e. subst.
     now constructor.
   Defined.
@@ -494,14 +494,14 @@ Qed.
     destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
     specialize_Σ wfΣ. inversion wt.
     inversion X0 ; subst.
-    clear wildcard. erewrite <- abstract_env_lookup_correct in e; eauto.
+    clear wildcard. erewrite <- abstract_env_lookup_correct' in e; eauto.
     rewrite isdecl in e. inversion e.
   Defined.
   Next Obligation.
     destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
     specialize_Σ wfΣ. inversion wt.
     inversion X0 ; subst.
-    clear wildcard. erewrite <- abstract_env_lookup_correct in e; eauto.
+    clear wildcard. erewrite <- abstract_env_lookup_correct' in e; eauto.
     rewrite isdecl in e. inversion e.
   Defined.
   Next Obligation.
diff --git a/safechecker/theories/PCUICTypeChecker.v b/safechecker/theories/PCUICTypeChecker.v
index 54a7033fc..4453dc82e 100644
--- a/safechecker/theories/PCUICTypeChecker.v
+++ b/safechecker/theories/PCUICTypeChecker.v
@@ -943,25 +943,25 @@ Section Typecheck.
       }.
   Next Obligation.
     destruct (abstract_env_ext_exists X) as [[Σ wfΣ]]; specialize_Σ wfΣ.
-    erewrite <- abstract_env_lookup_correct in e0; eauto.
+    erewrite <- abstract_env_lookup_correct' in e0; eauto.
     depelim X2.
     unfold declared_minductive, declared_minductive_gen in H. erewrite <- e0 in H.
     congruence.
   Qed.
   Next Obligation.
-    erewrite <- abstract_env_lookup_correct in e; eauto.
+    erewrite <- abstract_env_lookup_correct' in e; eauto.
     now split.
   Qed.
   Next Obligation.
     destruct (abstract_env_ext_exists X) as [[Σ wfΣ]]; specialize_Σ wfΣ.
-    erewrite <- abstract_env_lookup_correct in e1; eauto.
+    erewrite <- abstract_env_lookup_correct' in e1; eauto.
     depelim X2.
     unfold declared_minductive, declared_minductive_gen in H. erewrite <- e1 in H.
     congruence.
   Qed.
   Next Obligation.
     destruct (abstract_env_ext_exists X) as [[Σ wfΣ]]; specialize_Σ wfΣ.
-    erewrite <- abstract_env_lookup_correct in e0; eauto.
+    erewrite <- abstract_env_lookup_correct' in e0; eauto.
     depelim X2.
     unfold declared_minductive, declared_minductive_gen in H. erewrite <- e0 in H.
     congruence.
@@ -1651,17 +1651,17 @@ Section Typecheck.
   Next Obligation.
     pose proof (heΣ _ wfΣ) as [heΣ]. specialize_Σ wfΣ ; sq.
     eapply global_uctx_invariants_ext.
-    symmetry in HH. erewrite <- abstract_env_lookup_correct in HH; eauto.
+    symmetry in HH. erewrite <- abstract_env_lookup_correct' in HH; eauto.
     now apply (weaken_lookup_on_global_env' _ _ _ (heΣ : wf _) HH).
   Qed.
   Next Obligation.
     pose proof (heΣ _ wfΣ) as [heΣ]. specialize_Σ wfΣ ; sq.
     constructor; try assumption.
-    symmetry in HH. erewrite <- abstract_env_lookup_correct in HH; eauto.
+    symmetry in HH. erewrite <- abstract_env_lookup_correct' in HH; eauto.
   Qed.
   Next Obligation.
     apply absurd; intros. pose proof (heΣ _ wfΣ) as [heΣ]. specialize_Σ wfΣ ; sq.
-    erewrite <- abstract_env_lookup_correct in HH; eauto.
+    erewrite <- abstract_env_lookup_correct' in HH; eauto.
     inversion X1. unfold declared_constant, declared_constant_gen in isdecl.
     rewrite <- HH in isdecl. inversion isdecl. now subst.
   Qed.
@@ -1669,7 +1669,7 @@ Section Typecheck.
     destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
     cbn in *.
     pose proof (heΣ _ wfΣ) as [heΣ]. specialize_Σ wfΣ ; sq.
-    inversion X1 ; subst. erewrite <- abstract_env_lookup_correct in e0; eauto.
+    inversion X1 ; subst. erewrite <- abstract_env_lookup_correct' in e0; eauto.
     rewrite isdecl in e0.
     congruence.
   Qed.
@@ -1677,7 +1677,7 @@ Section Typecheck.
     destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
     cbn in *.
     pose proof (heΣ _ wfΣ) as [heΣ]. specialize_Σ wfΣ ; sq.
-    inversion X1 ; subst. erewrite <- abstract_env_lookup_correct in e0; eauto.
+    inversion X1 ; subst. erewrite <- abstract_env_lookup_correct' in e0; eauto.
     rewrite isdecl in e0.
     congruence.
   Qed.
@@ -2398,7 +2398,7 @@ Section Typecheck.
     = check_recursivity_kind (lookup_env Σ) a Finite.
   Proof using Type.
     unfold  check_recursivity_kind.
-    erewrite <- abstract_env_lookup_correct; eauto.
+    erewrite <- abstract_env_lookup_correct'; eauto.
   Qed.
 
   Definition abstract_wf_fixpoint mfix Σ (wfΣ: abstract_env_ext_rel X Σ):
@@ -2527,7 +2527,7 @@ Section Typecheck.
 
   Next Obligation.
     eapply eqb_eq in i. eapply eqb_eq in i0.
-    rewrite -(abstract_env_lookup_correct _ (Σ := Σ)) // in HH.
+    rewrite -(abstract_env_lookup_correct' _ (Σ := Σ)) // in HH.
     split. econstructor. rewrite eqp.
     erewrite abstract_primitive_constant_correct; try reflexivity. eassumption.  red.
     unfold declared_constant_gen. now rewrite -HH.
@@ -2539,7 +2539,7 @@ Section Typecheck.
     cbn in *. specialize_Σ wfΣ ; sq.
     depelim X1.
     eapply eqb_eq in i. eapply eqb_eq in i0.
-    rewrite -(abstract_env_lookup_correct _ (Σ := Σ)) // in HH.
+    rewrite -(abstract_env_lookup_correct' _ (Σ := Σ)) // in HH.
     rewrite (abstract_primitive_constant_correct _ _ _ wfΣ) in eqp.
     rewrite e1 in eqp. noconf eqp.
     symmetry in HH. rewrite /declared_constant in d0.
@@ -2551,7 +2551,7 @@ Section Typecheck.
     cbn in *. specialize_Σ wfΣ ; sq.
     depelim X1.
     eapply eqb_eq in i.
-    rewrite -(abstract_env_lookup_correct _ (Σ := Σ)) // in HH.
+    rewrite -(abstract_env_lookup_correct' _ (Σ := Σ)) // in HH.
     rewrite (abstract_primitive_constant_correct _ _ _ wfΣ) in eqp.
     rewrite e1 in eqp. noconf eqp.
     symmetry in HH. rewrite /declared_constant in d0.
@@ -2564,7 +2564,7 @@ Section Typecheck.
     destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
     cbn in *. specialize_Σ wfΣ ; sq.
     depelim X1.
-    rewrite -(abstract_env_lookup_correct _ (Σ := Σ)) // in HH.
+    rewrite -(abstract_env_lookup_correct' _ (Σ := Σ)) // in HH.
     rewrite (abstract_primitive_constant_correct _ _ _ wfΣ) in eqp.
     rewrite e1 in eqp. noconf eqp.
     symmetry in HH. rewrite /declared_constant in d0.
@@ -2576,7 +2576,7 @@ Section Typecheck.
     destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
     cbn in *. specialize_Σ wfΣ ; sq.
     depelim X1.
-    rewrite -(abstract_env_lookup_correct _ (Σ := Σ)) // in e0.
+    rewrite -(abstract_env_lookup_correct' _ (Σ := Σ)) // in e0.
     rewrite (abstract_primitive_constant_correct _ _ _ wfΣ) in eqp.
     rewrite e1 in eqp. noconf eqp.
     symmetry in e0. rewrite /declared_constant in d.
@@ -2587,7 +2587,7 @@ Section Typecheck.
     destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
     cbn in *. specialize_Σ wfΣ ; sq.
     depelim X1.
-    rewrite -(abstract_env_lookup_correct _ (Σ := Σ)) // in e0.
+    rewrite -(abstract_env_lookup_correct' _ (Σ := Σ)) // in e0.
     rewrite (abstract_primitive_constant_correct _ _ _ wfΣ) in eqp.
     rewrite e1 in eqp. noconf eqp.
     symmetry in e0. rewrite /declared_constant /declared_constant_gen in d.
diff --git a/safechecker/theories/PCUICWfEnv.v b/safechecker/theories/PCUICWfEnv.v
index fd68719c9..00018050b 100644
--- a/safechecker/theories/PCUICWfEnv.v
+++ b/safechecker/theories/PCUICWfEnv.v
@@ -103,8 +103,8 @@ Class abstract_env_prop {cf:checker_flags} (abstract_env_impl abstract_env_ext_i
                       Σ'.(declarations) = decls /\ Σ.(universes) = Σ'.(universes) /\
                       Σ.(retroknowledge) = Σ'.(retroknowledge);
 
-  abstract_env_lookup_correct X {Σ} c : abstract_env_ext_rel X Σ ->
-      lookup_env Σ c = abstract_env_lookup X c ;
+  abstract_env_lookup_correct X {Σ} kn decl : abstract_env_ext_rel X Σ ->
+      In (kn, decl) (declarations Σ) <-> abstract_env_lookup X kn = Some decl ;
 
   abstract_env_leqb_level_n_correct X {Σ} (wfΣ : abstract_env_ext_rel X Σ):
     let uctx := (wf_ext_gc_of_uctx (abstract_env_ext_wf X wfΣ)).π1 in
@@ -320,4 +320,19 @@ Proof.
     - erewrite <- (Hval'' l0). erewrite <- (Hval'' l'0) => //.
       + destruct s as [[Hs _] _]. now destruct (Hs _ Hl).
       + destruct s as [[Hs _] _]. now destruct (Hs _ Hl).
-Qed.
\ No newline at end of file
+Qed.
+
+Lemma abstract_env_lookup_correct' {cf:checker_flags} {X_type : abstract_env_impl}
+( X:X_type.π2.π1) {Σ} kn : abstract_env_ext_rel X Σ ->
+  lookup_env Σ kn = abstract_env_lookup X kn.
+Proof.
+  intro wfΣ; pose proof (HΣ := abstract_env_ext_wf X wfΣ); sq.
+  set (odecl := lookup_env _ _). case_eq odecl => [decl Hdecl| Hnotin].
+  - intros. destruct (abstract_env_lookup_correct X kn decl wfΣ) as [H _].
+    rewrite H; eauto. apply lookup_global_Some_iff_In_NoDup => //.
+    destruct HΣ as [[] _]. now eapply NoDup_on_global_decls.
+  - apply lookup_global_None in Hnotin. case_eq (abstract_env_lookup X kn) => //.
+    intros decl Hdecl. eapply abstract_env_lookup_correct in Hdecl; eauto.
+    destruct Hnotin. apply in_map_iff. now exists (kn,decl).
+Qed.
+
diff --git a/safechecker/theories/PCUICWfEnvImpl.v b/safechecker/theories/PCUICWfEnvImpl.v
index ca61e9ff2..783069597 100644
--- a/safechecker/theories/PCUICWfEnvImpl.v
+++ b/safechecker/theories/PCUICWfEnvImpl.v
@@ -288,6 +288,11 @@ Next Obligation. now split. Qed.
 Next Obligation.
   apply (reference_pop_decls_correct X decls prf X (referenced_pop X) eq_refl eq_refl).
 Qed.
+Next Obligation.
+  epose proof (HΣ := referenced_impl_ext_wf X). sq.
+  apply lookup_global_Some_iff_In_NoDup => //.
+  destruct HΣ as [[] _]. now eapply NoDup_on_global_decls.
+Qed.
 Next Obligation.
   pose proof (referenced_impl_ext_wf X); sq.
   set (uctx := wf_ext_gc_of_uctx _) in *; destruct uctx as [[lc ctrs] Huctx].
@@ -351,10 +356,15 @@ Next Obligation. unfold optim_pop. set (optim_pop_obligation_1 cf X). clearbody
   destruct (declarations X); cbn; inversion prf; inversion H0. subst.
   now destruct x.
 Qed.
-Next Obligation. pose (referenced_impl_ext_wf X). sq.
-    erewrite EnvMap.lookup_spec; try reflexivity.
+Next Obligation.
+  epose proof (HΣ := referenced_impl_ext_wf X). sq.
+  etransitivity; try apply abstract_env_lookup_correct => //.
+  assert (lookup_env X kn = EnvMap.lookup kn X).
+  { erewrite EnvMap.lookup_spec; try reflexivity.
     1: apply wf_fresh_globals; eauto.
-    1: apply wf_env_ext_map_repr. Qed.
+    1: apply wf_env_ext_map_repr. }
+  now rewrite <- H.
+Qed.
 Next Obligation.
     revert n l l' Hl Hl'. erewrite wf_ext_gc_of_uctx_irr.
     exact (abstract_env_leqb_level_n_correct X.(wf_env_ext_referenced) eq_refl).