diff --git a/_CoqProject b/_CoqProject
index 45e51474a7901806c7b5b7e2aefc33f1a3829536..3f81f7a4379372c7686ab9c83670a9ef1daaeae8 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -124,7 +124,7 @@ theories/stacked_borrows/examples/coinductive.v
 
 
 ## Tree Borrows
-theories/tree_borrows/helpers.v
+# theories/tree_borrows/helpers.v
 theories/tree_borrows/locations.v
 theories/tree_borrows/lang_base.v
 theories/tree_borrows/notation.v
@@ -139,7 +139,6 @@ theories/tree_borrows/lang.v
 # Actual Simuliris proof content for TB
 theories/tree_borrows/defs.v
 theories/tree_borrows/steps_foreach.v
-theories/tree_borrows/steps_access.v
 theories/tree_borrows/steps_preserve.v
 theories/tree_borrows/steps_wf.v
 theories/tree_borrows/steps_progress.v
diff --git a/theories/tree_borrows/bor_semantics.v b/theories/tree_borrows/bor_semantics.v
index 4fba6c16f82e56d3c312c8fcca3befd505d196d0..79a8ea91f9592cb8cd8589606343056053108be8 100755
--- a/theories/tree_borrows/bor_semantics.v
+++ b/theories/tree_borrows/bor_semantics.v
@@ -17,7 +17,7 @@ From Equations Require Import Equations.
 From iris.prelude Require Import prelude options.
 From stdpp Require Export gmap.
 
-From simuliris.tree_borrows Require Export lang_base notation tree tree_lemmas.
+From simuliris.tree_borrows Require Export lang_base notation tree  locations.
 From iris.prelude Require Import options.
 
 (*** TREE BORROWS SEMANTICS ---------------------------------------------***)
@@ -995,6 +995,7 @@ Inductive bor_steps trs cids nxtp nxtc
         trs2 cids2 nxtp2 nxtc2
   .
 
+(** Unit test for the tree relation definition, showing how it works *)
 (* conversion is magic *)
 Local Definition unpack_option {A:Type} (o : option A) {oo : A} (Heq : o = Some oo) : A := oo.
 Local Notation unwrap K := (unpack_option K eq_refl).
@@ -1016,6 +1017,8 @@ Local Definition with_three_children :=
 In particular, 4 is a non-immediate child of 1, but all other child relations are immediate.
 
 *)
+
+(** Having constructed the above tree, we can now check that all relations are computed correctly *)
 (* conversion keeps being magical *)
 Succeed Example foo : rel_dec with_three_children 1 1 = Child This                   := eq_refl.
 Succeed Example foo : rel_dec with_three_children 1 2 = Foreign (Parent Immediate)   := eq_refl.
diff --git a/theories/tree_borrows/defs.v b/theories/tree_borrows/defs.v
index e9f1a8c88356f85e1bc8e7e6b9eee179b9dd58a9..8f8c276b9c52a5cf1c98627ad50089adc7a69dbc 100755
--- a/theories/tree_borrows/defs.v
+++ b/theories/tree_borrows/defs.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 From iris.prelude Require Export prelude.
 From simuliris.tree_borrows Require Export tactics notation lang bor_semantics bor_lemmas.
 From iris.prelude Require Import options.
diff --git a/theories/tree_borrows/examples/protected/mutable_reorder_read_down.v b/theories/tree_borrows/examples/protected/mutable_reorder_read_down.v
index 2c49abb349e078eba831d71c4d35adf5aed0a5e7..e9b73792c03fe48031a2e4412c6159bbef2c1524 100755
--- a/theories/tree_borrows/examples/protected/mutable_reorder_read_down.v
+++ b/theories/tree_borrows/examples/protected/mutable_reorder_read_down.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 From simuliris.simulation Require Import lifting.
 From simuliris.tree_borrows Require Import primitive_laws proofmode examples.lib adequacy.
 From iris.prelude Require Import options.
diff --git a/theories/tree_borrows/examples/protected/mutable_reorder_read_up.v b/theories/tree_borrows/examples/protected/mutable_reorder_read_up.v
index 39171b47828256ea4a1109befe0d43dd587da936..fce0c9e8e270429bbd84220c414dfb08e453b6b8 100755
--- a/theories/tree_borrows/examples/protected/mutable_reorder_read_up.v
+++ b/theories/tree_borrows/examples/protected/mutable_reorder_read_up.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 From simuliris.simulation Require Import lifting.
 From simuliris.tree_borrows Require Import primitive_laws proofmode examples.lib adequacy.
 From iris.prelude Require Import options.
diff --git a/theories/tree_borrows/examples/protected/mutable_reorder_write_down_activated.v b/theories/tree_borrows/examples/protected/mutable_reorder_write_down_activated.v
index ae4933d020195ab3cdcf8b3b7736a7e87bf43f0e..1ad1d78a0c40084d8c78bedb8225e2fac12b3437 100755
--- a/theories/tree_borrows/examples/protected/mutable_reorder_write_down_activated.v
+++ b/theories/tree_borrows/examples/protected/mutable_reorder_write_down_activated.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 From simuliris.simulation Require Import lifting.
 From simuliris.tree_borrows Require Import proofmode lang adequacy examples.lib.
 From iris.prelude Require Import options.
diff --git a/theories/tree_borrows/examples/protected/mutable_reorder_write_up_activated.v b/theories/tree_borrows/examples/protected/mutable_reorder_write_up_activated.v
index a12caee72f3fa603437e194c583f7177dd7a106f..5e02c635270619c3bb79bb8bc8fc7066ef6f538a 100755
--- a/theories/tree_borrows/examples/protected/mutable_reorder_write_up_activated.v
+++ b/theories/tree_borrows/examples/protected/mutable_reorder_write_up_activated.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 From simuliris.simulation Require Import lifting.
 From simuliris.tree_borrows Require Import proofmode lang adequacy examples.lib.
 From iris.prelude Require Import options.
