diff --git a/iris_staging/algebra/monotone.v b/iris_staging/algebra/monotone.v
index a3b21e0ef78f615342ab07a9b427a17e7e112bcb..9ca5e3cb928c402217b3da43389dd1df1a1168bd 100644
--- a/iris_staging/algebra/monotone.v
+++ b/iris_staging/algebra/monotone.v
@@ -15,7 +15,7 @@ Local Arguments cmra_valid _  !_ /.
 
 (* Given a preorder relation R on a type A we construct a resource algebra mra R
    and an injection principal : A -> mra R such that:
-   R x y iff principal x ≼ principal y
+   [R x y] iff [principal x ≼ principal y]
    where ≼ is the extension order of mra R resource algebra. This is exactly
    what the lemma [principal_included] shows.