diff --git a/theories/tree_borrows/README.md b/theories/tree_borrows/README.md
index 5a988b7404e3ced19f6af3c9c64c25f72a392984..2f0ac37f0d841f2fa93df386232ceaa8d3dcce94 100644
--- a/theories/tree_borrows/README.md
+++ b/theories/tree_borrows/README.md
@@ -31,19 +31,19 @@ It is subdivided into
 
 Section 5 has three examples, one for deleting reads, one for deleting writes, and one for reordering reads.
 
-### Example 1: Deleting Reads
+### Paragraph 1: Deleting Reads (Example 16)
 
 This example corresponds to the one in  `examples/unprotected/shared_delete_read_escaped.v`.
 The Coq example is very close to the one in the paper.
 The only difference is that `f` has an extra argument in Coq, which corresponds to the implicit environment that closures have in Rust.
 
-### Example 2: Deleting Writes (Optimizing with Protectors)
+### Paragraph 2: Deleting Writes (Optimizing with Protectors) (Example 17)
 
 This example corresponds to the one in `examples/protected/mutable_reorder_write_up_activated_paper.v`.
 This Coq example corresponds very closely to the one in the paper.
 The only difference is that `f` and `g` have an extra argument in Coq, which corresponds to the implicit environment that closures have in Rust.
 
-### Example 3: Reordering Reads
+### Paragraph 3: Reordering Reads (Example 18)
 
 This is proven in `read_read_reorder`, particularly in `refinement.v`.
 These proofs do not use the `simuliris` library, but instead they do a much simpler equivalence proof directly against the operational semantics.
@@ -53,3 +53,15 @@ We suspect that they also hold in a concurrent setting, but this would require d
 Specifically, the extremely simple notion of "equivalence after a few steps" is in `refinement_def.v`.
 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.
+
+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.
+  But note that this does not insert a read if there is none. Also, the tag is not protected.
+* `examples/protected/shared_insert_read.v` demonstrates that reads can be inserted on protected tags.
+
+For the artifact submission, we will create a new example that corresponds to Example 14 more closely.
+
+
diff --git a/theories/tree_borrows/examples/protected/shared_insert_read.v b/theories/tree_borrows/examples/protected/shared_insert_read.v
index 80ecf51378c75eb0ea9ae25696b16a6177b535ad..207ddd866e01dd4ba16851df03b71da73a0749ac 100644
--- a/theories/tree_borrows/examples/protected/shared_insert_read.v
+++ b/theories/tree_borrows/examples/protected/shared_insert_read.v
@@ -112,7 +112,6 @@ Proof.
   sim_pures. simpl. rewrite !subst_result.
 
   source_bind (BinOp _ _ _).
-  Search BinOp.
   iApply source_red_safe_implies. 1: eapply (safe_implies_le r_s (ValR [ScInt 0]%V)%V).
   iIntros ((zres_s & z2 & -> & [= <-])).
   destruct r_t as [[|zres_t []]|]; simpl; try done.
@@ -148,7 +147,7 @@ Proof.
     iIntros "Hc". iEval (rewrite delete_insert) in "Hc".
     sim_apply (EndCall _) (EndCall _) (sim_endcall_own with "Hc") "".
     sim_pures.
-    sim_val. iModIntro. iSplit; first done.
+    sim_val. iModIntro. iSplit; first done. iApply big_sepL2_singleton. done.
 Qed.