diff --git a/implementation/facts/generic_schedule.v b/implementation/facts/generic_schedule.v
index 14207570894b28d4f244d72a7b337d79bac95e5c..7c092d4a9d01c62788d978f949a81dd7cc9c0ded 100644
--- a/implementation/facts/generic_schedule.v
+++ b/implementation/facts/generic_schedule.v
@@ -68,7 +68,7 @@ Section GenericScheduleProperties.
   Qed.
 
   (** A crucial fact is that a prefix up to horizon [h1] is identical to a
-       prefix up to a later horizon [h2] at times up to [h1]. *)
+      prefix up to a later horizon [h2] at times up to [h1]. *)
   Lemma schedule_up_to_prefix_inclusion:
     forall h1 h2,
       h1 <= h2 ->
@@ -84,4 +84,17 @@ Section GenericScheduleProperties.
     now apply (leq_trans t_H1).
   Qed.
 
+  (** It follows that [generic_schedule] and [schedule_up_to] for a given
+      horizon [h] share an identical prefix. *)
+  Corollary schedule_up_to_identical_prefix:
+    forall h t,
+      t <= h.+1 ->
+      identical_prefix (schedule_up_to policy idle_state h) (generic_schedule policy idle_state) t.
+  Proof.
+    move=> h t LE.
+    rewrite /identical_prefix /generic_schedule => t' LT.
+    rewrite (schedule_up_to_prefix_inclusion t' h) //.
+    by move: (leq_trans LT LE); rewrite ltnS.
+  Qed.
+
 End GenericScheduleProperties.
diff --git a/implementation/facts/ideal_uni/preemption_aware.v b/implementation/facts/ideal_uni/preemption_aware.v
index fa50d0604270753882b881f3414cb9867f729388..e00a3f96a63dcea269d02e607c0a975a107cb9be 100644
--- a/implementation/facts/ideal_uni/preemption_aware.v
+++ b/implementation/facts/ideal_uni/preemption_aware.v
@@ -150,8 +150,7 @@ Section NPUniprocessorScheduler.
             move: (H_chooses_from_set _ _ _ IN).
             rewrite mem_filter /backlogged => /andP [/andP [READY _]  _].
             rewrite -(H_nonclairvoyant_job_readiness (schedule_up_to policy idle_state t') schedule j t'.+1) //.
-            rewrite /identical_prefix /schedule /np_uni_schedule /generic_schedule => t'' LT.
-            now rewrite (schedule_up_to_prefix_inclusion _  _  t'' t') //. }
+            by apply schedule_up_to_identical_prefix. }
           case: (schedule_up_to _ _ t' t') => [j' | IN]; last by apply JOB.
           destruct (~~ job_preemptable j' _) eqn:NP => [EQ|IN]; last by apply JOB.
           apply H_valid_preemption_behavior.