From 1e2df25ee773706dcb1984f1db654ca5014c791a Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Thu, 4 Nov 2021 23:57:08 +0100
Subject: [PATCH] CHANGELOG

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index be362899..ee1ebd37 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -170,6 +170,10 @@ API-breaking change is listed.
   slightly weaker in case the left-hand side and right-hand side of the relation
   call a function with arguments that are convertible but not syntactically
   equal.
+- Add lemma `choose_proper` showing that `choose P` respects predicate
+  equivalence. (by Paolo G. Giarrusso, BedRock Systems)
+- Well-founded definitions: Add induction principle `Acc_dep_ind`, a dependent
+  version of `Acc_ind`. (by Paolo G. Giarrusso, BedRock Systems)
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
-- 
GitLab