diff --git a/theories/relations.v b/theories/relations.v
index 65b18462644bfa72e232ff8629011dcc37bfd324..d9e65e5da1064d7d1f345e3a36e0a825a7e9b8ce 100644
--- a/theories/relations.v
+++ b/theories/relations.v
@@ -54,6 +54,9 @@ Section definitions.
     | ex_loop_do_step x y : R x y → ex_loop y → ex_loop x.
 End definitions.
 
+(* Strongly normalizing elements *)
+Notation sn R := (Acc (flip R)).
+
 Hint Unfold nf red.
 
 (** * General theorems *)