diff --git a/theories/tree_borrows/bor_lemmas.v b/theories/tree_borrows/bor_lemmas.v
index 259269314005933e20baed9bc6bd5256e0303357..61f6e6877f97cf2c58fc397930a8711a8e8a27e8 100644
--- a/theories/tree_borrows/bor_lemmas.v
+++ b/theories/tree_borrows/bor_lemmas.v
@@ -868,7 +868,6 @@ Proof.
     exists br2. split; [|assumption]. right; right; assumption.
 Qed.
 
-(* FIXME: these proofs ane absolutely horrible, refactor them. *)
 Lemma unique_only_one_subtree
   {tr tg br1 br2} :
   tree_unique tg tr ->
diff --git a/theories/tree_borrows/bor_semantics.v b/theories/tree_borrows/bor_semantics.v
index 3ca74fe0a904bf06403a7c8c70e94d6a733a5d25..1c7d4a6929175b32a2558a644c355989ea3fac88 100755
--- a/theories/tree_borrows/bor_semantics.v
+++ b/theories/tree_borrows/bor_semantics.v
@@ -351,7 +351,6 @@ Definition apply_access_perm_inner (kind:access_kind) (rel:rel_pos) (isprot:bool
   | AccessRead, Foreign _ =>
       (* Foreign read. Makes [Reserved] conflicted, freezes [Active]. *)
       match perm with
-        (* FIXME: refactor *)
       | Reserved ResActivable => Some (Reserved (if isprot then ResConflicted else ResActivable))
       | Active => if isprot then
         (* So that the function is commutative on all states and not just on reachable states,
@@ -364,7 +363,7 @@ Definition apply_access_perm_inner (kind:access_kind) (rel:rel_pos) (isprot:bool
   | AccessWrite, Foreign _ =>
       (* Foreign write. Disables everything except interior mutable [Reserved]. *)
       match perm with
-      (* TODO: remove -- this can never happen, but having it simplifies theorems. *)
+      (* NOTE: this can never happen, but having it simplifies theorems. *)
       | ReservedIM => if isprot then Some Disabled else Some $ ReservedIM
       | Disabled => Some Disabled
       | _ => Some Disabled
@@ -401,11 +400,6 @@ Definition protector_is_for_call c prot := call_of_protector prot = Some c.
 Global Instance protector_is_for_call_dec c prot : Decision (protector_is_for_call c prot).
 Proof. rewrite /protector_is_for_call /call_of_protector. case_match; [case_match|]; solve_decision. Defined.
 
-(* FIXME: This definition overlaps with logical_state.v:protected_by
-   We should pick one of them. If we pick this one it should be simplified
-   to match prot with Some (mkProtector _ c) => c in cids | None => False end.
-
-   In practice: delete [protector_is_active]. rename [witness_protector_is_active]. fix proofs. *)
 Definition protector_is_active prot cids :=
   exists c, protector_is_for_call c prot /\ call_is_active c cids.
 
@@ -767,7 +761,7 @@ Definition trees_unique tg trs blk it :=
 Definition ParentChildInBlk tg tg' trs blk :=
   trees_at_block (ParentChildIn tg tg') trs blk.
 
-(* FIXME: order of args *)
+(* FIXME: Improve consistency of argument ordering *)
 
 (** Reborrow *)
 
@@ -859,7 +853,9 @@ Definition tree_access_all_protected_initialized (cids : call_id_set) (cid : nat
     (* finally we can combine this all *)
     set_fold (fun '(tg, init_locs) (tr:option (tree item)) => tr ← tr; reader_locs tg init_locs tr) (Some tr) init_locs.
 
-(* FIXME: IMPORTANT: don't make the access visible to children ! *)
+(* WARNING: don't make the access visible to children !
+    You can check in `trees_access_all_protected_initialized` that we properly use
+    `memory_access_nonchildren_only`. *)
 (* Finally we read all protected initialized locations on the entire trees by folding it
    for each tree separately.
    NOTE: be careful about how other properties assume the uniqueness of tags intra- and inter- trees,
@@ -875,7 +871,7 @@ Inductive bor_step (trs : trees) (cids : call_id_set) (nxtp : nat) (nxtc : call_
   : event -> trees -> call_id_set -> nat -> call_id -> Prop :=
   | AllocIS (blk : block) (off : Z) (sz : nat)
     (FRESH : trs !! blk = None)
-    (NONZERO : (sz > 0)%nat) : (* FIXME: should we have an event for zero-size allocations ? *)
+    (NONZERO : (sz > 0)%nat) :
     bor_step
       trs cids nxtp nxtc
       (AllocEvt blk nxtp (off, sz))
@@ -926,7 +922,6 @@ Inductive bor_step (trs : trees) (cids : call_id_set) (nxtp : nat) (nxtc : call_
                We want to do the read *after* the insertion so that it properly initializes the locations of the range. *)
     (EL: cid ∈ cids)
     (EXISTS_TAG: trees_contain parentt trs alloc)
-    (* TODO get rid of fresh_child assumption here *)
     (FRESH_CHILD: ~trees_contain nxtp trs alloc)
     (RETAG_EFFECT: apply_within_trees (create_child cids parentt nxtp pk im rk cid) alloc trs = Some trs')
     (READ_ON_REBOR: apply_within_trees (memory_access AccessRead cids nxtp range) alloc trs' = Some trs'') :
diff --git a/theories/tree_borrows/defs.v b/theories/tree_borrows/defs.v
index 4cd1a08e23c98fc10ecc2194fce41e9b52823a0a..bb15bd950d338a5d31e96a995034fed884946340 100755
--- a/theories/tree_borrows/defs.v
+++ b/theories/tree_borrows/defs.v
@@ -45,9 +45,8 @@ Definition tree_items_unique (tr:tree item) :=
 
 Definition tree_items_compat_nexts (tr:tree item) (nxtp:tag) (nxtc: call_id) :=
   every_node (λ it, item_wf it nxtp nxtc) tr.
-  (* FIXME: rename above to just tree_items_wf *)
+  (* FIXME: Improve consistency of naming conventions *)
 
-(* FIXME: consistent naming *)
 Definition wf_tree (tr:tree item) :=
   tree_items_unique tr.
 Definition each_tree_wf (trs:trees) :=
@@ -83,9 +82,8 @@ Definition wf_scalar t sc := ∀ t' l, sc = ScPtr l t' → t' < t.
 Definition same_blocks (hp:mem) (trs:trees) :=
   dom trs =@{gset _} set_map fst (dom hp).
 Arguments same_blocks / _ _.
-(* OLD: forall blk l, is_Some (hp !! (blk, l)) -> is_Some (trs !! blk). *)
-(* FIXME: map fst (dom hp) === dom trs *)
-(* FIXME: forall blk, (exists l, is_Some (hp !! (blk, l))) <-> is_Some (trs !! blk). *)
+(* Formerly: map fst (dom hp) === dom trs
+   However this is no longer accurate. *)
 
 Definition root_invariant blk it (shp : mem) :=
   it.(iprot) = None ∧ it.(initp) = Disabled ∧
@@ -103,21 +101,19 @@ Definition tree_roots_compatible (trs : trees) shp :=
 
 
 Record state_wf (s: state) := {
-  (*state_wf_dom : dom s.(shp) ≡ dom s.(strs); Do we care ? After all TB is very permissive about the range, so out-of-bounds UB is *always* triggered at the level of the heap, not the trees *)
+  (*state_wf_dom : dom s.(shp) ≡ dom s.(strs);
+     This was included in SB but we don't care anymore because TB
+     is very permissive about the range so out-of-bounds UB is *always*
+     triggered by `expr_semantics` not `bor_semantics`. *)
   state_wf_dom : same_blocks s.(shp) s.(strs);
-  (*state_wf_mem_tag : wf_mem_tag s.(shp) s.(snp);*) (* FIXME: this seems to state that all pointers are wf, it should be included *)
   state_wf_tree_unq : wf_trees s.(strs);
   state_wf_tree_more_init : each_tree_parents_more_init s.(strs);
   state_wf_tree_more_active : each_tree_parents_more_active s.(strs);
   state_wf_tree_not_disabled :  each_tree_protected_parents_not_disabled s.(scs) s.(strs);
   state_wf_tree_no_active_cousins : each_tree_no_active_cousins s.(scs) s.(strs);
   state_wf_tree_compat : trees_compat_nexts s.(strs) s.(snp) s.(snc);
-  (* state_wf_non_empty : wf_non_empty s.(strs); *)
   state_wf_roots_active : tree_roots_compatible s.(strs) s.(shp);
-  (*state_wf_cid_no_dup : NoDup s.(scs) ;*) (* FIXME: call ids are unique, include this *)
   state_wf_cid_agree: wf_cid_incl s.(scs) s.(snc);
-  (* state_wf_cid_non_empty : s.(scs) ≠ []; *)
-  (* state_wf_no_dup : wf_no_dup σ.(cst).(sst); *)
 }.
 
 Definition init_state := (mkState ∅ ∅ {[O]} O 1).
diff --git a/theories/tree_borrows/early_proofmode.v b/theories/tree_borrows/early_proofmode.v
index ac921fdaef4c191c6a4230a9ed01fef989219f35..d97906d38bd76ae1322b0102aacb3dde182d1fa2 100644
--- a/theories/tree_borrows/early_proofmode.v
+++ b/theories/tree_borrows/early_proofmode.v
@@ -378,7 +378,6 @@ Ltac sim_val := sim_finish; sim_result_head.
 
 (** ** Pure reduction *)
 Ltac solve_pure_sidecond :=
-  (*TODO: have tactic adapted to our instances *)
   fast_done || (left; fast_done) || (right; fast_done).
 
 (** The argument [efoc] can be used to specify the construct that should be
diff --git a/theories/tree_borrows/expr_semantics.v b/theories/tree_borrows/expr_semantics.v
index 2c95b010d4e274facbda4f9017743d9a527008db..08c034546b33a9a0a5a2c350b91bebbaf4f31948 100755
--- a/theories/tree_borrows/expr_semantics.v
+++ b/theories/tree_borrows/expr_semantics.v
@@ -465,15 +465,9 @@ Inductive pure_expr_step (P : prog) (h : mem) : expr → expr → list expr →
     pure_expr_step P h (Conc (Val v1) (Val v2))
                        (Val (v1 ++ v2)) []
 | RefPS l lbor T :
-    (* is_Some (h !! l) → *)
     pure_expr_step P h (Ref (Place l lbor T)) #[ScPtr l lbor] []
-| DerefPS l lbor T
-    (* (DEFINED: ∀ (i: nat), (i < tsize T)%nat → l +ₗ i ∈ dom h) *) :
+| DerefPS l lbor T :
     pure_expr_step P h (Deref #[ScPtr l lbor] T) (Place l lbor T) []
-(* | FieldBS l lbor T path off T'
-    (FIELD: field_access T path = Some (off, T')) :
-    pure_expr_step FNs h (Field (Place l lbor T) path)
-                         SilentEvt (Place (l +â‚— off) lbor T') *)
 | LetPS x e1 e2 e' :
     is_Some (to_result e1) →
     subst' x e1 e2 = e' →
@@ -506,7 +500,9 @@ Inductive mem_expr_step (h: mem) : expr → event → mem → expr → list expr
 | CopyBS blk l lbor sz (v: value)
     (READ: read_mem (blk, l) sz h = Some v) :
     mem_expr_step h (Copy (Place (blk, l) lbor sz)) (CopyEvt blk lbor (l, sz) v) h (Val v) []
-(*| FailedCopyBS blk l lbor sz
+(* This was a poison semantics for failing reads. We have removed this to be
+   closer to the actual semantics described in Tree Borrows.
+  | FailedCopyBS blk l lbor sz
     (READ: is_Some (read_mem (blk, l) sz h)) : 
     (* failed copies lead to poison, but still of the appropriate length *)
     mem_expr_step h (Copy (Place (blk, l) lbor sz)) (FailedCopyEvt blk lbor (l, sz)) h (Val $ replicate sz ScPoison) []*)
@@ -524,17 +520,17 @@ Inductive mem_expr_step (h: mem) : expr → event → mem → expr → list expr
               (AllocEvt blk lbor (0, sz))
               (init_mem (blk, 0) sz h) (Place (blk, 0) lbor sz) []
 | DeallocBS blk l (sz:nat) lbor :
-    (* FIXME: l here is an offset. But we usually want to deallocate at offset 0, right? *)
-    (* FIXME: This is wrong because it allows double-free of zero-sized allocations
-              Possible solutions:
-              - Change the heap from `gmap loc scalar` to `gmap blk (gmap Z scalar)`
-              - Require `sz > 0`      <- probably this
-              - special case for TB where if the size is zero we don't add a new tree
+    (* WARNING: If we are not careful here, it could allow double-free of zero-sized allocations.
+       Possible solutions that we have considered include
+       - changing the heap from `gmap loc scalar` to `gmap blk (gmap Z scalar)`
+       - requiring `sz . 0`
+       - having a special case for TB where if the size is zero we don't add a new tree.
+
+       We go for the second one and forbid zero-sized allocations, at the level of
+       `AllocIS` in `bor_semantics`.
+       FIXME: We could potentially be able to actually *prove* here that `sz > 0`
+       if we added this to `state_wf`. Until then it is UB to deallocate a zero-sized.
     *)
-    (* Actual solution: We forbid zero-sized allocations (see AllocIS in bor_semantics).
-       If we track that in state_wf, we should be able to prove that sz > 0 here,
-       instead of making it UB.
-       TODO actually add it to state_wf, until then it is UB *)
     (sz > 0)%nat →
     (∀ m, is_Some (h !! ((blk,l) +ₗ m)) ↔ 0 ≤ m < sz) →
     mem_expr_step
diff --git a/theories/tree_borrows/lang_base.v b/theories/tree_borrows/lang_base.v
index d621d0ad06d55cc1a327d58e5d039745f1d44ddb..9097539f3e59931359229466075f73e09a40bf24 100755
--- a/theories/tree_borrows/lang_base.v
+++ b/theories/tree_borrows/lang_base.v
@@ -191,7 +191,6 @@ Definition item_lookup (it : item) (l : Z) :=
 Definition trees := gmap block (tree item).
 
 (** Retag kinds *)
-(* FIXME: simplify related stuff *)
 Inductive retag_kind := FnEntry | Default.
 
 (** Language base constructs *)
diff --git a/theories/tree_borrows/logical_state.v b/theories/tree_borrows/logical_state.v
index 32c71941b929307fa65c319f9f3548909f216f0e..6aeab0bfccf7cd515c592ef70dc1979a5d098206 100755
--- a/theories/tree_borrows/logical_state.v
+++ b/theories/tree_borrows/logical_state.v
@@ -393,13 +393,12 @@ Section heap_defs.
                    ∧ ((item_lookup it l.2).(initialized) = PermInit → (item_lookup it l.2).(perm) ≠ Disabled)
     end.
 
-  (* FIXME: merge the two tk_unq ? *)
+  (* FIXME: Refactor potential: merge the two tk_unq *)
   Lemma bor_state_pre_unq_or l t tk σ : (tk = tk_unq tk_act ∨ tk = tk_unq tk_res) →
     bor_state_pre l t tk σ = bor_state_pre_unq l t σ.
   Proof. intros [-> | ->]; done. Qed.
 
 
-  (* TODO: we still want that the children are disabled and the cousins are not active even when this tag is frozen !protected. So perhaps we need 2 case distinctions here? *)
   Definition bor_state_post_unq (l : loc) (t : tag) (σ : state) it tr tkk:=
       let P := ((item_lookup it l.2).(perm) = Frozen → protector_is_active it.(iprot) σ.(scs)) in
       ( P →
@@ -1601,7 +1600,7 @@ Section val_rel.
         (* through [state_rel]:
           * the stacks are the same,
           * the allocation size is the same,
-          * and the locations are related (i.e.: public) TODO: previously, scalars could be untagged. this no longer works.
+          * and the locations are related (i.e.: public)
         *)
         ⌜l1 = l2⌝ ∗  ⌜p1 = p2⌝ ∗ p1 $$ tk_pub
     | ScCallId c, ScCallId c' => ⌜c = c'⌝ ∗ pub_cid c
diff --git a/theories/tree_borrows/refl.v b/theories/tree_borrows/refl.v
index ba7acb4eec4e1024373cffdee195139c3c52ee6e..e9509dea0bf7fc6a41c857a7bc3f59d29cf6c046 100755
--- a/theories/tree_borrows/refl.v
+++ b/theories/tree_borrows/refl.v
@@ -277,7 +277,6 @@ Section log_rel.
     iDestruct (value_rel_length with "Hv1") as %EqL.
     iDestruct (value_rel_lookup with "Hv1") as (sc_t sc_s Eqt Eqs) "Hsc".
     {  rewrite EqL. eapply Nat2Z.inj_lt, lookup_lt_Some; eauto. }
-    (* TODO: I don't know how to fix sim_pures to do this. *)
     target_proj; [done|]. source_proj; [done|]. solve_rrel_refl.
   Qed.
 
@@ -373,8 +372,6 @@ Section log_rel.
       iIntros (t) "Hv". sim_val. eauto.
   Qed.
 
-  (* TODO: this can be useful elsewhere. It's here because I'm relying on the
-    several useful tactics defined here. *)
   Local Lemma sim_case π e_t e_s el_t el_s Ψ :
     e_t ⪯{π} e_s {{ rrel }} -∗
     ([∗ list] e_t';e_s' ∈ el_t;el_s, e_t' ⪯{π} e_s' [{ Ψ }]) -∗
@@ -389,7 +386,6 @@ Section log_rel.
     rename select (_ !! _ = Some _) into Hls.
     assert (∃ e_t', el_t !! Z.to_nat i = Some e_t') as [? Hlt].
     { apply lookup_lt_is_Some_2. apply lookup_lt_Some in Hls. by rewrite EqL. }
-    (* TODO sim_pures? *)
     target_case; [done|]. source_case; [done|]. sim_pures.
     iApply (big_sepL2_lookup _ _ _ _ _ _ Hlt Hls with "Hle").
   Qed.
diff --git a/theories/tree_borrows/steps_progress.v b/theories/tree_borrows/steps_progress.v
index fde62d28633a1be6ace1d0d03d01b564490bda4d..783fd92e6d4c18f38ee2e6b195c5e196262c3c5a 100755
--- a/theories/tree_borrows/steps_progress.v
+++ b/theories/tree_borrows/steps_progress.v
@@ -6,7 +6,6 @@ From simuliris.tree_borrows Require Export steps_wf.
 From Equations Require Import Equations.
 From iris.prelude Require Import options.
 
-(* TODO: do we need non-empty condition? ie (sizeof ptr) > 0? *)
 Lemma alloc_base_step P σ sz :
   state_wf σ ->
   (sz > 0)%nat ->
@@ -528,60 +527,7 @@ Proof.
     intros tr Htr. simpl in Htr|-*. eapply (zero_sized_memory_access_unchanged false).
   - do 2 econstructor. all: eauto.
 Qed.
-(* TODO remove?
-Lemma copy_base_step P (σ: state) l bor T
-  (WF: state_wf σ)
-  (BLK: ∀ n, (n < tsize T)%nat → l +ₗ n ∈ dom σ.(shp))
-  (BOR: ∀ m stk, (m < tsize T)%nat → σ.(sst) !! (l +ₗ m) = Some stk →
-        access1_read_pre σ.(scs) stk bor) :
-  ∃ v α,
-  read_mem l (tsize T) σ.(shp) = Some v ∧
-  memory_read σ.(sst) σ.(scs) l bor (tsize T) = Some α ∧
-  let σ' := mkState σ.(shp) α σ.(scs) σ.(snp) σ.(snc) in
-  base_step P (Copy (Place l bor T)) σ (Val v) σ' [].
-Proof.
-  destruct (read_mem_is_Some _ _ _ BLK) as [v RM].
-  destruct (memory_read_is_Some σ.(sst) σ.(scs) l bor (tsize T));[|done|].
-  { move => ? /BLK. by rewrite (state_wf_dom _ WF). }
-  do 2 eexists. do 2 (split; [done|]). intros σ'.
-  eapply copy_base_step'; eauto.
-Qed. *)
-
-(*
-Lemma failed_copy_base_step' P (σ: state) l tg sz (WF: state_wf σ) :
-  trees_contain tg σ.(strs) l.1 →
-  apply_within_trees (memory_access AccessRead σ.(scs) tg (l.2, sz)) l.1 σ.(strs) = None →
-  is_Some (read_mem l sz σ.(shp)) →
-  base_step P (Copy (Place l tg sz)) σ (Val $ replicate sz ScPoison) σ [].
-Proof.
-  intros TC Happly. destruct l, σ. do 2 econstructor; by eauto.
-Qed.
-*)
-(*
-
-Lemma access1_write_is_Some cids stk bor
-  (BOR: access1_write_pre cids stk bor) :
-  is_Some (access1 stk AccessWrite bor cids).
-Proof.
-  destruct BOR as (i & it & Eqi & ND & Neqi & Eqit & Lti).
-  apply access1_is_Some. exists i, it. do 4 (split; [done|]).
-  intros j jt Lt Eq. by destruct (Lti _ _ Lt Eq).
-Qed.
 
-Lemma memory_written_is_Some α cids l bor (n: nat) :
-  (∀ m, (m < n)%nat → l +ₗ m ∈ dom α) →
-  (∀ (m: nat) stk, (m < n)%nat →
-    α !! (l +ₗ m) = Some stk → access1_write_pre cids stk bor) →
-  is_Some (memory_written α cids l bor n).
-Proof.
-  intros IN STK. apply for_each_is_Some.
-  - intros m []. rewrite -(Z2Nat.id m); [|done]. apply IN.
-    rewrite -(Nat2Z.id n) -Z2Nat.inj_lt; [done..|lia].
-  - intros m stk Lt Eq.
-    specialize (STK _ _ Lt Eq).
-    destruct (access1_write_is_Some _ _ _ STK) as [? Eq2]. rewrite Eq2. by eexists.
-Qed.
-*)
 Lemma write_base_step' P (σ: state) l bor sz v trs'
   (LEN: length v = sz)
   (BLK: ∀ n, (n < sz)%nat → l +ₗ n ∈ dom σ.(shp)) 
@@ -598,25 +544,6 @@ Proof.
   - econstructor 2; econstructor; eauto. by rewrite LEN.
 Qed.
 
-(*
-Lemma write_base_step P (σ: state) l bor T v
-  (WF: state_wf σ)
-  (LEN: length v = tsize T)
-  (*(LOCVAL: v <<t σ.(snp))*)
-  (BLK: ∀ n, (n < tsize T)%nat → l +ₗ n ∈ dom σ.(shp))
-  (STK: ∀ m stk, (m < tsize T)%nat → σ.(sst) !! (l +ₗ m) = Some stk →
-        access1_write_pre σ.(scs) stk bor) :
-  ∃ α,
-  memory_written σ.(sst) σ.(scs) l bor (tsize T) = Some α ∧
-  let σ' := mkState (write_mem l v σ.(shp)) α σ.(scs) σ.(snp) σ.(snc) in
-  base_step P (Write (Place l bor T) (Val v)) σ #[☠] σ' [].
-Proof.
-  destruct (memory_written_is_Some σ.(sst) σ.(scs) l bor (tsize T)); [|done|].
-  { move => ? /BLK. by rewrite (state_wf_dom _ WF). }
-  eexists. split; [done|]. by eapply write_base_step'.
-Qed.
- *)
-
 Lemma call_base_step P σ name e r fn :
   P !! name = Some fn →
   to_result e = Some r →
@@ -637,363 +564,3 @@ Lemma end_call_base_step P (σ: state) trs' c :
   base_step P (EndCall #[ScCallId c]) σ #[☠] σ' [].
 Proof. intros ??. by econstructor; econstructor. Qed.
 
-(*
-
-Lemma unsafe_action_is_Some_weak {A} (GI: A → nat → Prop)
-  (f: A → _ → nat → _ → _) a l last cur_dist n
-  (HF: ∀ a i j b, (last ≤ i ≤ j ∧ j ≤ last + cur_dist + n)%nat → GI a i →
-          ∃ a', f a (l +ₗ i) (Z.to_nat (j - i)) b = Some a' ∧ GI a' j) :
-  GI a last → ∃ a' last' cur_dist',
-  unsafe_action f a l last cur_dist n = Some (a', (last', cur_dist')) ∧ GI a' last'.
-Proof.
-  intros HI. rewrite /unsafe_action.
-  destruct (HF a last (last + cur_dist)%nat true) as [a' Eq1]; [lia|done|].
-  move : Eq1.
-  rewrite (_: Z.to_nat (Z.of_nat (last + cur_dist) - Z.of_nat last) = cur_dist);
-    last by rewrite Nat2Z.inj_add Z.add_simpl_l Nat2Z.id.
-  move => [-> HI'] /=.
-  destruct (HF a' (last + cur_dist)%nat (last + cur_dist + n)%nat false)
-    as [? [Eq2 HI2]]; [lia|done|].
-  move : Eq2.
-  rewrite (_: Z.to_nat (Z.of_nat (last + cur_dist + n) -
-                Z.of_nat (last + cur_dist)) = n);
-    last by rewrite Nat2Z.inj_add Z.add_simpl_l Nat2Z.id.
-  move => -> /=. by do 3 eexists.
-Qed.
-
-
-Lemma visit_freeze_sensitive'_is_Some {A} (GI: A → nat → Prop)
-  l (f: A → _ → nat → _ → _) a (last cur_dist: nat) T
-  (HF: ∀ a i j b, (last ≤ i ≤ j ∧ j ≤ last + cur_dist + tsize T)%nat → GI a i →
-          ∃ a', f a (l +ₗ i) (Z.to_nat (j - i)) b = Some a' ∧ GI a' j) :
-  GI a last → ∃ a' last' cur_dist',
-  visit_freeze_sensitive' l f a last cur_dist T = Some (a', (last', cur_dist')) ∧
-  GI a' last'.
-Proof.
-  revert HF.
-  apply (visit_freeze_sensitive'_elim
-    (* general goal P *)
-    (λ l f a last cur_dist T oalc,
-      (∀ a i j b,(last ≤ i ≤ j ∧ j ≤ last + cur_dist + tsize T)%nat → GI a i →
-          ∃ a', f a (l +ₗ i) (Z.to_nat (j - i)) b = Some a' ∧ GI a' j) →
-      GI a last → ∃ a' last' cur', oalc = Some (a', (last', cur')) ∧ GI a' last')
-    (λ l f _ _ _ _ a last cur_dist Ts oalc,
-      (∀ a i j b, (last ≤ i ≤ j ∧ j ≤ last + cur_dist + tsize (Product Ts))%nat →
-          GI a i → ∃ a', f a (l +ₗ i) (Z.to_nat (j - i)) b = Some a' ∧ GI a' j) →
-      GI a last → ∃ a' last' cur', oalc = Some (a', (last', cur')) ∧ GI a' last')).
-  - naive_solver.
-  - naive_solver.
-  - clear. intros ?????? HF. by apply unsafe_action_is_Some_weak.
-  - clear. intros l f a last cur_dist T HF.
-    case is_freeze; [by do 3 eexists|]. by apply unsafe_action_is_Some_weak.
-  - clear. intros l f a last cur_dist Ts IH Hf HI.
-    case is_freeze; [intros; simplify_eq/=; exists a, last; by eexists|by apply IH].
-  - clear. intros l f a last cur_dist T HF.
-    case is_freeze; [by do 3 eexists|]. by apply unsafe_action_is_Some_weak.
-  - naive_solver.
-  - clear.
-    intros l f a last cur_dist Ts a1 last1 cur_dist1 T1 Ts1 IH1 IH2 HF HI.
-    destruct IH2 as (a2 & last2 & cur_dist2 & Eq1 & HI2); [..|done|].
-    { intros ???? [? Le]. apply HF. split; [done|]. clear -Le.
-      rewrite tsize_product_cons. by lia. }
-    destruct (visit_freeze_sensitive'_offsets _ _ _ _ _ _ _ _ _ Eq1)
-      as [LeO EqO].
-    rewrite Eq1 /=. apply (IH1 (a2, (last2,cur_dist2))); [..|done].
-    intros a' i j b. cbn -[tsize]. intros Lej. apply HF.
-    clear -LeO EqO Lej. destruct Lej as [[Le2 Lei] Lej].
-    split; [lia|]. move : Lej. rewrite EqO tsize_product_cons. lia.
-Qed.
-
-Lemma visit_freeze_sensitive_is_Some' {A} (GI: A → nat → Prop)
-  l (f: A → _ → nat → _ → _) a T
-  (HF: ∀ a i j b, (i ≤ j ∧ j ≤ tsize T)%nat → GI a i →
-          ∃ a', f a (l +ₗ i) (Z.to_nat (j - i)) b = Some a' ∧ GI a' j) :
-  GI a O → ∃ a', visit_freeze_sensitive l T f a = Some a' ∧ GI a' (tsize T).
-Proof.
-  intros HI. rewrite /visit_freeze_sensitive.
-  destruct (visit_freeze_sensitive'_is_Some GI l f a O O T)
-    as (a1 & l1 & c1 & Eq1 & HI1); [|done|].
-  { rewrite 2!Nat.add_0_l. intros ???? [[??]?]. by apply HF. }
-  rewrite Eq1 -(Nat.add_sub c1 l1) -(Nat2Z.id (c1 + l1 - l1))
-          Nat2Z.inj_sub; [|lia].
-  move : Eq1. intros [? Eq]%visit_freeze_sensitive'_offsets.
-  destruct (HF a1 l1 (c1 + l1)%nat true) as (a2 & Eq2 & HI2); [|done|].
-  { split; [lia|]. move : Eq. rewrite 2!Nat.add_0_l. lia. }
-  exists a2. split; [done|].
-  move : Eq. by rewrite 2!Nat.add_0_l Nat.add_comm => [<-].
-Qed.
-
-Lemma visit_freeze_sensitive_is_Some'_2 {A} (GI: A → nat → Prop)
-  l (f: A → _ → nat → _ → _) a T
-  (HF: ∀ a i j b, (i ≤ j ∧ j ≤ tsize T)%nat → GI a i →
-          ∃ a', f a (l +ₗ i) (Z.to_nat (j - i)) b = Some a' ∧ GI a' j) :
-  GI a O → is_Some (visit_freeze_sensitive l T f a).
-Proof.
-  intros HI. destruct (visit_freeze_sensitive_is_Some' GI l f a T)
-    as [a' [Eq _]]; [done..|by eexists].
-Qed.
-
-Lemma visit_freeze_sensitive_is_Some {A}
-  l (f: A → _ → nat → _ → _) a T
-  (HF: ∀ a i j b, (i ≤ j ∧ j ≤ tsize T)%nat →
-          is_Some (f a (l +â‚— i) (Z.to_nat (j - i)) b)) :
-  is_Some (visit_freeze_sensitive l T f a).
-Proof.
-  destruct (visit_freeze_sensitive_is_Some' (λ _ _, True) l f a T)
-    as [a' [Eq _]]; [|done..|by eexists].
-  intros a1 i j b Le _. destruct (HF a1 i j b Le). by eexists.
-Qed.
-
-Lemma access1_find_granting_agree stk kind bor cids i1 i2 pm1 stk2:
-  find_granting stk kind bor = Some (i1, pm1) →
-  access1 stk kind bor cids = Some (i2, stk2) →
-  i1 = i2.
-Proof.
-  intros FI. rewrite /access1 FI /=.
-  destruct kind.
-  - case replace_check => [? /= ?|//]. by simplify_eq/=.
-  - case find_first_write_incompatible => [? /=|//].
-    case remove_check => [? /= ?|//]. by simplify_eq/=.
-Qed.
-
-Lemma find_granting_write stk bor i pi:
-  find_granting stk AccessWrite bor = Some (i, pi) →
-  pi ≠ Disabled ∧ pi ≠ SharedReadOnly.
-Proof.
-  move => /fmap_Some [[??] /= [IS ?]]. simplify_eq/=.
-  apply list_find_Some in IS as (? & [IS ?] & ?).
-  move : IS. rewrite /grants. case perm; naive_solver.
-Qed.
-
-(* The precondition `access1_pre` is too strong for the SharedReadWrite case:
-  we only need a granting item for that case, we don't need the access check. *)
-Lemma grant_is_Some stk old new cids :
-  let access :=
-    if grants new.(perm) AccessWrite then AccessWrite else AccessRead in
-  access1_pre cids stk access old →
-  is_Some (grant stk old new cids).
-Proof.
-  intros access ACC. rewrite /grant.
-  destruct (find_granting_is_Some stk access old) as [[i pi] Eqi].
-  { destruct ACC as (i & it & Eqi & ND & NEq & Eqt & Lt).
-    exists it. split; [by eapply elem_of_list_lookup_2|].
-    do 2 (split; [done|]). intros Eqa. apply NEq. by rewrite Eqa. }
-  rewrite Eqi. cbn -[item_insert_dedup].
-  destruct (access1_is_Some _ _ _ _ ACC) as [[i' stk'] Eq].
-  rewrite Eq. cbn -[item_insert_dedup].
-  destruct new.(perm); try by eexists.
-  apply find_granting_write in Eqi as [].
-  destruct (find_first_write_incompatible_is_Some (take i stk) pi) as [? Eq2];
-    [done..|rewrite Eq2; by eexists].
-Qed.
-
-Lemma reborrowN_is_Some α cids l n old new pm protector
-  (BLK: ∀ m, (m < n)%nat → l +ₗ m ∈ dom α):
-  let access := if grants pm AccessWrite then AccessWrite else AccessRead in
-  (∀ (m: nat) stk, (m < n)%nat → α !! (l +ₗ m) = Some stk →
-    access1_pre cids stk access old) →
-  is_Some (reborrowN α cids l n old new pm protector).
-Proof.
-  intros access STK.
-  rewrite /reborrowN. apply for_each_is_Some.
-  - intros m []. rewrite -(Z2Nat.id m); [|done]. apply BLK.
-    rewrite -(Nat2Z.id n) -Z2Nat.inj_lt; [done..|lia].
-  - intros m stk Lt Eq. apply grant_is_Some. by apply (STK _ _ Lt Eq).
-Qed.
-
-Lemma reborrowN_lookup (α1 α2 : stacks) cids l n old new pm protector
-  (EQB : reborrowN α1 cids l n old new pm protector = Some α2) :
-  (∀ m, (n ≤ m)%nat → α2 !! (l +ₗ m) = α1 !! (l +ₗ m)) ∧
-  (∀ m stk, (m < n)%nat → α1 !! (l +ₗ m) = Some stk →
-    ∃ stk', α2 !! (l +ₗ m) = Some stk' ∧
-    let item := mkItem pm new protector in
-    grant stk old item cids = Some stk') ∧
-  (∀ m stk', (m < n)%nat → α2 !! (l +ₗ m) = Some stk' →
-    ∃ stk, α1 !! (l +ₗ m) = Some stk ∧
-    let item := mkItem pm new protector in
-    grant stk old item cids = Some stk').
-Proof.
-  destruct (for_each_lookup _ _ _ _ _ EQB) as [HL1 [HL2 HL3]]. split; last split.
-  - intros m Ge. apply HL3. intros i Lt Eq%shift_loc_inj. subst. lia.
-  - by apply HL1.
-  - by apply HL2.
-Qed.
-
-Lemma visit_freeze_sensitive'_is_freeze {A}
-  l (f: A → _ → nat → _ → _) a (last cur_dist: nat) T :
-  is_freeze T →
-  visit_freeze_sensitive' l f a last cur_dist T
-    = Some (a, (last, (cur_dist + tsize T)%nat)).
-Proof.
-  apply (visit_freeze_sensitive'_elim
-    (* general goal P *)
-    (λ l f a last cur_dist T oalc,
-      is_freeze T → oalc = Some (a, (last, (cur_dist + tsize T)%nat)))
-    (λ l f _ _ _ _ a last cur_dist Ts oalc,
-      is_freeze (Product Ts) →
-      oalc = Some (a, (last, (cur_dist + tsize (Product Ts))%nat)))).
-  - done.
-  - clear. intros ??????? _. by rewrite /= Nat.add_1_r.
-  - done.
-  - clear. intros ??????. by move => /Is_true_eq_true ->.
-  - clear. intros ?????? _. by move => /Is_true_eq_true ->.
-  - clear. intros ??????. by move => /Is_true_eq_true ->.
-  - clear. intros _ _ _ _ _ _ ??? _. by rewrite /= Nat.add_0_r.
-  - clear. intros l f a last cur_dist Ts a' l1 c1 T Ts' IH1 IH2 FRZ.
-    rewrite IH2; first rewrite /= (IH1 (a', (l1, c1 + tsize T)%nat)).
-    + simpl. do 3 f_equal. change (tsize T) with (0 + tsize T)%nat.
-      rewrite -(foldl_fmap_shift_init _ (λ n, n + tsize T)%nat);
-        [by lia|intros ?? _; by lia].
-    + by eapply is_freeze_cons_product_inv.
-    + by eapply is_freeze_cons_product_inv.
-Qed.
-
-Lemma visit_freeze_sensitive_is_freeze {A}
-  l (f: A → _ → nat → _ → _) a T :
-  is_freeze T → visit_freeze_sensitive l T f a = f a l (tsize T) true.
-Proof.
-  intros FRZ. rewrite /visit_freeze_sensitive visit_freeze_sensitive'_is_freeze;
-    [by rewrite shift_loc_0_nat Nat.add_0_l|done].
-Qed.
-
-Lemma reborrow_is_freeze_is_Some α cids l old T kind new prot
-  (BLK: ∀ m, (m < tsize T)%nat → l +ₗ m ∈ dom α)
-  (FRZ: is_freeze T)
-  (STK: ∀ m stk, (m < tsize T)%nat → α !! (l +ₗ m) = Some stk →
-    let access := match kind with
-                  | SharedRef | RawRef false => AccessRead
-                  | _ => AccessWrite
-                  end in access1_pre cids stk access old) :
-  is_Some (reborrow α cids l old T kind new prot).
-Proof.
-  rewrite /reborrow. destruct kind as [[]| |[]].
-  - by apply reborrowN_is_Some.
-  - by apply reborrowN_is_Some.
-  - rewrite visit_freeze_sensitive_is_freeze //. by apply reborrowN_is_Some.
-  - by apply reborrowN_is_Some.
-  - rewrite visit_freeze_sensitive_is_freeze //. by apply reborrowN_is_Some.
-Qed.
-
-Lemma reborrow_is_freeze_lookup α cids l old T kind new prot α'
-  (FRZ: is_freeze T) :
-  reborrow α cids l old T kind new prot = Some α' →
-  ∀ m stk', (m < tsize T)%nat → α' !! (l +ₗ m) = Some stk' →
-  ∃ stk, α !! (l +ₗ m) = Some stk ∧
-  let pm := match kind with
-                        | SharedRef | RawRef false => SharedReadOnly
-                        | UniqueRef false => Unique
-                        | UniqueRef true | RawRef true => SharedReadWrite
-                        end in
-  let item := mkItem pm new prot in
-  grant stk old item cids = Some stk'.
-Proof.
-  rewrite /reborrow. destruct kind as [[]| |[]]; intros EQB m stk' Lt Eq'.
-  - apply reborrowN_lookup in EQB as [_ [_ HL]]. by apply HL.
-  - apply reborrowN_lookup in EQB as [_ [_ HL]]. by apply HL.
-  - move : EQB. rewrite visit_freeze_sensitive_is_freeze; [|done].
-    move => /reborrowN_lookup [_ [_ HL]]. by apply HL.
-  - apply reborrowN_lookup in EQB as [_ [_ HL]]. by apply HL.
-  - move : EQB. rewrite visit_freeze_sensitive_is_freeze; [|done].
-    move => /reborrowN_lookup [_ [_ HL]]. by apply HL.
-Qed.
-
-
-Lemma retag_ref_is_freeze_is_Some α cids nxtp l old T kind prot
-  (BLK: ∀ n, (n < tsize T)%nat → l +ₗ n ∈ dom α)
-  (FRZ: is_freeze T)
-  (STK: ∀ m stk, (m < tsize T)%nat → α !! (l +ₗ m) = Some stk →
-    let access := match kind with
-                  | SharedRef | RawRef false => AccessRead
-                  | _ => AccessWrite
-                  end in access1_pre cids stk access old) :
-  is_Some (retag_ref α cids nxtp l old T kind prot).
-Proof.
-  rewrite /retag_ref. destruct (tsize T) as [|sT] eqn:Eqs; [by eexists|].
-  set new := match kind with
-             | RawRef _ => Untagged
-             | _ => Tagged nxtp
-             end.
-  destruct (reborrow_is_freeze_is_Some α cids l old T kind new prot)
-    as [α1 Eq1]; [by rewrite Eqs|..|done| |].
-  { intros m stk Lt. apply STK. by rewrite -Eqs. }
-  rewrite Eq1 /=. by eexists.
-Qed.
-
-Definition valid_protector rkind (cids: call_id_set) c :=
-  match rkind with | FnEntry => c ∈ cids | _ => True end.
-Definition pointer_kind_access pk :=
-  match pk with
-  | RefPtr Mutable | RawPtr Mutable | BoxPtr => AccessWrite
-  | _ => AccessRead
-  end.
-Definition valid_block (α: stacks) cids (l: loc) (tg: tag) pk T :=
-  is_freeze T ∧
-  (∀ m, (m < tsize T)%nat → l +ₗ m ∈ dom α ∧ ∃ stk,
-    α !! (l +ₗ m) = Some stk ∧ access1_pre cids stk (pointer_kind_access pk) tg).
-
-Lemma retag_is_freeze_is_Some α nxtp cids c l otg kind pk T
-  (LOC: valid_block α cids l otg pk T) :
-  is_Some (retag α nxtp cids c l otg kind pk T).
-Proof.
-  destruct LOC as (FRZ & EQD).
-  destruct pk as [[]|mut|]; simpl.
-  - destruct (retag_ref_is_freeze_is_Some α cids nxtp l otg T
-                (UniqueRef (is_two_phase kind)) (adding_protector kind c))
-      as [bac Eq]; [by apply EQD|done..| |by eexists].
-    simpl. clear -EQD. intros m stk Lt Eq.
-    destruct (EQD _ Lt) as [_ [stk' [Eq' ?]]]. by simplify_eq/=.
-  - destruct (retag_ref_is_freeze_is_Some α cids nxtp l otg T SharedRef
-                      (adding_protector kind c))
-      as [bac Eq]; [by apply EQD|done..| |by eexists].
-    simpl. clear -EQD. intros m stk Lt Eq.
-    destruct (EQD _ Lt) as [_ [stk' [Eq' ?]]]. by simplify_eq/=.
-  - destruct kind; [by eexists..| |by eexists].
-    destruct (retag_ref_is_freeze_is_Some α cids nxtp l otg T
-              (RawRef (bool_decide (mut = Mutable))) None)
-      as [bac Eq]; [by apply EQD|done..| |by eexists].
-    simpl. clear -EQD. intros m stk Lt Eq.
-    destruct (EQD _ Lt) as [_ [stk' [Eq' ?]]]. simplify_eq/=. by destruct mut.
-  - destruct (retag_ref_is_freeze_is_Some α cids nxtp l otg T
-                          (UniqueRef false) None)
-      as [bac Eq]; [by apply EQD|done..| |by eexists].
-    simpl. clear -EQD. intros m stk Lt Eq.
-    destruct (EQD _ Lt) as [_ [stk' [Eq' ?]]]. by simplify_eq/=.
-Qed.
-
-
-Lemma retag_base_step' P σ l otg ntg pk T kind c' α' nxtp':
-  c' ∈ σ.(scs) →
-  retag σ.(sst) σ.(snp) σ.(scs) c' l otg kind pk T =
-    Some (ntg, α', nxtp') →
-  let σ' := mkState σ.(shp) α' σ.(scs) nxtp' σ.(snc) in
-  base_step P (Retag #[ScPtr l otg] #[ScCallId c'] pk T kind) σ #[ScPtr l ntg] σ' [].
-Proof.
-  econstructor. { econstructor; eauto. } simpl.
-  econstructor; eauto.
-Qed.
-
-Lemma retag_base_step P σ l c otg pk T kind
-  (BAR: c ∈ σ.(scs))
-  (LOC: valid_block σ.(sst) σ.(scs) l otg pk T)
-  (WF: state_wf σ) :
-  ∃ ntg α' nxtp',
-  retag σ.(sst) σ.(snp) σ.(scs) c l otg kind pk T =
-    Some (ntg, α', nxtp') ∧
-  let σ' := mkState σ.(shp) α' σ.(scs) nxtp' σ.(snc) in
-  base_step P (Retag #[ScPtr l otg] #[ScCallId c] pk T kind) σ #[ScPtr l ntg] σ' [].
-Proof.
-  destruct σ as [h α cids nxtp nxtc]; simpl in *.
-  destruct (retag_is_freeze_is_Some α nxtp cids c l otg kind pk T)
-    as [[[h' α'] nxtp'] Eq]; [done|].
-  exists h', α' , nxtp'. split; [done|].
-  eapply retag_base_step'; eauto.
-Qed.
- *)
-
-(* Lemma syscall_base_step σ id :
-  base_step (SysCall id) σ [SysCallEvt id] #☠ σ [].
-Proof.
-  have EE: ∃ σ', base_step (SysCall id) σ [SysCallEvt id] #☠ σ' [] ∧ σ' = σ.
-  { eexists. split. econstructor; econstructor. by destruct σ. }
-  destruct EE as [? [? ?]]. by subst.
-Qed. *)
diff --git a/theories/tree_borrows/steps_wf.v b/theories/tree_borrows/steps_wf.v
index 8aa035bd98f01cdb64c347fa46fc95a43f4d8e88..e78af25aa003c0a23f63498823579991db47ba3f 100755
--- a/theories/tree_borrows/steps_wf.v
+++ b/theories/tree_borrows/steps_wf.v
@@ -1850,22 +1850,6 @@ Proof.
   - by destruct σ.
 Qed.
 
-(*
-Lemma failed_copy_step_wf σ σ' e e' l bor T efs :
-  mem_expr_step σ.(shp) e (FailedCopyEvt l bor T) σ'.(shp) e' efs →
-  bor_step σ.(strs) σ.(scs) σ.(snp) σ.(snc)
-           (FailedCopyEvt l bor T)
-           σ'.(strs) σ'.(scs) σ'.(snp) σ'.(snc) →
-  state_wf σ → state_wf σ'.
-Proof.
-  destruct σ as [h α cids nxtp nxtc].
-  destruct σ' as [h' α' cids' nxtp' nxtc']. simpl.
-  intros BS IS WF.
-  inversion BS. clear BS. simplify_eq.
-  inversion IS; clear IS; simplify_eq.
-  done.
-Qed. *)
-
 (* TODO less equalities makes applying the rule easier, see _sane version below *)
 Lemma write_mem_dom l (vl : value) h h'
   (DEFINED: ∀ i : nat, (i < length vl)%nat → (l +ₗ i) ∈ dom h)
diff --git a/theories/tree_borrows/tkmap_view.v b/theories/tree_borrows/tkmap_view.v
index 1e2e3bf2fc7874a19492ab906eda7a0179119d99..0e0ff2801fa6e29b670d1f92f10150a5abf17e93 100755
--- a/theories/tree_borrows/tkmap_view.v
+++ b/theories/tree_borrows/tkmap_view.v
@@ -19,10 +19,8 @@ From simuliris.tree_borrows Require Export defs.
   - tk_loc: the tag is local
  *)
 
-(* TODO: allow a local update from tk_unq to tk_pub *)
 Definition tagKindR := csumR (exclR unitO) (csumR (csumR (exclR unitO) (exclR unitO)) unitR).
 
-
 Canonical Structure tag_kindO := leibnizO tag_kind.
 
 Global Instance tagKindR_discrete : CmraDiscrete tagKindR.
diff --git a/theories/tree_borrows/trees_equal/random_lemmas.v b/theories/tree_borrows/trees_equal/random_lemmas.v
index 6a745b9d77d59f30e91d744b643d021e789a51c3..2ae7810b9c3f77f44e3e840ff79dc49c4bccf5de 100644
--- a/theories/tree_borrows/trees_equal/random_lemmas.v
+++ b/theories/tree_borrows/trees_equal/random_lemmas.v
@@ -13,7 +13,6 @@ From simuliris.tree_borrows.trees_equal Require Import trees_equal_base.
 From iris.prelude Require Import options.
 
 
-(* TODO cleanup *)
 Section utils.
 
   Lemma every_node_iff_every_lookup
@@ -270,7 +269,7 @@ Section utils.
   Qed.
 
 
-  (* FIXME: move this elsewhere *)
+  (* FIXME: This is a very low level lemma, move this elsewhere ? *)
   Lemma if_fun_absorb_args {X Y} {b : bool} {x : X} {f g : X -> Y} :
     (if b then f else g) x = if b then f x else g x.
   Proof. destruct b; reflexivity. Qed.
@@ -443,4 +442,4 @@ Section utils.
   Qed.
 
 
-End utils.
\ No newline at end of file
+End utils.
diff --git a/theories/tree_borrows/trees_equal/trees_equal.v b/theories/tree_borrows/trees_equal/trees_equal.v
index c80419ce21dadf9cce1c612d7f9880feb2244b0c..9cf406198ac56d15f707aa595576c792f3825227 100644
--- a/theories/tree_borrows/trees_equal/trees_equal.v
+++ b/theories/tree_borrows/trees_equal/trees_equal.v
@@ -12,7 +12,6 @@ From simuliris.tree_borrows Require Import steps_progress.
 From iris.prelude Require Import options.
 
 
-(* TODO cleanup *)
 Section utils.
 
   Definition tag_valid (upper : tag) (n : tag) : Prop := (n < upper)%nat.
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 5bf54797952e7fc155966aeeca2f4609ba542644..f4342eef16da2065a05ebbe7709ce3116cdbde9a 100644
--- a/theories/tree_borrows/trees_equal/trees_equal_asymmetric_prot.v
+++ b/theories/tree_borrows/trees_equal/trees_equal_asymmetric_prot.v
@@ -12,7 +12,6 @@ From simuliris.tree_borrows Require Import steps_progress.
 From simuliris.tree_borrows.trees_equal Require Import trees_equal_base random_lemmas.
 From iris.prelude Require Import options.
 
-(* TODO cleanup *)
 Section utils.
 
 Context (C : call_id_set).
@@ -304,4 +303,4 @@ Context (C : call_id_set).
       destruct (item_lookup it0 loc) as [ii pp]. simpl in *; subst ii pp. econstructor 1.
   Qed.
 
-End utils.
\ No newline at end of file
+End utils.
diff --git a/theories/tree_borrows/trees_equal/trees_equal_base.v b/theories/tree_borrows/trees_equal/trees_equal_base.v
index 508e3a311bec21acd8c8d9131c60e2b603941b81..4ac52f8d45b42a4b6e1305e16f2ff27ad1991aae 100644
--- a/theories/tree_borrows/trees_equal/trees_equal_base.v
+++ b/theories/tree_borrows/trees_equal/trees_equal_base.v
@@ -12,8 +12,6 @@ From simuliris.tree_borrows Require Import steps_progress.
 From simuliris.tree_borrows Require Export trees_equal.disabled_in_practice.
 From iris.prelude Require Import options.
 
-
-(* TODO cleanup *)
 Section utils.
 
   Definition tag_valid (upper : tag) (n : tag) : Prop := (n < upper)%nat.
@@ -151,7 +149,6 @@ Section utils.
     (* and define all the same relationships between those tags *)
     /\ (forall tg tg', rel_dec tr1 tg tg' = rel_dec tr2 tg tg')
     (* and have their permissions be equal up to C on all locations *)
-    (* FIXME: maybe think about reformulating ∧ (∀ t it1 it2, tree_lookup t it1 tr1 -> tree_lookup t it2 tr2 -> it_rel it1 it2) *)
     /\ (forall tg, tree_contains tg tr1 ->
           exists it1 it2,
             tree_lookup tr1 tg it1
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 cd1d22fdcfe7eb410ebd5ec77ff01730b06b5db3..efda218a3529877b9e0dd1b0234ad267a0427c9d 100644
--- a/theories/tree_borrows/trees_equal/trees_equal_create_child.v
+++ b/theories/tree_borrows/trees_equal/trees_equal_create_child.v
@@ -12,7 +12,6 @@ From simuliris.tree_borrows Require Import steps_progress.
 From simuliris.tree_borrows.trees_equal Require Import trees_equal_base random_lemmas.
 From iris.prelude Require Import options.
 
-(* TODO cleanup *)
 Section utils.
 
 Context (C : call_id_set).
@@ -387,4 +386,4 @@ Context (C : call_id_set).
   Qed.
 
 
-End utils.
\ No newline at end of file
+End utils.
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 747c550bee3bd50e8defb09e93a8feadcb78be63..d8fb9630ef27122c61f72c1ecc18a58a046d5372 100644
--- a/theories/tree_borrows/trees_equal/trees_equal_more_access.v
+++ b/theories/tree_borrows/trees_equal/trees_equal_more_access.v
@@ -12,7 +12,6 @@ From simuliris.tree_borrows Require Import steps_progress.
 From simuliris.tree_borrows.trees_equal Require Import trees_equal_base random_lemmas.
 From iris.prelude Require Import options.
 
-(* TODO cleanup *)
 Section utils.
 
   Context (C : call_id_set).
@@ -79,11 +78,6 @@ Section utils.
        We now need to prove that actually there is also UB in the source,
        just not _here_, instead it occured at the cousin that creates the conflict. *)
     all: exfalso.
-    (* FIXME: here we need a lemma that shows
-       1. a Child/This access for tg is Foreign for tg_cous who is Cousin of tg
-       2. a Foreign access for such tg_cous is UB globally.
-       We can indeed check that in all of the following cases we have
-       rel = This or rel = Child and kind = AccessWrite. *)
     all: eapply cousin_write_for_initialized_protected_nondisabled_is_ub.
     all: try exact GlobalSuccess.
     all: try eassumption.
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 0fd6ff7f10f7ddc03139a1983b49d977bb59a813..d2124075c6e30fa030a41fadd7c12b69ef42bc22 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
@@ -13,7 +13,6 @@ From simuliris.tree_borrows.trees_equal Require Import trees_equal_base random_l
 From simuliris.tree_borrows.trees_equal Require Export trees_equal_preserved_by_access_base.
 From iris.prelude Require Import options.
 
-(* TODO cleanup *)
 Section utils.
 
   Context (C : call_id_set).
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 b40e646e177a081118228a1b02e905343af7158e..f02f2c20014b2bf6da714498562f32f58fdef076 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
@@ -12,7 +12,6 @@ From simuliris.tree_borrows Require Import steps_progress.
 From simuliris.tree_borrows.trees_equal Require Import trees_equal_base random_lemmas.
 From iris.prelude Require Import options.
 
-(* TODO cleanup *)
 Section utils.
 
   Context (C : call_id_set).
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 0f0b65b17690aaf3b7c7900ffe1a3cc59ec97b91..0cbe36a418b5355dfe3a48e6c8dc13e9145e1410 100644
--- a/theories/tree_borrows/trees_equal/trees_equal_source_read.v
+++ b/theories/tree_borrows/trees_equal/trees_equal_source_read.v
@@ -12,7 +12,6 @@ From simuliris.tree_borrows Require Import steps_progress.
 From simuliris.tree_borrows.trees_equal Require Import trees_equal_base random_lemmas.
 From iris.prelude Require Import options.
 
-(* TODO cleanup *)
 Section utils.
 
 Context (C : call_id_set).
@@ -132,4 +131,4 @@ Context (C : call_id_set).
       destruct pp; try done. all: repeat (simpl in *; simplify_eq); by econstructor 1.
   Qed.
 
-End utils.
\ No newline at end of file
+End utils.
diff --git a/theories/tree_borrows/trees_equal/trees_equal_transitivity.v b/theories/tree_borrows/trees_equal/trees_equal_transitivity.v
index 4906727bc23d759a663d21fafd4e80ad5665118c..e619696acc9458f641c9d303cf1203cc351b2e46 100644
--- a/theories/tree_borrows/trees_equal/trees_equal_transitivity.v
+++ b/theories/tree_borrows/trees_equal/trees_equal_transitivity.v
@@ -12,7 +12,6 @@ From simuliris.tree_borrows Require Import steps_progress.
 From simuliris.tree_borrows.trees_equal Require Import trees_equal_base random_lemmas.
 From iris.prelude Require Import options.
 
-(* TODO cleanup *)
 Section utils.
 Context (C : call_id_set).
 
@@ -617,4 +616,4 @@ Context (C : call_id_set).
   Qed.
 
 
-End utils.
\ No newline at end of file
+End utils.