diff --git a/classic/model/schedule/global/basic/schedule.v b/classic/model/schedule/global/basic/schedule.v
index 0aa8316a8aba5de960c5e046b1db1eee1dacb3f1..ee5f7f2181e5fd3a230cf356a2ed00afc15fe5a0 100644
--- a/classic/model/schedule/global/basic/schedule.v
+++ b/classic/model/schedule/global/basic/schedule.v
@@ -226,7 +226,7 @@ Module Schedule.
         {
           move: SCHED => /existsP [cpu SCHED]; des.
           rewrite -big_filter (bigD1_seq cpu);
-            [simpl | | by rewrite filter_index_enum enum_uniq];
+            [simpl | | by have [e _ [UNIQ _ ] _] := big_enumP];
               last by rewrite mem_filter; apply/andP; split.
           rewrite -big_filter -filter_predI big_filter.
           rewrite -> eq_bigr with (F2 := fun cpu => 0);
@@ -610,4 +610,4 @@ Module ScheduleOfSporadicTask.
 
   End BasicLemmas.
   
-End ScheduleOfSporadicTask.
\ No newline at end of file
+End ScheduleOfSporadicTask.