diff --git a/restructuring/model/job.v b/restructuring/model/job.v
index ba5d58e509a8abea00fb293d504acd1d4878fdcf..0e017838ef32111abf0f44aab8311e8261f41cd8 100644
--- a/restructuring/model/job.v
+++ b/restructuring/model/job.v
@@ -9,9 +9,9 @@ Section PropertesOfJob.
   Context `{JobCost Job}.
 
   (* Consider an arbitrary job. *)
-  Variable j: Job.
+  Variable j : Job.
 
   (* The job cost must be positive. *)
   Definition job_cost_positive := job_cost j > 0.
 
-End PropertesOfJob.
\ No newline at end of file
+End PropertesOfJob. 
\ No newline at end of file
diff --git a/restructuring/model/processor/platform_properties.v b/restructuring/model/processor/platform_properties.v
index 1c9a4552cb54c987ed439f9a9608143bf9e5aac5..dedc5544e22467012ed19ab9edfc12a30406f84b 100644
--- a/restructuring/model/processor/platform_properties.v
+++ b/restructuring/model/processor/platform_properties.v
@@ -4,14 +4,14 @@ From rt.restructuring.behavior Require Export schedule.
    following properties that a processor model might possess. *)
 Section ProcessorModels.
   (* Consider any job type and any processor state. *)
-  Context {Job: JobType}.
-  Context {PState: Type}.
+  Context {Job : JobType}.
+  Context {PState : Type}.
   Context `{ProcessorState Job PState}.
 
   (* We say that a processor model provides unit service if no
      job ever receives more than one unit of service at any time. *)
   Definition unit_service_proc_model :=
-    forall j s, service_in j s <= 1.
+    forall (j : Job) (s : PState), service_in j s <= 1.
 
   (* We say that a processor model offers ideal progress if a scheduled job
      always receives non-zero service. *)
diff --git a/restructuring/model/task.v b/restructuring/model/task.v
index ef934520d6b365a1e6aa57efea0747e4bfc1d14d..b325e42d6e59c2b150a42ec6851f56be14909953 100644
--- a/restructuring/model/task.v
+++ b/restructuring/model/task.v
@@ -1,6 +1,5 @@
 From mathcomp Require Export ssrbool.
 From rt.restructuring.behavior Require Export job.
-
 From rt.restructuring.behavior Require Export arrival_sequence.
   
 (* Throughout the library we assume that tasks have decidable equality *)
@@ -32,9 +31,11 @@ Section SameTask.
   Context {Task : TaskType}.
   Context `{JobTask Job Task}.
 
-  (* ... we say that two jobs j1 and j2 are from the same task iff job_task j1
-     is equal to job_task j2. *)
-  Definition same_task j1 j2 := job_task j1 == job_task j2.
+  (* ... we say that two jobs j1 and j2 are from the same task iff job_task j1 is equal to job_task j2, ... *)
+  Definition same_task (j1 j2 : Job) := job_task j1 == job_task j2.
+  
+  (* ... we also say that job j is a job of task tsk iff job_task j is equal to tsk. *)
+  Definition job_of_task (tsk : Task) (j : Job) := job_task j == tsk.
 
 End SameTask.