From c349ec8027412775e2e4f987bbc53a567508dc26 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 12 Jan 2018 13:43:27 -0800
Subject: [PATCH] Add a Notation for `sn`: strongly normalizing.

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

diff --git a/theories/relations.v b/theories/relations.v
index 65b18462..d9e65e5d 100644
--- a/theories/relations.v
+++ b/theories/relations.v
@@ -54,6 +54,9 @@ Section definitions.
     | ex_loop_do_step x y : R x y → ex_loop y → ex_loop x.
 End definitions.
 
+(* Strongly normalizing elements *)
+Notation sn R := (Acc (flip R)).
+
 Hint Unfold nf red.
 
 (** * General theorems *)
-- 
GitLab