diff --git a/rt/analysis/completion_time.v b/rt/analysis/completion_time.v
index 398b435e10ea0365df1fa91358b3e6d68036413b..dc1087910ac450d1d893f092b1627b26f610c256 100644
--- a/rt/analysis/completion_time.v
+++ b/rt/analysis/completion_time.v
@@ -1,5 +1,6 @@
 (* --------------------------------- Prosa ---------------------------------- *)
 From prosa.analysis Require Export facts.model.service_of_jobs.
+From prosa Require Export model.preemption.fully_preemptive.
 
 (* --------------------------------- ProBsa --------------------------------- *)
 From probsa.rt.model Require Export abort_readiness.
@@ -30,7 +31,7 @@ Section CompletionTimeExists.
   Variable sched : pr_schedule μ (ideal.processor_state Job).
   Hypothesis H_work_conserving : pr_work_conserving sched pr_abort_ready_instance.
   Hypothesis H_respects_policy_at_preemption_point :
-    pr_respects_policy_at_preemption_point sched pr_abort_ready_instance.
+    pr_respects_policy_at_preemption_point sched pr_abort_ready_instance fully_preemptive_model.
   Hypothesis H_pr_jobs_must_be_ready_to_execute :
     pr_jobs_must_be_ready_to_execute sched pr_abort_ready_instance.
 
diff --git a/rt/analysis/pRTA/pRTA.v b/rt/analysis/pRTA/pRTA.v
index fca5a2e4c29197997ccf1ea432344c0da6ba7411..9537a704855fa6820ab68c67f9bb0c1a05068076 100644
--- a/rt/analysis/pRTA/pRTA.v
+++ b/rt/analysis/pRTA/pRTA.v
@@ -165,7 +165,7 @@ Section WCDFPIsBounded.
   (** ... and assume that it is work conserving and respects the FP-FP policy. *)
   Hypothesis H_work_conserving : pr_work_conserving sched pr_abort_ready_instance.
   Hypothesis H_respects_policy_at_preemption_point :
-    pr_respects_policy_at_preemption_point sched pr_abort_ready_instance.
+    pr_respects_policy_at_preemption_point sched pr_abort_ready_instance fully_preemptive_model.
 
   Hypothesis H_jobs_come_from_arrival_sequence : pr_jobs_come_from_arrival_sequence sched.
   Hypothesis H_completed_jobs_dont_execute : pr_completed_jobs_dont_execute sched.
diff --git a/rt/analysis/scheduler_properties.v b/rt/analysis/scheduler_properties.v
index 75ecfd97f7ce96c67bd942429294e98d53e64545..839bc8854a17673304f9bc5f85bf2b943b309ea2 100644
--- a/rt/analysis/scheduler_properties.v
+++ b/rt/analysis/scheduler_properties.v
@@ -1,4 +1,5 @@
 (* --------------------------------- Prosa ---------------------------------- *)
+From prosa Require Export model.preemption.fully_preemptive.
 From prosa.implementation Require Import facts.ideal_uni.prio_aware.
 
 (* --------------------------------- ProBsa --------------------------------- *)
@@ -297,7 +298,8 @@ Section SchedulerProperties.
   Qed.
 
   Lemma FP_FP_sched_respects_policy_at_preemption_point :
-    pr_respects_policy_at_preemption_point pr_sched pr_abort_ready_instance.
+    pr_respects_policy_at_preemption_point
+      pr_sched pr_abort_ready_instance fully_preemptive_model.
   Proof.
     intros ω; apply schedule_respects_policy => //.
     { by apply pr_consistent_arrival_times. }
diff --git a/rt/model/assumptions/pr_respects_policy.v b/rt/model/assumptions/pr_respects_policy.v
index 32ff5f758f3f7d17fe51bb778baa4d83feef4b47..ad412ba7f81f9b648cf9995d3a86f201ffe7e4fd 100644
--- a/rt/model/assumptions/pr_respects_policy.v
+++ b/rt/model/assumptions/pr_respects_policy.v
@@ -1,8 +1,4 @@
 (* --------------------------------- Prosa ---------------------------------- *)
-(* TODO: switch to generic preemption policy *)
-(* From prosa Require Export model.preemption.parameter. *)
-From prosa Require Export model.preemption.fully_preemptive.
-
 From prosa.model Require Export schedule.priority_driven.
 
 (* --------------------------------- ProBsa --------------------------------- *)
@@ -29,8 +25,10 @@ Section PrRespectsPolicyAtPreemptionPoint.
         Job (ideal.processor_state Job)
         (fun j => odflt0 (job_cost j) ω) (fun j => odflt0 (job_arrival j) ω).
 
-  Definition pr_respects_policy_at_preemption_point (job_ready : JobReadyRV) :=
+  Definition pr_respects_policy_at_preemption_point
+             (job_ready : JobReadyRV) (job_preemptable : JobPreemptable Job) :=
     forall (ω : Ω),
-      @respects_policy_at_preemption_point _ _ _ _ (job_ready ω) (arr_seq ω) (sched ω) _.
+      @respects_policy_at_preemption_point
+        _ _ _ job_preemptable (job_ready ω) (arr_seq ω) (sched ω) _.
 
 End PrRespectsPolicyAtPreemptionPoint.