diff --git a/analysis/facts/busy_interval/priority_inversion.v b/analysis/facts/busy_interval/priority_inversion.v
index 88c90824a4fdacd103ca0e26265f44d2bd1fde55..168d33a62afd073aaf9059157051af8220882677 100644
--- a/analysis/facts/busy_interval/priority_inversion.v
+++ b/analysis/facts/busy_interval/priority_inversion.v
@@ -35,7 +35,7 @@ Section PriorityInversionIsBounded.
  
   (** Consider a JLFP policy that indicates a higher-or-equal priority relation,
       and assume that the relation is reflexive and transitive. *)
-  Context `{JLFP_policy Job}.
+  Context {JLFP : JLFP_policy Job}.
   Hypothesis H_priority_is_reflexive: reflexive_priorities.
   Hypothesis H_priority_is_transitive: transitive_priorities.
 
@@ -68,7 +68,7 @@ Section PriorityInversionIsBounded.
        predicate [job_preemptable] (i.e., bounded nonpreemptive
        segments). *)
   Hypothesis H_respects_policy:
-    respects_policy_at_preemption_point arr_seq sched.
+    respects_JLFP_policy_at_preemption_point arr_seq sched JLFP.
   
   (** Let's define some local names for clarity. *)
   Let job_scheduled_at := scheduled_at sched.
diff --git a/analysis/facts/edf_definitions.v b/analysis/facts/edf_definitions.v
index a17c05415ce1d2e4d65a2e20e8a6d3b4d84e1fd9..e79404bf9dbc534d0780565fc8cf8007084ce1ff 100644
--- a/analysis/facts/edf_definitions.v
+++ b/analysis/facts/edf_definitions.v
@@ -57,7 +57,7 @@ Section Equivalence.
       predicate. *)
   Lemma EDF_schedule_implies_respects_policy_at_preemption_point :
     EDF_schedule sched ->
-    respects_policy_at_preemption_point arr_seq sched.
+    respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).
   Proof.
     move=> EDF j' j t ARR PREEMPTION BL SCHED.
     have suff: exists t' : nat, t <= t' < job_deadline j' /\ scheduled_at sched j' t'.
@@ -73,7 +73,7 @@ Section Equivalence.
       the [respects_policy_at_preemption_point] predicate is also an EDF
       schedule in the sense of [EDF_schedule]. *)
   Lemma respects_policy_at_preemption_point_implies_EDF_schedule :
-    respects_policy_at_preemption_point arr_seq sched ->
+    respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job) ->
     EDF_schedule sched.
   Proof.
     move=> H_priority_driven t j_hp SCHED t' j LEQ SCHED' EARLIER_ARR.
@@ -94,7 +94,7 @@ Section Equivalence.
       definitions are indeed equivalent, which we note with the following
       corollary. *)
   Corollary EDF_schedule_equiv:
-    EDF_schedule sched <-> respects_policy_at_preemption_point arr_seq sched.
+    EDF_schedule sched <-> respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).
   Proof.
     split.
     - by apply EDF_schedule_implies_respects_policy_at_preemption_point.
diff --git a/analysis/facts/priority/edf.v b/analysis/facts/priority/edf.v
index a9d7d2ebb262dbd5a17acbad6471dd736b28a5cc..7de6b8dc2efacaf4d102c90abeb844abe5071f64 100644
--- a/analysis/facts/priority/edf.v
+++ b/analysis/facts/priority/edf.v
@@ -84,7 +84,7 @@ Section SequentialEDF.
   (** Next, we assume that the schedule respects the policy defined by
       the [job_preemptable] function (i.e., jobs have bounded
       non-preemptive segments). *)
-  Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
+  Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).
 
   (** To prove sequentiality, we use lemma
       [early_hep_job_is_scheduled]. Clearly, under the EDF priority
diff --git a/analysis/facts/priority/fifo.v b/analysis/facts/priority/fifo.v
index 94941ff1d6f1c5c403b85862c6cdb10dd7e401ef..9095e65405958f9073afe1846049372e38d13ef4 100644
--- a/analysis/facts/priority/fifo.v
+++ b/analysis/facts/priority/fifo.v
@@ -32,7 +32,7 @@ Section BasicLemmas.
 
   (** Assume that the schedule respects the FIFO scheduling policy whenever jobs
       are preemptable. *)
-  Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
+  Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job).
 
   (** We observe that there is no priority inversion in a
       FIFO-compliant schedule. *)
diff --git a/analysis/facts/priority/sequential.v b/analysis/facts/priority/sequential.v
index 06bcf3ac4fc8ff1d301fb4c8b558f8d5443f5fd0..5c6f8c24efc0e90e5a038cb7dd925b5220b8c28c 100644
--- a/analysis/facts/priority/sequential.v
+++ b/analysis/facts/priority/sequential.v
@@ -17,7 +17,7 @@ Section SequentialJLFP.
   
   (** Consider a JLFP-policy that indicates a higher-or-equal priority
       relation, and assume that this relation is transitive. *)             
-  Context `{JLFP_policy Job}.
+  Context {JLFP : JLFP_policy Job}.
   Hypothesis H_priority_is_transitive : transitive_priorities.
   
   (** Next, consider any ideal uni-processor schedule of this arrival sequence, ... *)