diff --git a/theories/tree_borrows/examples/protected/mutable_reorder_write_up_activated_paper.v b/theories/tree_borrows/examples/protected/mutable_reorder_write_up_activated_paper.v
index 78508609a1e3d42d826a5dc1469f68abbd97b9bd..dc7f4e69b3b039d0db18b6b34cd16d9798069600 100644
--- a/theories/tree_borrows/examples/protected/mutable_reorder_write_up_activated_paper.v
+++ b/theories/tree_borrows/examples/protected/mutable_reorder_write_up_activated_paper.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 From simuliris.simulation Require Import lifting.
 From simuliris.tree_borrows Require Import proofmode lang adequacy examples.lib.
 From iris.prelude Require Import options.
diff --git a/theories/tree_borrows/examples/protected/shared_insert_read.v b/theories/tree_borrows/examples/protected/shared_insert_read.v
index 207ddd866e01dd4ba16851df03b71da73a0749ac..3cec5d577ed7ac7c6b53ecefc25e2af5cf44f3e2 100644
--- a/theories/tree_borrows/examples/protected/shared_insert_read.v
+++ b/theories/tree_borrows/examples/protected/shared_insert_read.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 From simuliris.simulation Require Import lifting.
 From simuliris.tree_borrows Require Import proofmode lang adequacy examples.lib.
 From iris.prelude Require Import options.
diff --git a/theories/tree_borrows/examples/protected/shared_reorder_read_down_escaped.v b/theories/tree_borrows/examples/protected/shared_reorder_read_down_escaped.v
index ffa0acf2a0b111dd0b52e550bc1f975f4ce03b54..3aef44004067acdc6c5b7f08314b8a0131faf722 100755
--- a/theories/tree_borrows/examples/protected/shared_reorder_read_down_escaped.v
+++ b/theories/tree_borrows/examples/protected/shared_reorder_read_down_escaped.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 From simuliris.simulation Require Import lifting.
 From simuliris.tree_borrows Require Import proofmode lang examples.lib adequacy.
 From iris.prelude Require Import options.
diff --git a/theories/tree_borrows/examples/protected/shared_reorder_read_up_escaped.v b/theories/tree_borrows/examples/protected/shared_reorder_read_up_escaped.v
index 303d4c545b56d9f6e59da9c2dd145da4ae6d38ec..8b1634f49c80bdd921280aaa8f46ab0980c56fcd 100755
--- a/theories/tree_borrows/examples/protected/shared_reorder_read_up_escaped.v
+++ b/theories/tree_borrows/examples/protected/shared_reorder_read_up_escaped.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 From simuliris.simulation Require Import lifting.
 From simuliris.tree_borrows Require Import proofmode lang adequacy examples.lib.
 From iris.prelude Require Import options.
diff --git a/theories/tree_borrows/examples/unprotected/mutable_delete_read.v b/theories/tree_borrows/examples/unprotected/mutable_delete_read.v
index 910a6bb0662e7849934d8ec4a7c49cfc3172f4d7..09d2f2e22bf5a059e5759761e3bc00fad404f79c 100644
--- a/theories/tree_borrows/examples/unprotected/mutable_delete_read.v
+++ b/theories/tree_borrows/examples/unprotected/mutable_delete_read.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 From simuliris.simulation Require Import lifting.
 From simuliris.tree_borrows Require Import proofmode lang adequacy examples.lib.
 From iris.prelude Require Import options.
diff --git a/theories/tree_borrows/examples/unprotected/shared_delete_read_escaped.v b/theories/tree_borrows/examples/unprotected/shared_delete_read_escaped.v
index 74a81dc45a1bd730d8e20e88c89de17155cd3305..a82d996b26755a7e8dcd3a93fceb49922436a3d3 100644
--- a/theories/tree_borrows/examples/unprotected/shared_delete_read_escaped.v
+++ b/theories/tree_borrows/examples/unprotected/shared_delete_read_escaped.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 From simuliris.simulation Require Import lifting.
 From simuliris.tree_borrows Require Import proofmode lang adequacy examples.lib.
 From iris.prelude Require Import options.
diff --git a/theories/tree_borrows/expr_semantics.v b/theories/tree_borrows/expr_semantics.v
index a2a9728929abd9d309de5c910298f4d44b2fd5f1..d658e9918ce642613c8f19e53596f6b20bf2b110 100755
--- a/theories/tree_borrows/expr_semantics.v
+++ b/theories/tree_borrows/expr_semantics.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 From Equations Require Import Equations.
 From iris.prelude Require Import prelude options.
 From stdpp Require Export gmap.
diff --git a/theories/tree_borrows/helpers.v b/theories/tree_borrows/helpers.v
index 7e2a01e0cc0579c10bdf5637f0f5a769c013fdfa..2da99c05e8514509d13a6dfe80edabc5d135ba84 100755
--- a/theories/tree_borrows/helpers.v
+++ b/theories/tree_borrows/helpers.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 From Coq Require Import ssreflect.
 From stdpp Require Export list gmap.
 From iris.prelude Require Export prelude.
diff --git a/theories/tree_borrows/lang.v b/theories/tree_borrows/lang.v
index 8afd7c3a38c509d4e2f855510de7094379e472a4..89d58619b8e159d3b4a1fdfbe481f498ed87e04e 100755
--- a/theories/tree_borrows/lang.v
+++ b/theories/tree_borrows/lang.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 (** This file manages the interface between the expression semantics and
    the borrow semantics. *)
 
