diff --git a/analysis/abstract/restricted_supply/bounded_bi/aux.v b/analysis/abstract/restricted_supply/bounded_bi/aux.v
index f3251a490d4685481a6b331f2b923b128d5ecf12..6c5134a00d8b488406ec76fb918d5c3a12fd40b0 100644
--- a/analysis/abstract/restricted_supply/bounded_bi/aux.v
+++ b/analysis/abstract/restricted_supply/bounded_bi/aux.v
@@ -45,9 +45,6 @@ Section BoundedBusyIntervalsAux.
   (** ... and assume that the schedule is valid. *)
   Hypothesis H_sched_valid : valid_schedule sched arr_seq.
 
-  (** Furthermore, we assume that the schedule is work-conserving. *)
-  Hypothesis H_work_conserving : work_conserving arr_seq sched.
-
   (** Recall that [busy_intervals_are_bounded_by] is an abstract
       notion. Hence, we need to introduce interference and interfering
       workload. We will use the restricted-supply instantiations. *)
@@ -65,6 +62,9 @@ Section BoundedBusyIntervalsAux.
   #[local] Instance rs_jlfp_interfering_workload : InterferingWorkload Job :=
     rs_jlfp_interfering_workload arr_seq sched.
 
+  (** Assume that the schedule is work-conserving in the abstract sense. *)
+  Hypothesis H_work_conserving : abstract.definitions.work_conserving arr_seq sched.
+
   (** Consider any job [j] of task [tsk] that has a positive job cost
       and is in the arrival sequence. *)
   Variable j : Job.