@@ -40,7 +40,7 @@ Section SequentialJLFP.
   (** Next, we assume that the schedule respects the policy defined by
      the [job_preemptable] function (i.e., jobs have bounded
      non-preemptive segments)... *)
-  Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
+  Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched JLFP.
 
   (** ... and that jobs must arrive to execute. *)
   Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
diff --git a/implementation/facts/ideal_uni/prio_aware.v b/implementation/facts/ideal_uni/prio_aware.v
index 2b9b519ad064871dbbffadf3a0d2829e67c55a45..ab8e493df36f782328c56de8c16f1f1bc4b6e729 100644
--- a/implementation/facts/ideal_uni/prio_aware.v
+++ b/implementation/facts/ideal_uni/prio_aware.v
@@ -30,7 +30,7 @@ Section PrioAwareUniprocessorScheduler.
   Hypothesis H_valid_preemption_behavior: valid_nonpreemptive_readiness RM.
 
   (** ... and reflexive, total, and transitive JLDP priority policy. *)
-  Context `{JLDP_policy Job}.
+  Context `{JLDP : JLDP_policy Job}.
   Hypothesis H_reflexive_priorities: reflexive_priorities.
   Hypothesis H_total: total_priorities.
   Hypothesis H_transitive: transitive_priorities.
@@ -118,7 +118,7 @@ Section PrioAwareUniprocessorScheduler.
     (** From the preceding facts, we conclude that [uni_schedule arr_seq]
         respects the priority policy at preemption times. *)
     Theorem schedule_respects_policy :
-      respects_policy_at_preemption_point arr_seq schedule.
+      respects_JLDP_policy_at_preemption_point arr_seq schedule JLDP.
     Proof.
       move=> j1 j2 t ARRIVES PREEMPT BACK_j1 SCHED_j2.
       case: (boolP (scheduled_at (uni_schedule arr_seq) j1 t)) => [SCHED_j1|NOT_SCHED_j1].
diff --git a/model/schedule/priority_driven.v b/model/schedule/priority_driven.v
index cb8d74027d5fac0955bf7e774d66f7e6193dd861..e78273ab3ad4377c6c217e5ec70e8f72829fbd37 100644
--- a/model/schedule/priority_driven.v
+++ b/model/schedule/priority_driven.v
@@ -38,13 +38,28 @@ Section Priority.
   (** ...and an ideal uniprocessor schedule of these jobs, *)
   Variable sched : schedule (ideal.processor_state Job).
 
