diff --git a/theories/relations.v b/theories/relations.v
index c957ea8a53024d19dffa81beeae821c812dfcf95..a17f51cbfe87c1bea190dddc00163803f08c0b9b 100644
--- a/theories/relations.v
+++ b/theories/relations.v
@@ -198,6 +198,9 @@ Notation wf := well_founded.
 Section wf.
   Context `{R : relation A}.
 
+  Lemma Acc_def x : Acc R x ↔ (∀ y : A, R y x → Acc R y).
+  Proof. split. by destruct 1. by constructor. Qed.
+
   (** A trick by Thomas Braibant to compute with well-founded recursions:
   it lazily adds [2^n] [Acc_intro] constructors in front of a well foundedness
   proof, so that the actual proof is never reached in practise. *)