@@ -143,8 +143,7 @@ Section BoundedBusyIntervalsAux.
     { rewrite /service_during /cumulative_interference /cumul_cond_interference  /cond_interference /service_at.
       rewrite -big_split //= -{1}(sum_of_ones t1 δ) big_nat [in X in _ <= X]big_nat.
       apply leq_sum => x /andP[Lo Hi].
-      { eapply instantiated_i_and_w_are_coherent_with_schedule in H_work_conserving; eauto 2 => //.
-        move: (H_work_conserving j t1 t2 x) => Workj.
+      { move: (H_work_conserving j t1 t2 x) => Workj.
         feed_n 4 Workj; try done.
         { by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix. }
         { by apply/andP; split; eapply leq_trans; eauto. }
diff --git a/analysis/abstract/restricted_supply/bounded_bi/edf.v b/analysis/abstract/restricted_supply/bounded_bi/edf.v
index b7c3dabeed069eda52da76408d82ba198d5a26c1..0eb61050f3abe0d1da0344634afeb0afbdee6915 100644
--- a/analysis/abstract/restricted_supply/bounded_bi/edf.v
+++ b/analysis/abstract/restricted_supply/bounded_bi/edf.v
@@ -66,10 +66,7 @@ Section BoundedBusyIntervals.
   Hypothesis H_valid_model_with_bounded_nonpreemptive_segments :
     valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
 
-  (** Furthermore, we assume that the schedule is work-conserving ... *)
-  Hypothesis H_work_conserving : work_conserving arr_seq sched.
-
-  (** ... and that it respects the scheduling policy. *)
+  (** Furthermore, assume that the schedule respects the scheduling policy. *)
   Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).
 
   (** Recall that [busy_intervals_are_bounded_by] is an abstract
@@ -89,6 +86,9 @@ Section BoundedBusyIntervals.
   #[local] Instance rs_jlfp_interfering_workload : InterferingWorkload Job :=
     rs_jlfp_interfering_workload arr_seq sched.
 
+  (** Assume that the schedule is work-conserving in the abstract sense. *)
+  Hypothesis H_work_conserving : abstract.definitions.work_conserving arr_seq sched.
+
   (** Consider an arbitrary task set [ts], ... *)
   Variable ts : seq Task.
 
@@ -173,7 +173,7 @@ Section BoundedBusyIntervals.
         { apply workload_of_jobs_weaken => jo; move: LP; clear.
           by rewrite /hep_job /EDF /job_deadline /job_deadline_from_task_deadline; lia. }
         erewrite workload_of_jobs_partitioned_by_tasks with (ts := undup ts).
-        + eapply leq_trans; first by apply sum_le_subseq, undup_subseq. 
+        + eapply leq_trans; first by apply sum_le_subseq, undup_subseq.
           apply leq_sum_seq => tsk_o INo HEP; rewrite -(leqRW (workload_le_rbf' _ _ _ _ _ _ _)) //.
           have [A | B] := (leqP δ (task_deadline (job_task jlp) - task_deadline tsk_o)).
           { by apply workload_of_jobs_reduce_range; lia. }
@@ -320,7 +320,6 @@ Section BoundedBusyIntervals.
         }
         eapply busy_interval.busy_interval_is_bounded; eauto 2 => //.
         - by eapply instantiated_i_and_w_no_speculative_execution; eauto 2 => //.
-        - by eapply instantiated_i_and_w_are_coherent_with_schedule; eauto 2 => //.
         - by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix => //.
         - by apply workload_is_bounded => //.
       Qed.
diff --git a/analysis/abstract/restricted_supply/bounded_bi/fp.v b/analysis/abstract/restricted_supply/bounded_bi/fp.v
index 2311d885c7eb831597aeb47bb81d543a49b3f129..374a602e29dfdb1fc09699033645d8c19378e26f 100644
--- a/analysis/abstract/restricted_supply/bounded_bi/fp.v
+++ b/analysis/abstract/restricted_supply/bounded_bi/fp.v
@@ -59,10 +59,7 @@ Section BoundedBusyIntervals.
   Hypothesis H_valid_model_with_bounded_nonpreemptive_segments :
     valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
 
-  (** Furthermore, we assume that the schedule is work-conserving ... *)
-  Hypothesis H_work_conserving : work_conserving arr_seq sched.
-
-  (** ... and that it respects the scheduling policy. *)
+  (** Furthermore, assume that the schedule respects the scheduling policy. *)
   Hypothesis H_respects_policy : respects_FP_policy_at_preemption_point arr_seq sched FP.
 
   (** Recall that [busy_intervals_are_bounded_by] is an abstract
@@ -82,6 +79,9 @@ Section BoundedBusyIntervals.
   #[local] Instance rs_jlfp_interfering_workload : InterferingWorkload Job :=
     rs_jlfp_interfering_workload arr_seq sched.
 
+  (** Assume that the schedule is work-conserving in the abstract sense. *)
+  Hypothesis H_work_conserving : definitions.work_conserving arr_seq sched.
+
   (** Consider an arbitrary task set [ts], ... *)
   Variable ts : list Task.
 
@@ -186,7 +186,6 @@ Section BoundedBusyIntervals.
         }
         eapply busy_interval.busy_interval_is_bounded; eauto 2 => //.
         - by eapply instantiated_i_and_w_no_speculative_execution; eauto 2 => //.
-        - by eapply instantiated_i_and_w_are_coherent_with_schedule; eauto 2 => //.
         - by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix => //.
         - by apply workload_is_bounded => //.
       Qed.
@@ -303,3 +302,4 @@ Section BoundedBusyIntervals.
   Qed.
 
 End BoundedBusyIntervals.
+
diff --git a/analysis/abstract/restricted_supply/bounded_bi/jlfp.v b/analysis/abstract/restricted_supply/bounded_bi/jlfp.v
index 044c60cda29cefd0b7ec87d33d082fbfa90b59e3..86064a3e5a1ec347d45128de0853d5733c974fb1 100644
--- a/analysis/abstract/restricted_supply/bounded_bi/jlfp.v
+++ b/analysis/abstract/restricted_supply/bounded_bi/jlfp.v
@@ -61,13 +61,6 @@ Section BoundedBusyIntervals.
   Hypothesis H_valid_model_with_bounded_nonpreemptive_segments :
     valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
 
-  (** Furthermore, we assume that the schedule is work-conserving ... *)
-  Hypothesis H_work_conserving : work_conserving arr_seq sched.
-
-  (** ... and that it respects the scheduling policy. *)
-  Hypothesis H_respects_policy :
-    respects_JLFP_policy_at_preemption_point arr_seq sched JLFP.
-
   (** Recall that [busy_intervals_are_bounded_by] is an abstract
       notion. Hence, we need to introduce interference and interfering
       workload. We will use the restricted-supply instantiations. *)
@@ -85,6 +78,10 @@ Section BoundedBusyIntervals.
   #[local] Instance rs_jlfp_interfering_workload : InterferingWorkload Job :=
     rs_jlfp_interfering_workload arr_seq sched.
 
+  (** In the following, we assume that the scheduler is work-conserving in the
+      abstract sense. *)
+  Hypothesis H_work_conserving : abstract.definitions.work_conserving arr_seq sched.
+
   (** Consider an arbitrary task set [ts], ... *)
   Variable ts : list Task.
 
@@ -199,7 +196,6 @@ Section BoundedBusyIntervals.
         }
         eapply busy_interval.busy_interval_is_bounded; eauto 2 => //.
         - by eapply instantiated_i_and_w_no_speculative_execution; eauto 2 => //.
-        - by eapply instantiated_i_and_w_are_coherent_with_schedule; eauto 2 => //.
         - by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix => //.
         - by apply workload_is_bounded => //.
       Qed.
diff --git a/results/rs/edf/floating_nonpreemptive.v b/results/rs/edf/floating_nonpreemptive.v
index 997bd1cdeb9591b9feca9a36200639508807a21f..13883298a84b1f3d564a777f72ed82d77b739a73 100644
--- a/results/rs/edf/floating_nonpreemptive.v
+++ b/results/rs/edf/floating_nonpreemptive.v
@@ -205,6 +205,7 @@ Section RTAforFloatingEDFModelwithArrivalCurves.
     - exact: EDF_implies_sequential_tasks.
     - exact: instantiated_interference_and_workload_consistent_with_sequential_tasks.
     - apply: busy_intervals_are_bounded_rs_edf => //.
+      by apply: instantiated_i_and_w_are_coherent_with_schedule.
     - apply: valid_pred_sbf_switch_predicate; last by exact: H_valid_SBF.
       move => ? ? ? ? [? ?]; split => //.
       by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
diff --git a/results/rs/edf/fully_nonpreemptive.v b/results/rs/edf/fully_nonpreemptive.v
index 15560d9a79d5f8b6a7217b7dfe84eed9e77e6e9f..ac7a615b6cd5d65c699e9ff20c296abbcb7cb77a 100644
--- a/results/rs/edf/fully_nonpreemptive.v
+++ b/results/rs/edf/fully_nonpreemptive.v
@@ -197,6 +197,7 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
     - exact: EDF_implies_sequential_tasks.
     - exact: instantiated_interference_and_workload_consistent_with_sequential_tasks.
     - apply: busy_intervals_are_bounded_rs_edf => //.
+      exact: instantiated_i_and_w_are_coherent_with_schedule.
     - apply: valid_pred_sbf_switch_predicate; last by exact: H_valid_SBF.
       move => ? ? ? ? [? ?]; split => //.
       by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
@@ -211,4 +212,5 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
         by split; [rewrite -(leqRW FIX1) /task_rbf | ]; lia.
   Qed.
 
+
 End RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
diff --git a/results/rs/edf/fully_preemptive.v b/results/rs/edf/fully_preemptive.v
index e6ee0ffedd298561141d787f768ee5a974a5aadc..1e093cb891628142e2c8dae1cd2524c974fd4863 100644
--- a/results/rs/edf/fully_preemptive.v
+++ b/results/rs/edf/fully_preemptive.v
@@ -188,6 +188,7 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
     - exact: EDF_implies_sequential_tasks.
     - exact: instantiated_interference_and_workload_consistent_with_sequential_tasks.
     - eapply busy_intervals_are_bounded_rs_jlfp; try done.
+      + exact: instantiated_i_and_w_are_coherent_with_schedule.
       + apply: service_inversion_is_bounded => // => ? ? ? ? ? ?.
         exact: nonpreemptive_segments_bounded_by_blocking.
       + by rewrite BLOCK add0n; apply H_fixed_point.
@@ -206,4 +207,5 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
         by rewrite BLOCK subnn //= add0n addn0 subn0.
   Qed.
 
+
 End RTAforFullyPreemptiveEDFModelwithArrivalCurves.
diff --git a/results/rs/edf/limited_preemptive.v b/results/rs/edf/limited_preemptive.v
index 2d5bbbf9a46a417fa106fd1ac75bccca9b803edb..b65deb5fea3ed9955c1b4153317ff438005f0bdf 100644
--- a/results/rs/edf/limited_preemptive.v
+++ b/results/rs/edf/limited_preemptive.v
@@ -207,6 +207,7 @@ Section RTAforLimitedPreemptiveEDFModelwithArrivalCurves.
     - exact: EDF_implies_sequential_tasks.
     - exact: instantiated_interference_and_workload_consistent_with_sequential_tasks.
     - apply: busy_intervals_are_bounded_rs_edf => //.
+      by apply: instantiated_i_and_w_are_coherent_with_schedule.
     - apply: valid_pred_sbf_switch_predicate; last by exact: H_valid_SBF.
       move => ? ? ? ? [? ?]; split => //.
       by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
diff --git a/results/rs/fifo/bounded_nps.v b/results/rs/fifo/bounded_nps.v
index 0eb2b8f48edd4cf188d3045884de54e39de2c508..4f311265bde1da23d03113996f14a59f54acf4ee 100644
--- a/results/rs/fifo/bounded_nps.v
+++ b/results/rs/fifo/bounded_nps.v
@@ -190,7 +190,8 @@ Section RTAforFullyPreemptiveFIFOModelwithArrivalCurves.
            (intra_IBF  := fun A Δ => (\sum_(tsko <- ts) task_request_bound_function tsko (A + ε)) - task_cost tsk) => //.
     - exact: instantiated_i_and_w_are_coherent_with_schedule.
     - eapply busy_intervals_are_bounded_rs_jlfp with (blocking_bound := fun _ => 0)=> //.
-      by apply: FIFO_implies_no_service_inversion.
+      + exact: instantiated_i_and_w_are_coherent_with_schedule.
+      + by apply: FIFO_implies_no_service_inversion.
     - apply: valid_pred_sbf_switch_predicate; last by exact: H_valid_SBF.
       move => ? ? ? ? [? ?]; split => //.
       by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
diff --git a/results/rs/fp/floating_nonpreemptive.v b/results/rs/fp/floating_nonpreemptive.v
index 5dcf0ffe831c599c3342321d0e50c0999c4bfee1..c66b9a9abc3cc8017e18ee225bf894bf080315f1 100644
--- a/results/rs/fp/floating_nonpreemptive.v
+++ b/results/rs/fp/floating_nonpreemptive.v
@@ -212,7 +212,8 @@ Section RTAforFloatingFPModelwithArrivalCurves.
     - exact: instantiated_i_and_w_are_coherent_with_schedule.
     - exact: sequential_readiness_implies_sequential_tasks.
     - exact: instantiated_interference_and_workload_consistent_with_sequential_tasks.
-    - exact: busy_intervals_are_bounded_rs_fp.
+    - apply: busy_intervals_are_bounded_rs_fp => //=.
+      by apply: instantiated_i_and_w_are_coherent_with_schedule.
     - apply: valid_pred_sbf_switch_predicate; last by exact: H_valid_SBF.
       move => ? ? ? ? [? ?]; split => //.
       by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
diff --git a/results/rs/fp/fully_nonpreemptive.v b/results/rs/fp/fully_nonpreemptive.v
index 60e2f739aa42c8d34922bae834b29b2f22003c32..723f0edca5b8c8ce9688c1d9ed2260ab47e5c190 100644
--- a/results/rs/fp/fully_nonpreemptive.v
+++ b/results/rs/fp/fully_nonpreemptive.v
@@ -203,7 +203,8 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
     - exact: instantiated_i_and_w_are_coherent_with_schedule.
     - exact: sequential_readiness_implies_sequential_tasks.
     - exact: instantiated_interference_and_workload_consistent_with_sequential_tasks.
-    - by apply: busy_intervals_are_bounded_rs_fp => //; rewrite BLOCK add0n.
+    - apply: busy_intervals_are_bounded_rs_fp => //.
+      by apply: instantiated_i_and_w_are_coherent_with_schedule.
     - apply: valid_pred_sbf_switch_predicate; last by exact: H_valid_SBF.
       move => ? ? ? ? [? ?]; split => //.
       by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
diff --git a/results/rs/fp/fully_preemptive.v b/results/rs/fp/fully_preemptive.v
index 110b7fa4c07bba4a399c461dab5196d97d3a6abb..d815ee2bdac9cfe4ae5bac5408c528b223f33c04 100644
--- a/results/rs/fp/fully_preemptive.v
+++ b/results/rs/fp/fully_preemptive.v
@@ -201,7 +201,9 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
     - exact: instantiated_i_and_w_are_coherent_with_schedule.
     - exact: sequential_readiness_implies_sequential_tasks.
     - exact: instantiated_interference_and_workload_consistent_with_sequential_tasks.
-    - by apply: busy_intervals_are_bounded_rs_fp => //; rewrite BLOCK add0n.
+    - apply: busy_intervals_are_bounded_rs_fp => //=.
+      + exact: instantiated_i_and_w_are_coherent_with_schedule.
+      + by rewrite BLOCK add0n.
     - apply: valid_pred_sbf_switch_predicate; last by exact: H_valid_SBF.
       move => ? ? ? ? [? ?]; split => //.
       by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
@@ -217,4 +219,5 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
         by rewrite BLOCK subnn //= add0n addn0 subn0.
   Qed.
 
+
 End RTAforFullyPreemptiveFPModelwithArrivalCurves.
diff --git a/results/rs/fp/limited_preemptive.v b/results/rs/fp/limited_preemptive.v
index 78572798a3dcaf2b9d0db8d861b99fc44edc6b9e..bae6d9e03936f3adee71953551983aa214fc113f 100644
--- a/results/rs/fp/limited_preemptive.v
+++ b/results/rs/fp/limited_preemptive.v
@@ -214,7 +214,8 @@ Section RTAforLimitedPreemptiveFPModelwithArrivalCurves.
     - exact: instantiated_i_and_w_are_coherent_with_schedule.
     - exact: sequential_readiness_implies_sequential_tasks.
     - exact: instantiated_interference_and_workload_consistent_with_sequential_tasks.
-    - exact: busy_intervals_are_bounded_rs_fp.
+    - apply: busy_intervals_are_bounded_rs_fp => //=.
+      by apply: instantiated_i_and_w_are_coherent_with_schedule.
     - apply: valid_pred_sbf_switch_predicate; last by exact: H_valid_SBF.
       move => ? ? ? ? [? ?]; split => //.
       by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.