add ref to nonlexical

README.md

@@ -36,9 +36,10 @@ Our Coq proof is based on the [RustBelt formalization](https://gitlab.mpi-sws.or
 
 ## Where to find the proofs
 
-- The `BrandedVec` soundness proof is in [`theories/typing/lib/brandedvec.v`](theories/typing/lib/brandedvec.v).
-- The `GhostCell` soundness proof is in [`theories/typing/lib/ghostcell.v`](theories/typing/lib/ghostcell.v).
-- The new version of the "lifetime equalization" rule is `type_equivalize_lft` in [`theories/typing/programs.v`](theories/typing/programs.v).
+- The `BrandedVec` soundness proof (§4.3) is in [`theories/typing/lib/brandedvec.v`](theories/typing/lib/brandedvec.v).
+- The `GhostCell` soundness proof (§4.4) is in [`theories/typing/lib/ghostcell.v`](theories/typing/lib/ghostcell.v).
+- The new version of the "lifetime equalization" rule (§4.2) is `type_equivalize_lft` in [`theories/typing/programs.v`](theories/typing/programs.v).
+  The example that motivated the rule is [`theories/typing/examples/nonlexical.v`](theories/typing/examples/nonlexical.v).
 
 ## Prerequisites