diff --git a/_CoqProject b/_CoqProject
index beb86d0b6b1388862c2c8c4da7e9e0e2223235aa..431e69086a52007c444311a2b5c63d49fee1bf9b 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -197,6 +197,7 @@ theories/tree_borrows/examples/protected/shared_reorder_read_down_escaped.v
 theories/tree_borrows/examples/protected/shared_reorder_read_up_escaped.v
 theories/tree_borrows/examples/protected/mutable_reorder_write_down_activated.v
 theories/tree_borrows/examples/protected/mutable_reorder_write_up_activated.v
+theories/tree_borrows/examples/protected/mutable_reorder_write_up_activated_paper.v
 theories/tree_borrows/examples/unprotected/mutable_delete_read.v
 theories/tree_borrows/examples/unprotected/shared_delete_read_escaped.v
 theories/tree_borrows/examples/unprotected/shared_delete_read_escaped_coinductive.v
@@ -206,7 +207,7 @@ theories/tree_borrows/examples/pure.v
 # Proofs directly against the operational semantics.
 # This results in a proof that reads can be reordered.
 theories/tree_borrows/read_read_reorder/low_level.v
-theories/tree_borrows/read_read_reorder/refinement.v
-theories/tree_borrows/read_read_reorder/refinement_def.v
+theories/tree_borrows/read_read_reorder/read_reorder.v
+theories/tree_borrows/read_read_reorder/equivalence_def.v
 
 
diff --git a/theories/tree_borrows/README.md b/theories/tree_borrows/README.md
index bb1c7659adfce51b18ed1ba08467c853013bffd7..5a988b7404e3ced19f6af3c9c64c25f72a392984 100644
--- a/theories/tree_borrows/README.md
+++ b/theories/tree_borrows/README.md
@@ -2,6 +2,8 @@
 
 Forked and adapted from the sibling folder `../stacked_borrows` with the same structure.
 
+## Structure
+
 * `tree.v`, `locations.v` contain preliminary definitions.
 * `lang_base.v`, `expr_semantics.v`, `bor_semantics.v`, and `lang.v` contain the language definition.
 * `tree_lemmas.v`, `bor_lemmas.v`, `steps_wf.v` and `steps_preserve.v` contain basic lemmas to help with the manipulation of trees.
@@ -24,3 +26,30 @@ It is subdivided into
  * `refinement_def.v`: definition of a bisimulation relation for a sequential setting.
  * `low_level.v`: lemmas against the operational semantics.
  * `refinement.v`: actual proof of bisimulation between two programs in which adjacent reads have been swapped.