-  (** we say that a JLDP policy ...*)
-  Context `{JLDP_policy Job}.
-
-  (** ...is respected by the schedule iff, at every preemption point, the
-     priority of the scheduled job is higher than or equal to the priority of
-     any backlogged job. *)
-  Definition respects_policy_at_preemption_point :=
+  (** we say that a priority policy is respected by the schedule iff, 
+      at every preemption point, the priority of the scheduled job is 
+      higher than or equal to the priority of any backlogged job.
+      We define three separate notions of priority policy compliance 
+      based on the three types of scheduling policies : [JLDP]... *)
+  Definition respects_JLDP_policy_at_preemption_point (policy: JLDP_policy Job) :=
+    forall j j_hp t,
+      arrives_in arr_seq j ->
+      preemption_time sched t ->
+      backlogged sched j t ->
+      scheduled_at sched j_hp t ->
+      hep_job_at t j_hp j. 
+   (** ... [JLFP], and... *)
+  Definition respects_JLFP_policy_at_preemption_point (policy: JLFP_policy Job) :=
+    forall j j_hp t,
+      arrives_in arr_seq j ->
+      preemption_time sched t ->
+      backlogged sched j t ->
+      scheduled_at sched j_hp t ->
+      hep_job_at t j_hp j.
+  (** [FP].  *)
+  Definition respects_FP_policy_at_preemption_point (policy: FP_policy Task) :=
     forall j j_hp t,
       arrives_in arr_seq j ->
       preemption_time sched t ->
diff --git a/results/edf/optimality.v b/results/edf/optimality.v
index 4450724d00251ed78bf508f6b022d276d7a1e68c..79abd84ee19f6b8278d333ebdeb7d443e22ef9c0 100644
--- a/results/edf/optimality.v
+++ b/results/edf/optimality.v
@@ -111,7 +111,7 @@ Section Optimality.
         valid_schedule priority_compliant_sched arr_seq /\
         all_deadlines_of_arrivals_met arr_seq priority_compliant_sched /\
         work_conserving arr_seq priority_compliant_sched /\
-        respects_policy_at_preemption_point arr_seq priority_compliant_sched.
+        respects_JLFP_policy_at_preemption_point arr_seq priority_compliant_sched (EDF Job).
   Proof.
     move /EDF_WC_optimality => [edf_sched [[ARR READY] [DL_MET [WC EDF]]]].
     exists edf_sched.
diff --git a/results/edf/rta/bounded_nps.v b/results/edf/rta/bounded_nps.v
index 123cb771cde38c82c8ef92e8839e01c0e9eed4e1..648ddd82cd095a50a1043b559f246112da90b311 100644
--- a/results/edf/rta/bounded_nps.v
+++ b/results/edf/rta/bounded_nps.v
@@ -72,7 +72,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
 
   (** ... and the schedule respects the policy defined by the [job_preemptable]
      function (i.e., jobs have bounded non-preemptive segments). *)
-  Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
+  Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched EDF.
 
   (** Consider an arbitrary task set ts, ... *)
   Variable ts : list Task.
diff --git a/results/edf/rta/floating_nonpreemptive.v b/results/edf/rta/floating_nonpreemptive.v
index 1c1bc8101dc328b376637b049f7c74fd1e7c6db6..341a6543b125bdfe69545e24add4795b8c5f5010 100644
--- a/results/edf/rta/floating_nonpreemptive.v
+++ b/results/edf/rta/floating_nonpreemptive.v
@@ -81,7 +81,7 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
   (** ... and the schedule respects the policy defined by the
       job_preemptable function (i.e., jobs have bounded non-preemptive
       segments). *)
-  Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
+  Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).
 
   (** ** Total Workload and Length of Busy Interval *)
 
diff --git a/results/edf/rta/fully_nonpreemptive.v b/results/edf/rta/fully_nonpreemptive.v
index ff4d924cc4d1657d4578fef5854a8d26ac07b558..e7277894cb5f7e73cbb6d682e7d90c121f5473d6 100644
--- a/results/edf/rta/fully_nonpreemptive.v
+++ b/results/edf/rta/fully_nonpreemptive.v
@@ -71,7 +71,7 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
   (** ... and the schedule respects the policy defined by the
       job_preemptable function (i.e., jobs have bounded nonpreemptive
       segments). *)
-  Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
+  Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).
 
   (** ** Total Workload and Length of Busy Interval *)
 
diff --git a/results/edf/rta/fully_preemptive.v b/results/edf/rta/fully_preemptive.v
index aa060227ef6f3f12c9bf280336f0f56e2fd1d35d..dd9f0c512ad669e999019709c24ee56b32b47699 100644
--- a/results/edf/rta/fully_preemptive.v
+++ b/results/edf/rta/fully_preemptive.v
@@ -71,7 +71,7 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
   (** ... and the schedule respects the policy defined by the
       [job_preemptable] function (i.e., jobs have bounded non-preemptive
       segments). *)
-  Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
+  Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).
 
   (** ** Total Workload and Length of Busy Interval *)
 
diff --git a/results/edf/rta/limited_preemptive.v b/results/edf/rta/limited_preemptive.v
index 2004a0e5d28263c2dbe0500e2f151b08b17a3980..90c0c2ddc868b67ef8d4802b0782e7c46d256f22 100644
--- a/results/edf/rta/limited_preemptive.v
+++ b/results/edf/rta/limited_preemptive.v
@@ -82,7 +82,7 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
   (** ... and the schedule respects the policy defined by the
       [job_preemptable] function (i.e., jobs have bounded non-preemptive
       segments). *)
-  Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
+  Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).
 
   (** ** Total Workload and Length of Busy Interval *)
 
diff --git a/results/fifo/rta.v b/results/fifo/rta.v
index 78b8099a2ecd1295adf36dc1b0526dda4f88db4b..61bb18bdfa525c9418b5d71179b66782c6854348 100644
--- a/results/fifo/rta.v
+++ b/results/fifo/rta.v
@@ -89,7 +89,7 @@ Section AbstractRTAforFIFOwithArrivalCurves.
   Hypothesis H_valid_run_to_completion_threshold : valid_task_run_to_completion_threshold arr_seq tsk.
 
   (** We also assume that the schedule respects the policy defined by the preemption model. *)
-  Hypothesis H_respects_policy_at_preemption_point : respects_policy_at_preemption_point arr_seq sched. 
+  Hypothesis H_respects_policy_at_preemption_point : respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job). 
 
   (** We introduce [rbf] as an abbreviation of the task request bound function,
       which is defined as [task_cost(T) × max_arrivals(T,Δ)] for a given task [T]. *)
diff --git a/results/fixed_priority/rta/bounded_nps.v b/results/fixed_priority/rta/bounded_nps.v
index 1a7068ab5babe7ff2ce7722541ec9f9dddf6a212..02db6d99f7ca68c2255363ab5eee1fe00d08c6c6 100644
--- a/results/fixed_priority/rta/bounded_nps.v
+++ b/results/fixed_priority/rta/bounded_nps.v
@@ -36,7 +36,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
   (** Consider an FP policy that indicates a higher-or-equal priority
       relation, and assume that the relation is reflexive and
       transitive. *)
-  Context `{FP_policy Task}.
+  Context {FP : FP_policy Task}.
   Hypothesis H_priority_is_reflexive : reflexive_priorities.
   Hypothesis H_priority_is_transitive : transitive_priorities.
   
