From 005887ee4cd20b48f85c4e6811e41731d2656f83 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 30 Nov 2018 15:21:08 +0100
Subject: [PATCH] Show that accessible elements do not loop.

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

diff --git a/theories/relations.v b/theories/relations.v
index 3d761f54..a67e7535 100644
--- a/theories/relations.v
+++ b/theories/relations.v
@@ -171,6 +171,9 @@ Section rtc.
   Lemma tc_rtc x y : tc R x y → rtc R x y.
   Proof. induction 1; eauto. Qed.
 
+  Lemma acc_not_ex_loop x : Acc (flip R) x → ¬ex_loop R x.
+  Proof. unfold not. induction 1; destruct 1; eauto. Qed.
+
   Lemma all_loop_red x : all_loop R x → red R x.
   Proof. destruct 1; auto. Qed.
   Lemma all_loop_step x y : all_loop R x → R x y → all_loop R y.
-- 
GitLab