Tree Borrows (done)
Tis is the Tree Borrows development, complete with a formalization of the entire semantics, a bunch of proofs about it, and also example simulation proofs. The examples in particular can be found in theories/tree_borrows/examples
and have a very rudimentary README.md