From 2bcdfc85178b9d0aef2933475587e0f8ec809c7a Mon Sep 17 00:00:00 2001
From: Simcha van Collem <simcha@vancollem.nl>
Date: Tue, 17 Jan 2023 12:58:02 +0100
Subject: [PATCH] Add changelog entry

---
 CHANGELOG.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 16d50c100..3cbf18eb2 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -17,6 +17,8 @@ lemma.
   PROP-level binary relations.
 * Use `binder` in notations for big ops. This means one can write things such
   as `[∗ map] '(k,_) ↦ '(_,y) ∈ m, ⌜ k = y ⌝`.
+* Add a construction `bi_nsteps` to create `n`-step reductions of
+  PROP-level binary relations.
 
 **Changes in `proofmode`:**
 
-- 
GitLab