diff --git a/analysis/facts/transform/replace_at.v b/analysis/facts/transform/replace_at.v
index 51a0aad4fc49e7e111dc8a36f4f3da40fc90098e..eabb219985c2d69283bedd9f2ea43822ccad92d2 100644
--- a/analysis/facts/transform/replace_at.v
+++ b/analysis/facts/transform/replace_at.v
@@ -25,8 +25,16 @@ Section ReplaceAtFacts.
      t'. *)
   Let sched' := replace_at sched t' nstate.
 
-  (** We begin with the trivial observation that the schedule doesn't change at
-      other times. *)
+  (** We begin with the trivial observation that [replace_at sched t' nstate]
+      indeed returns [nstate] at time [t']. *)
+  Lemma replace_at_def:
+    sched' t' = nstate.
+  Proof.
+    rewrite /sched' /replace_at.
+    now apply ifT.
+  Qed.
+
+  (** Equally trivially, the schedule doesn't change at other times. *)
   Lemma rest_of_schedule_invariant:
     forall t, t <> t' -> sched' t = sched t.
   Proof.