diff --git a/iris/proofmode/environments.v b/iris/proofmode/environments.v
index 9415109158145316c46cd640bae50a34cb82f304..cce61fffba925fb894959a55d6850d0f65b7ae40 100644
--- a/iris/proofmode/environments.v
+++ b/iris/proofmode/environments.v
@@ -863,14 +863,13 @@ Proof.
   - rewrite /= IH (comm _ Q _) assoc. done.
 Qed.
 
-Lemma env_to_prop_and_pers_sound Γ :
-  □ env_to_prop_and Γ ⊣⊢ <affine> [∧] (env_map_pers Γ).
+Lemma env_to_prop_and_pers_sound Γ i P :
+  □ env_to_prop_and (Esnoc Γ i P) ⊣⊢ <affine> [∧] (env_map_pers (Esnoc Γ i P)).
 Proof.
-  destruct Γ as [|Γ i P]; simpl.
-  { rewrite /bi_intuitionistically persistent_persistently //. }
   revert P. induction Γ as [|Γ IH ? Q]=>P; simpl.
   - by rewrite right_id.
-  - rewrite /= IH (comm _ Q _) assoc. f_equiv.
-    rewrite persistently_and. done.
+  - rewrite /= IH. clear IH. f_equiv. simpl.
+    rewrite assoc. f_equiv.
+    rewrite persistently_and comm. done.
 Qed.
 End envs.
diff --git a/iris/proofmode/reduction.v b/iris/proofmode/reduction.v
index b70aef0a39f3fb4edde630b0d2657e13902ca3ba..ff036d248d5ef899886c9e5041a9a1ffa2815475 100644
--- a/iris/proofmode/reduction.v
+++ b/iris/proofmode/reduction.v
@@ -4,7 +4,9 @@ From iris.prelude Require Import options.
 
 (** Called by all tactics to perform computation to lookup items in the
     context.  We avoid reducing anything user-visible here to make sure we
-    do not reduce e.g. before unification happens in [iApply].*)
+    do not reduce e.g. before unification happens in [iApply].
+    This needs to contain all definitions used in the user-visible statements in
+    [coq_tactics], and their dependencies. *)
 Declare Reduction pm_eval := cbv [
   (* base *)
   base.negb base.beq