diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 124ae4a4107fe6e8fe6503301e1e64777f4c5d8c..ac28a1a1b9a0277ee281e51379b7bade677e0bc3 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -418,6 +418,17 @@ Lemma tac_eval Δ Q Q' :
   envs_entails Δ Q' → envs_entails Δ Q.
 Proof. by intros <-. Qed.
 
+Lemma tac_eval_in Δ Δ' i p P P' Q :
+  envs_lookup i Δ = Some (p, P) →
+  (P ⊢ P') →
+  envs_simple_replace i p (Esnoc Enil i P') Δ  = Some Δ' →
+  envs_entails Δ' Q → envs_entails Δ Q.
+Proof.
+  rewrite /envs_entails. intros ? HP ? <-.
+  rewrite envs_simple_replace_sound //; simpl.
+  by rewrite HP right_id wand_elim_r.
+Qed.
+
 Lemma tac_assumption Δ i p P Q :
   envs_lookup i Δ = Some (p,P) → FromAssumption p P Q →
   envs_entails Δ Q.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 0dd09eebe82e594177b8556d8504380fd7832a97..a894b9475584445c009b6729d93a5b6b42e45e10 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -85,7 +85,16 @@ Tactic Notation "iEval" tactic(t) :=
   iStartProof;
   eapply tac_eval; [t; reflexivity|].
 
+Tactic Notation "iEval" tactic(t) "in" constr(H) :=
+  iStartProof;
+  eapply tac_eval_in with _ H _ _ _;
+    [env_reflexivity || fail "iEval:" H "not found"
+    |t; reflexivity
+    |env_reflexivity
+    |].
+
 Tactic Notation "iSimpl" := iEval simpl.
+Tactic Notation "iSimpl" "in" constr(H) := iEval simpl in H.
 
 (** * Context manipulation *)
 Tactic Notation "iRename" constr(H1) "into" constr(H2) :=