diff --git a/theories/tree_borrows/bor_semantics.v b/theories/tree_borrows/bor_semantics.v
index f7fec05bcd093c452a3588111b0b456f37076779..3ca74fe0a904bf06403a7c8c70e94d6a733a5d25 100755
--- a/theories/tree_borrows/bor_semantics.v
+++ b/theories/tree_borrows/bor_semantics.v
@@ -896,14 +896,14 @@ Inductive bor_step (trs : trees) (cids : call_id_set) (nxtp : nat) (nxtc : call_
       trs cids nxtp nxtc
       (CopyEvt alloc tg range val)
       trs cids nxtp nxtc
-  | FailedCopyIS (alloc : block) range tg
+(*  | FailedCopyIS (alloc : block) range tg
     (* Unsuccessful read access just returns poison instead of causing UB *)
     (EXISTS_TAG : trees_contain tg trs alloc)
     (ACC : apply_within_trees (memory_access AccessRead cids tg range) alloc trs = None) :
     bor_step
       trs cids nxtp nxtc
       (FailedCopyEvt alloc tg range)
-      trs cids nxtp nxtc
+      trs cids nxtp nxtc *)
   | WriteIS trs' (alloc : block) range tg val
     (* Successful write access *)
     (EXISTS_TAG: trees_contain tg trs alloc)
diff --git a/theories/tree_borrows/class_instances.v b/theories/tree_borrows/class_instances.v
index 8401138f2397639cebc274b6ca856c3cdb03f8e0..985b8b09679927f47dc5321c9b6c27d266d64b72 100755
--- a/theories/tree_borrows/class_instances.v
+++ b/theories/tree_borrows/class_instances.v
@@ -224,7 +224,7 @@ Section safe_reach.
   Global Instance safe_implies_copy_place P σ l tg (sz:nat) :
     SafeImplies (  (∃ v, read_mem l sz σ.(shp) = Some v ∧ trees_contain tg σ.(strs) l.1 ∧ is_Some (apply_within_trees (memory_access AccessRead σ.(scs) tg (l.2, sz)) l.1 σ.(strs)) ∧ sz ≠ 0%nat)
                  ∨ (∃ v, read_mem l sz σ.(shp) = Some v ∧ sz = 0%nat)
-                 ∨ (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)))) P (Copy (Place l tg sz)) σ.
+                 (*∨ (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)))*)) P (Copy (Place l tg sz)) σ.
   Proof. prove_safe_implies. Qed.
 
   Global Instance safe_implies_write_val_left1 P σ v v' :
diff --git a/theories/tree_borrows/examples/unprotected/mutable_delete_read.v b/theories/tree_borrows/examples/unprotected/mutable_delete_read.v
index 64b2cf7e67f2237bc2ba739a81f479335c352453..910a6bb0662e7849934d8ec4a7c49cfc3172f4d7 100644
--- a/theories/tree_borrows/examples/unprotected/mutable_delete_read.v
+++ b/theories/tree_borrows/examples/unprotected/mutable_delete_read.v
@@ -115,7 +115,7 @@ Proof.
 
   iApply (source_copy_in_simulation with "[] Htag_i Hi_s"). 1: done.
   2: simpl; lia. 1: rewrite read_range_heaplet_to_list // Z.sub_diag /= //.
-  { iLeft. iApply value_rel_int. }
+  { iApply value_rel_int. }
   iIntros (v_res) "Hi_s Htag_i Hv_res". source_pures. source_finish.
   sim_pures.
 
diff --git a/theories/tree_borrows/expr_semantics.v b/theories/tree_borrows/expr_semantics.v
index 330bbabfc65dc1995a68db26cf3fea8bd20a493f..2c95b010d4e274facbda4f9017743d9a527008db 100755
--- a/theories/tree_borrows/expr_semantics.v
+++ b/theories/tree_borrows/expr_semantics.v
@@ -506,10 +506,10 @@ 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
+(*| 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) []
+    mem_expr_step h (Copy (Place (blk, l) lbor sz)) (FailedCopyEvt blk lbor (l, sz)) h (Val $ replicate sz ScPoison) []*)
 | WriteBS blk l lbor sz v
     (LEN: length v = sz)
     (DEFINED: ∀ (i: nat), (i < length v)%nat → (blk,l) +ₗ i ∈ dom h) :
diff --git a/theories/tree_borrows/lang_base.v b/theories/tree_borrows/lang_base.v
index 1fa25466917890ce8c85b3c778367bc6cc71b7fc..d621d0ad06d55cc1a327d58e5d039745f1d44ddb 100755
--- a/theories/tree_borrows/lang_base.v
+++ b/theories/tree_borrows/lang_base.v
@@ -457,7 +457,7 @@ Inductive event :=
 | AllocEvt (alloc : block) (lbor : tag) (range : Z * nat)
 | DeallocEvt (alloc : block) (lbor: tag) (range : Z * nat)
 | CopyEvt (alloc : block) (lbor : tag) (range : Z * nat) (v : value)
-| FailedCopyEvt (alloc : block) (lbor : tag) (range : Z * nat)
+(* | FailedCopyEvt (alloc : block) (lbor : tag) (range : Z * nat) *)
 | WriteEvt (alloc : block) (lbor : tag) (range : Z * nat) (v : value)
 | InitCallEvt (c : call_id)
 | EndCallEvt (c : call_id)
diff --git a/theories/tree_borrows/logical_state.v b/theories/tree_borrows/logical_state.v
index 6ccfadcc1ca53f6b429a5cf29976a92051ed5d55..32c71941b929307fa65c319f9f3548909f216f0e 100755
--- a/theories/tree_borrows/logical_state.v
+++ b/theories/tree_borrows/logical_state.v
@@ -1799,8 +1799,8 @@ Section val_rel.
     rewrite /value_rel. iApply (big_sepL2_app with "Hv1 Hv2").
   Qed.
 
