Ongoing Tree Borrows development

This is work on Tree Borrows that has been going on in https://gitlab.mpi-sws.org/neven/simuliris then https://gitlab.mpi-sws.org/iris/simuliris/-/tree/ci/tree-borrows?ref_type=heads.

From now on the reference for the Coq development should be in master.