@@ -69,7 +69,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
   
   (** ... and the schedule respects the policy defined by the [job_preemptable]
      function (i.e., jobs have bounded non-preemptive segments). *)
-  Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
+  Hypothesis H_respects_policy : respects_FP_policy_at_preemption_point arr_seq sched FP.
 
   (** Assume we have sequential tasks, i.e, jobs from the 
       same task execute in the order of their arrival. *)
diff --git a/results/fixed_priority/rta/floating_nonpreemptive.v b/results/fixed_priority/rta/floating_nonpreemptive.v
index 73a987d3e4e305ada2747bab4eb1cde8f97ee9be..db79391cfb3bb935365c3654239b4365011783a2 100644
--- a/results/fixed_priority/rta/floating_nonpreemptive.v
+++ b/results/fixed_priority/rta/floating_nonpreemptive.v
@@ -78,7 +78,7 @@ Section RTAforFloatingModelwithArrivalCurves.
 
   (** Consider an FP policy that indicates a higher-or-equal priority relation,
       and assume that the relation is reflexive and transitive. *)
-  Context `{FP_policy Task}.
+  Context {FP :FP_policy Task}.
   Hypothesis H_priority_is_reflexive : reflexive_priorities.
   Hypothesis H_priority_is_transitive : transitive_priorities.
   
@@ -87,7 +87,7 @@ Section RTAforFloatingModelwithArrivalCurves.
   
   (** ... and the schedule respects the policy defined by the [job_preemptable] 
      function (i.e., jobs have bounded non-preemptive segments). *)
-  Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
+  Hypothesis H_respects_policy : respects_FP_policy_at_preemption_point arr_seq sched FP.
 
   (** ** Total Workload and Length of Busy Interval *)
 
diff --git a/results/fixed_priority/rta/fully_nonpreemptive.v b/results/fixed_priority/rta/fully_nonpreemptive.v
index e3d35cf107bef20c00f437ce0563bc2dce03d302..3baf51c5bcd0a13f1a19354058f8933eac0ac208 100644
--- a/results/fixed_priority/rta/fully_nonpreemptive.v
+++ b/results/fixed_priority/rta/fully_nonpreemptive.v
@@ -70,7 +70,7 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
 
   (** Consider an FP policy that indicates a higher-or-equal priority relation,
      and assume that the relation is reflexive and transitive. *)
-  Context `{FP_policy Task}.
+  Context {FP : FP_policy Task}.
   Hypothesis H_priority_is_reflexive : reflexive_priorities.
   Hypothesis H_priority_is_transitive : transitive_priorities.
   