-  Definition will_read_in_simulation v_src v_tgt l_rd t : iProp Σ :=
-    value_rel v_tgt v_src ∨ (⌜length v_src = length v_tgt⌝ ∗ ispoison (replicate (length v_tgt) ScPoison) l_rd t (length v_tgt)).
+  Definition will_read_in_simulation v_src v_tgt (l_rd : loc) (t : tag) : iProp Σ :=
+    value_rel v_tgt v_src(* ∨ (⌜length v_src = length v_tgt⌝ ∗ ispoison (replicate (length v_tgt) ScPoison) l_rd t (length v_tgt))*).
 
 End val_rel.
 
diff --git a/theories/tree_borrows/read_read_reorder/low_level.v b/theories/tree_borrows/read_read_reorder/low_level.v
index 7eebd89f171e28d27c05b7ad8d9f2ea6e6edf372..3406e20301ab63bff80a75169a209ab45975414c 100644
--- a/theories/tree_borrows/read_read_reorder/low_level.v
+++ b/theories/tree_borrows/read_read_reorder/low_level.v
@@ -831,9 +831,9 @@ Lemma CopyEvt_commutes
       trs2 cids2 nxtp2 nxtc2
   .
 Proof.
-  inversion Step1 as [|????? EXISTS1 ACC1 SZ1| | | | | | | | |].
+  inversion Step1 as [|????? EXISTS1 ACC1 SZ1| | | | | | | |].
   - subst.
