diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index c8424ccff0b39347090aae9b372b7f9e0677dc9c..c9b1a2f949fc9c3f0fcf292cffcf8ad892d35820 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -1699,8 +1699,9 @@ Proof.
   by apply discrete_funO_map_ne=>c; apply urFunctor_map_contractive.
 Qed.
 
-(** * Constructing a camera [B] through a bijection with [A] that
-is mostly an isomorphism but restricts validity. *)
+(** * Constructing a camera [B] through a bijection with [A]
+
+The bijection must be mostly an isomorphism but may restrict validity. *)
 Lemma iso_cmra_mixin_restrict {A : cmra} {B : Type}
   `{!Dist B, !Equiv B, !PCore B, !Op B, !Valid B, !ValidN B}
   (f : A → B) (g : B → A)