diff --git a/model/preemption/parameter.v b/model/preemption/parameter.v
index 210792017ff0d552584e460df207df4072426cc6..be3211a50708c98690c0c506fcd55d23989680b4 100644
--- a/model/preemption/parameter.v
+++ b/model/preemption/parameter.v
@@ -1,5 +1,6 @@
 Require Export prosa.util.all.
 Require Export prosa.behavior.all.
+Require Export prosa.model.priority.classes.
 
 (** * Job-Level Preemption Model *)
 (** There are many equivalent ways to represent at which points in time a job
@@ -95,6 +96,9 @@ Section PreemptionModel.
   (** ... and any preemption model. *)
   Context `{JobPreemptable Job}.
 
+  (** Consider any JLDP policy. *)
+  Context `{JLDP_policy Job}.
+
   (** Consider any kind of processor model, ... *)
   Context {PState : Type}.
   Context `{ProcessorState Job PState}.
@@ -146,5 +150,13 @@ Section PreemptionModel.
       /\ job_cannot_be_nonpreemptive_after_completion j
       /\ not_preemptive_implies_scheduled j
       /\ execution_starts_with_preemption_point j.
+  
+  (** We say that there are no superfluous preemptions if a job can 
+      only be preempted by another job having strictly higher priority. *)
+  Definition no_superfluous_preemptions :=
+    forall t j j_hp,
+      preempted_at j t ->
+      scheduled_at sched j_hp t ->
+      ~~ hep_job_at t j j_hp.
 
 End PreemptionModel.