diff --git a/analysis/abstract/abstract_rta.v b/analysis/abstract/abstract_rta.v
index 5ba0516f44a97a3a8814a9b3281fbc589bb39e44..2e68fdeffccfe0ba1c93643e9cef22586bc02a0b 100644
--- a/analysis/abstract/abstract_rta.v
+++ b/analysis/abstract/abstract_rta.v
@@ -25,8 +25,7 @@ Section Abstract_RTA.
   Context `{JobPreemptable Job}.
 
   (** Consider any kind of uni-service ideal processor state model. *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
   Hypothesis H_ideal_progress_proc_model : ideal_progress_proc_model PState.
   Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.  
   
@@ -271,7 +270,7 @@ Section Abstract_RTA.
             move: H_busy_interval => [[/andP [GT LT] _] _].
             have ESERV :=
               @j_receives_at_least_run_to_completion_threshold
-                _ _ H1 H2 H3 PState H5 _ _  arr_seq sched tsk interference interfering_workload
+                _ _ H1 H2 H3 PState _ _  arr_seq sched tsk interference interfering_workload
                 _ j _ _ _ t1 t2 _ (job_rtct j) _ ((A + F) - optimism). 
             feed_n 7 ESERV; eauto 2.
             specialize (ESERV H3 H4).
@@ -500,7 +499,7 @@ Section Abstract_RTA.
           simpl in IB; rewrite H_equivalent in IB; last by apply ltn_trans with A.
           have ESERV :=
             @j_receives_at_least_run_to_completion_threshold
-              _ _ H1 H2 H3 PState H5 _ _ arr_seq sched tsk
+              _ _ H1 H2 H3 PState _ _ arr_seq sched tsk
               interference interfering_workload _ j _ _ _ t1 t2 _ (job_rtct j) _ (A_sp + F_sp). 
           feed_n 7 ESERV; eauto 2.
           specialize (ESERV H3 H4).
@@ -552,4 +551,4 @@ Section Abstract_RTA.
                    with (j := j) (t1 := t1) (t2 := t2) (A_sp := A1) (F_sp := F1); auto.
   Qed.
 
-End Abstract_RTA. 
+End Abstract_RTA.
diff --git a/analysis/abstract/definitions.v b/analysis/abstract/definitions.v
index f5da2b51bda0e4252770c65d1fb6e8e66297c1b6..686db10433d3044af8bf42935276b4570f0d6aac 100644
--- a/analysis/abstract/definitions.v
+++ b/analysis/abstract/definitions.v
@@ -22,8 +22,7 @@ Section AbstractRTADefinitions.
     Context `{JobCost Job}.
 
     (** Consider any kind of processor state model. *)