@@ -80,7 +80,7 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
   (** ... and the schedule respects the policy defined by the
      [job_preemptable] function (i.e., jobs have bounded nonpreemptive
      segments). *)
-  Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.    
+  Hypothesis H_respects_policy : respects_FP_policy_at_preemption_point arr_seq sched FP.    
 
   (** ** Total Workload and Length of Busy Interval *)
 
diff --git a/results/fixed_priority/rta/fully_preemptive.v b/results/fixed_priority/rta/fully_preemptive.v
index 31574f38f760e4b538e97df8871d2b9827c3fe6b..8c82268666a259db13d4c06de24ba056c28c4cef 100644
--- a/results/fixed_priority/rta/fully_preemptive.v
+++ b/results/fixed_priority/rta/fully_preemptive.v
@@ -70,7 +70,7 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
 
   (** Consider an FP policy that indicates a higher-or-equal priority relation,
      and assume that the relation is reflexive and transitive. *)
-  Context `{FP_policy Task}.
+  Context {FP : FP_policy Task}.
   Hypothesis H_priority_is_reflexive : reflexive_priorities.
   Hypothesis H_priority_is_transitive : transitive_priorities.
 
@@ -79,7 +79,7 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
   
   (** ... and the schedule respects the policy defined by the [job_preemptable] 
      function (i.e., jobs have bounded non-preemptive segments). *)
-  Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.  
+  Hypothesis H_respects_policy : respects_FP_policy_at_preemption_point arr_seq sched FP.  
 
   (** ** Total Workload and Length of Busy Interval *)
 
diff --git a/results/fixed_priority/rta/limited_preemptive.v b/results/fixed_priority/rta/limited_preemptive.v
index 4d39b8f3246447fb9418dd1dd4764f6d72ad50e6..c6a35f50fb82c09279052d8c7c7d9f90e7787679 100644
--- a/results/fixed_priority/rta/limited_preemptive.v
+++ b/results/fixed_priority/rta/limited_preemptive.v
@@ -78,7 +78,7 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
 
   (** Consider an FP policy that indicates a higher-or-equal priority relation,
      and assume that the relation is reflexive and transitive. *)
-  Context `{FP_policy Task}.
+  Context {FP : FP_policy Task}.
   Hypothesis H_priority_is_reflexive : reflexive_priorities.
   Hypothesis H_priority_is_transitive : transitive_priorities.
   
@@ -87,7 +87,7 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
   
   (** ... and the schedule respects the policy defined by the [job_preemptable]
      function (i.e., jobs have bounded non-preemptive segments). *)
-  Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.  
+  Hypothesis H_respects_policy : respects_FP_policy_at_preemption_point arr_seq sched FP.  
 
   (** ** Total Workload and Length of Busy Interval *)