diff --git a/theories/bi/derived_laws_sbi.v b/theories/bi/derived_laws_sbi.v
index 8b40c1edfda078a2ead7fb197f1132b02ff94a07..d1afdc565ce02c37ad4ee57dc782157e2ac494f7 100644
--- a/theories/bi/derived_laws_sbi.v
+++ b/theories/bi/derived_laws_sbi.v
@@ -204,7 +204,8 @@ Global Instance later_absorbing P : Absorbing P → Absorbing (▷ P).
 Proof. intros ?. by rewrite /Absorbing -later_absorbingly absorbing. Qed.
 
 Section löb.
-  (* Proof following https://en.wikipedia.org/wiki/L%C3%B6b's_theorem#Proof_of_L%C3%B6b's_theorem *)
+  (* Proof following https://en.wikipedia.org/wiki/L%C3%B6b's_theorem#Proof_of_L%C3%B6b's_theorem.
+     Their Ψ is called Q in our proof. *)
   Lemma weak_löb P : (▷ P ⊢ P) → (True ⊢ P).
   Proof.
     pose (flöb_pre (P Q : PROP) := (▷ Q → P)%I).