diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v
index 131b1753aad52c862b1339fa8830c34ef6d2bca8..f630857a0eb0378d788355881f8fb6f0fe7bbe5a 100644
--- a/iris/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -194,8 +194,12 @@ Section fractional.
 
   (* Not an instance because of performance; you can locally add it if you are
   willing to pay the cost. We have concrete instances for certain fractional
-  assertions such as ↦. *)
-  Lemma frame_fractional p R P Φ qR qP r :
+  assertions such as ↦.
+
+  Coq is sometimes unable to infer the [Φ], hence it might be useful to write
+  [apply: (frame_fractional (λ q, ...))] when using the lemma to prove your
+  custom instance. *)
+  Lemma frame_fractional Φ p R P qR qP r :
     AsFractional R Φ qR →
     AsFractional P Φ qP →
     FrameFractionalQp qR qP r →