diff --git a/theories/logic/model.v b/theories/logic/model.v
index 37a26751ffc3534a7b1b4cfdd1c111a81ada8ee4..e10eacd968d5c3192527fbfe4360c90d2303b9a8 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -336,18 +336,22 @@ Section related_facts.
 
 End related_facts.
 
+(** TODO this is a terrible hack and I should be ashamed of myself.
+    See iris issue 225. *)
+Notation is_closed_expr' := (λ e, ∀ vs, subst_map vs e = e).
+
 Section monadic.
   Context `{relocG Σ}.
 
   Lemma refines_ret' E Γ e1 e2 A :
-    is_closed_expr [] e1 →
-    is_closed_expr [] e2 →
+    is_closed_expr' e1 →
+    is_closed_expr' e2 →
     interp_expr E e1 e2 A -∗ {E;Γ} ⊨ e1 << e2 : A.
   Proof.
-    iIntros (??) "HA".
+    iIntros (Hcl1 Hcl2) "HA".
     rewrite refines_eq /refines_def.
     iIntros (vvs ρ) "#Hs #HΓ".
-    rewrite !subst_map_is_closed_nil//.
+    by rewrite Hcl1 Hcl2.
   Qed.
 
   Lemma refines_bind K K' E Γ A A' e e' :
diff --git a/theories/logic/rules.v b/theories/logic/rules.v
index c1b53cecba10be0526ebcbde0652a8d1f568e3ea..c6e7265100893183affdad5d95068f34d887a711 100644
--- a/theories/logic/rules.v
+++ b/theories/logic/rules.v
@@ -74,9 +74,6 @@ Section rules.
     by rewrite subst_map_fill.
   Qed.
 
-  (* See iris issue 225 *)
-  Notation is_closed_expr' := (λ e, ∀ vs, subst_map vs e = e).
-
   Lemma refines_wp_l Γ K e1 e2 A :
     is_closed_expr' e1 →
     (WP e1 {{ v,