diff --git a/theories/tree_borrows/read_read_reorder/equivalence_def.v b/theories/tree_borrows/read_read_reorder/equivalence_def.v
index d0e6c122938f5a27548602a3e8e3dd1c4571ad55..8a3b266d6259e841e6eb804ed6bc530c147ab6c0 100644
--- a/theories/tree_borrows/read_read_reorder/equivalence_def.v
+++ b/theories/tree_borrows/read_read_reorder/equivalence_def.v
@@ -10,7 +10,8 @@ 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 σ *)
+(* This says that after n steps, any state reachable in from e_1 in σ must be reachable from e_2 in σ.
+   This is just a helper definition used for [eventually_equal]; on its own it is not very meaningful. *)
 Definition identical_states_after P e1 e2 σ n := 
   ∀ e' σ', nsteps P e1 σ e' σ' n → nsteps P e2 σ e' σ' n.
 
@@ -23,9 +24,8 @@ Inductive no_termination_within P : expr → state → nat → Prop :=
     (∀ 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. *)
+(* Two programs are eventually equal if they both do not terminate with n steps,
+  and after n steps, they are equal. *)
 Definition eventually_equal P e1 e2 :=
   ∃ n, ∀ σ, state_wf σ →
     no_termination_within P e1 σ n ∧