From 9d1092a06e38ada2ffe25c12069de82d972a7d60 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 24 Sep 2017 22:44:19 +0200
Subject: [PATCH] Unfolding lemma for Acc.

---
 theories/relations.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/theories/relations.v b/theories/relations.v
index c957ea8a..a17f51cb 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. *)
-- 
GitLab