-    inversion Step2 as [|????? EXISTS2 ACC2 SZ2| | | | | | | | |].
+    inversion Step2 as [|????? EXISTS2 ACC2 SZ2| | | | | | | |].
     + subst.
       destruct (apply_read_within_trees_commutes _ _ _ ACC1 ACC2) as [trs1' [ACC2' ACC1']].
       exists trs1'. exists cids2. exists nxtp2. exists nxtc2.
@@ -853,7 +853,7 @@ Proof.
       1: econstructor 3; auto.
       econstructor; eauto.
   - subst.
-    inversion Step2 as [|????? EXISTS2 ACC2 SZ2| | | | | | | | |].
+    inversion Step2 as [|????? EXISTS2 ACC2 SZ2| | | | | | | |].
     + subst.
       repeat eexists.
       1: econstructor; eauto.
diff --git a/theories/tree_borrows/read_read_reorder/read_reorder.v b/theories/tree_borrows/read_read_reorder/read_reorder.v
index d62d4deb8348b127d8f4c21c92103cf687eb4740..0cfc440c632b8aac8eed83b841afab716a398148 100644
--- a/theories/tree_borrows/read_read_reorder/read_reorder.v
+++ b/theories/tree_borrows/read_read_reorder/read_reorder.v
@@ -73,7 +73,7 @@ Lemma prim_step_copy_inv l tg sz P σ e' σ' tt :
   prim_step P (Copy (Place l tg sz)) σ e' σ' tt →
   (∃ v trs', e' = (#v)%E ∧ tt = nil ∧ read_mem l sz (shp σ) = Some v ∧ trees_contain tg (strs σ) l.1 ∧ apply_within_trees (memory_access AccessRead (scs σ) tg (l.2, sz)) l.1 (strs σ) = Some trs' ∧ sz ≠ 0 ∧ σ' = mkState (shp σ) trs' (scs σ) (snp σ) (snc σ))
 ∨ (∃ v, e' = (#v)%E ∧ tt = nil ∧ read_mem l sz (shp σ) = Some v ∧ sz = 0 ∧ σ' = σ)
-∨ (e' = (#(replicate sz ☠%S))%E ∧ tt = nil ∧ is_Some (read_mem l sz (shp σ)) ∧ trees_contain tg (strs σ) l.1 ∧ apply_within_trees (memory_access AccessRead (scs σ) tg (l.2, sz)) l.1 (strs σ) = None ∧ σ' = σ).
+(*∨ (e' = (#(replicate sz ☠%S))%E ∧ tt = nil ∧ is_Some (read_mem l sz (shp σ)) ∧ trees_contain tg (strs σ) l.1 ∧ apply_within_trees (memory_access AccessRead (scs σ) tg (l.2, sz)) l.1 (strs σ) = None ∧ σ' = σ)*).
 Proof.
   intros H%prim_base_step.
   2: solve_sub_redexes_are_values.
@@ -82,11 +82,11 @@ Proof.
   inversion ME; simplify_eq.
   - inversion IE; simplify_eq.
     + left. do 2 eexists. done.
-    + right. left. eexists. do 4 (split; first done). by destruct σ.
-  - simpl in *.
+    + right. eexists. do 4 (split; first done). by destruct σ.
+(*  - simpl in *.
     inversion IE; simplify_eq. right. right.
     do 5 (split; first done).
-    by destruct σ.
+    by destruct σ. *)
 Qed.
 
 Lemma subst_val_twice_exchange e x1 x2 v1 v2 :
@@ -114,10 +114,10 @@ Lemma read_reorder_onesided x1 x2 l1 tg1 sz1 l2 tg2 sz2 erest P σ :
 Proof.
   destruct l1 as [blk1 off1], l2 as [blk2 off2].
   intros Hwf Hne.
-  intros e4 σ4 (e1' & σ1 & [(?&[=]&_)|(e1&_&[(v1&trs1&->&_&Hread1&Hcontain1&Happly1&Hne1&->)|[(v1&->&_&Hrd1&->&->)|(->&_&Hread1&Hcontains1&HapplyNone1&->)]]%prim_step_copy_inv&->)]%prim_step_let_inv & Hrst).
+  intros e4 σ4 (e1' & σ1 & [(?&[=]&_)|(e1&_&[(v1&trs1&->&_&Hread1&Hcontain1&Happly1&Hne1&->)|(v1&->&_&Hrd1&->&->)]%prim_step_copy_inv&->)]%prim_step_let_inv & Hrst).
   all: destruct Hrst as (e2 & σ2 & [(?&[= <-]&_&->&->)|(?&[=]&_)]%prim_step_let_inv & Hrst).
   all: simpl in *|-.
-  all: destruct Hrst as (e3' & σ3 & [(?&[=]&_)|(e3&_&[(v3&trs3&->&_&Hread3&Hcontain3&Happly3&Hne2&->)|[(v3&->&_&Hrd3&->&->)|(->&_&Hread3&Hcontains3&HapplyNone3&->)]]%prim_step_copy_inv&->)]%prim_step_let_inv & Hrst).
+  all: destruct Hrst as (e3' & σ3 & [(?&[=]&_)|(e3&_&[(v3&trs3&->&_&Hread3&Hcontain3&Happly3&Hne2&->)|(v3&->&_&Hrd3&->&->)]%prim_step_copy_inv&->)]%prim_step_let_inv & Hrst).
   all: simpl in *|-.
   all: destruct Hrst as (e4' & σ4' & [(?&[= <-]&_&->&->)|(?&[=]&_)]%prim_step_let_inv & <- & <-).
   all: rewrite /target. 
@@ -162,7 +162,7 @@ Proof.
     { simpl. eapply base_prim_step.
       econstructor 1. econstructor. 1: done. done. }
     split; last done. rewrite bool_decide_decide decide_True //; congruence.
-  - (* read x1: succeed, read x2: fail *)
+(*  - (* read x1: succeed, read x2: fail *)
     do 2 eexists. split.
     { change (Let x2 ?a ?b) with (fill [LetEctx x2 b] a).
       eapply fill_prim_step. eapply base_prim_step.
@@ -174,7 +174,6 @@ Proof.
         * eassumption.
         * eassumption.
     }
-    (* this admit needs the theorem saying that if it fails after the other read has succeeded, it also succeeds earlier *)
     do 2 eexists. split.
     { simpl. eapply base_prim_step.
       econstructor 1. econstructor. 1: done. done. }
@@ -186,7 +185,7 @@ Proof.
     do 2 eexists. split.
     { simpl. eapply base_prim_step.
       econstructor 1. econstructor. 1: done. done. }
-    split; last done. rewrite bool_decide_decide decide_True //; congruence.
+    split; last done. rewrite bool_decide_decide decide_True //; congruence. *)
   - (* read x1: zerosized, read x2: succeed *)
     do 2 eexists. split.
     { change (Let x2 ?a ?b) with (fill [LetEctx x2 b] a).
@@ -223,7 +222,7 @@ Proof.
     { simpl. eapply base_prim_step.
       econstructor 1. econstructor. 1: done. done. }
     split; last by destruct σ. rewrite bool_decide_decide decide_True //; congruence.
-  - (* read x1: zerosized, read x2: fail *)
+(*  - (* read x1: zerosized, read x2: fail *)
     do 2 eexists. split.
     { change (Let x2 ?a ?b) with (fill [LetEctx x2 b] a).
       eapply fill_prim_step. eapply base_prim_step.
@@ -302,7 +301,7 @@ Proof.
     do 2 eexists. split.
     { simpl. eapply base_prim_step.
       econstructor 1. econstructor. 1: done. done. }
-    split; last by destruct σ. rewrite bool_decide_decide decide_True //; congruence.
+    split; last by destruct σ. rewrite bool_decide_decide decide_True //; congruence. *)
 Qed.
 
 Lemma read_example_no_termination x1 x2 l1 tg1 sz1 l2 tg2 sz2 erest P σ :
@@ -311,11 +310,11 @@ Lemma read_example_no_termination x1 x2 l1 tg1 sz1 l2 tg2 sz2 erest P σ :
 Proof.
   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.
+  intros e' σ' [(?&[=]&_)|(e1&_&[(v1&trs1&->&_&Hread1&Hcontain1&Happly1&Hne1&->)|(v1&->&_&Hrd1&->&->)]%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: intros e' σ' [(?&[=]&_)|(e3&_&[(v3&trs3&->&_&Hread3&Hcontain3&Happly3&Hne2&->)|(v3&->&_&Hrd3&->&->)]%prim_step_copy_inv&->)]%prim_step_let_inv.
   all: econstructor; first done.
   all: intros e' σ' [(?&[= <-]&_&->&->)|(?&[=]&_)]%prim_step_let_inv.
   all: econstructor.
diff --git a/theories/tree_borrows/step_laws/steps_local.v b/theories/tree_borrows/step_laws/steps_local.v
index b5f8c61987663cd9f6637567fba867a2404f87e6..512e4adb2c4d5439e7912a19beca28f00aef80f9 100644
--- a/theories/tree_borrows/step_laws/steps_local.v
+++ b/theories/tree_borrows/step_laws/steps_local.v
@@ -50,19 +50,19 @@ Proof.
   { iPureIntro. do 3 eexists. eapply copy_base_step'. 1: done. 2: exact READ_MEM. 2: exact TREES_NOCHANGE.
     rewrite /trees_contain /trees_at_block /= Hit. subst t. cbv. tauto. }
   iIntros (??? Hstep).
-  eapply head_copy_inv in Hstep as (->&[((HNone&_&_&_)&_)|(trs'&v'&->&->&Hreadv'&[(_&Happly&Hnon)|(Hzero&->&->)])]).
-  1: rewrite /= TREES_NOCHANGE // in HNone.
+  eapply head_copy_inv in Hstep as (->&trs'&v'&->&->&Hreadv'&[(_&Happly&Hnon)|(Hzero&->&->)]).
   - iModIntro. iSplitR; first done.
     assert (v_rd = v') as -> by congruence.
     iSplitR "Htag Ht Hsim"; last first.
     1: iApply ("Hsim" with "Ht Htag").
-    iFrame. simpl in Happly. assert (trs' = strs σ_t) as -> by congruence.
+    iFrame "HP_t HP_s".
+    simpl in Happly. assert (trs' = strs σ_t) as -> by congruence.
     iExists _, _, _, _. destruct σ_t. iApply "Hbor".
   - iModIntro. iSplitR; first done.
     assert (v_rd = []) as -> by by destruct v_rd.
     iSplitR "Htag Ht Hsim"; last first.
     1: iApply ("Hsim" with "Ht Htag").
-    iFrame.
+    iFrame "HP_t HP_s".
     iExists _, _, _, _. destruct σ_t. iApply "Hbor".
 Qed.
 
@@ -96,7 +96,7 @@ Proof.
   iModIntro.
   iSplitR "Htag Ht Hsim"; last first.
   1: iApply ("Hsim" with "Ht Htag").
-  iFrame. destruct σ_s; simpl.
+  iFrame "HP_t HP_s". destruct σ_s; simpl.
   iExists _, _, _, _. iApply "Hbor".
 Qed.
 
@@ -134,7 +134,8 @@ Proof.
   iIntros (??? Hstep). pose proof Hstep as Hstep2.
   eapply head_write_inv in Hstep2 as (trs'&->&->&->&_&Hiinv&[(Hcont&Happly&Hlen)|(Hlen&->)]); last first.
   { iModIntro. iSplit; first done.
-    assert (v_wr = nil) as -> by by destruct v_wr. iFrame.
+    assert (v_wr = nil) as -> by by destruct v_wr.
+    iFrame "HP_t HP_s".
     iSplitL "Hbor". 1: repeat iExists _; destruct σ_t; done.
     eapply write_range_to_list_is_Some in Hwrite as (x&Hx&_). simpl in Hx. subst v_t'.
     iApply ("Hsim" with "Ht Htag"). }
diff --git a/theories/tree_borrows/step_laws/steps_prot.v b/theories/tree_borrows/step_laws/steps_prot.v
index f83ce82d265e96dd57f1bc839e59cf716c202760..1b9df53a76b362a1d4a96bee2f1db18e25157a8d 100644
--- a/theories/tree_borrows/step_laws/steps_prot.v
+++ b/theories/tree_borrows/step_laws/steps_prot.v
@@ -54,8 +54,8 @@ Proof.
   iSplit.
   { iPureIntro. do 3 eexists. eapply copy_base_step'. 1: done. 2: exact READ_MEM. 2: exact Htrs'. done. }
   iIntros (??? Hstep). pose proof Hstep as Hstep2.
-  eapply head_copy_inv in Hstep2 as (->&[((HNone&_&_&_)&_)|(trs''&v'&->&->&Hreadv'&[(_&Htrs''&Hnon)|(Hzero&->&->)])]).
-  1: rewrite /= Htrs' // in HNone. 2: done.
+  eapply head_copy_inv in Hstep2 as (->&trs''&v'&->&->&Hreadv'&[(_&Htrs''&Hnon)|(Hzero&->&->)]).
+  2: done.
   assert (trs'' = trs') as ->.
   { rewrite /memory_access Htrs' in Htrs''. congruence. }
   assert (v_rd = v') as -> by congruence.
diff --git a/theories/tree_borrows/step_laws/steps_read_write_simple.v b/theories/tree_borrows/step_laws/steps_read_write_simple.v
index 458bff3772d72c0160f0f5240b513445aa942785..d839a85f9e7f00af6757310d2bffae3716eaaf81 100644
--- a/theories/tree_borrows/step_laws/steps_read_write_simple.v
+++ b/theories/tree_borrows/step_laws/steps_read_write_simple.v
@@ -33,9 +33,7 @@ Proof.
   { iPureIntro. do 3 eexists. econstructor 2. 1: eapply CopyBS. 1: done.
     eapply ZeroCopyIS. done. }
   iIntros (e_t' efs_t σ_t' Hstep).
-  eapply head_copy_inv in Hstep as (->&[((HNone&->&->&HH1)&Hintree)|(trs'&v'&->&->&Hread&[(_&_&HH)|(_&->&->)])]).
-  - iModIntro. iSplit; first done. simpl. iFrame "Hsim".
-    iFrame.
+  eapply head_copy_inv in Hstep as (->&trs'&v'&->&->&Hread&[(_&_&HH)|(_&->&->)]).
   - lia.
   - iModIntro. iSplit; first done. simpl. iFrame "HP_s HP_t Hsim". do 4 iExists _. destruct σ_t. done.
 Qed.
@@ -69,7 +67,7 @@ Proof.
   eapply head_write_inv in Hstep as (trs'&->&->&->&_&_&[(_&_&?)|(_&->)]).
   - lia.
   - iModIntro. iSplit; first done. simpl. iFrame "Hsim".
-    iFrame. destruct σ_t. by repeat iExists _.
+    iFrame "HP_t HP_s". destruct σ_t. by repeat iExists _.
 Qed.
 
 Lemma source_write_zero l t v π Ψ :
@@ -102,9 +100,9 @@ Proof.
   destruct Hsafe as [Hpool Hsafe].
   iPoseProof (bor_interp_get_pure with "Hbor") as "%Hp".
   destruct Hp as (Hstrs_eq & Hsnp_eq & Hsnc_eq & Hscs_eq & Hwf_s & Hwf_t & Hdom_eq).
-  specialize (pool_safe_implies Hsafe Hpool) as [(vr_s&Hreadmem&Hcontain_s&(trs_s'&Htrss)&_)|[(_&_&[]%Hne)|(Hcontain_s&Hnotrees&Hisval)]];
+  specialize (pool_safe_implies Hsafe Hpool) as [(vr_s&Hreadmem&Hcontain_s&(trs_s'&Htrss)&_)|(_&_&[]%Hne)];
   pose proof Hcontain_s as Hcontain_t; rewrite trees_equal_same_tags in Hcontain_t; try done; last first.
-  { (* We get poison *)
+(*  { (* We get poison *)
     assert (apply_within_trees (memory_access AccessRead (scs σ_s) bor_s (l_s.2, sz)) l_s.1 (strs σ_t) = None) as Hnotrees_t.
     { destruct apply_within_trees eqn:HSome in |-*; try done.
       eapply mk_is_Some, trees_equal_allows_more_access in HSome as (x&Hx); first by erewrite Hnotrees in Hx.
@@ -120,7 +118,7 @@ Proof.
     { iPureIntro. subst e_t'. destruct σ_s, l_s. simpl. do 2 econstructor; by eauto. }
     simpl. iFrame. iSplit; last done. subst e_t'.
     iApply "Hsim". iApply big_sepL_sepL2_diag. iApply big_sepL_forall. by iIntros (k v (->&_)%lookup_replicate_1).
-  }
+  } *)
   edestruct trees_equal_allows_more_access as (trs_t'&Htrst).
   1: done. 1: eapply Hwf_s. 1,2,3: rewrite ?Hscs_eq; eapply Hwf_t. 1: done. 1: done. 1: by eapply mk_is_Some.
   opose proof (trees_equal_preserved_by_access _ _ _ _ _ _ _ Hstrs_eq _ Htrss Htrst) as Hstrs_eq'.
@@ -131,7 +129,7 @@ Proof.
   { iPureIntro. do 3 eexists. eapply copy_base_step'. 1-3: done. rewrite -Hscs_eq. done. }
   (* we keep the base_step hypotheses to use the [base_step_wf] lemma below *)
   iIntros (e_t' efs_t σ_t') "%Hhead_t".
-  specialize (head_copy_inv _ _ _ _ _ _ _ _ Hhead_t) as (->&[((Hnotree&->&Hpoison&Hheapsome)&Hcontains_t)|(tr'&vr_t'&->&Hσ_t'&H3&[(Hcontains_t&H4&_)|([]%Hne&_&_)])]); first congruence.
+  specialize (head_copy_inv _ _ _ _ _ _ _ _ Hhead_t) as (->&tr'&vr_t'&->&Hσ_t'&H3&[(Hcontains_t&H4&_)|([]%Hne&_&_)]).
   assert (vr_t' = vr_t) as -> by congruence.
   assert (tr' = trs_t') as -> by congruence.
   clear H3 H4.
diff --git a/theories/tree_borrows/step_laws/steps_source_only.v b/theories/tree_borrows/step_laws/steps_source_only.v
index c8f1ee6db2b25898a8abf53d54a1ab8f50a9ce18..b1c08a4e44195bf797e6d24ddb656cd18f4c5cd8 100644
--- a/theories/tree_borrows/step_laws/steps_source_only.v
+++ b/theories/tree_borrows/step_laws/steps_source_only.v
@@ -31,7 +31,7 @@ Lemma source_copy_any v_t v_rd sz l_hl l_rd t π Ψ tk :
   l_hl.1 = l_rd.1 →
   t $$ tk -∗
   l_hl ↦s∗[tk]{t} v_t -∗
-  (∀ v_res, l_hl ↦s∗[tk]{t} v_t -∗ t $$ tk -∗ (⌜v_res = v_rd⌝ ∨ ispoison v_res l_rd t sz) -∗ source_red #v_res π Ψ)%E -∗
+  (∀ v_res, l_hl ↦s∗[tk]{t} v_t -∗ t $$ tk -∗ (⌜v_res = v_rd⌝) -∗ source_red #v_res π Ψ)%E -∗
   source_red (Copy (Place l_rd t sz)) π Ψ.
 Proof.
   iIntros (Hnz Hread Hsameblk) "Htag Hs Hsim". eapply read_range_length in Hread as HH. subst sz.
@@ -40,9 +40,9 @@ Proof.
   destruct Hp as (Hstrs_eq & Hsnp_eq & Hsnc_eq & Hscs_eq & Hwf_s & Hwf_t & Hdom_eq).
   iModIntro. iDestruct "Hbor" as "(%M_call & %M_tag & %M_t & %M_s & Hbor)".
   eapply pool_safe_implies in Ht_s as Hfoo. 2: done.
-  destruct Hfoo as [(v_rd'&Hv_rd&Hcont&Hreadsome&_)|[(v_nil&Hread_nil&Hiszero)|(Hcont&Happly_none&Hmemsome)]]; last first.
+  destruct Hfoo as [(v_rd'&Hv_rd&Hcont&Hreadsome&_)|(v_nil&Hread_nil&Hiszero)].
   2: lia.
-  { (* poison *)
+(*  { (* poison *)
     pose proof Happly_none as Hn2.
     rewrite /apply_within_trees in Hn2.
     rewrite /trees_contain /trees_at_block in Hcont.
@@ -88,7 +88,7 @@ Proof.
       1: simpl; lia. simpl. assert ((l_rd +â‚— Z.to_nat (l - l_rd.2) = (l_rd.1, l))) as ->. 2: done.
       rewrite /shift_loc /=. simpl. f_equal. lia. }
     1: iSplitR "Hsim"; last by iApply "Hsim".
-    do 4 iExists _; destruct σ_s; iFrame. iFrame "Hsrel". done. }
+    do 4 iExists _; destruct σ_s; iFrame. iFrame "Hsrel". done. } *)
   iPoseProof (bor_interp_readN_source_after_accesss with "Hbor Hs Htag") as "(%it&%tr&%Hit&%Htr&%Hown)".
   1: exact Hread. 1: done. 1: done. 1: done. 1: exact Hreadsome.
   opose proof* (read_range_list_to_heaplet_read_memory_strict) as READ_MEM. 1: exact Hread. 1: done.
@@ -122,7 +122,7 @@ Proof.
 
   iModIntro.
   iSplitR "Hs Htag Hsim".
-  2: { iApply ("Hsim" with "Hs Htag"). iLeft. by iPureIntro. }
+  2: { iApply ("Hsim" with "Hs Htag"). by iPureIntro. }
   iFrame "HP_t HP_s". iExists M_call, M_tag, M_t, M_s.
   iFrame "Hc Htag_auth Htag_t_auth Htag_s_auth".
   iSplitL "Htainted"; last iSplitL "Hpub_cid". 3: iSplit; last iSplit; last (iPureIntro; split_and!).
@@ -145,7 +145,7 @@ Proof.
   - eapply (base_step_wf P_s). 2: exact Hwf_s. eapply copy_base_step'. 1: done. 2: exact READ_MEM. 2: exact Htrs'. done.
   - done.
 Qed.
-
+(*
 Lemma source_copy_poison v_t v_rd sz l_hl l_rd t π Ψ tk v_read_earlier :
   sz ≠ 0%nat → (* if it is 0, it will not be poison *)
   read_range l_rd.2 sz (list_to_heaplet v_t l_hl.2) = Some v_rd →
@@ -183,7 +183,7 @@ Proof.
     opose proof (disabled_tag_no_access _ false _ AccessRead _ (l_rd.2 + i) (l_rd.2, length v_rd) _ HH _) as HNone.
     1: by eapply Hwf_s. 1: split; simpl in *; lia.
     rewrite /memory_access HNone in Hreadsome. simpl in Hreadsome. by destruct Hreadsome.
-Qed.
+Qed. *)
 
 
 Lemma source_copy_in_simulation v_t v_rd v_tgt sz l_hl l_rd t π Ψ tk :
@@ -198,12 +198,13 @@ Lemma source_copy_in_simulation v_t v_rd v_tgt sz l_hl l_rd t π Ψ tk :
 Proof.
   iIntros (Hsz Hrr Hhl).
   eapply read_range_length in Hrr as Hszlen.
-  iIntros "#[Hrel|Hpoison] Htk Hhl Hsim".
+  iIntros "#Hrel Htk Hhl Hsim".
+  rewrite /will_read_in_simulation.
   - iPoseProof (value_rel_length with "Hrel") as "%Hlen".
     iApply (source_copy_any with "Htk Hhl [Hsim]"). 1-3: done.
-    iIntros (v_res) "Hhl Htk [->|#(%i&(%Hp1&%Hp2)&Hpoison2)]";
+    iIntros (v_res) "Hhl Htk ->";
       iApply ("Hsim" with "Hhl Htk").
-    + done.
+    + done. (*
     + rewrite Hp2. iApply big_sepL2_forall. iSplit. 1: iPureIntro; rewrite length_replicate; lia.
       iIntros (k sc1 sc2 _ (->&HH2)%lookup_replicate_1). iApply sc_rel_source_poison.
   - subst sz. iDestruct "Hpoison" as "(%Hlen&Hpoison)".
@@ -212,7 +213,7 @@ Proof.
     iIntros (v_res) "Hhl Htk #(%i&(%Hp1&%Hp2)&Hpoison2)".
     iApply ("Hsim" with "Hhl Htk").
     rewrite Hp2. iApply big_sepL2_forall. iSplit. 1: iPureIntro; rewrite length_replicate; lia.
-    iIntros (k sc1 sc2 _ (->&HH2)%lookup_replicate_1). iApply sc_rel_source_poison.
+    iIntros (k sc1 sc2 _ (->&HH2)%lookup_replicate_1). iApply sc_rel_source_poison. *)
 Qed.
 
 
diff --git a/theories/tree_borrows/step_laws/steps_unique.v b/theories/tree_borrows/step_laws/steps_unique.v
index 3f067ec989d8b903d10a0add74c94c0e61ce7041..03cede0bdaed34d5d9a0235f5685500bdb5ed927 100644
--- a/theories/tree_borrows/step_laws/steps_unique.v
+++ b/theories/tree_borrows/step_laws/steps_unique.v
@@ -34,7 +34,7 @@ Lemma sim_copy v_t v_s v_rd_t v_rd_s sz l_hl l_rd t π tk Φ :
   t $$ tk -∗
   l_hl ↦s∗[tk]{t} v_s -∗
   l_hl ↦t∗[tk]{t} v_t -∗
-  (∀ v_res_s v_res_t, l_hl ↦s∗[tk]{t} v_s -∗ l_hl ↦t∗[tk]{t} v_t -∗ t $$ tk -∗ (⌜v_res_s = v_rd_s ∧ v_res_t = v_rd_t⌝ ∨ ispoison v_res_s l_rd t sz ∗ ispoison v_res_t l_rd t sz) -∗ #v_res_t ⪯{π} #v_res_s  [{ Φ }])%E -∗
+  (∀ v_res_s v_res_t, l_hl ↦s∗[tk]{t} v_s -∗ l_hl ↦t∗[tk]{t} v_t -∗ t $$ tk -∗ (⌜v_res_s = v_rd_s ∧ v_res_t = v_rd_t⌝ (*∨ ispoison v_res_s l_rd t sz ∗ ispoison v_res_t l_rd t sz*)) -∗ #v_res_t ⪯{π} #v_res_s  [{ Φ }])%E -∗
   (Copy (Place l_rd t sz))  ⪯{π} (Copy (Place l_rd t sz))  [{ Φ }].
 Proof.
   iIntros (Hsz Hreadt Hreads Hl) "Htk Hs Ht Hsim".
@@ -43,9 +43,9 @@ Proof.
   destruct Hsafe as [Hpool Hsafe].
   iPoseProof (bor_interp_get_pure with "Hbor") as "%Hp".
   destruct Hp as (Hstrs_eq & Hsnp_eq & Hsnc_eq & Hscs_eq & Hwf_s & Hwf_t & Hdom_eq).
-  specialize (pool_safe_implies Hsafe Hpool) as [(vr_s&Hreadmem&Hcontain_s&(trs_s'&Htrss)&_)|[(_&_&[]%Hsz)|(Hcontain_s&Hnotrees&Hisval)]];
+  specialize (pool_safe_implies Hsafe Hpool) as [(vr_s&Hreadmem&Hcontain_s&(trs_s'&Htrss)&_)|(_&_&[]%Hsz)];
   pose proof Hcontain_s as Hcontain_t; rewrite trees_equal_same_tags in Hcontain_t; try done; last first.
-  { (* We get poison *)
+(*  { (* We get poison *)
     assert (apply_within_trees (memory_access AccessRead (scs σ_s) t (l_rd.2, sz)) l_rd.1 (strs σ_t) = None) as Hnotrees_t.
     { destruct apply_within_trees eqn:HSome in |-*; try done.
       eapply mk_is_Some, trees_equal_allows_more_access in HSome as (x&Hx); first by erewrite Hnotrees in Hx.
@@ -112,7 +112,7 @@ Proof.
      iSplitR "Hsim".
      { do 4 iExists _; destruct σ_s; iFrame. iFrame "Hsrel". done. }
      simpl. rewrite Hpoison. subst sz. iSplit; last done. iApply "Hsim".
-  }
+  } *)
   edestruct trees_equal_allows_more_access as (trs_t'&Htrst).
   1: done. 1: eapply Hwf_s. 1,2,3: rewrite ?Hscs_eq; eapply Hwf_t. 1: done. 1: done. 1: by eapply mk_is_Some.
   opose proof (trees_equal_preserved_by_access _ _ _ _ _ _ _ Hstrs_eq _ Htrss Htrst) as Hstrs_eq'.
@@ -123,7 +123,7 @@ Proof.
   { iPureIntro. do 3 eexists. eapply copy_base_step'. 1-3: done. rewrite -Hscs_eq. done. }
   (* we keep the base_step hypotheses to use the [base_step_wf] lemma below *)
   iIntros (e_t' efs_t σ_t') "%Hhead_t".
-  specialize (head_copy_inv _ _ _ _ _ _ _ _ Hhead_t) as (->&[((Hnotree&->&Hpoison&Hheapsome)&Hcontains_t)|(tr'&vr_t'&->&Hσ_t'&H3&[(Hcontains_t&H4&_)|([]%Hsz&_&_)])]); first congruence.
+  specialize (head_copy_inv _ _ _ _ _ _ _ _ Hhead_t) as (->&tr'&vr_t'&->&Hσ_t'&H3&[(Hcontains_t&H4&_)|([]%Hsz&_&_)]).
   assert (vr_t' = vr_t) as -> by congruence.
   assert (tr' = trs_t') as -> by congruence.
   clear H3 H4.
@@ -190,7 +190,7 @@ Proof.
   }
   iSplitL; last done.
 
-  iApply ("Hsim" with "Hs Ht Htk"). iLeft. iPureIntro.
+  iApply ("Hsim" with "Hs Ht Htk"). iPureIntro.
   eapply read_range_list_to_heaplet_read_memory_strict in Hreads. 2: done.
   2: intros i Hi; specialize (Howns i Hi) as (_&H); exact H.
   eapply read_range_list_to_heaplet_read_memory_strict in Hreadt. 2: done.
@@ -203,37 +203,37 @@ Qed.
 Lemma sim_into_read_for_simulation v_res_t v_res_s v_rd_t v_rd_s l_rd t :
   let sz := length v_rd_t in
   value_rel v_rd_t v_rd_s -∗
-  (⌜v_res_s = v_rd_s ∧ v_res_t = v_rd_t⌝ ∨ ispoison v_res_s l_rd t sz ∗ ispoison v_res_t l_rd t sz) -∗
+  (⌜v_res_s = v_rd_s ∧ v_res_t = v_rd_t⌝ (*∨ ispoison v_res_s l_rd t sz ∗ ispoison v_res_t l_rd t sz*)) -∗
   will_read_in_simulation v_rd_s v_res_t l_rd t.
 Proof.
   intros sz. iIntros "Hv1 Hor".
   iPoseProof (value_rel_length with "Hv1") as "%Hlen".
-  iDestruct "Hor" as "[(->&->)|(Hp1&Hp2)]".
-  { iLeft. done. }
+  iDestruct "Hor" as "(->&->)".
+  { done. } (*
   iRight. subst sz.
   iDestruct "Hp2" as "(%i&(_&%HH)&_)". rewrite HH.
   rewrite length_replicate Hlen. iSplit; first done.
   iDestruct "Hp1" as "(%ip&(%H1&%H2)&Hpp)". iExists ip. iSplit; last done.
   rewrite length_replicate. iPureIntro; split. 2: done.
-  rewrite H2 length_replicate in H1. lia.
+  rewrite H2 length_replicate in H1. lia. *)
 Qed.
 
-Lemma sim_read_result_value_rel v_res_t v_res_s v_rd_t v_rd_s l_rd t :
+Lemma sim_read_result_value_rel v_res_t v_res_s v_rd_t v_rd_s :
   let sz := length v_rd_t in
   value_rel v_rd_t v_rd_s -∗
-  (⌜v_res_s = v_rd_s ∧ v_res_t = v_rd_t⌝ ∨ ispoison v_res_s l_rd t sz ∗ ispoison v_res_t l_rd t sz) -∗
+  (⌜v_res_s = v_rd_s ∧ v_res_t = v_rd_t⌝ (* ∨ ispoison v_res_s l_rd t sz ∗ ispoison v_res_t l_rd t sz *) ) -∗
   value_rel v_res_t v_res_s.
 Proof.
   intros sz. iIntros "Hv1 Hor".
   iPoseProof (value_rel_length with "Hv1") as "%Hlen".
-  iDestruct "Hor" as "[(->&->)|(Hp1&Hp2)]".
-  { done. }
+  iDestruct "Hor" as "(->&->)".
+  { done. } (*
   subst sz.
   iDestruct "Hp2" as "(%i&(_&%HH)&_)". rewrite HH.
   iDestruct "Hp1" as "(%ip&(%H1&%H2)&Hpp)". rewrite H2.
   iApply big_sepL2_forall. iSplit.
   { rewrite length_replicate //. }
-  iIntros (k x1 x2 (->&_)%lookup_replicate_1 (->&_)%lookup_replicate_1). done.
+  iIntros (k x1 x2 (->&_)%lookup_replicate_1 (->&_)%lookup_replicate_1). done. *)
 Qed.
 
 
diff --git a/theories/tree_borrows/steps_inv.v b/theories/tree_borrows/steps_inv.v
index 998037c114e8cfe56efb74d009881fbdbe3d6702..bfbd451b3aca0a6a9588eec7cb7096b585d2461d 100755
--- a/theories/tree_borrows/steps_inv.v
+++ b/theories/tree_borrows/steps_inv.v
@@ -17,11 +17,11 @@ Proof. intros Hhead. inv_base_step. eauto 8. Qed.
 Lemma head_copy_inv (P : prog) l bor sz σ σ' e' efs :
   base_step P (Copy (Place l bor sz)) σ e' σ' efs →
   efs = [] ∧
-((apply_within_trees (memory_access AccessRead (scs σ) bor (l.2, sz)) l.1 σ.(strs) = None ∧
+((*(apply_within_trees (memory_access AccessRead (scs σ) bor (l.2, sz)) l.1 σ.(strs) = None ∧
   σ = σ' ∧
   e' = ValR (replicate sz ScPoison)%V ∧
   is_Some (read_mem l sz σ.(shp))) ∧
-  trees_contain bor σ.(strs) l.1 ∨
+  trees_contain bor σ.(strs) l.1 ∨  *)
   ∃ trs' (v':value),
   e' = (v')%E ∧
   σ' = mkState σ.(shp) trs' σ.(scs) σ.(snp) σ.(snc) ∧
diff --git a/theories/tree_borrows/steps_progress.v b/theories/tree_borrows/steps_progress.v
index 455b3620788b349ef60647a9115c9d41dd1b56d4..fde62d28633a1be6ace1d0d03d01b564490bda4d 100755
--- a/theories/tree_borrows/steps_progress.v
+++ b/theories/tree_borrows/steps_progress.v
@@ -547,6 +547,7 @@ Proof.
   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 →
@@ -555,7 +556,7 @@ Lemma failed_copy_base_step' P (σ: state) l tg sz (WF: state_wf σ) :
 Proof.
   intros TC Happly. destruct l, σ. do 2 econstructor; by eauto.
 Qed.
-
+*)
 (*
 
 Lemma access1_write_is_Some cids stk bor
diff --git a/theories/tree_borrows/steps_wf.v b/theories/tree_borrows/steps_wf.v
index 2d4409a92391365c4019134ddd00e36fcd0053b7..8aa035bd98f01cdb64c347fa46fc95a43f4d8e88 100755
--- a/theories/tree_borrows/steps_wf.v
+++ b/theories/tree_borrows/steps_wf.v
@@ -888,7 +888,7 @@ Proof.
   destruct σ as [h trs cids nxtp nxtc].
   destruct σ' as [h' trs' cids' nxtp' nxtc']. simpl.
   intros BS IS WF. inversion BS. clear BS. simplify_eq.
-  inversion IS as [x| | | | | | | | | |]; clear IS. simpl in *; simplify_eq. constructor; simpl.
+  inversion IS as [x| | | | | | | | |]; clear IS. simpl in *; simplify_eq. constructor; simpl.
   - apply same_blocks_init_extend; [lia|].
     apply WF.
   - apply extend_trees_wf.
@@ -1758,7 +1758,7 @@ Proof.
   destruct σ' as [h' trs' cids' nxtp' nxtc']. simpl.
   intros BS IS WF.
   inversion BS; clear BS; simplify_eq.
-  inversion IS as [ | | | | | | | |trs'' ???? ACC | | ]; clear IS; simplify_eq.
+  inversion IS as [ | | | | | | |trs'' ???? ACC | | ]; clear IS; simplify_eq.
   destruct (trees_deallocate_isSome _ _ _ _ _ _ (mk_is_Some _ _ ACC)) as [x [Lookup Update]].
   assert (each_tree_parents_more_init trs'') as HH1.
   { eapply apply_within_trees_deallocate_compat_parents_more_init; try done.
@@ -1845,11 +1845,12 @@ Proof.
   destruct σ' as [h' trs' cids' nxtp' nxtc']. simpl.
   intros BS IS WF.
   inversion BS; clear BS; simplify_eq.
-  inversion IS as [ |?????? ACC| | | | | | | | | ]; clear IS; simplify_eq.
+  inversion IS as [ |?????? ACC| | | | | | | | ]; clear IS; simplify_eq.
   - eapply (access_step_wf_inner σ false); done.
   - 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)
@@ -1863,7 +1864,7 @@ Proof.
   inversion BS. clear BS. simplify_eq.
   inversion IS; clear IS; simplify_eq.
   done.
-Qed.
+Qed. *)
 
 (* TODO less equalities makes applying the rule easier, see _sane version below *)
 Lemma write_mem_dom l (vl : value) h h'
@@ -2004,7 +2005,7 @@ Proof.
   destruct σ' as [h' trs' cids' nxtp' nxtc']. simpl.
   intros BS IS WF.
   inversion BS; clear BS; simplify_eq.
-  inversion IS as [ | | | |?????? ACC |???? RANGE_SIZE| | | | | ]; clear IS; simplify_eq.
+  inversion IS as [ | | |?????? ACC |???? RANGE_SIZE| | | | | ]; clear IS; simplify_eq.
   2: { simpl in RANGE_SIZE. destruct vl; last done. simpl. done. }
   constructor; simpl.
   - rewrite /same_blocks.
@@ -3217,7 +3218,7 @@ Proof.
   destruct σ' as [h' trs' cids' nxtp' nxtc']. simpl.
   intros BS IS WF.
   inversion BS. clear BS. simplify_eq.
-  inversion IS as [| | | | | |trsmid ???????? EXISTS_TAG FRESH_CHILD RETAG_EFFECT READ_ON_REBOR| | | |].
+  inversion IS as [| | | | |trsmid ???????? EXISTS_TAG FRESH_CHILD RETAG_EFFECT READ_ON_REBOR| | | |].
   2: by simplify_eq. simplify_eq.
   eapply retag_step_wf_inner in WF as (WF&TAG_AFTER_ADD); simpl in WF|-*. 2-5: try done.
   eapply access_step_wf_inner in WF. all: done.
@@ -3231,7 +3232,7 @@ Proof.
   - eapply alloc_step_wf; eauto.
   - eapply dealloc_step_wf; eauto.
   - eapply read_step_wf; eauto.
-  - eapply failed_copy_step_wf; eauto.
+ (* - eapply failed_copy_step_wf; eauto. *)
   - eapply write_step_wf; eauto.
   - eapply initcall_step_wf; eauto.
   - eapply endcall_step_wf; eauto.