diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 34a366329c31312b5899a34103ca6515d157b02c..3c20309d309e3874a64b1d9ed8932fb65f55fa28 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -205,6 +205,12 @@ Section ectx_language.
       eexists e2', σ2, efs. by apply head_prim_step.
     - intros σ1 e2' σ2 efs ? ?%head_reducible_prim_step; eauto.
   Qed.
+
+  Global Instance pure_exec_fill K e1 e2 φ :
+    PureExec φ e1 e2 →
+    PureExec φ (fill K e1) (fill K e2).
+  Proof. apply: pure_exec_ctx. Qed.
+
 End ectx_language.
 
 Arguments ectx_lang : clear implicits.
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index b9d10beb85ddde0964e3f0810c7eada0284fd404..a3704c7029b09f3873f4bd844ad2cfcede647c92 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -140,7 +140,8 @@ Section language.
     PureExec P e1 e2.
   Proof. intros HPE. split; intros; eapply HPE; eauto. Qed.
 
-  Global Instance pure_exec_ctx K `{LanguageCtx Λ K} e1 e2 φ :
+  (* We do not make this an instance because it is awfully general. *)
+  Lemma pure_exec_ctx K `{LanguageCtx Λ K} e1 e2 φ :
     PureExec φ e1 e2 →
     PureExec φ (K e1) (K e2).
   Proof.