From 83ecef0f7960d62b5b9045197e628e58483cf781 Mon Sep 17 00:00:00 2001
From: Johannes Hostert <jhostert@ethz.ch>
Date: Fri, 15 Nov 2024 10:28:38 +0100
Subject: [PATCH] whoops example 1 is a different file

---
 theories/tree_borrows/README.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/tree_borrows/README.md b/theories/tree_borrows/README.md
index b9460154..2579f9db 100644
--- a/theories/tree_borrows/README.md
+++ b/theories/tree_borrows/README.md
@@ -55,7 +55,8 @@ The proof that the two reads can be reordered is in `read_reorder.v`.
 The file `low_level.v` contains low-level lemmas used in `read_reorder.v`
 
 ### Other Examples From The Paper
-Example 1 is subsumed by Example 16, if one instantiates the unknown code properly.
+Example 1 is similar to the one shown in `examples/unprotected/mutable_delete_read.v`.
+The one shown in Coq has two places where arbitrary unknown functions are called, and Example 1 is just a special case of that, if one instantiates these unknown functions correctly.
 
 We have not shown Example 14, but two examples similar to it:
 * `examples/unprotected/shared_delete_read_escaped_coinductive.v` demonstrates reasoning in a loop.
-- 
GitLab