diff --git a/theories/relations.v b/theories/relations.v
index 80e6af26f1de31e6a05a2085b54421ad0a21281d..fdadac438988e9b2efad90480765211cad0b3b1f 100644
--- a/theories/relations.v
+++ b/theories/relations.v
@@ -280,6 +280,10 @@ Section properties.
   Lemma wn_step_rtc x y : wn R y → rtc R x y → wn R x.
   Proof. induction 2; eauto using wn_step. Qed.
 
+  (** The following theorem requires that [red R] is decidable. The intuition
+  for this requirement is that [wn R] is a very "positive" statement as it
+  points out a particular trace. In contrast, [sn R] just says "this also holds
+  for all successors", there is no "data"/"trace" there. *)
   Lemma sn_wn `{!∀ y, Decision (red R y)} x : sn R x → wn R x.
   Proof.
     induction 1 as [x _ IH]. destruct (decide (red R x)) as [[x' ?]|?].