actually split simulation def and proof

theories/tree_borrows/read_read_reorder/refinement.v

 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.
+From simuliris.tree_borrows.read_read_reorder Require Import low_level refinement_def.
 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 source (x1 x2 : string) l1 tg1 sz1 l2 tg2 sz2 erest : expr :=
   let: x1 := Copy (Place l1 tg1 sz1) in
   let: x2 := Copy (Place l2 tg2 sz2) in