diff --git a/model/priority/classes.v b/model/priority/classes.v
index c7766865b99a018209bc3b080f19236bcd600819..a6e953a8145a552bf6e5b356e54b0252efe9417f 100644
--- a/model/priority/classes.v
+++ b/model/priority/classes.v
@@ -49,6 +49,11 @@ Instance FP_to_JLFP (Job: JobType) (Task: TaskType)
 Instance JLFP_to_JLDP (Job: JobType) `{JLFP_policy Job} : JLDP_policy Job :=
   fun _ j1 j2 => hep_job j1 j2.
 
+(** We add coercions to enable automatic conversion from [JLFP] to [JLDP]... *)
+Coercion JLFP_to_JLDP : JLFP_policy >-> JLDP_policy.
+(** ...and from [FP] to [JLFP]. *)
+Coercion FP_to_JLFP : FP_policy >-> JLFP_policy.
+
 (** ** Properties of Priority Policies *)
 
 (** In the following section, we define key properties of common priority
diff --git a/model/schedule/priority_driven.v b/model/schedule/priority_driven.v
index 49357bead7cc2c0de54d5bf8c2d031e29f94872d..a8c23380de616d0a31b0f490f0ed4e4d411fa6e5 100644
--- a/model/schedule/priority_driven.v
+++ b/model/schedule/priority_driven.v
@@ -46,22 +46,14 @@ Section Priority.
       preemption_time sched t ->
       backlogged sched j t ->
       scheduled_at sched j_hp t ->
-      hep_job_at t j_hp j. 
+      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.
+    respects_JLDP_policy_at_preemption_point policy.
+     
   (** [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 ->
-      backlogged sched j t ->
-      scheduled_at sched j_hp t ->
-      hep_job_at t j_hp j.
+    respects_JLDP_policy_at_preemption_point (FP_to_JLFP Job Task ).
 
 End Priority.
diff --git a/scripts/wordlist.pws b/scripts/wordlist.pws
index 3de0d0f0d368340205499f5b8c70460bff89fdbb..208f1bb0f0983ca3f51a2cc90079502b4ff7d0de 100644
--- a/scripts/wordlist.pws
+++ b/scripts/wordlist.pws
@@ -77,3 +77,4 @@ et
 al
 discoverable
 formedness
+coercions