-    Context {PState : Type}.
-    Context `{ProcessorState Job PState}.
+    Context {PState : ProcessorState Job}.
     
     (** Consider any arrival sequence... *) 
     Variable arr_seq : arrival_sequence Job.
diff --git a/analysis/abstract/run_to_completion.v b/analysis/abstract/run_to_completion.v
index ba9a0ca0ed5c54eddf0ff8fd2338326fd59b4857..c717c5c4d3337699fea921d551c934db0aba7020 100644
--- a/analysis/abstract/run_to_completion.v
+++ b/analysis/abstract/run_to_completion.v
@@ -28,8 +28,7 @@ Section AbstractRTARunToCompletionThreshold.
   Context `{JobPreemptable Job}.
 
   (** Consider any kind of uni-service ideal processor state model. *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
   Hypothesis H_ideal_progress_proc_model : ideal_progress_proc_model PState.
   Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.
 
@@ -181,7 +180,7 @@ Section AbstractRTARunToCompletionThreshold.
       move => t ES.
       set (job_cost j - job_rtct j) as job_last.
       have LSNP := @job_nonpreemptive_after_run_to_completion_threshold
-                     Job H2 H3 _ _ arr_seq sched _ j _ t.
+                     Job H2 H3 _ arr_seq sched _ j _ t.
       apply negbNE; apply/negP; intros CONTR.
       have SCHED: forall t', t <= t' <= t + job_last -> scheduled_at sched j t'.
       { move => t' /andP [GE LT].
diff --git a/analysis/definitions/busy_interval.v b/analysis/definitions/busy_interval.v
index 16e2e45896cf0a2e6b8d4130321bf23a11dd9f82..05f34720fbdc20a0f24e4944f6b33129f07be54a 100644
--- a/analysis/definitions/busy_interval.v
+++ b/analysis/definitions/busy_interval.v
@@ -11,8 +11,7 @@ Section BusyIntervalJLFP.
   Context `{JobCost Job}.    
 
   (** Consider any kind of processor state model. *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.  
+  Context {PState : ProcessorState Job}.
 
   (** Consider any arrival sequence with consistent arrivals ... *)
   Variable arr_seq : arrival_sequence Job.
diff --git a/analysis/definitions/carry_in.v b/analysis/definitions/carry_in.v
index b83bf9798e08c5427bfcc7dd26318ff6dcdfc95c..dc49b2269504061f28ea10255e5bcf37b86df564 100644
--- a/analysis/definitions/carry_in.v
+++ b/analysis/definitions/carry_in.v
@@ -18,7 +18,7 @@ Section NoCarryIn.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
 
   (** ... and the resultant schedule. *)
-  Context {PState : Type} `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
   Variable sched : schedule PState.
 
   (** There is no carry-in at time [t] iff every job (regardless of priority)
diff --git a/analysis/definitions/completion_sequence.v b/analysis/definitions/completion_sequence.v
index d53960d6527a35c2cb51bcf5f568b80f0c0e1708..c3a34a49e704d4fdc6ee56e75cb03e268dc4069d 100644
--- a/analysis/definitions/completion_sequence.v
+++ b/analysis/definitions/completion_sequence.v
@@ -11,8 +11,7 @@ Section CompletionSequence.
 
   (** Consider any kind of jobs with a cost
      and any kind of processor state. *)
-  Context {Job : JobType} `{JobCost Job} {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {Job : JobType} `{JobCost Job} {PState : ProcessorState Job}.
 
   (** Consider any job arrival sequence. *)
   Variable arr_seq: arrival_sequence Job.
diff --git a/analysis/definitions/job_response_time.v b/analysis/definitions/job_response_time.v
index 78375007ff4e61b9d43a3caf425995c5c0b72f80..9cc463eb11535419f6e0c00e4a7bfc2cb54bb8f1 100644
--- a/analysis/definitions/job_response_time.v
+++ b/analysis/definitions/job_response_time.v
@@ -10,8 +10,7 @@ Section JobResponseTimeExceeds.
   Context `{JobArrival Job}.
 
   (** ... and any kind of processor state. *)
-  Context `{PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context `{PState : ProcessorState Job}.
 
   (** Consider any schedule. *)
   Variable sched : schedule PState.
diff --git a/analysis/definitions/progress.v b/analysis/definitions/progress.v
index ce5480af5b8d2d2f1fb4d51fd29dc38244ffdd21..40962cb310a3610e8043f6de9df7b2a1679fd1ae 100644
--- a/analysis/definitions/progress.v
+++ b/analysis/definitions/progress.v
@@ -12,8 +12,7 @@ Section Progress.
   Context `{JobCost Job}.
 
   (** ... and any kind of schedule. *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
 
   (** For a given job and a given schedule... *)
   Variable sched : schedule PState.
diff --git a/analysis/definitions/readiness.v b/analysis/definitions/readiness.v
index d03d7fa589dc35114f62e5edeea49e232c00a387..c54d8a99a4a3c724b3fbac2cc94158b79ab90dac 100644
--- a/analysis/definitions/readiness.v
+++ b/analysis/definitions/readiness.v
@@ -12,7 +12,7 @@ Section ReadinessModelProperties.
   Context {Job : JobType} `{JobCost Job} `{JobArrival Job}.
 
   (** ... and any kind of processor model, ... *)
-  Context {PState: Type} `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.
 
   (** ... consider a  notion of job readiness. *)
   Variable ReadinessModel : JobReady Job PState.
@@ -46,5 +46,3 @@ Section ReadinessModelProperties.
         ~~ job_preemptable j (service sched j t) -> job_ready sched j t.
   
 End ReadinessModelProperties.
-
-
diff --git a/analysis/definitions/schedulability.v b/analysis/definitions/schedulability.v
index 2d0974ca8e367f68c8e87c198ae4e2266fc25e7e..d3ee7d7bf68ed811545a1c7185f3dfe4c40821cf 100644
--- a/analysis/definitions/schedulability.v
+++ b/analysis/definitions/schedulability.v
@@ -18,8 +18,7 @@ Section Task.
   Context `{JobTask Job Task}.
 
   (** ... and any kind of processor state. *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
 
   (** Consider any job arrival sequence... *)
   Variable arr_seq: arrival_sequence Job.
@@ -65,8 +64,7 @@ Section Schedulability.
   Context `{JobTask Job Task}.
 
   (** ... and any kind of processor state. *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
   
   (** Consider any job arrival sequence... *)
   Variable arr_seq: arrival_sequence Job.
@@ -115,8 +113,7 @@ Section AllDeadlinesMet.
   Context `{JobDeadline Job}.
 
   (** ... any given type of processor states. *)
-  Context {PState: eqType}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.
 
   (** We say that all deadlines are met if every job scheduled at some
      point in the schedule meets its deadline. Note that this is a
diff --git a/analysis/definitions/schedule_prefix.v b/analysis/definitions/schedule_prefix.v
index 1f7c8053c9d28aa8a61e1eb68f9c5235d97c8dd2..38cd8797f40684c856df3c21688baefb12c404f0 100644
--- a/analysis/definitions/schedule_prefix.v
+++ b/analysis/definitions/schedule_prefix.v
@@ -9,7 +9,7 @@ Section PrefixDefinition.
   Context {Job : JobType}.
 
   (** ... and any kind of processor model, ... *)
-  Context {PState: Type} `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.
 
   (** ... two schedules share an identical prefix if they are pointwise
           identical (at least) up to a fixed horizon. *)
diff --git a/analysis/definitions/tardiness.v b/analysis/definitions/tardiness.v
index 6a5519cc3187b1097f52b94feb6bac298c72df5b..5970274d43615e85824ba034e5a84c0657d9babd 100644
--- a/analysis/definitions/tardiness.v
+++ b/analysis/definitions/tardiness.v
@@ -18,8 +18,7 @@ Section Tardiness.
   Context `{JobTask Job Task}.
 
   (** ... and any kind of processor state. *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
 
   (** Further, consider any job arrival sequence... *)
   Variable arr_seq: arrival_sequence Job.
diff --git a/analysis/definitions/work_bearing_readiness.v b/analysis/definitions/work_bearing_readiness.v
index cf010bd7b922ff06deaa2d6f6be2ce430a9540bd..9d5a80b0bf5ac615e2e9ab573d8902ebbe8c53a3 100644
--- a/analysis/definitions/work_bearing_readiness.v
+++ b/analysis/definitions/work_bearing_readiness.v
@@ -18,11 +18,10 @@ Section WorkBearingReadiness.
   Context {Job : JobType} {Task : TaskType} `{JobArrival Job} `{JobCost Job}.
 
   (** ... and any kind of processor state. *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
 
   (** Further, allow for any notion of job readiness. *)
-  Context `{JobReady Job PState}.
+  Context {jr : JobReady Job PState}.
 
   (** Consider any job arrival sequence, ... *)
   Variable arr_seq : arrival_sequence Job.
diff --git a/analysis/facts/behavior/arrivals.v b/analysis/facts/behavior/arrivals.v
index 7c7f02d7a662f1c479273a95b112e16679bd6224..606b9313544325289f16af364f2627121f3b7d42 100644
--- a/analysis/facts/behavior/arrivals.v
+++ b/analysis/facts/behavior/arrivals.v
@@ -39,8 +39,7 @@ End ArrivalPredicates.
 Section Arrived.
   
   (** Consider any kinds of jobs and any kind of processor state. *)
-  Context {Job : JobType} {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {Job : JobType} {PState : ProcessorState Job}.
 
   (** Consider any schedule... *)
   Variable sched : schedule PState.
@@ -49,7 +48,7 @@ Section Arrived.
       notion of readiness. *)
   Context `{JobCost Job}.
   Context `{JobArrival Job}.
-  Context `{JobReady Job PState}.
+  Context {jr : JobReady Job PState}.
 
   (** First, we note that readiness models are by definition consistent
       w.r.t. [pending]. *)
@@ -57,7 +56,7 @@ Section Arrived.
     forall j t,
       job_ready sched j t -> pending sched j t.
   Proof.
-    move: H5 => [is_ready CONSISTENT].
+    move: jr => [is_ready CONSISTENT].
     move=> j t READY.
     apply CONSISTENT.
     by exact READY.
@@ -345,4 +344,4 @@ Section ArrivalSequencePrefix.
 
   End ArrivalTimes.
 
-End ArrivalSequencePrefix. 
+End ArrivalSequencePrefix.
diff --git a/analysis/facts/behavior/completion.v b/analysis/facts/behavior/completion.v
index 484910f6df945f1ba81d9065d7e8b2281e684c77..f7ce9f59f7a5f299c4c95caade2467ae4633f22f 100644
--- a/analysis/facts/behavior/completion.v
+++ b/analysis/facts/behavior/completion.v
@@ -14,8 +14,7 @@ Section CompletionFacts.
   Context `{JobArrival Job}.
 
   (** ...any kind of processor model,... *)
-  Context {PState: Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.
 
   (** ...and a given schedule. *)
   Variable sched: schedule PState.
@@ -163,8 +162,7 @@ Section ServiceAndCompletionFacts.
   Context `{JobCost Job}.
 
   (** ...any kind of processor model,... *)
-  Context {PState: Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.
 
   (** ...and a given schedule. *)
   Variable sched: schedule PState.
@@ -277,8 +275,7 @@ Section PositiveCost.
   Context `{JobArrival Job}.
 
   (** ...any kind of processor model,... *)
-  Context {PState: Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.
 
   (** ...and a given schedule. *)
   Variable sched: schedule PState.
@@ -325,8 +322,7 @@ End PositiveCost.
 Section CompletedJobs.
   
   (** Consider any kinds of jobs and any kind of processor state. *)
-  Context {Job : JobType} {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {Job : JobType} {PState : ProcessorState Job}.
 
   (** Consider any schedule... *)
   Variable sched : schedule PState.
@@ -335,7 +331,7 @@ Section CompletedJobs.
      readiness. *)
   Context `{JobCost Job}.
   Context `{JobArrival Job}.
-  Context `{JobReady Job PState}.
+  Context {jr : JobReady Job PState}.
 
   (** We observe that a given job is ready only if it is also incomplete... *)
   Lemma ready_implies_incomplete:
@@ -393,7 +389,8 @@ Global Hint Resolve valid_schedule_implies_completed_jobs_dont_execute : basic_f
 (** Next, we relate the completion of jobs in schedules with identical prefixes. *)
 Section CompletionInTwoSchedules.
   (** Consider any processor model and any type of jobs with costs, arrival times, and a notion of readiness. *)
-  Context {PState: Type} {Job: JobType} `{ProcessorState Job PState} `{JobReady Job PState}.
+  Context {Job: JobType} {PState: ProcessorState Job}.
+  Context {jc : JobCost Job} {ja : JobArrival Job} {jr : JobReady Job PState}.
 
   (** If two schedules share a common prefix, then (in the prefix) jobs
       complete in one schedule iff they complete in the other. *)
@@ -424,5 +421,3 @@ Section CompletionInTwoSchedules.
 
 
 End CompletionInTwoSchedules.
-
-
diff --git a/analysis/facts/behavior/deadlines.v b/analysis/facts/behavior/deadlines.v
index 1cc4e63740c22d9ea554cbe656da3b1fd847ab82..eab3862b82de4aa3971db3b4481ab4d562b62633 100644
--- a/analysis/facts/behavior/deadlines.v
+++ b/analysis/facts/behavior/deadlines.v
@@ -10,8 +10,7 @@ Section DeadlineFacts.
   Context {Job : JobType} `{JobCost Job} `{JobDeadline Job}.
 
   (** ... any given type of processor states. *)
-  Context {PState: eqType}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.
 
   (** First, we derive two properties from the fact that a job is incomplete at
       some point in time. *)
diff --git a/analysis/facts/behavior/service.v b/analysis/facts/behavior/service.v
index d835330c03d4b3b0fbb7d19964327bae65b4ec81..94d0d4fc46a7223b1a0b2e43a5a8052e93724b04 100644
--- a/analysis/facts/behavior/service.v
+++ b/analysis/facts/behavior/service.v
@@ -14,8 +14,7 @@ Section Composition.
   
   (** Consider any job type and any processor state. *)
   Context {Job: JobType}.
-  Context {PState: Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.
 
   (** For any given schedule... *)
   Variable sched: schedule PState.
@@ -137,8 +136,7 @@ Section UnitService.
 
   (** Consider any job type and any processor state. *)
   Context {Job : JobType}.
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
 
   (** Let's consider a unit-service model... *)
   Hypothesis H_unit_service: unit_service_proc_model PState.
@@ -239,8 +237,7 @@ Section Monotonicity.
 
   (** Consider any job type and any processor model. *)
   Context {Job: JobType}.
-  Context {PState: Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.
 
   (** Consider any given schedule... *)
   Variable sched: schedule PState.
@@ -264,8 +261,7 @@ End Monotonicity.
 Section RelationToScheduled.
 
   Context {Job: JobType}.
-  Context {PState: Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.
 
   (** Consider any given schedule... *)
   Variable sched: schedule PState.
@@ -640,8 +636,7 @@ Section ServiceInTwoSchedules.
   
   (** Consider any job type and any processor model. *)
   Context {Job: JobType}.
-  Context {PState: Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.
 
   (** Consider any two given schedules... *)
   Variable sched1 sched2: schedule PState.
diff --git a/analysis/facts/busy_interval/busy_interval.v b/analysis/facts/busy_interval/busy_interval.v
index e4e7a001d0f2d008cb4468930bed4b20fdd0935a..7cf5cd230d77d29631f92077c3351314c5ec9423 100644
--- a/analysis/facts/busy_interval/busy_interval.v
+++ b/analysis/facts/busy_interval/busy_interval.v
@@ -40,7 +40,7 @@ Section ExistsBusyIntervalJLFP.
   Context `{JLFP_policy Job}.
 
   (** Further, allow for any work-bearing notion of job readiness. *)
-  Context `{@JobReady Job (ideal.processor_state Job) _ Cost Arrival}.
+  Context `{@JobReady Job (ideal.processor_state Job) Cost Arrival}.
   Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
 
   (** For simplicity, let's define some local names. *)
@@ -301,7 +301,7 @@ Section ExistsBusyIntervalJLFP.
       rewrite -{3}[Δ](sum_of_ones t1) exchange_big //=.
       apply/eqP; rewrite eqn_leq; apply/andP; split.
       { rewrite leq_sum // => t' _.
-        have SCH := @service_of_jobs_le_1 _ _ _ _ _ sched predT (arrivals_between 0 (t1 + Δ)).        
+        have SCH := @service_of_jobs_le_1 _ _ _ _ sched predT (arrivals_between 0 (t1 + Δ)).        
         by eapply leq_trans; last apply SCH; eauto using arrivals_uniq with basic_facts. }
       { rewrite [in X in X <= _]big_nat_cond [in X in _ <= X]big_nat_cond //=
                 leq_sum // => t' /andP [/andP [LT GT] _]; apply/sum_seq_gt0P.
diff --git a/analysis/facts/busy_interval/carry_in.v b/analysis/facts/busy_interval/carry_in.v
index e4fe3aeff9eaf9b1109fe85e218979ef2d2df79d..2601666fde846e64585ed75b1d0ffb6ad135636f 100644
--- a/analysis/facts/busy_interval/carry_in.v
+++ b/analysis/facts/busy_interval/carry_in.v
@@ -50,7 +50,7 @@ Section ExistsNoCarryIn.
   Let quiet_time := quiet_time arr_seq sched.
 
   (** Further, allow for any work-bearing notion of job readiness. *)
-  Context `{@JobReady Job (ideal.processor_state Job) _ Cost Arrival}.
+  Context `{@JobReady Job (ideal.processor_state Job) Cost Arrival}.
   Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
   
   (** Assume that the schedule is work-conserving, ... *)
diff --git a/analysis/facts/busy_interval/priority_inversion.v b/analysis/facts/busy_interval/priority_inversion.v
index dbb3f5f22b06b3f64e1ef6f015a9bdd6eae97fd1..b8d88135e0c806873c5434bb19bdc1dbb51acacd 100644
--- a/analysis/facts/busy_interval/priority_inversion.v
+++ b/analysis/facts/busy_interval/priority_inversion.v
@@ -54,7 +54,7 @@ Section PriorityInversionIsBounded.
     valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
 
   (** Further, allow for any work-bearing notion of job readiness. *)
-  Context `{@JobReady Job (ideal.processor_state Job) _ Cost Arrival}.
+  Context `{@JobReady Job (ideal.processor_state Job) Cost Arrival}.
   Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
 
   (** We assume that the schedule is valid and that all jobs come from the arrival sequence. *)
@@ -577,7 +577,7 @@ Section PriorityInversionIsBounded.
               have Fact: exists Δ, t' = t1 + Δ.
               { by exists (t' - t1); apply/eqP; rewrite eq_sym; apply/eqP; rewrite subnKC. }
               move: Fact => [Δ EQ]; subst t'.
-              have NPPJ := @no_intermediate_preemption_point (@service _ _ _ sched jlp (t1 + Δ)).
+              have NPPJ := @no_intermediate_preemption_point (@service _ _ sched jlp (t1 + Δ)).
               apply proj1 in CORR; specialize (CORR jlp ARRs).
               move: CORR => [_ [_ [T _] ]].
               apply T; apply: NPPJ; apply/andP; split.
diff --git a/analysis/facts/model/preemption.v b/analysis/facts/model/preemption.v
index d2feb8504d1b862217683797f8798e8e5d1d3c7d..f38a46af59f50a86f95102acc4f746f292c1b8d6 100644
--- a/analysis/facts/model/preemption.v
+++ b/analysis/facts/model/preemption.v
@@ -63,7 +63,7 @@ Section PreemptionFacts.
   Context {Job : JobType}.
   Context `{Arrival : JobArrival Job}.
   Context `{Cost : JobCost Job}.
-  Context `{@JobReady Job (ideal.processor_state Job) _ Cost Arrival}.
+  Context `{@JobReady Job (ideal.processor_state Job) Cost Arrival}.
 
   (** Consider any arrival sequence. *)
   Variable arr_seq : arrival_sequence Job.
diff --git a/analysis/facts/model/rbf.v b/analysis/facts/model/rbf.v
index 8dd1a69118985c68f9ec944b754fdccac14465b1..31df27fef863916755d82c869bf0c4655a6246e7 100644
--- a/analysis/facts/model/rbf.v
+++ b/analysis/facts/model/rbf.v
@@ -28,7 +28,7 @@ Section ProofWorkloadBound.
   Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
 
   (** ... any schedule corresponding to this arrival sequence, ... *)
-  Context {PState : Type} `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
   Variable sched : schedule PState.
   Hypothesis H_jobs_come_from_arrival_sequence :
     jobs_come_from_arrival_sequence sched arr_seq.
diff --git a/analysis/facts/model/sequential.v b/analysis/facts/model/sequential.v
index 352ac9cb15678d059084dfc69ccc4f59a2e97bc0..c4a79f3a27279167677a296cc76db948a76d5786 100644
--- a/analysis/facts/model/sequential.v
+++ b/analysis/facts/model/sequential.v
@@ -12,8 +12,7 @@ Section ExecutionOrder.
   Context `{JobCost Job}.
 
   (** ... and any kind of processor state model. *)
-  Context {PState: Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.
 
 
   (** Consider any arrival sequence ... *) 
diff --git a/analysis/facts/model/service_of_jobs.v b/analysis/facts/model/service_of_jobs.v
index aa7acd2a6cc6e30f94037040924b261599ec3aa5..83fca850a79e744afb73fa5af044a72abf39d3b0 100644
--- a/analysis/facts/model/service_of_jobs.v
+++ b/analysis/facts/model/service_of_jobs.v
@@ -23,8 +23,7 @@ Section GenericModelLemmas.
   Context `{JobCost Job}.
 
   (** Consider any kind of processor state model, ... *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
 
   (** ... any job arrival sequence with consistent arrivals, .... *)
   Variable arr_seq : arrival_sequence Job.
@@ -103,8 +102,7 @@ Section UnitServiceModelLemmas.
   Context `{JobCost Job}.
 
   (** Consider any kind of unit-service processor state model. *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
   Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.
   
   (** Consider any arrival sequence with consistent arrivals. *)
@@ -245,8 +243,7 @@ Section UnitServiceUniProcessorModelLemmas.
   Context `{JobCost Job}.
 
   (** Consider any kind of unit-service uniprocessor state model. *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
   Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.
   Hypothesis H_uniprocessor_model : uniprocessor_model PState.
   
@@ -400,5 +397,4 @@ Section IdealModelLemmas.
     by rewrite eqxx.
   Qed.
 
-  
 End IdealModelLemmas.
diff --git a/analysis/facts/preemption/job/preemptive.v b/analysis/facts/preemption/job/preemptive.v
index 95319c4249efc2d863b4888365abfe3369e731d9..bb8fc1366d272fccef3b9420575238c1b727e9e1 100644
--- a/analysis/facts/preemption/job/preemptive.v
+++ b/analysis/facts/preemption/job/preemptive.v
@@ -15,8 +15,7 @@ Section FullyPreemptiveModel.
   Context `{JobCost Job}.
 
   (** Consider any kind of processor state model, ... *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
 
   (** ... any job arrival sequence, ... *)
   Variable arr_seq : arrival_sequence Job.
@@ -42,7 +41,7 @@ Section FullyPreemptiveModel.
     intros.
     rewrite /job_max_nonpreemptive_segment /lengths_of_segments
             /job_preemption_points. 
-      by rewrite H2; compute.
+      by rewrite H1; compute.
   Qed.
 
   (** ... or ε when [job_cost j > 0]. *)  
@@ -65,4 +64,4 @@ Section FullyPreemptiveModel.
   Qed.    
   
 End FullyPreemptiveModel.
-Global Hint Resolve valid_fully_preemptive_model : basic_facts. 
\ No newline at end of file
+Global Hint Resolve valid_fully_preemptive_model : basic_facts.
diff --git a/analysis/facts/preemption/rtc_threshold/job_preemptable.v b/analysis/facts/preemption/rtc_threshold/job_preemptable.v
index 8dba9cc61fa51bcf998daa6696c875db9746d56c..8f8a503d721b99723395bf7f62c8f0ed024ba81e 100644
--- a/analysis/facts/preemption/rtc_threshold/job_preemptable.v
+++ b/analysis/facts/preemption/rtc_threshold/job_preemptable.v
@@ -17,8 +17,7 @@ Section RunToCompletionThreshold.
   Context `{JobPreemptable Job}.
 
   (** Consider any kind of processor state model, ... *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
 
   (** ... any job arrival sequence, ... *)
   Variable arr_seq: arrival_sequence Job.
diff --git a/analysis/facts/preemption/task/preemptive.v b/analysis/facts/preemption/task/preemptive.v
index 8c073c2596ee8ca195e626e1c858d0ea30223c4c..512b68311695e7cfc416802030ab756b1edacf53 100644
--- a/analysis/facts/preemption/task/preemptive.v
+++ b/analysis/facts/preemption/task/preemptive.v
@@ -22,8 +22,7 @@ Section FullyPreemptiveModel.
   Context `{JobCost Job}.
 
   (** Consider any kind of processor state model, ... *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
 
   (** ... any job arrival sequence, ... *)
   Variable arr_seq : arrival_sequence Job.
diff --git a/analysis/facts/priority/edf.v b/analysis/facts/priority/edf.v
index e367906248b3295dcae5a4d2a22622a789c4cf5b..ed19b6a0af3b4db710a6e12090bc45267925ad93 100644
--- a/analysis/facts/priority/edf.v
+++ b/analysis/facts/priority/edf.v
@@ -66,7 +66,7 @@ Section SequentialEDF.
   Variable sched : schedule (ideal.processor_state Job).
   
   (** ... allow for any work-bearing notion of job readiness, ... *)
-  Context `{@JobReady Job (ideal.processor_state Job) _ Cost Arrival}.
+  Context `{@JobReady Job (ideal.processor_state Job) Cost Arrival}.
   Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
 
   (** ... and assume that the schedule is valid. *)
diff --git a/analysis/facts/priority/sequential.v b/analysis/facts/priority/sequential.v
index 0834ff21c0594aa3c4dcea0fee8acb44b997ab7d..54acdac9705efc410fb65308ba6fc4d343146407 100644
--- a/analysis/facts/priority/sequential.v
+++ b/analysis/facts/priority/sequential.v
@@ -24,7 +24,7 @@ Section SequentialJLFP.
   Variable sched : schedule (ideal.processor_state Job).
   
   (** ... allow for any work-bearing notion of job readiness, ... *)
-  Context `{@JobReady Job (ideal.processor_state Job) _ Cost Arrival}.
+  Context `{@JobReady Job (ideal.processor_state Job) Cost Arrival}.
   Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
 
   (** ... and assume that the schedule is valid. *)
diff --git a/analysis/facts/readiness/backlogged.v b/analysis/facts/readiness/backlogged.v
index f7b88aa84b14b0f9fce8fbaf48ddeb0e1a9e827c..bae0ed03c722ceb089d96d4ee3c2d5bb88b5f1de 100644
--- a/analysis/facts/readiness/backlogged.v
+++ b/analysis/facts/readiness/backlogged.v
@@ -10,10 +10,10 @@ Section BackloggedJobs.
   Context {Job : JobType} `{JobCost Job} `{JobArrival Job}.
 
   (** ... and any kind of processor model, ... *)
-  Context {PState : Type} `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
 
   (** ... and allow for any notion of job readiness. *)
-  Context `{JobReady Job PState}.
+  Context {jr : JobReady Job PState}.
 
   (** Given an arrival sequence and a schedule ... *)
   Variable arr_seq : arrival_sequence Job.
@@ -65,7 +65,7 @@ Section NonClairvoyance.
   Context {Job : JobType} `{JobCost Job} `{JobArrival Job}.
 
   (** ... any kind of processor model, ... *)
-  Context {PState : Type} `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
 
   (** ... and allow for any non-clairvoyant notion of job readiness. *)
   Context {RM : JobReady Job PState}.
diff --git a/analysis/facts/readiness/basic.v b/analysis/facts/readiness/basic.v
index 2c83ce771d21b90e7232ef45f2486ddfaec5d8a4..c3e0d39f5216c6a1a10bd4d4dffc2808cd418a10 100644
--- a/analysis/facts/readiness/basic.v
+++ b/analysis/facts/readiness/basic.v
@@ -11,8 +11,7 @@ Section LiuAndLaylandReadiness.
   Context {Job : JobType}.
 
   (** ... and any kind of processor state. *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
 
   (** Suppose jobs have an arrival time and a cost. *)
   Context `{JobArrival Job} `{JobCost Job}.
diff --git a/analysis/facts/readiness/sequential.v b/analysis/facts/readiness/sequential.v
index 219a7244a7f2e9fa13d3d2884dc28dea25a3257d..9330505d73ee702b3ffdfcd6900a4810fff87eac 100644
--- a/analysis/facts/readiness/sequential.v
+++ b/analysis/facts/readiness/sequential.v
@@ -18,8 +18,7 @@ Section SequentialTasksReadiness.
   Context `{JobCost Job}.
   
   (** ... and any kind of processor state. *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
   
   (** Consider any arrival sequence with consistent arrivals. *)
   Variable arr_seq : arrival_sequence Job.
diff --git a/analysis/facts/transform/edf_opt.v b/analysis/facts/transform/edf_opt.v
index 4350c7c6c0e998b079e05c85fca654f18e8e389f..952163fbc261f7157a4040fbfa66e34402683691 100644
--- a/analysis/facts/transform/edf_opt.v
+++ b/analysis/facts/transform/edf_opt.v
@@ -424,8 +424,7 @@ Section MakeEDFAtFacts.
         have ARR_j: job_arrival j <= t_edf by apply fsc_found_job_arrival with (sched := sched) (j1 := j_orig) => //; rewrite scheduled_at_def.
         now rewrite -EQ'.
       + move=> SCHED_j.
-        apply H_jobs_must_arrive_to_execute.
-        now rewrite scheduled_at_def /scheduled_in /pstate_instance.
+        by apply H_jobs_must_arrive_to_execute; rewrite scheduled_at_def.
   Qed.
 
   (** We connect the fact that a job is scheduled in [sched'] to the
diff --git a/analysis/facts/transform/replace_at.v b/analysis/facts/transform/replace_at.v
index 3dc797d62b9fa226f48caf29f7f405482148529b..ea0039ef41c70ebf1c3dac984f711cf5a05b9c82 100644
--- a/analysis/facts/transform/replace_at.v
+++ b/analysis/facts/transform/replace_at.v
@@ -9,8 +9,7 @@ Section ReplaceAtFacts.
   Context {Job : JobType}.
 
   (** ... and any given type of processor states, ... *)
-  Context {PState: Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.
 
   (** ...consider any given reference schedule. *)
   Variable sched: schedule PState.
diff --git a/analysis/facts/transform/swaps.v b/analysis/facts/transform/swaps.v
index 575e19c7cd70a55aa8c1ea1f435cc5370aaab51b..70125852043c64e71e4e6b304be9f1933c1f11de 100644
--- a/analysis/facts/transform/swaps.v
+++ b/analysis/facts/transform/swaps.v
@@ -9,8 +9,7 @@ Section SwappedFacts.
   (** For any given type of jobs... *)
   Context {Job : JobType}.
   (** ... any given type of processor states: *)
-  Context {PState: Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.
 
   (** ...consider any given reference schedule. *)
   Variable sched: schedule PState.
@@ -282,8 +281,7 @@ Section SwappedScheduleProperties.
   (** For any given type of jobs... *)
   Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
   (** ... any given type of processor states: *)
-  Context {PState: eqType}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.
 
   (** ...consider any given reference schedule. *)
   Variable sched: schedule PState.
@@ -364,8 +362,7 @@ Section EDFSwap.
   (** For any given type of jobs with costs and deadlines... *)
   Context {Job : JobType} `{JobCost Job} `{JobDeadline Job}.
   (** ... any given type of processor states... *)
-  Context {PState: eqType}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.
 
   (** ...consider a given reference schedule... *)
   Variable sched: schedule PState.
@@ -469,4 +466,4 @@ Section EDFSwap.
       + by apply uninvolved_implies_deadline_met.
   Qed.
 
- End EDFSwap.
+End EDFSwap.
diff --git a/analysis/transform/prefix.v b/analysis/transform/prefix.v
index 99670dad18b11d97f4e8df0a4706323fe4676fb3..82f976f515bbd90decf13968ee8885672ac907e4 100644
--- a/analysis/transform/prefix.v
+++ b/analysis/transform/prefix.v
@@ -11,8 +11,7 @@ Section SchedulePrefixMap.
   Context {Job : JobType}.
 
   (** ... any given type of processor states ... *)
-  Context {PState: eqType}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.
 
   (** ... we define a procedure that applies a given function to every
      point in a given finite prefix of the schedule.
diff --git a/analysis/transform/swap.v b/analysis/transform/swap.v
index 268bd4d13e29f74d9717758032420db1ba6430cd..8c6dd170487ef6a0e1a8d4353ec91ea2e2a4f929 100644
--- a/analysis/transform/swap.v
+++ b/analysis/transform/swap.v
@@ -9,8 +9,7 @@ Section ReplaceAt.
   (** For any given type of jobs... *)
   Context {Job : JobType}.
   (** ... any given type of processor states, ... *)
-  Context {PState: Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.
 
   (** ...consider any given reference schedule. *)
   Variable original_sched: schedule PState.
@@ -23,20 +22,18 @@ Section ReplaceAt.
 
   (** Then the schedule with replacement is simply one that returns the given
      [new_state] at [t'], and the original allocation at all other times. *)
-  Definition replace_at (t : instant) :=
-    if t' == t then new_state else (original_sched t).
+  Definition replace_at : schedule PState :=
+    fun t => if t' == t then new_state else (original_sched t).
 
 End ReplaceAt.
 
-
 (** Based on [replace_at], we define the notion of a schedule with swapped
     allocations. *)
 Section Swapped.
   (** For any given type of jobs... *)
   Context {Job : JobType}.
   (** ... any given type of processor states, ... *)
-  Context {PState: Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.
 
   (** ...consider any given reference schedule. *)
   Variable original_sched: schedule PState.
diff --git a/analysis/transform/wc_trans.v b/analysis/transform/wc_trans.v
index 8a984bb23d79bcff29ff9118b88589c186e09ef7..4722e17201164676842284474c87cf5688f59bbe 100644
--- a/analysis/transform/wc_trans.v
+++ b/analysis/transform/wc_trans.v
@@ -59,7 +59,7 @@ Section WCTransformation.
   (** The point-wise transformation procedure: given a schedule and a
       time [t1], ensure that the schedule is work-conserving at time
       [t1]. *)
-  Definition make_wc_at sched t1 :=
+  Definition make_wc_at sched t1 : schedule PState :=
     match sched t1 with
     | Some j => sched (* leave working instants alone *)
     | None =>
diff --git a/behavior/ready.v b/behavior/ready.v
index 049b1d43cb3699fed717584441db85f429de8f10..c13bc91436c01a546be7b717651a723aace0b739 100644
--- a/behavior/ready.v
+++ b/behavior/ready.v
@@ -9,8 +9,8 @@ Require Export prosa.behavior.service.
    used to model jitter, self-suspensions, etc.  Crucially, we require
    that any sensible notion of readiness is a refinement of the notion
    of a pending job, i.e., any ready job must also be pending. *)
-Class JobReady (Job : JobType) (PState : Type)
-      `{ProcessorState Job PState} `{JobCost Job} `{JobArrival Job} :=
+Class JobReady (Job : JobType) (PState : ProcessorState Job)
+      {jc : JobCost Job} {ja : JobArrival Job} :=
   {
     job_ready : schedule PState -> Job -> instant -> bool;
 
@@ -26,11 +26,10 @@ Class JobReady (Job : JobType) (PState : Type)
    backlogged, i.e., ready to run but not executing. *)
 Section Backlogged.
   (** Consider any kinds of jobs and any kind of processor state. *)
-  Context {Job : JobType} {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {Job : JobType} {PState : ProcessorState Job}.
 
   (** Allow for any notion of readiness. *)
-  Context `{JobReady Job PState}.
+  Context {jc : JobCost Job} {ja : JobArrival Job} {jr : JobReady Job PState}.
 
   (** Job j is backlogged at time t iff it is ready and not scheduled. *)
   Definition backlogged (sched : schedule PState) (j : Job) (t : instant) :=
@@ -44,8 +43,7 @@ End Backlogged.
 (** With the readiness concept in place, we define the notion of valid schedules. *)
 Section ValidSchedule.
   (** Consider any kind of jobs and any kind of processor state. *)
-  Context {Job : JobType} {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {Job : JobType} {PState : ProcessorState Job}.
 
   (** Consider any schedule. *)
   Variable sched : schedule PState.
@@ -60,8 +58,7 @@ Section ValidSchedule.
   Definition jobs_must_arrive_to_execute :=
     forall j t, scheduled_at sched j t -> has_arrived j t.
 
-  Context `{JobCost Job}.
-  Context `{JobReady Job PState}.
+  Context {jc : JobCost Job} {ja : JobArrival Job} {jr : JobReady Job PState}.
 
   (** ..., whether a job can only be scheduled if it is ready ... *)
   Definition jobs_must_be_ready_to_execute :=
diff --git a/behavior/schedule.v b/behavior/schedule.v
index 2353d536baffb269c839f55d99925d4b3235823f..1eb487cef0d4b34fabe56fcb70f4fd215eac40aa 100644
--- a/behavior/schedule.v
+++ b/behavior/schedule.v
@@ -20,8 +20,9 @@ Require Export prosa.behavior.arrival_sequence.
     In the most simple case (i.e., an ideal uniprocessor state—see
     [model/processor/ideal.v]), at any given time, either a particular job is
     scheduled or the processor is idle. *)
-Class ProcessorState (Job : JobType) (State : Type) :=
+Class ProcessorState (Job : JobType) :=
   {
+    State : Type;
     (** A [ProcessorState] instance provides a finite set of cores on which
         jobs can be scheduled. In the case of uniprocessors, this is irrelevant
         and may be ignored (by convention, the unit type is used as a
@@ -42,6 +43,7 @@ Class ProcessorState (Job : JobType) (State : Type) :=
     service_on_implies_scheduled_on :
       forall j s r, ~~ scheduled_on j s r -> service_on j s r = 0
   }.
+Coercion State : ProcessorState >-> Sortclass.
 
 (** The above definition of the [ProcessorState] interface provides
     the predicate [scheduled_on] and the function [service_on], which
@@ -57,7 +59,7 @@ Section ProcessorIn.
   (** Consider any type of jobs... *)
   Context {Job : JobType}.
   (** ...and any type of processor state. *)
-  Context {State : Type} `{ProcessorState Job State}.
+  Context {State : ProcessorState Job}.
 
   (** For a given processor state, the [scheduled_in] predicate checks
       whether a given job is running on any core in that state. *)
@@ -78,7 +80,8 @@ End ProcessorIn.
     each instant to a processor state, which reflects state of the computing
     platform at the specific time (e.g., which job is presently scheduled). *)
 
-Definition schedule (PState : Type) := instant -> PState.
+Definition schedule {Job : JobType} (PState : ProcessorState Job) :=
+  instant -> PState.
 
 (** The following line instructs Coq to not let proofs use knowledge of how
     [scheduled_on] and [service_on] are defined. Instead,
diff --git a/behavior/service.v b/behavior/service.v
index b4ff0fa7e745df08ed404dd3d26f19c2f6682005..f503d7ef0451544363843bbd92f1b412651e030f 100644
--- a/behavior/service.v
+++ b/behavior/service.v
@@ -6,8 +6,7 @@ Section Service.
   (** * Service of a Job *)
 
   (** Consider any kind of jobs and any kind of processor state. *)
-  Context {Job : JobType} {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {Job : JobType} {PState : ProcessorState Job}.
 
   (** Consider any schedule. *)
   Variable sched : schedule PState.
diff --git a/implementation/definitions/generic_scheduler.v b/implementation/definitions/generic_scheduler.v
index 7270f996bc4203e97b3814d4ac1d8a55dae3dfa7..bfd21eaf299b76ec4f487cfd0581995d7a1dec6d 100644
--- a/implementation/definitions/generic_scheduler.v
+++ b/implementation/definitions/generic_scheduler.v
@@ -11,7 +11,7 @@ Require Export prosa.analysis.transform.swap.
 Section PointwisePolicy.
   (** Consider any type of jobs and type of schedule. *)
   Context {Job : JobType}.
-  Variable PState : Type.
+  Variable PState : ProcessorState Job.
 
   (** A pointwise scheduling policy is a function that, given a schedule prefix
       that is valid up to time [t - 1], decides what to schedule at time
@@ -21,8 +21,7 @@ End PointwisePolicy.
 
 Section GenericSchedule.
   (** Consider any type of jobs and type of schedule. *)
-  Context {Job : JobType} {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {Job : JobType} {PState : ProcessorState Job}.
 
   (** Suppose we are given a policy function that, given a schedule prefix that
       is valid up to time [t - 1], decides what to schedule at time [t]. *)
@@ -52,4 +51,3 @@ Section GenericSchedule.
     schedule_up_to t t.
 
 End GenericSchedule.
-
diff --git a/implementation/facts/generic_schedule.v b/implementation/facts/generic_schedule.v
index 7c092d4a9d01c62788d978f949a81dd7cc9c0ded..6de5e8de08a19f2b9997bbbedf928c3542a8b1b6 100644
--- a/implementation/facts/generic_schedule.v
+++ b/implementation/facts/generic_schedule.v
@@ -10,8 +10,7 @@ Require Export prosa.analysis.facts.transform.replace_at.
 
 Section GenericScheduleProperties.
   (** For any type of jobs and type of schedule, ... *)
-  Context {Job : JobType} {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {Job : JobType} {PState : ProcessorState Job}.
 
   (** ... any scheduling policy, and ... *)
   Variable policy : PointwisePolicy PState.
@@ -61,7 +60,7 @@ Section GenericScheduleProperties.
     elim: h => [LT|h IH LT].
     { rewrite /schedule_up_to rest_of_schedule_invariant // => ZERO.
       now subst. }
-    { rewrite /schedule_up_to rest_of_schedule_invariant -/(schedule_up_to _ h t);
+    { rewrite /schedule_up_to rest_of_schedule_invariant -/(schedule_up_to _ _ h t);
         first by apply IH => //; apply ltn_trans with (n := h.+1).
       move=> EQ. move: LT.
       now rewrite EQ ltnn. }
diff --git a/model/aggregate/service_of_jobs.v b/model/aggregate/service_of_jobs.v
index 0771d2ce73f0730d41653088455a2f9ea2b01aef..83bb8f0ad3c4326bd1c0e044caaf8b369ac41d34 100644
--- a/model/aggregate/service_of_jobs.v
+++ b/model/aggregate/service_of_jobs.v
@@ -15,8 +15,7 @@ Section ServiceOfJobs.
   Context `{JobTask Job Task}.
   
   (** Consider any kind of processor model, ... *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
 
   (** ... any job arrival sequence, ... *) 
   Variable arr_seq : arrival_sequence Job.
diff --git a/model/preemption/parameter.v b/model/preemption/parameter.v
index be3211a50708c98690c0c506fcd55d23989680b4..46e04302acc05d665dd2aca6c021439ae9940bdd 100644
--- a/model/preemption/parameter.v
+++ b/model/preemption/parameter.v
@@ -100,8 +100,7 @@ Section PreemptionModel.
   Context `{JLDP_policy Job}.
 
   (** Consider any kind of processor model, ... *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
 
   (** ... any job arrival sequence, ... *)
   Variable arr_seq : arrival_sequence Job.
diff --git a/model/processor/ideal.v b/model/processor/ideal.v
index e41aa090394569b0da3feff462301aa021961c1f..8d384aa3ca61aa2b3572a957524486d3ac88745a 100644
--- a/model/processor/ideal.v
+++ b/model/processor/ideal.v
@@ -17,33 +17,26 @@ Section State.
   (** Consider any type of jobs. *)
   Variable Job: JobType.
 
-  (** We define the ideal "processor state" as an [option Job], which means
-      that it is either [Some j] (where [j] is a [Job]) or [None] (which we use
-      to indicate an idle instant). *)
-  Definition processor_state := option Job.
-
-  (** Based on this definition, we say that a given job [j] is scheduled in a
-      given state [s] iff [s] is [Some j]. *)
-  Let ideal_scheduled_at (j : Job) (s : processor_state) := s == Some j.
-
-  (** Similarly, we say that a given job [j] receives service in a given state
-      [s] iff [s] is [Some j]. *)
-  Let ideal_service_in (j : Job) (s : processor_state) := s == Some j.
-
-  (** Next, we connect the just-defined notion of an ideal processor state with
+  (** We connect the notion of an ideal processor state with
       the generic interface for the processor-state abstraction in Prosa by
       declaring a so-called instance of the [ProcessorState] typeclass. *)
-  Global Program Instance pstate_instance : ProcessorState Job processor_state :=
+  Global Program Instance processor_state : ProcessorState Job :=
     {
+      (** We define the ideal "processor state" as an [option Job],
+          which means that it is either [Some j] (where [j] is a
+          [Job]) or [None] (which we use to indicate an idle
+          instant). *)
+      State := option Job;
       (** As this is a uniprocessor model, cores are implicitly defined
           as the [unit] type containing a single element as a placeholder. *)
-      scheduled_on j s (_ : unit) := ideal_scheduled_at j s;
-      service_on j s (_ : unit) := ideal_service_in j s;
+      (** We say that a given job [j] is scheduled in a
+          given state [s] iff [s] is [Some j]. *)
+      scheduled_on j s (_ : unit) := s == Some j;
+      (** Similarly, we say that a given job [j] receives service in a
+          given state [s] iff [s] is [Some j]. *)
+      service_on j s (_ : unit) := s == Some j;
     }.
-  Next Obligation.
-    rewrite /ideal_service_in /nat_of_bool.
-    by case: ifP H =>// SOME /negP [].
-  Defined.
+  Next Obligation. by rewrite /nat_of_bool; case: ifP H => // ? /negP[]. Qed.
 
 End State.
 
diff --git a/model/processor/multiprocessor.v b/model/processor/multiprocessor.v
index 5c015eff7a820fd2a54c208f616cfecac97dce63..c4cd507ea8263dcf921b08c051ed33969e3e495f 100644
--- a/model/processor/multiprocessor.v
+++ b/model/processor/multiprocessor.v
@@ -22,8 +22,7 @@ Section Schedule.
   Variable Job: JobType.
 
   (** ... and consider any type of per-processor state. *)
-  Variable processor_state: Type.
-  Context `{ProcessorState Job processor_state}.
+  Variable processor_state: ProcessorState Job.
 
   (** Given a desired number of processors [num_cpus], we define a finite type
       of integers from [0] to [num_cpus - 1]. The purpose of this definition is
@@ -59,16 +58,17 @@ Section Schedule.
 
   (** Finally, we connect the above definitions with the generic Prosa
       interface for processor models. *)
-  Global Program Instance multiproc_state : ProcessorState Job multiprocessor_state :=
+  Global Program Instance multiproc_state : ProcessorState Job :=
     {
+      State := multiprocessor_state;
       scheduled_on := multiproc_scheduled_on;
       service_on := multiproc_service_on
     }.
   Next Obligation.
-    move: j s r H0.
+    move: j s r H.
     move=> j mps cpu.
     by apply: service_in_implies_scheduled_in.
-  Defined.
+  Qed.
 
   (** From the instance [multiproc_state], we get the function [service_in].
       The service received by a given job [j] in a given multiprocessor state
diff --git a/model/processor/platform_properties.v b/model/processor/platform_properties.v
index f33c8dc6b3d856897a85861c812f883221f2e4f9..bc26d070ad5b1de806bdeacb1cd28f7aaf247e0d 100644
--- a/model/processor/platform_properties.v
+++ b/model/processor/platform_properties.v
@@ -10,8 +10,7 @@ Section ProcessorModels.
       implicit context) because it is the primary subject of the following
       definitions. *)
   Context {Job : JobType}.
-  Variable PState : Type.
-  Context `{ProcessorState Job PState}.
+  Variable PState : ProcessorState Job.
 
   (** We say that a processor model provides unit service if no job ever
       receives more than one unit of service at any time. *)
diff --git a/model/processor/spin.v b/model/processor/spin.v
index e570c266c9595bc1ca4db857a476831bb176bee9..e3a1faad32776dd79b614cd4dac8b967eb84c595 100644
--- a/model/processor/spin.v
+++ b/model/processor/spin.v
@@ -48,8 +48,9 @@ Section State.
 
   (** Finally, we connect the above definitions with the generic Prosa
       interface for abstract processor states. *)
-  Global Program Instance pstate_instance : ProcessorState Job (processor_state) :=
+  Global Program Instance pstate_instance : ProcessorState Job :=
     {
+      State := processor_state;
       scheduled_on := spin_scheduled_on;
       service_on   := spin_service_on
     }.
@@ -58,5 +59,5 @@ Section State.
     case: s=>//= j' _.
     rewrite /nat_of_bool.
     by case: ifP.
-  Defined.
+  Qed.
 End State.
diff --git a/model/processor/varspeed.v b/model/processor/varspeed.v
index bddd7f508f9829a1b1a2df365913a49d6d72df2d..d03f3629343e5a727d7fdc43fe315c39bd5a28cd 100644
--- a/model/processor/varspeed.v
+++ b/model/processor/varspeed.v
@@ -45,8 +45,9 @@ Section State.
 
   (** Finally, we connect the above definitions to the generic Prosa interface
       for processor states. *)
-  Global Program Instance pstate_instance : ProcessorState Job processor_state :=
+  Global Program Instance pstate_instance : ProcessorState Job :=
     {
+      State := processor_state;
       scheduled_on := varspeed_scheduled_on;
       service_on   := varspeed_service_on
     }.
@@ -54,6 +55,6 @@ Section State.
     move: r H.
     case: s=>//= j' v _.
     by case: ifP.
-  Defined.
+  Qed.
 
 End State.
diff --git a/model/readiness/basic.v b/model/readiness/basic.v
index e08463dac4a8a000a92bdf38fb43bb8b08021e79..05eef0bee86a48bf28dba2e50e6ecc381232b194 100644
--- a/model/readiness/basic.v
+++ b/model/readiness/basic.v
@@ -11,8 +11,7 @@ Section LiuAndLaylandReadiness.
   Context {Job : JobType}.
 
   (** ... and any kind of processor state. *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
 
   (** Suppose jobs have an arrival time and a cost. *)
   Context `{JobArrival Job} `{JobCost Job}.
@@ -24,4 +23,3 @@ Section LiuAndLaylandReadiness.
     }.
 
 End LiuAndLaylandReadiness.
-
diff --git a/model/readiness/jitter.v b/model/readiness/jitter.v
index 82530a73c7625bcf439fe5e04f9017249ac6f29a..ada5b38ceff40df2ee8878fbff9c09b9164e845d 100644
--- a/model/readiness/jitter.v
+++ b/model/readiness/jitter.v
@@ -23,8 +23,7 @@ Section ReadinessOfJitteryJobs.
   Context {Job : JobType}.
 
   (** ... and any kind of processor state. *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
 
   (** Suppose jobs have an arrival time, a cost, and exhibit release jitter. *)
   Context `{JobArrival Job} `{JobCost Job} `{JobJitter Job}.
@@ -41,10 +40,10 @@ Section ReadinessOfJitteryJobs.
       job_ready sched j t := is_released j t && ~~ completed_by sched j t
     }.
   Next Obligation.
-    move: H3 => /andP [REL UNFINISHED].
+    move: H2 => /andP [REL UNFINISHED].
     rewrite /pending. apply /andP. split => //.
     move: REL. rewrite /is_released /has_arrived.
     by apply leq_addk.
-  Defined.
+  Qed.
 
 End ReadinessOfJitteryJobs.
diff --git a/model/readiness/sequential.v b/model/readiness/sequential.v
index e6e4aef4d85dd53c160ffa9a544eb99ef54b0cb4..1a85f7b1b2805fa09062667c87d73314692c8c96 100644
--- a/model/readiness/sequential.v
+++ b/model/readiness/sequential.v
@@ -19,8 +19,7 @@ Section SequentialTasksReadiness.
   Context `{JobCost Job}.
 
   (** ... and any kind of processor state. *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
 
   (** Consider any job arrival sequence ... *)
   Variable arr_seq : arrival_sequence Job.
@@ -34,8 +33,6 @@ Section SequentialTasksReadiness.
       pending sched j t &&
       prior_jobs_complete arr_seq sched j t
     }.
-  Next Obligation.
-    by move: H3 => /andP [T _].
-  Defined.
-  
+  Next Obligation. by move: H2 => /andP[]. Qed.
+
 End SequentialTasksReadiness.
diff --git a/model/readiness/suspension.v b/model/readiness/suspension.v
index 0db533d8c9c0c41ff79dd8a72e38b6ba3ac1b255..43926684f67bcbc3b899fa33e172916698960eb7 100644
--- a/model/readiness/suspension.v
+++ b/model/readiness/suspension.v
@@ -22,8 +22,7 @@ Section ReadinessOfSelfSuspendingJobs.
   Context {Job : JobType}.
 
   (** ... and any kind of processor state. *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
 
   (** Suppose jobs have an arrival time, a cost, and that they exhibit
       self-suspensions. *)
@@ -49,11 +48,11 @@ Section ReadinessOfSelfSuspendingJobs.
       job_ready sched j t := suspension_has_passed sched j t && ~~ completed_by sched j t
     }.
   Next Obligation.
-    move: H3 => /andP [PASSED UNFINISHED].
+    move: H2 => /andP [PASSED UNFINISHED].
     rewrite /pending. apply /andP. split => //.
     move: PASSED. rewrite /suspension_has_passed /has_arrived => /andP [ARR _].
     by move: ARR; apply leq_addk.
-  Defined.
+  Qed.
 
 End ReadinessOfSelfSuspendingJobs.
 
diff --git a/model/schedule/edf.v b/model/schedule/edf.v
index 632d90adf413212ff7be1664669c7afc94a1b1c5..947d79c584395708fb75858d0bb3ec53637ded26 100644
--- a/model/schedule/edf.v
+++ b/model/schedule/edf.v
@@ -31,8 +31,7 @@ Section AlternativeDefinitionOfEDF.
   Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
 
   (** ... and any processor model. *)
-  Context {PState: eqType}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
 
   (** We say that a schedule is _locally EDF-compliant_ at a given point in
       time [t] if the job [j] scheduled at time [t] has a deadline that is
@@ -59,10 +58,3 @@ Section AlternativeDefinitionOfEDF.
   Definition EDF_schedule (sched: schedule PState) := forall t, EDF_at sched t.
 
 End AlternativeDefinitionOfEDF.
-
-
-
-
-
-
-
diff --git a/model/schedule/limited_preemptive.v b/model/schedule/limited_preemptive.v
index cf32cb78a923c3323e8f17bc5c1123aa248792ff..dbf659caf64ddbe671a35a2b8fcf96ecac676f1c 100644
--- a/model/schedule/limited_preemptive.v
+++ b/model/schedule/limited_preemptive.v
@@ -12,7 +12,7 @@ Section ScheduleWithLimitedPreemptions.
   Context {Job : JobType}.
 
   (** ... any processor model, ... *)
-  Context {PState : Type} `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
   
   (** ... and any preemption model. *)
   Context `{JobPreemptable Job}.
diff --git a/model/schedule/nonpreemptive.v b/model/schedule/nonpreemptive.v
index 36c3858e27266646b904752ddb9c4e740b95f37f..803e88a97b8b93a7e965e569db8d6641c40019bd 100644
--- a/model/schedule/nonpreemptive.v
+++ b/model/schedule/nonpreemptive.v
@@ -13,8 +13,7 @@ Section NonpreemptiveSchedule.
   Context `{JobCost Job}.
 
   (** ... and any kind of processor model. *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
   
   (** We say that a given schedule is _nonpreemptive_ if every job,
       once it is scheduled, remains scheduled until completion. *)
diff --git a/model/schedule/priority_driven.v b/model/schedule/priority_driven.v
index 14dbe0d964d2cde0128787460345b20a29103c6e..cb8d74027d5fac0955bf7e774d66f7e6193dd861 100644
--- a/model/schedule/priority_driven.v
+++ b/model/schedule/priority_driven.v
@@ -30,7 +30,7 @@ Section Priority.
 
   (** ... and consider any preemption model and notion of readiness. *)
   Context `{JobPreemptable Job}.
-  Context `{JobReady Job (ideal.processor_state Job)}.
+  Context {jr : JobReady Job (ideal.processor_state Job)}.
 
   (** Given any job arrival sequence... *)
   Variable arr_seq : arrival_sequence Job.
@@ -53,4 +53,3 @@ Section Priority.
       hep_job_at t j_hp j.
 
 End Priority.
-
diff --git a/model/schedule/tdma.v b/model/schedule/tdma.v
index 68f5fd46fb134da15c25c89e8d3aed296272261c..5f79fecc17a70b739f1df0726c3879da1c047d04 100644
--- a/model/schedule/tdma.v
+++ b/model/schedule/tdma.v
@@ -113,7 +113,8 @@ Section TDMASchedule.
 
   Context {Task : TaskType} {Job : JobType}.
 
-  Context `{JobArrival Job} `{JobCost Job} `{JobReady Job (option Job)} `{JobTask Job Task}.
+  Context {ja : JobArrival Job} {jc : JobCost Job}.
+  Context {jr : JobReady Job (ideal.processor_state Job)} `{JobTask Job Task}.
 
   (** Consider any job arrival sequence... *)
   Variable arr_seq : arrival_sequence Job.
diff --git a/model/schedule/work_conserving.v b/model/schedule/work_conserving.v
index 41f23a3a5408baca553dbf8274b7984f1901e5a0..47a97cd57fa0136adc645572fe4b8e2d43887b2a 100644
--- a/model/schedule/work_conserving.v
+++ b/model/schedule/work_conserving.v
@@ -20,11 +20,10 @@ Section WorkConserving.
   Context `{JobCost Job}.
 
   (** ... and any kind of processor model. *)
-  Context {PState: Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState: ProcessorState Job}.
 
   (** Further, allow for any notion of job readiness. *)
-  Context `{JobReady Job PState}.
+  Context {jr : JobReady Job PState}.
 
   (** Given an arrival sequence and a schedule ... *)
   Variable arr_seq : arrival_sequence Job.
@@ -47,4 +46,3 @@ Section WorkConserving.
     [seq j <- arrivals_up_to arr_seq t | backlogged sched j t].
 
 End WorkConserving.
-
diff --git a/model/task/preemption/parameters.v b/model/task/preemption/parameters.v
index bd034d7df0e4ff584b902223904ce90fe39453f3..914978dbfb816ac474a684e660a88c0460ec5e04 100644
--- a/model/task/preemption/parameters.v
+++ b/model/task/preemption/parameters.v
@@ -78,8 +78,7 @@ Section ValidPreemptionModel.
   Context `{JobPreemptable Job}.
 
   (** Consider any kind of processor state model, ... *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
 
   (** ... any job arrival sequence, ... *)
   Variable arr_seq : arrival_sequence Job.
@@ -150,8 +149,7 @@ Section ValidTaskRunToCompletionThreshold.
   Context `{TaskRunToCompletionThreshold Task}.
 
   (** Further, consider any kind of processor model, ... *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
 
   (** ... any job arrival sequence, ... *)
   Variable arr_seq: arrival_sequence Job.
diff --git a/model/task/sequentiality.v b/model/task/sequentiality.v
index d2562128f1a84452bae109ecff6c20198bffae6d..d836729e84f4c1c89bc7c0a99610d6fb0fd3982a 100644
--- a/model/task/sequentiality.v
+++ b/model/task/sequentiality.v
@@ -17,8 +17,7 @@ Section PropertyOfSequentiality.
   Context `{JobCost Job}.
 
   (** ... and any kind of processor model. *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
+  Context {PState : ProcessorState Job}.
 
   (** Consider any arrival sequence ... *) 
   Variable arr_seq : arrival_sequence Job.
@@ -44,6 +43,5 @@ Section PropertyOfSequentiality.
     all 
       (fun j_tsk => completed_by sched j_tsk t) 
       (task_arrivals_before arr_seq (job_task j) (job_arrival j)).
-      
 
 End PropertyOfSequentiality.
diff --git a/results/fixed_priority/rta/bounded_nps.v b/results/fixed_priority/rta/bounded_nps.v
index 4b072f3df933d6d9577c30891c2ceb3eaf92dd70..40bce6903858ddbed284a3bb66c4bba8d5e69d5d 100644
--- a/results/fixed_priority/rta/bounded_nps.v
+++ b/results/fixed_priority/rta/bounded_nps.v
@@ -49,7 +49,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
   Variable sched : schedule (ideal.processor_state Job).
   
   (** ... allow for any work-bearing notion of job readiness, ... *)
-  Context `{@JobReady Job (ideal.processor_state Job) _ Cost Arrival}.
+  Context `{@JobReady Job (ideal.processor_state Job) Cost Arrival}.
   Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
 
   (** ... and assume that the schedule is valid.  *)
diff --git a/results/fixed_priority/rta/bounded_pi.v b/results/fixed_priority/rta/bounded_pi.v
index 2285d0e243e4b06954871160468cf7824c837b46..3f59660980b9a93a8b8107c8fe79b9339f2e3528 100644
--- a/results/fixed_priority/rta/bounded_pi.v
+++ b/results/fixed_priority/rta/bounded_pi.v
@@ -54,7 +54,7 @@ Section AbstractRTAforFPwithArrivalCurves.
   Variable sched : schedule (ideal.processor_state Job).
   
   (** ... allow for any work-bearing notion of job readiness, ... *)
-  Context `{@JobReady Job (ideal.processor_state Job) _ Cost Arrival}.
+  Context `{@JobReady Job (ideal.processor_state Job) Cost Arrival}.
   Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
 
   (** ... and assume that the schedule is valid.  *)