diff --git a/theories/tree_borrows/locations.v b/theories/tree_borrows/locations.v
index b8ce6b0adf40188e1d56183752d0568bbf40a719..c2feb5335b2ffd3f7ad7f971a37e195a028f9ef2 100755
--- a/theories/tree_borrows/locations.v
+++ b/theories/tree_borrows/locations.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 (** Internal representation of memory.
     We opt for a view in which a location is composed of
     an allocation id and an offset into that allocation. *)
diff --git a/theories/tree_borrows/notation.v b/theories/tree_borrows/notation.v
index d150892eccab499efa85dd19633af1e8cd539dd2..d3bb1ec740cb20e421bdc10945651a5e10a48cc9 100755
--- a/theories/tree_borrows/notation.v
+++ b/theories/tree_borrows/notation.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 From iris.prelude Require Import prelude options.
 From simuliris.tree_borrows Require Export lang_base.
 From iris.prelude Require Import options.
diff --git a/theories/tree_borrows/steps_access.v b/theories/tree_borrows/steps_access.v
deleted file mode 100755
index 6d2bad746d47c180ab14a3e1b5bba9afafb4c3d8..0000000000000000000000000000000000000000
--- a/theories/tree_borrows/steps_access.v
+++ /dev/null
@@ -1,109 +0,0 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
-From simuliris.tree_borrows Require Export defs steps_foreach.
-From iris.prelude Require Import options.
-
-Lemma free_mem_lookup l n h :
-  (∀ (i: nat), (i < n)%nat → free_mem l n h !! (l +ₗ i) = None) ∧
-  (∀ (l': loc), (∀ (i: nat), (i < n)%nat → l' ≠ l +ₗ i) →
-    free_mem l n h !! l' = h !! l').
-Proof.
-  revert l. induction n as [|n IH]; intros l; simpl.
-  { split; intros ??; by [lia|]. } split.
-  - intros i Lt. destruct i as [|i].
-    + rewrite shift_loc_0 lookup_delete //.
-    + rewrite lookup_delete_ne.
-      * specialize (IH (l +â‚— 1))as [IH _].
-        rewrite (_: l +â‚— S i = l +â‚— 1 +â‚— i).
-        { apply IH. lia. }
-        { rewrite shift_loc_assoc. f_equal. lia. }
-      * rewrite -{1}(shift_loc_0 l).
-        move => /shift_loc_inj ?. lia.
-  - intros l' Lt.
-    rewrite lookup_delete_ne.
-    + apply IH. intros i Lti.
-      rewrite (_: l +â‚— 1 +â‚— i = l +â‚— S i).
-      * apply Lt. lia.
-      * rewrite shift_loc_assoc. f_equal. lia.
-    + rewrite -(shift_loc_0_nat l). intros ?. subst l'. apply (Lt O); [lia|done].
-Qed.
-
-Lemma free_mem_lookup_case l' l n h :
-  (∀ i : nat, (i < n)%nat → l' ≠ l +ₗ i) ∧ free_mem l n h !! l' = h !! l' ∨
-  ∃ i : nat, (i < n)%nat ∧ l' = l +ₗ i ∧ free_mem l n h !! (l +ₗ i) = None.
-Proof.
-  destruct (free_mem_lookup l n h) as [EQ1 EQ2].
-  destruct (block_case l l' n) as [NEql|Eql].
-  - left. rewrite -EQ2 //.
-  - right. destruct Eql as (i & Lt & ?). exists i. do 2 (split; [done|]).
-    subst l'. by apply EQ1.
-Qed.
-
-Lemma free_mem_dom_inv l' l n h:
-  l' ∈ dom (free_mem l n h) →
-  l' ∈ dom h ∧
-  (∀ i : nat, (i < n)%nat → l' ≠ l +ₗ i) ∧ free_mem l n h !! l' = h !! l'.
-Proof.
-  intros [? EqD]%elem_of_dom.
-  destruct (free_mem_lookup_case l' l n h) as [Eqn|(i & Lt & ? & EqN)].
-  - split; [|done]. apply elem_of_dom. destruct Eqn as [? Eqn].
-    rewrite -Eqn. by eexists.
-  - exfalso. subst l'. by rewrite EqD in EqN.
-Qed.
-
-
-
-Lemma init_mem_lookup_fresh_poison blk off (n:nat) h :
-  0 ≤ off ∧ off < n →
-  init_mem (blk, 0) n h !! (blk, off) = Some ScPoison.
-Proof.
-  intros (Hpos & Hlt).
-  pose proof (init_mem_lookup (blk, 0) n h) as (Hinit1&_).
-  ospecialize (Hinit1 (Z.to_nat off) _); first lia.
-  rewrite /= /shift_loc /= Z.add_0_l Z2Nat.id // in Hinit1.
-Qed.
-
-Lemma init_mem_lookup_fresh_None blk off (n:nat) h :
-  (forall off, (blk, off) ∉ dom h) →
-  (off < 0 ∨ n ≤ off) →
-  init_mem (blk, 0) n h !! (blk, off) = None.
-Proof.
-  intros Hfresh Hout.
-  pose proof (init_mem_lookup (blk, 0) n h) as (_&Hinit2).
-  rewrite (Hinit2 (blk, off)).
-  + eapply not_elem_of_dom, Hfresh.
-  + intros i Hlt.
-    rewrite /= /shift_loc /= Z.add_0_l.
-    intros [= ->]. destruct Hout as [Hout|Hout]; lia.
-Qed.
-
-Lemma init_mem_lookup_fresh_old blk blk' off (n:nat) h :
-  blk ≠ blk' →
-  init_mem (blk, 0) n h !! (blk', off) = h !! (blk', off).
-Proof.
-  intros Hfresh.
-  pose proof (init_mem_lookup (blk, 0) n h) as (_&Hinit2).
-  apply Hinit2.
-  intros ? _ [=]. done.
-Qed.
-
-
-Lemma init_mem_lookup_fresh_inv blk blk' off (n:nat) h k :
-  (forall off, (blk, off) ∉ dom h) →
-  init_mem (blk, 0) n h !! (blk', off) = k →
-  (k = Some ScPoison ∧ blk = blk' ∧ 0 ≤ off ∧ off < n)
-∨ (k = None ∧ blk = blk' ∧ (off < 0 ∨ n ≤ off))
-∨ (k = h !! (blk', off) ∧ blk ≠ blk').
-Proof.
-  intros Hfresh Hinit.
-  destruct (decide (blk = blk')) as [Heqblk|Hne].
-  1: subst blk'; destruct (decide (0 ≤ off)) as [Hpos|Hneg].
-  1: destruct (decide (off < n)) as [Hlt|Hge].
-  { left. subst k. split_and!; try done. by rewrite init_mem_lookup_fresh_poison. }
-  1-2: right; left; split_and!; try done; last lia.
-  1-2: subst k; rewrite init_mem_lookup_fresh_None; try done; lia.
-  { right. right. split; last done. subst k. by apply init_mem_lookup_fresh_old. }
-Qed.
-
diff --git a/theories/tree_borrows/steps_foreach.v b/theories/tree_borrows/steps_foreach.v
index fd2b12066bcc5259093ccdf83fd12d00ddfaabcc..ba77c310d12e413f4beb5df0e52883e99a37a252 100755
--- a/theories/tree_borrows/steps_foreach.v
+++ b/theories/tree_borrows/steps_foreach.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 From simuliris.tree_borrows Require Export defs.
 From iris.prelude Require Import options.
 
@@ -139,3 +135,105 @@ Lemma extend_trees_lookup_ne trs tg off sz blk blk' :
 Proof. apply lookup_insert_ne. Qed.
 
 
+Lemma free_mem_lookup l n h :
+  (∀ (i: nat), (i < n)%nat → free_mem l n h !! (l +ₗ i) = None) ∧
+  (∀ (l': loc), (∀ (i: nat), (i < n)%nat → l' ≠ l +ₗ i) →
+    free_mem l n h !! l' = h !! l').
+Proof.
+  revert l. induction n as [|n IH]; intros l; simpl.
+  { split; intros ??; by [lia|]. } split.
+  - intros i Lt. destruct i as [|i].
+    + rewrite shift_loc_0 lookup_delete //.
+    + rewrite lookup_delete_ne.
+      * specialize (IH (l +â‚— 1))as [IH _].
+        rewrite (_: l +â‚— S i = l +â‚— 1 +â‚— i).
+        { apply IH. lia. }
+        { rewrite shift_loc_assoc. f_equal. lia. }
+      * rewrite -{1}(shift_loc_0 l).
+        move => /shift_loc_inj ?. lia.
+  - intros l' Lt.
+    rewrite lookup_delete_ne.
+    + apply IH. intros i Lti.
+      rewrite (_: l +â‚— 1 +â‚— i = l +â‚— S i).
+      * apply Lt. lia.
+      * rewrite shift_loc_assoc. f_equal. lia.
+    + rewrite -(shift_loc_0_nat l). intros ?. subst l'. apply (Lt O); [lia|done].
+Qed.
+
+Lemma free_mem_lookup_case l' l n h :
+  (∀ i : nat, (i < n)%nat → l' ≠ l +ₗ i) ∧ free_mem l n h !! l' = h !! l' ∨
+  ∃ i : nat, (i < n)%nat ∧ l' = l +ₗ i ∧ free_mem l n h !! (l +ₗ i) = None.
+Proof.
+  destruct (free_mem_lookup l n h) as [EQ1 EQ2].
+  destruct (block_case l l' n) as [NEql|Eql].
+  - left. rewrite -EQ2 //.
+  - right. destruct Eql as (i & Lt & ?). exists i. do 2 (split; [done|]).
+    subst l'. by apply EQ1.
+Qed.
+
+Lemma free_mem_dom_inv l' l n h:
+  l' ∈ dom (free_mem l n h) →
+  l' ∈ dom h ∧
+  (∀ i : nat, (i < n)%nat → l' ≠ l +ₗ i) ∧ free_mem l n h !! l' = h !! l'.
+Proof.
+  intros [? EqD]%elem_of_dom.
+  destruct (free_mem_lookup_case l' l n h) as [Eqn|(i & Lt & ? & EqN)].
+  - split; [|done]. apply elem_of_dom. destruct Eqn as [? Eqn].
+    rewrite -Eqn. by eexists.
+  - exfalso. subst l'. by rewrite EqD in EqN.
+Qed.
+
+
+
+Lemma init_mem_lookup_fresh_poison blk off (n:nat) h :
+  0 ≤ off ∧ off < n →
+  init_mem (blk, 0) n h !! (blk, off) = Some ScPoison.
+Proof.
+  intros (Hpos & Hlt).
+  pose proof (init_mem_lookup (blk, 0) n h) as (Hinit1&_).
+  ospecialize (Hinit1 (Z.to_nat off) _); first lia.
+  rewrite /= /shift_loc /= Z.add_0_l Z2Nat.id // in Hinit1.
+Qed.
+
+Lemma init_mem_lookup_fresh_None blk off (n:nat) h :
+  (forall off, (blk, off) ∉ dom h) →
+  (off < 0 ∨ n ≤ off) →
+  init_mem (blk, 0) n h !! (blk, off) = None.
+Proof.
+  intros Hfresh Hout.
+  pose proof (init_mem_lookup (blk, 0) n h) as (_&Hinit2).
+  rewrite (Hinit2 (blk, off)).
+  + eapply not_elem_of_dom, Hfresh.
+  + intros i Hlt.
+    rewrite /= /shift_loc /= Z.add_0_l.
+    intros [= ->]. destruct Hout as [Hout|Hout]; lia.
+Qed.
+
+Lemma init_mem_lookup_fresh_old blk blk' off (n:nat) h :
+  blk ≠ blk' →
+  init_mem (blk, 0) n h !! (blk', off) = h !! (blk', off).
+Proof.
+  intros Hfresh.
+  pose proof (init_mem_lookup (blk, 0) n h) as (_&Hinit2).
+  apply Hinit2.
+  intros ? _ [=]. done.
+Qed.
+
+
+Lemma init_mem_lookup_fresh_inv blk blk' off (n:nat) h k :
+  (forall off, (blk, off) ∉ dom h) →
+  init_mem (blk, 0) n h !! (blk', off) = k →
+  (k = Some ScPoison ∧ blk = blk' ∧ 0 ≤ off ∧ off < n)
+∨ (k = None ∧ blk = blk' ∧ (off < 0 ∨ n ≤ off))
+∨ (k = h !! (blk', off) ∧ blk ≠ blk').
+Proof.
+  intros Hfresh Hinit.
+  destruct (decide (blk = blk')) as [Heqblk|Hne].
+  1: subst blk'; destruct (decide (0 ≤ off)) as [Hpos|Hneg].
+  1: destruct (decide (off < n)) as [Hlt|Hge].
+  { left. subst k. split_and!; try done. by rewrite init_mem_lookup_fresh_poison. }
+  1-2: right; left; split_and!; try done; last lia.
+  1-2: subst k; rewrite init_mem_lookup_fresh_None; try done; lia.
+  { right. right. split; last done. subst k. by apply init_mem_lookup_fresh_old. }
+Qed.
+
diff --git a/theories/tree_borrows/steps_progress.v b/theories/tree_borrows/steps_progress.v
index 81bacaf5460575cdda5a1456bc599cec6e984bcf..2fca45fb02a394a6fa3773501abffe7e791cbe57 100755
--- a/theories/tree_borrows/steps_progress.v
+++ b/theories/tree_borrows/steps_progress.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-  https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 (** Statements of success conditions for borrow steps.
     The goal is to be able to prove a [bor_step] statement. *)
 
diff --git a/theories/tree_borrows/steps_wf.v b/theories/tree_borrows/steps_wf.v
index d3b65255e4be4b8aabe9d143285927f3a276d597..4a2644ab6123e17c4b61538f4127e5af93f83e03 100755
--- a/theories/tree_borrows/steps_wf.v
+++ b/theories/tree_borrows/steps_wf.v
@@ -1,65 +1,22 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
-https://gitlab.mpi-sws.org/FP/stacked-borrows
-*)
-
 (** The core idea of this file is to prove that all borrow steps preserve
     well-formedness of trees. *)
 
-From simuliris.tree_borrows Require Import helpers.
-From simuliris.tree_borrows Require Export defs steps_foreach steps_access steps_preserve bor_lemmas.
+From simuliris.tree_borrows Require Export defs tree_lemmas steps_foreach steps_preserve bor_lemmas.
 From iris.prelude Require Import options.
 
 (* weird GMAP stuff *)
 
-Lemma gmap_dep_fold_ind_strong {B A P} (f : positive → A → B → B) (Q : B → gmap_dep A P → Prop) (b : B) j :
-  Q b GEmpty →
-  (∀ i p x mt r, gmap.gmap_dep_lookup i mt = None →
-    r = gmap.gmap_dep_fold f j b mt →
-    (∀ B' f' (b':B'), (f' (Pos.reverse_go i j) x (gmap.gmap_dep_fold f' j b' mt)) = gmap.gmap_dep_fold f' j b' (gmap.gmap_dep_partial_alter (λ _, Some x) i p mt)) →
-    Q r mt →
-    Q (f (Pos.reverse_go i j) x r) (gmap.gmap_dep_partial_alter (λ _, Some x) i p mt)) →
-  ∀ mt, Q (gmap.gmap_dep_fold f j b mt) mt.
-Proof.
-  intros Hemp Hinsert mt. revert Q b j Hemp Hinsert.
-  induction mt as [|P ml mx mr ? IHl IHr] using gmap.gmap_dep_ind;
-    intros Q b j Hemp Hinsert; [done|].
-  rewrite gmap.gmap_dep_fold_GNode; try done.
-  apply (IHr (λ y mt, Q y (gmap.GNode ml mx mt))).
-  { apply (IHl (λ y mt, Q y (gmap.GNode mt mx GEmpty))).
-    { destruct mx as [[p x]|]; [|done].
-      replace (gmap.GNode gmap.GEmpty (Some (p,x)) gmap.GEmpty) with
-        (gmap.gmap_dep_partial_alter (λ _, Some x) 1 p gmap.GEmpty) by done.
-      by apply Hinsert. }
-    intros i p x mt r H1 H2 H3 H4.
-    replace (gmap.GNode (gmap.gmap_dep_partial_alter (λ _, Some x) i p mt) mx gmap.GEmpty)
-      with (gmap.gmap_dep_partial_alter (λ _, Some x) (i~0) p (gmap.GNode mt mx gmap.GEmpty))
-      by (by destruct mt, mx as [[]|]).
-    apply Hinsert. 1,4: by rewrite ?gmap.gmap_dep_lookup_GNode.
-    1: by destruct mt, mx as [[]|]; done.
-    intros B' f' b'. destruct mt, mx as [[]|]; simpl in *.
-    1: done. 1: done. all: rewrite H3; by destruct gmap.gmap_dep_ne_partial_alter. }
-  intros i p x mt r H1 H2 H3 H4.
-  replace (gmap.GNode ml mx (gmap.gmap_dep_partial_alter (λ _, Some x) i p mt))
-    with (gmap.gmap_dep_partial_alter (λ _, Some x) (i~1) p (gmap.GNode ml mx mt))
-    by (by destruct ml, mx as [[]|], mt).
-  apply Hinsert. all: rewrite ?gmap.gmap_dep_lookup_GNode; try done.
-  1: destruct ml, mx as [[]|], mt; simpl in *; done.
-  intros B' f' b'. destruct ml, mx as [[]|], mt; simpl in *.
-  1,3,5,7: done. all: rewrite H3; by destruct gmap.gmap_dep_ne_partial_alter.
-Qed.
 
 Lemma map_fold_ind_strong {K V B} `{Countable K} (P : B → gmap K V → Prop) (f : K → V → B → B) (b:B) (M : gmap K V) :
   P b ∅ →
   (∀ k v M, M !! k = None → (∀ B' f' (b':B'), map_fold f' b' (<[k:=v]> M) = f' k v (map_fold f' b' M)) → P (map_fold f b M) M → P (f k v (map_fold f b M)) (<[k:=v]> M)) →
   P (map_fold f b M) M.
 Proof.
-  intros H1 H2. destruct M as [M]. rewrite /map_fold /=.
-  apply (gmap_dep_fold_ind_strong _ (λ r M, P r (GMap M))); clear M; [done|].
-  intros i [Hk] x mt r H0 -> H3; simpl. destruct (fmap_Some_1 _ _ _ Hk) as (k&Hk1&Hk2). subst i.
-  rewrite Hk1.
-  assert (GMapKey Hk = gmap_key_encode k) as Hk3 by (apply proof_irrel). rewrite Hk3.
-  apply (H2 _ _ (GMap mt)). 1: done.
-  intros ???. simpl. rewrite /map_fold /gmap_fold /= -Hk3 -H3 /= Hk1 //.
+  intros Hbase Hstep. eapply (map_first_key_ind (fun mm => P (map_fold f b mm) mm)).
+  - rewrite map_fold_empty. apply Hbase.
+  - intros k v m Hnone Hfirstkey HIH.
+    rewrite map_fold_insert_first_key //. eapply Hstep; [done| |done].
+    intros B' f' b'. rewrite map_fold_insert_first_key //.
 Qed.
 
 
diff --git a/theories/tree_borrows/tkmap_view.v b/theories/tree_borrows/tkmap_view.v
index 0e0ff2801fa6e29b670d1f92f10150a5abf17e93..51c4c5fcfbc198490db1be440dd50398e5b3f091 100755
--- a/theories/tree_borrows/tkmap_view.v
+++ b/theories/tree_borrows/tkmap_view.v
@@ -1,7 +1,3 @@
-(** This file has been adapted from the Iris development, available at 
-  https://gitlab.mpi-sws.org/iris/iris
-*)
-
 From Coq.QArith Require Import Qcanon.
 From iris.algebra Require Export view gmap frac dfrac.
 From iris.algebra Require Import local_updates proofmode_classes big_op.
@@ -13,10 +9,10 @@ From simuliris.tree_borrows Require Export defs.
 (gmap_view has since been updated so we could now use it directly, but this code predates the generalized gmap_view for arbitrary CRMA.) *)
 
 (* Currently, we place a strong restriction on the shape of a location's stack:
-  A tag can be of one of two kinds:
+  A tag can be of one of several kinds:
   - tk_pub: the tag is public (can be shared, assertion is persistent)
-  - tk_unq: the tag is unique (cannot be shared, assertion is not persistent).
-  - tk_loc: the tag is local
+  - tk_unq: the tag is unique (cannot be shared, assertion is not persistent). This is further parameterized by whether it is reserved or activated.
+  - tk_loc: the tag is local (a local variable whose address has not been taken)
  *)
 
 Definition tagKindR := csumR (exclR unitO) (csumR (csumR (exclR unitO) (exclR unitO)) unitR).
diff --git a/theories/tree_borrows/tree_lemmas.v b/theories/tree_borrows/tree_lemmas.v
index b0470ca7cc6f46af96a3b25c25fa87215563e2ad..2eb5bf0dba6bb863eb05af30d48ef3974bae97b1 100644
--- a/theories/tree_borrows/tree_lemmas.v
+++ b/theories/tree_borrows/tree_lemmas.v
@@ -1,7 +1,7 @@
 From Equations Require Import Equations.
 From iris.prelude Require Import prelude options.
 From stdpp Require Export gmap.
-From simuliris.tree_borrows Require Export lang_base notation tree.
+From simuliris.tree_borrows Require Export tree.
 From iris.prelude Require Import options.
 
 Implicit Type (V W X Y:Type).
@@ -246,42 +246,6 @@ Proof.
     all: simpl; auto.
 Qed.
 
-(*
-Lemma exists_child_transitive {X} (search search':Tprop X) :
-  forall tr,
-  exists_node search tr ->
-  tree_AtNode search (tree_ChildExists search') tr ->
-  exists_node search' tr.
-Proof.
-  intros tr Exists Search.
-  induction tr; simpl; auto.
-  destruct Search as [Search0 [Search1 Search2]].
-  destruct Exists as [Exists0 | [Exists1 | Exists2]]; auto.
-  destruct (Search0 Exists0); auto.
-Qed.
-
-Lemma AtNodeExists_transitive {X} (search search' search'':Tprop X) :
-  forall tr,
-  tree_AtNode search (tree_ChildExists search') tr ->
-  tree_AtNode search' (tree_ChildExists search'') tr ->
-  tree_AtNode search (tree_ChildExists search'') tr.
-Proof.
-  intros tr Search Search'.
-  induction tr; auto.
-  destruct Search' as [Search' [Search'1 Search'2]].
-  destruct Search as [Search [Search1 Search2]].
-  pose Found1 := (IHtr1 Search1 Search'1).
-  pose Found2 := (IHtr2 Search2 Search'2).
-  simpl; try repeat split; auto.
-  clear Found1; clear Found2; clear IHtr1; clear IHtr2.
-  intro Found; destruct (Search Found) as [Found' | FoundSub].
-  - destruct (Search' Found') as [Found'' | Found'Sub]; auto.
-  - right; clear Found; clear Search; clear Search1; clear Search2.
-    clear Search'.
-    apply (ExistsAtNode_transitive search'); auto.
-Qed.
-*)
-
 Lemma insert_true_preserves_every {X} (tr:tree X) (ins:X) (search prop:X -> Prop)
   {search_dec:forall x, Decision (search x)} :
   prop ins ->
@@ -370,21 +334,6 @@ Proof.
     * right; right; auto.
 Qed.
 
-(*
-Lemma insert_preserves_ChildExists {X} (ins:X) (tr:tree X) (search prop:Tprop X)
-  {search_dec:forall x, Decision (search x)} :
-  tree_ChildExists prop tr -> tree_ChildExists prop (insert_child_at tr ins search).
-Proof.
-  intro Exists.
-  destruct tr; simpl; auto.
-  destruct (decide (search data)) eqn:Found; simpl; auto.
-  all: simpl in Exists.
-  all: inversion Exists as [Ex0 | Ex2]; auto.
-  1: right; right; left; apply insert_preserves_Exists; auto.
-  right; apply insert_preserves_Exists; auto.
-Qed.
-*)
-
 Lemma exists_insert_requires_parent {X} (ins:X) (search prop:X -> Prop)
   {search_dec:forall x, Decision (search x)} :
   forall tr,
@@ -414,7 +363,7 @@ Proof.
   right; right. destruct Hyp2 as [Contra | [Hyp2Sub | Hyp2Empty]]; auto; contradiction.
 Qed.
 
-Lemma exists_subtree_transitive br prop (tr:tree item) :
+Lemma exists_subtree_transitive T br prop (tr:tree T) :
   exists_subtree (eq br) tr ->
   exists_subtree prop (of_branch br) ->
   exists_subtree prop tr.
@@ -428,7 +377,7 @@ Proof.
   - right; right. apply IHtr2; auto.
 Qed.
 
-Lemma every_subtree_transitive br prop (tr:tree item) :
+Lemma every_subtree_transitive T br prop (tr:tree T) :
   every_subtree (eq br) tr ->
   every_subtree prop (of_branch br) ->
   every_subtree prop tr.
@@ -442,7 +391,7 @@ Proof.
   try repeat split; auto.
 Qed.
 
-Lemma exists_node_transitive br prop (tr:tree item) :
+Lemma exists_node_transitive T br prop (tr:tree T) :
   exists_subtree (eq br) tr ->
   exists_node prop (of_branch br) ->
   exists_node prop tr.
diff --git a/theories/tree_borrows/trees_equal/disabled_in_practice.v b/theories/tree_borrows/trees_equal/disabled_in_practice.v
index 6bdb6d5be7b7c86b38b420d876dc78bc07ac225b..9e635cd1f8421b380ce331273814b6a179e8e6d6 100644
--- a/theories/tree_borrows/trees_equal/disabled_in_practice.v
+++ b/theories/tree_borrows/trees_equal/disabled_in_practice.v
@@ -1,4 +1,3 @@
-(** This file provides the basic heap and ghost state support for the BorIngLang program logic. *)
 From iris.proofmode Require Export proofmode.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Import ghost_map.
diff --git a/theories/tree_borrows/trees_equal/random_lemmas.v b/theories/tree_borrows/trees_equal/random_lemmas.v
index 2ae7810b9c3f77f44e3e840ff79dc49c4bccf5de..7abccdfb6156b37c222dffa7f93d225eb1ef9d17 100644
--- a/theories/tree_borrows/trees_equal/random_lemmas.v
+++ b/theories/tree_borrows/trees_equal/random_lemmas.v
@@ -1,4 +1,3 @@
-(** This file provides the basic heap and ghost state support for the BorIngLang program logic. *)
 From iris.proofmode Require Export proofmode.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Import ghost_map.
diff --git a/theories/tree_borrows/trees_equal/trees_equal_asymmetric_prot.v b/theories/tree_borrows/trees_equal/trees_equal_asymmetric_prot.v
index f4342eef16da2065a05ebbe7709ce3116cdbde9a..4c081cee9ea29cae84d8ad35909e3f13d5f2c98b 100644
--- a/theories/tree_borrows/trees_equal/trees_equal_asymmetric_prot.v
+++ b/theories/tree_borrows/trees_equal/trees_equal_asymmetric_prot.v
@@ -1,4 +1,3 @@
-(** This file provides the basic heap and ghost state support for the BorIngLang program logic. *)
 From iris.proofmode Require Export proofmode.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Import ghost_map.
diff --git a/theories/tree_borrows/trees_equal/trees_equal_base.v b/theories/tree_borrows/trees_equal/trees_equal_base.v
index 4ac52f8d45b42a4b6e1305e16f2ff27ad1991aae..8c0500b124be830ac4cdacea099a18cd0f9b5ee2 100644
--- a/theories/tree_borrows/trees_equal/trees_equal_base.v
+++ b/theories/tree_borrows/trees_equal/trees_equal_base.v
@@ -1,4 +1,3 @@
-(** This file provides the basic heap and ghost state support for the BorIngLang program logic. *)
 From iris.proofmode Require Export proofmode.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Import ghost_map.
diff --git a/theories/tree_borrows/trees_equal/trees_equal_create_child.v b/theories/tree_borrows/trees_equal/trees_equal_create_child.v
index efda218a3529877b9e0dd1b0234ad267a0427c9d..e9b0cb19f1bc003a73078ae1cd4fdca4bdffb7d2 100644
--- a/theories/tree_borrows/trees_equal/trees_equal_create_child.v
+++ b/theories/tree_borrows/trees_equal/trees_equal_create_child.v
@@ -1,4 +1,3 @@
-(** This file provides the basic heap and ghost state support for the BorIngLang program logic. *)
 From iris.proofmode Require Export proofmode.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Import ghost_map.
diff --git a/theories/tree_borrows/trees_equal/trees_equal_initcall.v b/theories/tree_borrows/trees_equal/trees_equal_initcall.v
index 10c03dc2a07980a59bfd05ace6a18233c74f27e0..dbb1a8883e64b0edec994a08f1d8ac561a6bf9f8 100644
--- a/theories/tree_borrows/trees_equal/trees_equal_initcall.v
+++ b/theories/tree_borrows/trees_equal/trees_equal_initcall.v
@@ -1,4 +1,3 @@
-(** This file provides the basic heap and ghost state support for the BorIngLang program logic. *)
 From iris.proofmode Require Export proofmode.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Import ghost_map.
diff --git a/theories/tree_borrows/trees_equal/trees_equal_more_access.v b/theories/tree_borrows/trees_equal/trees_equal_more_access.v
index d8fb9630ef27122c61f72c1ecc18a58a046d5372..c6382850a64bdd89baf2278335d4c907b355eff6 100644
--- a/theories/tree_borrows/trees_equal/trees_equal_more_access.v
+++ b/theories/tree_borrows/trees_equal/trees_equal_more_access.v
@@ -1,4 +1,3 @@
-(** This file provides the basic heap and ghost state support for the BorIngLang program logic. *)
 From iris.proofmode Require Export proofmode.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Import ghost_map.
diff --git a/theories/tree_borrows/trees_equal/trees_equal_preserved_by_access.v b/theories/tree_borrows/trees_equal/trees_equal_preserved_by_access.v
index d2124075c6e30fa030a41fadd7c12b69ef42bc22..17f81ed1504a5cdc633a37573a81fa16d6881295 100644
--- a/theories/tree_borrows/trees_equal/trees_equal_preserved_by_access.v
+++ b/theories/tree_borrows/trees_equal/trees_equal_preserved_by_access.v
@@ -1,4 +1,3 @@
-(** This file provides the basic heap and ghost state support for the BorIngLang program logic. *)
 From iris.proofmode Require Export proofmode.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Import ghost_map.
diff --git a/theories/tree_borrows/trees_equal/trees_equal_preserved_by_access_base.v b/theories/tree_borrows/trees_equal/trees_equal_preserved_by_access_base.v
index f02f2c20014b2bf6da714498562f32f58fdef076..b0e6444ac195c68aa5e2388e026fb0e21db827f4 100644
--- a/theories/tree_borrows/trees_equal/trees_equal_preserved_by_access_base.v
+++ b/theories/tree_borrows/trees_equal/trees_equal_preserved_by_access_base.v
@@ -1,4 +1,3 @@
-(** This file provides the basic heap and ghost state support for the BorIngLang program logic. *)
 From iris.proofmode Require Export proofmode.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Import ghost_map.
diff --git a/theories/tree_borrows/trees_equal/trees_equal_source_read.v b/theories/tree_borrows/trees_equal/trees_equal_source_read.v
index 0cbe36a418b5355dfe3a48e6c8dc13e9145e1410..902f3963a39d6c7d82c09ac2b1c1742a1f2ff956 100644
--- a/theories/tree_borrows/trees_equal/trees_equal_source_read.v
+++ b/theories/tree_borrows/trees_equal/trees_equal_source_read.v
@@ -1,4 +1,3 @@
-(** This file provides the basic heap and ghost state support for the BorIngLang program logic. *)
 From iris.proofmode Require Export proofmode.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Import ghost_map.
diff --git a/theories/tree_borrows/trees_equal/trees_equal_transitivity.v b/theories/tree_borrows/trees_equal/trees_equal_transitivity.v
index e619696acc9458f641c9d303cf1203cc351b2e46..9ebf91f1563912994ba5254b1856bdab590e27cc 100644
--- a/theories/tree_borrows/trees_equal/trees_equal_transitivity.v
+++ b/theories/tree_borrows/trees_equal/trees_equal_transitivity.v
@@ -1,4 +1,3 @@
-(** This file provides the basic heap and ghost state support for the BorIngLang program logic. *)
 From iris.proofmode Require Export proofmode.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Import ghost_map.