From 7ecb64e6cb38f3ec4b82e0726c094d6ef8c408ac Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Tue, 21 Jul 2020 18:38:14 +0200
Subject: [PATCH] Tweak docs of tc_finite_sn.
---
theories/relations.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/relations.v b/theories/relations.v
index 56e257a9..32522c05 100644
--- a/theories/relations.v
+++ b/theories/relations.v
@@ -280,8 +280,8 @@ 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.
- (** An acyclic relation that can only take finitely many steps is strongly
- normalizing *)
+ (** 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.
Proof.
intros Hirr [xs Hfin]. remember (length xs) as n eqn:Hn.
--
GitLab