From 6997e05a611d47be505fbbd4aa8e06487309a5eb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 21 Jul 2020 19:16:22 +0200
Subject: [PATCH] Some basic lemmas about `sn`.

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

diff --git a/theories/relations.v b/theories/relations.v
index 32522c05..036ef015 100644
--- a/theories/relations.v
+++ b/theories/relations.v
@@ -280,6 +280,13 @@ Section properties.
   Lemma wn_step_rtc x y : wn R y → rtc R x y → wn R x.
   Proof. induction 2; eauto using wn_step. Qed.
 
+  Lemma nf_sn x : nf R x → sn R x.
+  Proof. intros Hnf. constructor; intros y Hxy. destruct Hnf; eauto. Qed.
+  Lemma sn_step x y : sn R x → R x y → sn R y.
+  Proof. induction 1; eauto. Qed.
+  Lemma sn_step_rtc x y : sn R x → rtc R x y → sn R y.
+  Proof. induction 2; eauto using sn_step. Qed.
+
   (** An acyclic relation that can only take finitely many steps (sometimes
   called "globally finite") is strongly normalizing *)
   Lemma tc_finite_sn x : Irreflexive (tc R) → pred_finite (tc R x) → sn R x.
-- 
GitLab