diff --git a/theories/tree_borrows/README.md b/theories/tree_borrows/README.md
index c984d8a191dc73737ad61a3ef212e710b3655e2d..3ba9ba335715f28e1d209be5ef6c49bd718f6adb 100644
--- a/theories/tree_borrows/README.md
+++ b/theories/tree_borrows/README.md
@@ -149,7 +149,7 @@ This program logic can prove refinements, and uses several separation logic reso
 You can see the separation logic in action in the examples shown above.
 Here, we explain the resources that you will encounter when stepping through the proof.
 
-The `$$` resource associates a "tag" with a "tag kind." Remember that each tag corresponds to a specific node in the borrow tree.
+The `t $$ tk` resource associates a "tag" `t` with a "tag kind" `tk`. Remember that each tag corresponds to a specific node in the borrow tree.
 The tag kind is a very coarse over-approximation of the shape of the tree from that specific node.
 
 The simplest kind is `tk_local`, which says that the tree here is a singleton, and this tag is the only tag in the tree.