diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 448ec6427233809dfc3069aae56f7bc99e19d611..093d14d77528c2d8716beb4528251492ce565582 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -154,7 +154,8 @@ Proof.
 Qed.
 
 (** Since the full adequacy statement is quite a mouthful, we prove some more
-intuitive and simpler corollaries. *)
+intuitive and simpler corollaries. These lemmas are morover stated in terms of
+[rtc erased_step] so one does not have to provide the trace. *)
 Record adequate {Λ} (s : stuckness) (e1 : expr Λ) (σ1 : state Λ)
     (φ : val Λ → state Λ → Prop) := {
   adequate_result t2 σ2 v2 :