diff --git a/README.md b/README.md
index 955f1b967a20e5fb0d31871c3b6d0624840545de..7dbf2b9530dbaac84693f34dfd7b4d54806485e8 100644
--- a/README.md
+++ b/README.md
@@ -61,10 +61,11 @@ followed by `make build-dep`.
 ## Where to Find the Proof Rules From the Paper
 
 The derived rules mentioned in the paper can be found [here](theories/typing/examples/derived_rules.v).
-### Type System Rules
+
+### Type System Rules --- from the RustBelt Paper
 
 The files in [typing](theories/typing) prove semantic versions of the proof
-rules given in the (RustBelt) paper.  Notice that mutable borrows are called
+rules given in the *RustBelt* paper.  Notice that mutable borrows are called
 "unique borrows" in the Coq development.
 
 | Proof Rule            | File            | Lemma                 |