diff --git a/theories/logic/model.v b/theories/logic/model.v
index 0a5a020baf2d2af663677afb702d47686990a25d..3f88adf863359caf9458c2e6f0f4a2d252145abf 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -245,8 +245,8 @@ Section monadic.
   Lemma refines_bind K K' E A A' e e' :
     (REL e << e' @ E : A) -∗
     (∀ v v', A v v' -∗
-      (REL fill K (of_val v) << fill K' (of_val v') : A')) -∗
-    (REL fill K e << fill K' e' @ E : A').
+      REL fill K (of_val v) << fill K' (of_val v') : A') -∗
+    REL fill K e << fill K' e' @ E : A'.
   Proof.
     iIntros "Hm Hf".
     rewrite refines_eq /refines_def.