diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index be46ac7c9f88ce63c87129cdf46f6b45e854cc76..fd6705348f7e7e34ddf5ba20d241ddb6cfb59a27 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -316,8 +316,11 @@ Definition envs_clear_spatial {PROP} (Δ : envs PROP) : envs PROP :=
 Definition envs_clear_intuitionistic {PROP} (Δ : envs PROP) : envs PROP :=
   Envs Enil (env_spatial Δ) (env_counter Δ).
 
+Definition envs_set_counter {PROP} (c : positive) (Δ : envs PROP) : envs PROP :=
+  Envs (env_intuitionistic Δ) (env_spatial Δ) c.
+
 Definition envs_incr_counter {PROP} (Δ : envs PROP) : envs PROP :=
-  Envs (env_intuitionistic Δ) (env_spatial Δ) (Pos_succ (env_counter Δ)).
+  envs_set_counter (Pos_succ (env_counter Δ)) Δ.
 
 Fixpoint envs_split_go {PROP}
     (js : list ident) (Δ1 Δ2 : envs PROP) : option (envs PROP * envs PROP) :=
@@ -665,10 +668,12 @@ Proof.
   - destruct (Γp !! i); simplify_eq/=; by rewrite ?env_lookup_env_delete_ne.
 Qed.
 
-Lemma envs_incr_counter_equiv Δ : envs_Forall2 (⊣⊢) Δ (envs_incr_counter Δ).
+Lemma envs_set_counter_equiv c Δ : envs_Forall2 (⊣⊢) Δ (envs_set_counter c Δ).
 Proof. done. Qed.
-Lemma envs_incr_counter_sound Δ : of_envs (envs_incr_counter Δ) ⊣⊢ of_envs Δ.
+Lemma envs_set_counter_sound c Δ : of_envs (envs_set_counter c Δ) ⊣⊢ of_envs Δ.
 Proof. by f_equiv. Qed.
+Lemma envs_incr_counter_sound Δ : of_envs (envs_incr_counter Δ) ⊣⊢ of_envs Δ.
+Proof. apply envs_set_counter_sound. Qed.
 
 Lemma envs_split_go_sound js Δ1 Δ2 Δ1' Δ2' :
   (∀ j P, envs_lookup j Δ1 = Some (false, P) → envs_lookup j Δ2 = None) →
diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
index 1c48602219c85f36c83c59c5e7ee171006e48321..690e6866e5bce7145750a8ba82acac4a3ec86cf9 100644
--- a/theories/proofmode/reduction.v
+++ b/theories/proofmode/reduction.v
@@ -12,7 +12,7 @@ Declare Reduction pm_eval := cbv [
   env_dom env_intuitionistic env_spatial env_counter env_spatial_is_nil envs_dom
   envs_lookup envs_lookup_delete envs_delete envs_snoc envs_app
   envs_simple_replace envs_replace envs_split
-  envs_clear_spatial envs_clear_intuitionistic envs_incr_counter
+  envs_clear_spatial envs_clear_intuitionistic envs_set_counter envs_incr_counter
   envs_split_go envs_split env_to_prop
   (* PM option combinators *)
   pm_option_bind pm_from_option pm_option_fun