+
+## Correspondence with Section 5
+
+Section 5 has three examples, one for deleting reads, one for deleting writes, and one for reordering reads.
+
+### Example 1: Deleting Reads
+
+This example corresponds to the one in  `examples/unprotected/shared_delete_read_escaped.v`.
+The Coq example is very close to the one in the paper.
+The only difference is that `f` has an extra argument in Coq, which corresponds to the implicit environment that closures have in Rust.
+
+### Example 2: Deleting Writes (Optimizing with Protectors)
+
+This example corresponds to the one in `examples/protected/mutable_reorder_write_up_activated_paper.v`.
+This Coq example corresponds very closely to the one in the paper.
+The only difference is that `f` and `g` have an extra argument in Coq, which corresponds to the implicit environment that closures have in Rust.
+
+### Example 3: Reordering Reads
+
+This is proven in `read_read_reorder`, particularly in `refinement.v`.
+These proofs do not use the `simuliris` library, but instead they do a much simpler equivalence proof directly against the operational semantics.
+This is because these proofs only hold for a non-concurrent language.
+We suspect that they also hold in a concurrent setting, but this would require data race reasoning, and thus we have not proven that.
+
+Specifically, the extremely simple notion of "equivalence after a few steps" is in `refinement_def.v`.
+The proof that the two reads can be reordered is in `read_reorder.v`.
+The file `low_level.v` contains low-level lemmas used in `read_reorder.v`
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
new file mode 100644
index 0000000000000000000000000000000000000000..61295fb8fd575677cbd23a7d1b467a91a7d2da13
--- /dev/null
+++ b/theories/tree_borrows/examples/protected/mutable_reorder_write_up_activated_paper.v
@@ -0,0 +1,160 @@
+(** 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.
+
+
+(** Moving a write to a mutable reference up across unknown code. *)
+
+(* Assuming x : &mut i32 *)
+Definition prot_mutable_reorder_write_up_activated_paper_unopt : expr :=
+    let: "c" := InitCall in
+    (* "x" is the local variable that stores the pointer value "i" *)
+    let: "x" := new_place sizeof_scalar "i" in
+
+    (* retag_place reborrows the pointer value stored in "x" (which is "i"),
+      then updates "x" with the new pointer value. This relies on protectors,
+      hence [FnEntry]. *)
+    retag_place "x" MutRef TyFrz sizeof_scalar FnEntry "c";;
+
+    (* Call the unknown function "f" *)
+    Call #[ScFnPtr "f"] "f_closure_arg" ;;
+
+    (* Write 10 to the cell pointed to by the pointer in "x" *)
+    *{sizeof_scalar} "x" <- #[10] ;;
+
+    (* The unknown code is represented by a call to an unknown function "f" *)
+    let: "v" := Call #[ScFnPtr "g"] "g_closure_arg" in
+
+    (* Write 13 to the cell pointed to by the pointer in "x" *)
+    *{sizeof_scalar} "x" <- #[0] ;;
+
+    (* Free the local variable *)
+    Free "x" ;;
+
+    (* Finally, return the value *)
+    EndCall "c";;
+    "v"
+  .
+
+Definition prot_mutable_reorder_write_up_activated_paper_opt : expr :=
+    let: "c" := InitCall in
+    let: "x" := new_place sizeof_scalar "i" in
+    retag_place "x" MutRef TyFrz sizeof_scalar FnEntry "c";;
+    Call #[ScFnPtr "f"] "f_closure_arg" ;;
+    *{sizeof_scalar} "x" <- #[0] ;;
+    let: "v" := Call #[ScFnPtr "g"] "g_closure_arg" in
+    Free "x" ;;
+    EndCall "c";;
+    "v"
+  .
+
+Lemma prot_mutable_reorder_write_up_activated_paper `{sborGS Σ} :
+  ⊢ log_rel prot_mutable_reorder_write_up_activated_paper_opt prot_mutable_reorder_write_up_activated_paper_unopt.
+Proof.
+  log_rel.
+  iIntros "%f_closure_t %f_closure_s #Hrel_f_closure".
+  iIntros "%r_t %r_s #Hrel".
+  iIntros "%g_closure_t %g_closure_s #Hrel_g_closure".
+  iIntros "!# %Ï€ _".
+  sim_pures.
+  rewrite !subst_result.
+  sim_apply InitCall InitCall sim_init_call "". iIntros (c) "Hcall". iApply sim_expr_base. sim_pures.
+
+  (* new place *)
+  simpl. source_bind (new_place _ _).
+  iApply source_red_safe_reach.
+  { intros. rewrite subst_result. eapply new_place_safe_reach. }
+  simpl. iIntros "(%v_s & -> & %Hsize)". destruct v_s as [|v_s [|?]]; try done.
+  iPoseProof (rrel_value_source with "Hrel") as (v_t) "(-> & #Hv)".
+  iPoseProof (value_rel_length with "Hv") as "%Hlen". destruct v_t as [|v_t [|?]]; try done.
+  iApply source_red_base. iModIntro. to_sim.
+  sim_apply (new_place _ _) (new_place _ _) sim_new_place_local "%t %l % % Htag Ht Hs"; first done.
+  sim_pures.
+
+  target_apply (Copy _) (target_copy_local with "Htag Ht") "Ht Htag". 2: done. 1: rewrite read_range_heaplet_to_list // Z.sub_diag /= //.
+  source_apply (Copy _) (source_copy_local with "Htag Hs") "Hs Htag". 2: done. 1: rewrite read_range_heaplet_to_list // Z.sub_diag /= //.
+
+  (* do the retag *)
+  sim_bind (Retag _ _ _ _ _ _) (Retag _ _ _ _ _ _).
+  iApply sim_safe_implies.
+  iIntros ((_ & ot & i & [= ->] & _)).
+  iPoseProof (value_rel_singleton_source with "Hv") as (sc_t [= ->]) "Hscrel".
+  iPoseProof (sc_rel_ptr_source with "Hscrel") as ([= ->]) "Htagged".
+  iApply (sim_retag_fnentry with "Hscrel Hcall"). 1: by cbv.
+  iIntros (t_i v_t v_s _ Hlen_t Hlen_s) "Hcall #Hvrel Htag_i Hi_t Hi_s".
+  destruct v_t as [|v_t []]; try done.
+  destruct v_s as [|v_s []]; try done. iSimpl in "Hcall".
+  iApply sim_expr_base.
+  target_apply (Write _ _) (target_write_local with "Htag Ht") "Ht Htag".
+  2-3: done. 1: rewrite /write_range bool_decide_true. 2: simpl; lia. 1: rewrite Z.sub_diag /= //.
+  source_apply (Write _ _) (source_write_local with "Htag Hs") "Hs Htag".
+  2: done. 1: rewrite /write_range bool_decide_true. 2: simpl; lia. 1: rewrite Z.sub_diag /= //.
+  sim_pures.
+
+  (* arbitrary code (call to f) *)
+  rewrite !subst_result.
+  sim_apply (Call _ _) (Call _ _) (sim_call _ _ _) ""; first done.
+  iIntros (r_t_f r_s_f) "Hsamef". sim_pures.
+
+  (* do the activation write *)
+  source_apply (Copy (Place _ _ _)) (source_copy_local with "Htag Hs") "Hs Htag". 2: done.
+  1: rewrite read_range_heaplet_to_list // Z.sub_diag /= //.
+  source_pures. source_finish.
+  target_apply (Copy (Place _ _ _)) (target_copy_local with "Htag Ht") "Ht Htag". 2: done.
+  1: rewrite read_range_heaplet_to_list // Z.sub_diag /= //.
+  target_pures.
+
+  sim_apply (Write _ _) (Write _ _) (sim_write_activate_protected with "Htag_i Hi_t Hi_s Hcall") "Htag_i Hi_t Hi_s Hcall". 1-3: done.
+  { intros off Hoff. simpl in *. assert (off = 0)%nat as -> by lia. rewrite /shift_loc /= Z.add_0_r /call_set_in lookup_insert /=. do 2 eexists; split; first done.
+    by rewrite lookup_insert. }
+  sim_pures.
+
+  (* arbitrary code (call to g) *)
+  sim_apply (Call _ _) (Call _ _) (sim_call _ _ _) ""; first done.
+  iIntros (r_t r_s) "Hsame1". sim_pures.
+
+  (* do the source store *)
+  source_apply (Copy (Place _ _ _)) (source_copy_local with "Htag Hs") "Hs Htag". 2: done.
+  1: rewrite read_range_heaplet_to_list // Z.sub_diag /= //.
+  source_pures. 
+  source_apply (Write (Place _ _ _) _) (source_write_protected_active with "Hcall Htag_i Hi_s") "Hi_s Htag_i Hcall". 1,3,4: done.
+  1: { rewrite write_range_to_to_list; last (simpl; lia). rewrite Z.sub_diag /= //. }
+  2: rewrite lookup_insert //.
+  1: intros off (?&?); assert (off = i.2) as -> by (simpl in *; lia); rewrite /shift_loc /= Z.add_0_r lookup_insert; by eexists.
+  source_pures. source_finish.
+
+  (* cleanup: remove the protector ghost state, make the external locations public, free the local locations*)
+  sim_apply (Free _) (Free _) (sim_free_local with "Htag Ht Hs") "Htag"; [done..|]. sim_pures.
+  iApply (sim_make_unique_public with "Hi_t Hi_s Htag_i Hcall []"). 1: by rewrite lookup_insert.
+  { iIntros "_". iApply value_rel_int. }
+  iIntros  "Htag_i Hcall". iEval (rewrite !fmap_insert !fmap_empty !insert_insert /=) in "Hcall".
+  iApply (sim_protected_unprotect_public with "Hcall Htag_i"). 1: by rewrite lookup_insert.
+  iIntros "Hc". iEval (rewrite delete_insert) in "Hc".
+  sim_apply (EndCall _) (EndCall _) (sim_endcall_own with "Hc") "".
+  sim_pures.
+  sim_val. iModIntro. iSplit; first done. done.
+Qed.
+
+Section closed.
+  (** Obtain a closed proof of [ctx_ref]. *)
+  Lemma prot_mutable_reorder_write_up_activated_paper_ctx : ctx_ref prot_mutable_reorder_write_up_activated_paper_opt prot_mutable_reorder_write_up_activated_paper_unopt.
+  Proof.
+    set Σ := #[sborΣ].
+    apply (log_rel_adequacy Σ)=>?.
+    apply prot_mutable_reorder_write_up_activated_paper.
+  Qed.
+End closed.
+
+Check prot_mutable_reorder_write_up_activated_paper_ctx.
+Print Assumptions prot_mutable_reorder_write_up_activated_paper_ctx.
+(* 
+prot_mutable_reorder_write_up_activated_paper_ctx
+     : ctx_ref prot_mutable_reorder_write_up_activated_paper_opt prot_mutable_reorder_write_up_activated_paper_unopt
+Axioms:
+IndefiniteDescription.constructive_indefinite_description : ∀ (A : Type) (P : A → Prop), (∃ x : A, P x) → {x : A | P x}
+Classical_Prop.classic : ∀ P : Prop, P ∨ ¬ P
+*)
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 1a18add3ffc301e3cc10c7d4a3ce8fecd54f6682..74a81dc45a1bd730d8e20e88c89de17155cd3305 100644
--- a/theories/tree_borrows/examples/unprotected/shared_delete_read_escaped.v
+++ b/theories/tree_borrows/examples/unprotected/shared_delete_read_escaped.v
@@ -18,12 +18,12 @@ Definition unprot_shared_delete_read_escaped_unopt : expr :=
       then updates "x" with the new pointer value. A [Default] retag is
       sufficient for this, we don't need the protector. *)
     retag_place "x" ShrRef TyFrz sizeof_scalar Default #[ScCallId 0];;
-    (* a "dummy load" -- since we can not insert loads, we must have a load here to so that it can remain in the target *)
-    (* This load is not used here, but later the target will use the value loaded here *)
-    Copy *{sizeof_scalar} "x" ;;
+    (* Note that val is not actually used in the source, but it will be used in the target. *)
+    let: "val" := Copy *{sizeof_scalar} "x" in
     (* The unknown code is represented by a call to an unknown function "f",
-      which does take the pointer value from "x" as an argument. *)
-    Call #[ScFnPtr "f"] (Copy "x") ;;
+       which does take the pointer value from "x" as an argument.
+       To simulate Rust closures, it also takes an arbitrary closure env. *)
+    Call #[ScFnPtr "f"] (Conc "f_closure_env" (Copy "x")) ;;
 
     (* Read the value "v" from the cell pointed to by the pointer in "x" *)
     let: "v" := Copy *{sizeof_scalar} "x" in
@@ -38,8 +38,9 @@ Definition unprot_shared_delete_read_escaped_unopt : expr :=
 Definition unprot_shared_delete_read_escaped_opt : expr :=
     let: "x" := new_place sizeof_scalar "i" in
     retag_place "x" ShrRef TyFrz sizeof_scalar Default #[ScCallId 0];;
-    let: "v" := Copy *{sizeof_scalar} "x" in
-    Call #[ScFnPtr "f"] (Copy "x") ;;
+    let: "val" := Copy *{sizeof_scalar} "x" in
+    Call #[ScFnPtr "f"] (Conc "f_closure_env" (Copy "x")) ;;
+    let: "v" := "val" in
     Free "x" ;;
     "v"
   .
@@ -49,8 +50,9 @@ Lemma unprot_shared_delete_read_escaped `{sborGS Σ} :
   ⊢ log_rel unprot_shared_delete_read_escaped_opt unprot_shared_delete_read_escaped_unopt.
 Proof.
   log_rel.
-  iIntros "%r_t %r_s #Hrel !# %Ï€ _".
+  iIntros "%closure_env_t %closure_env_s #Hclosure_env_rel %r_t %r_s #Hrel !# %Ï€ _".
   sim_pures.
+  rewrite !subst_result.
 
   (* new place *)
   simpl. source_bind (new_place _ _).
@@ -102,8 +104,14 @@ Proof.
   1: rewrite read_range_heaplet_to_list // Z.sub_diag /= //.
   source_apply (Copy _) (source_copy_local with "Htag Hs") "Hs Htag". 2: done.
   1: rewrite read_range_heaplet_to_list // Z.sub_diag /= //. sim_pures.
-  sim_apply (Call _ _) (Call _ _) (sim_call _ (ValR [ScPtr i _]) (ValR [ScPtr i _])) "".
-  { iApply big_sepL2_singleton. iFrame "Htag_i". done. }
+  rewrite !subst_result.
+  source_bind (Conc _ _).
+  iApply source_red_safe_implies. 1: eapply irred_conc with (r2 := ValR _).
+  iIntros ((closure_env_s_v & v2 & -> & [= <-])).
+  destruct closure_env_t as [closure_env_t_v|]; last done.
+  source_pures. to_sim. sim_pures.
+  sim_apply (Call _ _) (Call _ _) (sim_call _ (ValR _) (ValR _)) "".
+  { iApply big_sepL2_app; first iAssumption. iApply big_sepL2_singleton. iFrame "Htag_i". done. }
   iIntros (r_t r_s) "_". sim_pures.
 
   (* source load (not existing in the target) *)
diff --git a/theories/tree_borrows/read_read_reorder/equivalence_def.v b/theories/tree_borrows/read_read_reorder/equivalence_def.v
new file mode 100644
index 0000000000000000000000000000000000000000..d0e6c122938f5a27548602a3e8e3dd1c4571ad55
--- /dev/null
+++ b/theories/tree_borrows/read_read_reorder/equivalence_def.v
@@ -0,0 +1,34 @@
+From iris.prelude Require Import prelude options.
+From stdpp Require Export gmap.
+From simuliris.tree_borrows Require Import defs lang_base lang notation bor_semantics tree tactics class_instances.
+From simuliris.tree_borrows.read_read_reorder Require Import low_level.
+From iris.prelude Require Import options.
+
+(* [nsteps ... n] says that one can transition from one state to the other in exactly [n]
+primitive steps. *)
+Fixpoint nsteps P (e : expr) σ e'' σ'' n : Prop := match n with
+  0 => e = e'' ∧ σ = σ''
+| S n => ∃ e' σ', prim_step P e σ e' σ' nil ∧ nsteps P e' σ' e'' σ'' n end.
+
+(* This says that after n steps, any state reachable in from e_1 in σ must be reachable from e_2 in σ *)
+Definition identical_states_after P e1 e2 σ n := 
+  ∀ e' σ', nsteps P e1 σ e' σ' n → nsteps P e2 σ e' σ' n.
+
+(* This says that the program will not terminate within a number of steps.
+   It can, in that time, only make progress or have UB *)
+Inductive no_termination_within P : expr → state → nat → Prop := 
+  | no_steps_left e σ : no_termination_within P e σ 0
+  | no_termination_now e σ n :
+     to_result e = None →
+    (∀ e' σ', prim_step P e σ e' σ' nil → no_termination_within P e' σ' n) →
+    no_termination_within P e σ (S n).
+
+(* So, two programs are eventually equal if they are equal after n steps, for some n.
+   This only holds as long as they don't terminate within these n steps.
+   If either program has UB within these n steps, the other program must do so as well. *)
+Definition eventually_equal P e1 e2 :=
+  ∃ n, ∀ σ, state_wf σ →
+    no_termination_within P e1 σ n ∧
+    no_termination_within P e2 σ n ∧
+    identical_states_after P e1 e2 σ n ∧
+    identical_states_after P e2 e1 σ n.
diff --git a/theories/tree_borrows/read_read_reorder/refinement.v b/theories/tree_borrows/read_read_reorder/read_reorder.v
similarity index 92%
rename from theories/tree_borrows/read_read_reorder/refinement.v
rename to theories/tree_borrows/read_read_reorder/read_reorder.v
index f822194ed0357ce1712017e772e44b86cd779225..d62d4deb8348b127d8f4c21c92103cf687eb4740 100644
--- a/theories/tree_borrows/read_read_reorder/refinement.v
+++ b/theories/tree_borrows/read_read_reorder/read_reorder.v
@@ -1,7 +1,7 @@
 From iris.prelude Require Import prelude options.
 From stdpp Require Export gmap.
-From simuliris.tree_borrows Require Import defs lang_base lang notation bor_semantics tree tree_lemmas bor_lemmas steps_preserve tactics class_instances refinement_def.
-From simuliris.tree_borrows.read_read_reorder Require Import low_level refinement_def.
+From simuliris.tree_borrows Require Import defs lang_base lang notation bor_semantics tree tree_lemmas bor_lemmas steps_preserve tactics class_instances.
+From simuliris.tree_borrows.read_read_reorder Require Import low_level equivalence_def.
 From iris.prelude Require Import options.
 
 Definition source (x1 x2 : string) l1 tg1 sz1 l2 tg2 sz2 erest : expr :=
@@ -305,22 +305,34 @@ Proof.
     split; last by destruct σ. rewrite bool_decide_decide decide_True //; congruence.
 Qed.
 
-Lemma read_reorder' x1 x2 l1 tg1 sz1 l2 tg2 sz2 erest P σ :
-  state_wf σ →
+Lemma read_example_no_termination x1 x2 l1 tg1 sz1 l2 tg2 sz2 erest P σ :
   x1 ≠ x2 →
-  identical_states_after P (source x1 x2 l1 tg1 sz1 l2 tg2 sz2 erest) (target x1 x2 l1 tg1 sz1 l2 tg2 sz2 erest) σ 4
-∧ identical_states_after P (target x1 x2 l1 tg1 sz1 l2 tg2 sz2 erest) (source x1 x2 l1 tg1 sz1 l2 tg2 sz2 erest) σ 4.
+  no_termination_within P (source x1 x2 l1 tg1 sz1 l2 tg2 sz2 erest) σ 4.
 Proof.
-  split.
-  all: eapply read_reorder_onesided; done.
+  intros Hne.
+  econstructor; first done.
+  intros e' σ' [(?&[=]&_)|(e1&_&[(v1&trs1&->&_&Hread1&Hcontain1&Happly1&Hne1&->)|[(v1&->&_&Hrd1&->&->)|(->&_&Hread1&Hcontains1&HapplyNone1&->)]]%prim_step_copy_inv&->)]%prim_step_let_inv.
+  all: econstructor; first done.
+  all: intros e' σ' [(?&[= <-]&_&->&->)|(?&[=]&_)]%prim_step_let_inv.
+  all: econstructor; first done.
+  all: intros e' σ' [(?&[=]&_)|(e3&_&[(v3&trs3&->&_&Hread3&Hcontain3&Happly3&Hne2&->)|[(v3&->&_&Hrd3&->&->)|(->&_&Hread3&Hcontains3&HapplyNone3&->)]]%prim_step_copy_inv&->)]%prim_step_let_inv.
+  all: econstructor; first done.
+  all: intros e' σ' [(?&[= <-]&_&->&->)|(?&[=]&_)]%prim_step_let_inv.
+  all: econstructor.
 Qed.
 
 Theorem read_reorder x1 x2 l1 tg1 sz1 l2 tg2 sz2 erest P :
   x1 ≠ x2 →
-  refines_after_nsteps P (source x1 x2 l1 tg1 sz1 l2 tg2 sz2 erest) (target x1 x2 l1 tg1 sz1 l2 tg2 sz2 erest) 4.
+  eventually_equal P (source x1 x2 l1 tg1 sz1 l2 tg2 sz2 erest) (target x1 x2 l1 tg1 sz1 l2 tg2 sz2 erest).
 Proof.
-  intros H1 σ Hσ.
-  eapply read_reorder'; done.
+  intros H1.
+  exists 4.
+  intros σ Hσ.
+  split; first by eapply read_example_no_termination.
+  split; first by eapply read_example_no_termination.
+  split; eapply read_reorder_onesided; done.
 Qed.
 
+
+
 Print Assumptions read_reorder.
diff --git a/theories/tree_borrows/read_read_reorder/refinement_def.v b/theories/tree_borrows/read_read_reorder/refinement_def.v
deleted file mode 100644
index e663ec7f9f688c63469e92a29730b5055eff5fc5..0000000000000000000000000000000000000000
--- a/theories/tree_borrows/read_read_reorder/refinement_def.v
+++ /dev/null
@@ -1,18 +0,0 @@
-From iris.prelude Require Import prelude options.
-From stdpp Require Export gmap.
-From simuliris.tree_borrows Require Import defs lang_base lang notation bor_semantics tree tactics class_instances.
-From simuliris.tree_borrows.read_read_reorder Require Import low_level.
-From iris.prelude Require Import options.
-
-Fixpoint nsteps P (e : expr) σ e'' σ'' n : Prop := match n with
-  0 => e = e'' ∧ σ = σ''
-| S n => ∃ e' σ', prim_step P e σ e' σ' nil ∧ nsteps P e' σ' e'' σ'' n end.
-
-(* An extremely simple simulation relation: After n steps, all actions on one side are reproducible in the other *)
-Definition identical_states_after P e1 e2 σ n := 
-  ∀ e' σ', nsteps P e1 σ e' σ' n → nsteps P e2 σ e' σ' n.
-
-Definition refines_after_nsteps P e1 e2 n :=
-  ∀ σ, state_wf σ →
-    identical_states_after P e1 e2 σ n ∧
-    identical_states_after P e2 e1 σ n.