From db2da9af69df9e0f0f116b5e1941907c7ff4478d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 14 Mar 2017 10:50:42 +0100
Subject: [PATCH] prove rtc_subrel

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

diff --git a/theories/relations.v b/theories/relations.v
index 5eb95e6b..83cfc39c 100644
--- a/theories/relations.v
+++ b/theories/relations.v
@@ -188,6 +188,8 @@ Section subrel.
   Proof. intros ? [y ?]; eauto. Qed.
   Lemma nf_subrel x : subrel → nf R2 x → nf R1 x.
   Proof. intros ? H1 H2; destruct H1; by apply red_subrel. Qed.
+  Lemma rtc_subrel x y : subrel → rtc R1 x y → rtc R2 x y.
+  Proof. induction 2; [by apply rtc_refl|]. eapply rtc_l; eauto. Qed.
 End subrel.
 
 (** * Theorems on well founded relations *)
-- 
GitLab