diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index a6729546dd29b3baf450cc0664a13ae4d7bda5b3..299d9b5cd9392dbf7f120552a36df7f5e3393999 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -413,6 +413,11 @@ Proof.
 Qed.
 
 (** * Basic rules *)
+Lemma tac_eval Δ Q Q' :
+  Q = Q' →
+  envs_entails Δ Q' → envs_entails Δ Q.
+Proof. by intros ->. 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 315d0dccc9a885be5f3dabf85e8a23c8fa72b7c1..e470ea48c3540538e34a64fe87c69283be912819 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -80,6 +80,13 @@ Ltac iStartProof :=
                |apply tac_adequate]
   end.
 
+(** * Simplification *)
+Tactic Notation "iEval" tactic(t) :=
+  try iStartProof;
+  try (eapply tac_eval; [t; reflexivity|]).
+
+Tactic Notation "iSimpl" := iEval simpl.
+
 (** * Context manipulation *)
 Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
   eapply tac_rename with _ H1 H2 _ _; (* (i:=H1) (j:=H2) *)