diff --git a/theories/tree_borrows/read_read_reorder/equivalence_def.v b/theories/tree_borrows/read_read_reorder/equivalence_def.v
index 8a3b266d6259e841e6eb804ed6bc530c147ab6c0..2892d463a0515659331aae2eecc95f457f6ea4b1 100644
--- a/theories/tree_borrows/read_read_reorder/equivalence_def.v
+++ b/theories/tree_borrows/read_read_reorder/equivalence_def.v
@@ -24,7 +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).
 
-(* Two programs are eventually equal if they both do not terminate with n steps,
+(* Two programs are eventually equal if there exists an n such that they
+   both do not terminate with n steps,
   and after n steps, they are equal. *)
 Definition eventually_equal P e1 e2 :=
   ∃ n, ∀ σ, state_wf σ →