diff --git a/analysis/abstract/abstract_rta.v b/analysis/abstract/abstract_rta.v
index f3bfb0084c0cfa93c28c026ea6f6381b7e4071a8..cf64d773bc5972e1a662a59cfe2fe7b4170643e1 100644
--- a/analysis/abstract/abstract_rta.v
+++ b/analysis/abstract/abstract_rta.v
@@ -33,8 +33,7 @@ Section Abstract_RTA.
   (** Consider any arrival sequence with consistent, non-duplicate arrivals... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-  Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
-  
+
   (** Next, consider any schedule of this arrival sequence...*)
   Variable sched : schedule PState.
   Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
diff --git a/analysis/abstract/abstract_seq_rta.v b/analysis/abstract/abstract_seq_rta.v
index 5e6fdf1f0e3e03e08be25fa9bfe0ba2d08d2b08d..7c7b38bde9b51710c370b90badb347fcd9890428 100644
--- a/analysis/abstract/abstract_seq_rta.v
+++ b/analysis/abstract/abstract_seq_rta.v
@@ -32,7 +32,6 @@ Section Sequential_Abstract_RTA.
   (** Consider any arrival sequence with consistent, non-duplicate arrivals... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-  Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
 
   (** Next, consider any ideal uniprocessor schedule of this arrival sequence...*)
   Variable sched : schedule (ideal.processor_state Job).
@@ -584,7 +583,7 @@ Section Sequential_Abstract_RTA.
         { apply arrived_between_implies_in_arrivals; try done.
           apply/andP; split; rewrite /A subnKC //.
           by rewrite addn1 ltnSn //. }
-        have Fact4: j \in arrivals_at arr_seq (t1 + A).
+        have Fact4: j \in arr_seq (t1 + A).
         { by move: ARR => [t ARR]; rewrite subnKC //; feed (H_arrival_times_are_consistent j t); try (subst t). }
         have Fact1: 1 <= number_of_task_arrivals arr_seq tsk (t1 + A) (t1 + A + ε).
         { rewrite /number_of_task_arrivals /task_arrivals_between /arrival_sequence.arrivals_between.
diff --git a/analysis/abstract/ideal_jlfp_rta.v b/analysis/abstract/ideal_jlfp_rta.v
index c27b606f69b2b0b223533f948a31b44c0f6b3281..2200ab015ed6a0d43f67ca647e503db41375fc61 100644
--- a/analysis/abstract/ideal_jlfp_rta.v
+++ b/analysis/abstract/ideal_jlfp_rta.v
@@ -25,8 +25,7 @@ Section JLFPInstantiation.
   (** Consider any arrival sequence with consistent arrivals. *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-  Hypothesis H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq. 
-  
+
   (** Next, consider any ideal uni-processor schedule of this arrival sequence ... *)
   Variable sched : schedule (ideal.processor_state Job).
   Hypothesis H_jobs_come_from_arrival_sequence:
@@ -117,7 +116,7 @@ Section JLFPInstantiation.
       workload are generated by jobs with higher or equal priority
       released at time [t]. *)
   Definition interfering_workload_of_hep_jobs (j : Job) (t : instant) :=
-    \sum_(jhp <- arrivals_at arr_seq t | another_hep_job jhp j) job_cost jhp.
+    \sum_(jhp <- arr_seq t | another_hep_job jhp j) job_cost jhp.
 
   (** Instantiation of Interference *)
   (** We say that job [j] incurs interference at time [t] iff it
diff --git a/analysis/definitions/completion_sequence.v b/analysis/definitions/completion_sequence.v
index d53960d6527a35c2cb51bcf5f568b80f0c0e1708..22b8dc9cbf7b295636d961f06a510ca92efb55e5 100644
--- a/analysis/definitions/completion_sequence.v
+++ b/analysis/definitions/completion_sequence.v
@@ -1,5 +1,5 @@
 From mathcomp Require Export ssreflect seq ssrnat ssrbool eqtype.
-Require Import prosa.behavior.service.
+Require Import prosa.behavior.service prosa.analysis.facts.behavior.arrivals.
 
 (** This module contains basic definitions and properties of job
     completion sequences. *)
@@ -11,18 +11,28 @@ Section CompletionSequence.
 
   (** Consider any kind of jobs with a cost
      and any kind of processor state. *)
-  Context {Job : JobType} `{JobCost Job} {PState : Type}.
+  Context {Job : JobType} `{JobCost Job} `{JobArrival Job} {PState : Type}.
   Context `{ProcessorState Job PState}.
 
   (** Consider any job arrival sequence. *)
   Variable arr_seq: arrival_sequence Job.
 
+  Variable consistent_JobArrival : consistent_arrival_times arr_seq.
+
   (** Consider any schedule. *)
   Variable sched : schedule PState.
 
+  Definition completion_sequence_subdef :=
+    fun t => [seq j <- arrivals_up_to arr_seq t | completes_at sched j t].
+
+  Lemma completion_sequence_subproof t : uniq (completion_sequence_subdef t).
+  Proof. exact/filter_uniq/arrivals_uniq. Qed.
+
   (** For each instant [t], the completion sequence returns all
      arrived jobs that have completed at [t]. *)
-  Definition completion_sequence : arrival_sequence Job :=
-    fun t => [seq j <- arrivals_up_to arr_seq t | completes_at sched j t].
+  Definition completion_sequence : arrival_sequence Job := {|
+    arrival_sequence_seq := completion_sequence_subdef;
+    arrival_sequence_uniq := completion_sequence_subproof
+  |}.
 
 End CompletionSequence.
diff --git a/analysis/facts/behavior/arrivals.v b/analysis/facts/behavior/arrivals.v
index 7c7f02d7a662f1c479273a95b112e16679bd6224..9ab882562cb2010ef79c42f3245562b167e5b463 100644
--- a/analysis/facts/behavior/arrivals.v
+++ b/analysis/facts/behavior/arrivals.v
@@ -226,11 +226,7 @@ Section ArrivalSequencePrefix.
       forall t j,
         j \in arr_seq t ->
         arrives_in arr_seq j.
-    Proof.
-      move => t j J_ARR.
-      exists t.
-      now rewrite /arrivals_at.
-    Qed.
+    Proof. by move=> t j J_ARR; exists t. Qed.
 
     (** Next, we prove that if a job belongs to the prefix
          (jobs_arrived_between t1 t2), then it indeed arrives between t1 and
@@ -305,12 +301,11 @@ Section ArrivalSequencePrefix.
     (** Next, we prove that if the arrival sequence doesn't contain duplicate
         jobs, the same applies for any of its prefixes. *)
     Lemma arrivals_uniq:
-      arrival_sequence_uniq arr_seq ->
       forall t1 t2, uniq (arrivals_between arr_seq t1 t2).
     Proof.
       rename H_consistent_arrival_times into CONS.
-      unfold arrivals_up_to; intros SET t1 t2.
-      apply bigcat_nat_uniq; first by done.
+      unfold arrivals_up_to; intros t1 t2.
+      apply bigcat_nat_uniq; first exact: arrival_sequence_uniq.
       intros x t t' IN1 IN2.
         by apply CONS in IN1; apply CONS in IN2; subst.
     Qed.
diff --git a/analysis/facts/busy_interval/busy_interval.v b/analysis/facts/busy_interval/busy_interval.v
index fcf7a6af27833657fc8444cb45ad1dd52fa1e535..1ee98baa52c7605202340056c8a6b426c42a34a8 100644
--- a/analysis/facts/busy_interval/busy_interval.v
+++ b/analysis/facts/busy_interval/busy_interval.v
@@ -243,10 +243,6 @@ Section ExistsBusyIntervalJLFP.
     (** Assume that the schedule is work-conserving ... *)
     Hypothesis H_work_conserving : work_conserving arr_seq sched.
 
-    (** ... and there are no duplicate job arrivals. *)
-    Hypothesis H_arrival_sequence_is_a_set:
-      arrival_sequence_uniq arr_seq.
-
     (** Let [t1] be a quiet time. *)
     Variable t1 : instant.
     Hypothesis H_quiet_time : quiet_time t1.
@@ -341,10 +337,6 @@ Section ExistsBusyIntervalJLFP.
     (** Assume that the schedule is work-conserving, ... *)
     Hypothesis H_work_conserving : work_conserving arr_seq sched.
 
-    (** ... and there are no duplicate job arrivals, ... *)
-    Hypothesis H_arrival_sequence_is_a_set:
-      arrival_sequence_uniq arr_seq.        
-
     (** ... and the priority relation is reflexive and transitive. *)
     Hypothesis H_priority_is_reflexive: reflexive_priorities.
     Hypothesis H_priority_is_transitive: transitive_priorities.
diff --git a/analysis/facts/busy_interval/carry_in.v b/analysis/facts/busy_interval/carry_in.v
index e4fe3aeff9eaf9b1109fe85e218979ef2d2df79d..17a33d1062d3c0d43f98896c1d9ef0feedb43f6a 100644
--- a/analysis/facts/busy_interval/carry_in.v
+++ b/analysis/facts/busy_interval/carry_in.v
@@ -56,10 +56,6 @@ Section ExistsNoCarryIn.
   (** Assume that the schedule is work-conserving, ... *)
   Hypothesis H_work_conserving : work_conserving arr_seq sched.
 
-  (** ... and there are no duplicate job arrivals. *)
-  Hypothesis H_arrival_sequence_is_a_set:
-    arrival_sequence_uniq arr_seq.
-  
   (** The fact that there is no carry-in at time instant [t] trivially
       implies that [t] is a quiet time. *)
   Lemma no_carry_in_implies_quiet_time :
diff --git a/analysis/facts/hyperperiod.v b/analysis/facts/hyperperiod.v
index 1915643296c3fb6e24f1edb7df85be841b1c97d6..8ca806d9056e546d1e8860ac09c0ed88747c6038 100644
--- a/analysis/facts/hyperperiod.v
+++ b/analysis/facts/hyperperiod.v
@@ -66,8 +66,7 @@ Section PeriodicLemmas.
   (** ... and a consistent arrival sequence with non-duplicate arrivals. *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
-  Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
-  
+
   (** Consider a task set [ts] such that all tasks in
       [ts] have valid periods. *)
   Variable ts : TaskSet Task.
diff --git a/analysis/facts/job_index.v b/analysis/facts/job_index.v
index d2909cd8cbaf9b1556b3c40bcbacf04960ce59cd..c62606018a26a9d730001bbf80fe4bf61f3d25f7 100644
--- a/analysis/facts/job_index.v
+++ b/analysis/facts/job_index.v
@@ -14,8 +14,7 @@ Section JobIndexLemmas.
   (** Consider any arrival sequence with consistent and non-duplicate arrivals, ... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_consistent_arrivals : consistent_arrival_times arr_seq. 
-  Hypothesis H_uniq_arr_seq : arrival_sequence_uniq arr_seq.
-  
+
   (** ... and any two jobs [j1] and [j2] from this arrival sequence
    that stem from the same task. *)
   Variable j1 j2 : Job.
@@ -245,8 +244,7 @@ Section PreviousJob.
   (** Consider any unique arrival sequence with consistent arrivals ... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_consistent_arrivals : consistent_arrival_times arr_seq. 
-  Hypothesis H_uniq_arr_seq : arrival_sequence_uniq arr_seq.
-  
+
   (** ... and an arbitrary job with a positive [job_index]. *)
   Variable j : Job.
   Hypothesis H_arrives_in_arr_seq: arrives_in arr_seq j.
@@ -268,9 +266,9 @@ Section PreviousJob.
   Lemma prev_job_index:
     index (prev_job arr_seq j) (task_arrivals_up_to_job_arrival arr_seq j) = job_index arr_seq j - 1.
   Proof.
-    apply index_uniq; last by apply uniq_task_arrivals.
+    apply: index_uniq; last exact: uniq_task_arrivals.
     apply leq_ltn_trans with (n := job_index arr_seq j); try by ssrlia.
-    now apply index_job_lt_size_task_arrivals_up_to_job.
+    exact: index_job_lt_size_task_arrivals_up_to_job.
   Qed.
 
   (** Observe that job [j] and [prev_job j] stem from the same task. *)
@@ -288,7 +286,7 @@ Section PreviousJob.
   Proof.
     rewrite /prev_job -index_mem index_uniq;
       try by apply job_index_minus_one_lt_size_task_arrivals_up_to.
-    now apply uniq_task_arrivals.
+    exact: uniq_task_arrivals.
   Qed.       
 
   (** We observe that for any job [j] the arrival time of [prev_job j] is 
@@ -364,7 +362,7 @@ Section PreviousJob.
     have JK_ARR : (arrives_in arr_seq jk) by apply in_arrseq_implies_arrives with (t := i) => //.
     have INDJK : (index jk (task_arrivals_up_to_job_arrival arr_seq j) = k).
     { apply index_uniq => //.
-      now apply uniq_task_arrivals => //. }
+      exact: uniq_task_arrivals. }
     repeat split => //.    
     { rewrite -> diff_jobs_iff_diff_indices => //; eauto.
       rewrite /job_index; rewrite [in X in _ <> X] (job_index_same_in_task_arrivals _ _ jk j) => //.
diff --git a/analysis/facts/model/offset.v b/analysis/facts/model/offset.v
index c19f246cb91b341a16677a90b61e709f773b9bb9..42b19c2230054359d27db34cfbb420b8ee6b3eb0 100644
--- a/analysis/facts/model/offset.v
+++ b/analysis/facts/model/offset.v
@@ -16,7 +16,6 @@ Section OffsetLemmas.
   (** Consider any arrival sequence with consistent and non-duplicate arrivals ... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
-  Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
 
   (** ... and any job [j] (that stems from the arrival sequence) of any 
       task [tsk] with a valid offset. *)
diff --git a/analysis/facts/model/rbf.v b/analysis/facts/model/rbf.v
index bed12269173e77c228483e522d93b352c65081cb..f93e4003de3aa6c99d326d7f32ce703b66c6f623 100644
--- a/analysis/facts/model/rbf.v
+++ b/analysis/facts/model/rbf.v
@@ -25,7 +25,6 @@ Section ProofWorkloadBound.
   (** Consider any arrival sequence with consistent, non-duplicate arrivals, ... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-  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}.
diff --git a/analysis/facts/model/task_arrivals.v b/analysis/facts/model/task_arrivals.v
index ee44311df2053760b9beab7009733a7ba71fee2a..077ead4f8fb73d0d6840f2b8252123bb3e30d7e2 100644
--- a/analysis/facts/model/task_arrivals.v
+++ b/analysis/facts/model/task_arrivals.v
@@ -71,7 +71,7 @@ Section TaskArrivals.
     split; first by apply /eqP => //. 
     move : ARR => [t ARR]; move : (ARR) => EQ.
     apply H_consistent_arrivals in EQ.
-    rewrite (mem_bigcat_nat _ (fun t => arrivals_at arr_seq t) j 0 _ (job_arrival j)) // EQ //.
+    rewrite (mem_bigcat_nat _ (fun t => arr_seq t) j 0 _ (job_arrival j)) // EQ //.
     now ssrlia.
   Qed.
 
@@ -85,7 +85,6 @@ Section TaskArrivals.
     intros j ARR.
     rewrite mem_filter; apply /andP.
     split; first by apply /eqP => //. 
-    rewrite /arrivals_at.
     move : ARR => [t ARR].
     now rewrite (H_consistent_arrivals j t ARR).
   Qed.
@@ -173,13 +172,8 @@ Section TaskArrivals.
       task arrivals also contain non-duplicate arrivals. *)
   Lemma uniq_task_arrivals:
     forall t,
-      arrival_sequence_uniq arr_seq ->
       uniq (task_arrivals_up_to arr_seq tsk t).
-  Proof.
-    intros * UNQ_SEQ.
-    apply filter_uniq.
-    now apply arrivals_uniq.
-  Qed.
+  Proof. move=> t; exact/filter_uniq/arrivals_uniq. Qed.
   
   (** A job cannot arrive before it's arrival time. *) 
   Lemma job_notin_task_arrivals_before:
diff --git a/analysis/facts/model/workload.v b/analysis/facts/model/workload.v
index 6ad3ed36768cccbfb131ba84ff70eff76996dce8..0d86206a2e947cc788cee6e3ee3b11553d13f4a5 100644
--- a/analysis/facts/model/workload.v
+++ b/analysis/facts/model/workload.v
@@ -69,7 +69,6 @@ Section WorkloadFacts.
 
     (** Assume that arrival times are consistent and that arrivals are unique. *)
     Hypothesis H_consistent_arrival_times : consistent_arrival_times arr_seq.
-    Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
 
     (** Consider a time interval <<[t1, t2)>> and a time instant [t]. *)
     Variable t1 t2 t : instant.
@@ -88,7 +87,8 @@ Section WorkloadFacts.
     Proof.
       rewrite /workload_of_jobs big_seq_cond.
       rewrite -[in X in X <= _]big_filter -[in X in _ <= X]big_filter.
-      apply leq_sum_sub_uniq; first by apply filter_uniq, arrivals_uniq.
+      apply leq_sum_sub_uniq.
+      { apply/filter_uniq/arrivals_uniq => //; exact: arrival_sequence_uniq. }
       move => j'; rewrite mem_filter => [/andP [/andP [A /andP [C D]] _]].
       rewrite mem_filter; apply/andP; split; first by done.
       apply job_in_arrivals_between; eauto.
diff --git a/analysis/facts/periodic/arrival_separation.v b/analysis/facts/periodic/arrival_separation.v
index 0849781ea5ad9067ee93757ead04147fb138bf89..6c133c118b627785dbf3017f420ed2cc9c95f25d 100644
--- a/analysis/facts/periodic/arrival_separation.v
+++ b/analysis/facts/periodic/arrival_separation.v
@@ -18,7 +18,6 @@ Section JobArrivalSeparation.
   (** Consider any unique arrival sequence with consistent arrivals, ... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
-  Hypothesis H_uniq_arrseq: arrival_sequence_uniq arr_seq.
 
   (** ... and any task [tsk] that is to be analyzed. *)
   Variable tsk : Task.
@@ -95,7 +94,7 @@ Section JobArrivalSeparation.
       }
       { intros j1 j2 TSKj1 TSKj2 STEP LT ARRj2 ARRj1.
         specialize (exists_jobs_before_j
-                      arr_seq H_consistent_arrivals H_uniq_arrseq j2 ARRj2 (job_index arr_seq j2 - s)) => BEFORE.
+                      arr_seq H_consistent_arrivals j2 ARRj2 (job_index arr_seq j2 - s)) => BEFORE.
         destruct s.
         - exists 1; repeat split.
           now rewrite (consecutive_job_separation j1) //; ssrlia.
diff --git a/analysis/facts/periodic/arrival_times.v b/analysis/facts/periodic/arrival_times.v
index 15a7501986b72f12916e1d7fa4a6f9d15ddb1032..8bd2e338bcac1a9806d030b68a98537471828396 100644
--- a/analysis/facts/periodic/arrival_times.v
+++ b/analysis/facts/periodic/arrival_times.v
@@ -19,7 +19,6 @@ Section PeriodicArrivalTimes.
   (** Consider any unique arrival sequence with consistent arrivals ... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
-  Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
 
   (** ... and any periodic task [tsk] with a valid offset and period. *)
     Variable tsk : Task.
diff --git a/analysis/facts/periodic/sporadic.v b/analysis/facts/periodic/sporadic.v
index 07bc889a7e99682b32cddb50f7c1443e8cf5e9bd..b4ff90789a66c2c7545e2810896a4dcb5db7cb64 100644
--- a/analysis/facts/periodic/sporadic.v
+++ b/analysis/facts/periodic/sporadic.v
@@ -22,8 +22,7 @@ Section PeriodicTasksAsSporadicTasks.
 
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
-  Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
-  
+
   (** ... may be interpreted as a type of sporadic tasks by using each task's
       period as its minimum inter-arrival time ... *)
   Global Instance periodic_as_sporadic : SporadicModel Task :=
diff --git a/analysis/facts/periodic/task_arrivals_size.v b/analysis/facts/periodic/task_arrivals_size.v
index 4c6658cd1154eb9449137d1fa6712e06e2829a00..160154b25f20e281528db2729f2ee00b8ed559df 100644
--- a/analysis/facts/periodic/task_arrivals_size.v
+++ b/analysis/facts/periodic/task_arrivals_size.v
@@ -18,7 +18,6 @@ Section TaskArrivalsSize.
   (** Consider any unique arrival sequence with consistent arrivals ... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
-  Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
 
   (** ... and any periodic task [tsk] with a valid offset and period. *)
   Variable tsk : Task.
@@ -43,7 +42,7 @@ Section TaskArrivalsSize.
     destruct (EMPT_OR_EXISTS Job (task_arrivals_at arr_seq tsk t)) as [EMPT | [a A_IN]] => //.
     rewrite /task_arrivals_at mem_filter in A_IN; move : A_IN => /andP [/eqP TSK A_ARR].
     move : (A_ARR) => A_IN; apply H_consistent_arrivals in A_IN.
-    rewrite -A_IN in T; rewrite /arrivals_at in A_ARR.
+    rewrite -A_IN in T.
     apply in_arrseq_implies_arrives in A_ARR.
     have EXISTS_N : exists n, job_arrival a = task_offset tsk + n * task_period tsk by
           apply job_arrival_times with (arr_seq0 := arr_seq) => //.
@@ -62,10 +61,12 @@ Section TaskArrivalsSize.
     case: (ltngtP (size (task_arrivals_at arr_seq tsk t)) 1) => [LT|GT|EQ]; try by auto.
     destruct (size (task_arrivals_at arr_seq tsk t)); now left.
     specialize (exists_two (task_arrivals_at arr_seq tsk t)) => EXISTS_TWO.
-    destruct EXISTS_TWO as [a [b [NEQ [A_IN B_IN]]]]; [by done | by apply filter_uniq | ].
+    have uniq_task : uniq (task_arrivals_at arr_seq tsk t).
+    { exact/filter_uniq/arrival_sequence_uniq. }
+    have [a [b [NEQ [A_IN B_IN]]]] := EXISTS_TWO GT uniq_task.
     rewrite mem_filter in A_IN; rewrite mem_filter in B_IN.
     move: A_IN B_IN => /andP [/eqP TSKA ARRA] /andP [/eqP TSKB ARRB].
-    move: (ARRA); move: (ARRB); rewrite /arrivals_at => A_IN B_IN.
+    move: (ARRA) (ARRB) => A_IN B_IN.
     apply in_arrseq_implies_arrives in A_IN; apply in_arrseq_implies_arrives in B_IN.
     have SPO : respects_sporadic_task_model arr_seq tsk; try by auto with basic_facts.
     have EQ_ARR_A : (job_arrival a = t) by apply H_consistent_arrivals.
diff --git a/analysis/facts/shifted_job_costs.v b/analysis/facts/shifted_job_costs.v
index 5cd9b2c620a6009f9502fdf9b0f6cace5c047538..bf6a276733c7147d76069ad46bd67d5459a12749 100644
--- a/analysis/facts/shifted_job_costs.v
+++ b/analysis/facts/shifted_job_costs.v
@@ -23,7 +23,6 @@ Section ValidJobCostsShifted.
   (** Consider a consistent arrival sequence with non-duplicate arrivals. *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
-  Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
 
   (** Furthermore, assume that arrivals have valid job costs. *) 
   Hypothesis H_arrivals_have_valid_job_costs: arrivals_have_valid_job_costs arr_seq.
diff --git a/analysis/facts/sporadic.v b/analysis/facts/sporadic.v
index f8895b2586ec1a80c27de4807be3aae24d7d076b..9c7b1b5ac60c8eb67325a11861e8bf81cefda2a1 100644
--- a/analysis/facts/sporadic.v
+++ b/analysis/facts/sporadic.v
@@ -21,8 +21,7 @@ Section SporadicModelIndexLemmas.
   (** Consider any unique arrival sequence with consistent arrivals, ... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
-  Hypothesis H_uniq_arrseq: arrival_sequence_uniq arr_seq.
-  
+
   (** ... and any sporadic task [tsk] that is to be analyzed. *)
   Variable tsk : Task.
   Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
@@ -73,8 +72,7 @@ Section DifferentJobsImplyDifferentArrivalTimes.
   (** Consider any unique arrival sequence with consistent arrivals, ... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
-  Hypothesis H_uniq_arrseq: arrival_sequence_uniq arr_seq.
-  
+
   (** ... and any sporadic task [tsk] that is to be analyzed. *)
   Variable tsk : Task.
   Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
@@ -135,7 +133,6 @@ Section SporadicArrivals.
   (** Consider any unique arrival sequence with consistent arrivals, ... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
-  Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
 
   (** ... and any sporadic task [tsk] to be analyzed. *)
   Variable tsk : Task.
@@ -165,10 +162,12 @@ Section SporadicArrivals.
   Proof.
     move => [j [SIZE_G [PERIODIC VALID_TMIA]]].
     specialize (exists_two (task_arrivals_at_job_arrival arr_seq j)) => EXISTS_TWO.
-    destruct EXISTS_TWO as [a [b [NEQ [A_IN B_IN]]]]; [by done | by apply filter_uniq | ].
+    have uniq_tasks : uniq (task_arrivals_at_job_arrival arr_seq j).
+    { exact/filter_uniq/arrival_sequence_uniq. }
+    have [a [b [NEQ [A_IN B_IN]]]] := EXISTS_TWO SIZE_G uniq_tasks.
     rewrite mem_filter in A_IN; rewrite mem_filter in B_IN.
     move: A_IN B_IN => /andP [/eqP TSKA ARRA] /andP [/eqP TSKB ARRB].
-    move: (ARRA); move: (ARRB); rewrite /arrivals_at => A_IN B_IN.
+    move: (ARRA) (ARRB) => A_IN B_IN.
     apply in_arrseq_implies_arrives in A_IN; apply in_arrseq_implies_arrives in B_IN.
     have EQ_ARR_A : (job_arrival a = job_arrival j) by apply H_consistent_arrivals.
     have EQ_ARR_B : (job_arrival b = job_arrival j) by apply H_consistent_arrivals.
diff --git a/analysis/facts/transform/wc_correctness.v b/analysis/facts/transform/wc_correctness.v
index 2042cb138ca649a6fe44b44a5ea258440859b31c..5de4762c9b7bc316f1733171811cbcb46fdb1493 100644
--- a/analysis/facts/transform/wc_correctness.v
+++ b/analysis/facts/transform/wc_correctness.v
@@ -208,9 +208,7 @@ Section AuxiliaryLemmasWorkConservingTransformation.
       move=> j t' ARR_IN ARR.
       rewrite /max_deadline_for_jobs_arrived_before.
       apply in_max0_le; apply map_f.
-      rewrite /arrivals_up_to.
-      apply arrived_between_implies_in_arrivals;
-        by move:H_arr_seq_valid => [CONS UNIQ].
+      exact: arrived_between_implies_in_arrivals.
     Qed.
 
     (** Next, we want to show that, if a job arriving from the arrival
diff --git a/behavior/arrival_sequence.v b/behavior/arrival_sequence.v
index 4e9fde5ada178e8ea2b4dc8fbcc7c5ef17dc80b0..33667ed5879530d81f3613e45fb61aabca151e13 100644
--- a/behavior/arrival_sequence.v
+++ b/behavior/arrival_sequence.v
@@ -2,6 +2,10 @@ From mathcomp Require Export ssreflect seq ssrnat ssrbool bigop eqtype ssrfun.
 Require Export prosa.behavior.job.
 Require Export prosa.util.notation.
 
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
 (** This module contains basic definitions and properties of job arrival
     sequences. *)
 
@@ -14,33 +18,25 @@ Section ArrivalSequence.
   Variable Job: JobType.
 
   (** ..., an arrival sequence is a mapping from any time to a (finite) sequence of jobs. *)
-  Definition arrival_sequence := instant -> seq Job.
+  Record arrival_sequence := Arrival_sequence {
+    arrival_sequence_seq :> instant -> seq Job;
+    (** sequences don't contain duplicates. *)
+    arrival_sequence_uniq : forall t, uniq (arrival_sequence_seq t)
+  }.
 
 End ArrivalSequence.
 
 (** * Arrival of a Job *)
 
-(** Next, we define properties of jobs in a given arrival sequence. *)
-Section JobProperties.
-
-  (** Consider any job arrival sequence. *)
-  Context {Job: JobType}.
-  Variable arr_seq: arrival_sequence Job.
-
-  (** First, we define the sequence of jobs arriving at time t. *)
-  Definition arrivals_at (t : instant) := arr_seq t.
-
-  (** Next, we say that job j arrives at a given time t iff it belongs to the
-       corresponding sequence. *)
-  Definition arrives_at (j : Job) (t : instant) := j \in arrivals_at t.
+Notation arrives_at arr_seq j t := (j \in arrival_sequence_seq arr_seq t).
 
-  (** Similarly, we define whether job j arrives at some (unknown) time t, i.e.,
-       whether it belongs to the arrival sequence. *)
-  Definition arrives_in (j : Job) := exists t, j \in arrivals_at t.
+(** We denote [arrive_in arr_seq j] the fact that job j arrives at
+    some (unknown) time t, i.e., whether it belongs to the arrival
+    sequence. *)
+Notation arrives_in arr_seq j :=
+  (exists t, j \in arrival_sequence_seq arr_seq t).
 
-End JobProperties.
-
-(** * Validity of an Arrival Sequence *)
+(** * Validity of an Arrival Sequence w.r.t. some JobArrival *)
 
 (** Next, we define valid arrival sequences. *)
 Section ValidArrivalSequence.
@@ -48,27 +44,22 @@ Section ValidArrivalSequence.
   (** Assume that job arrival times are known. *)
   Context {Job: JobType}.
   Context `{JobArrival Job}.
-  
+
   (** Consider any job arrival sequence. *)
   Variable arr_seq: arrival_sequence Job.
 
   (** We say that arrival times are consistent if any job that arrives in the
-     sequence has the corresponding arrival time. *)
+      sequence has the corresponding arrival time. *)
   Definition consistent_arrival_times :=
     forall j t,
       arrives_at arr_seq j t -> job_arrival j = t.
 
-  (** We say that the arrival sequence is a set iff it doesn't contain duplicate
-     jobs at any given time. *)
-  Definition arrival_sequence_uniq := forall t, uniq (arrivals_at arr_seq t).
-
-  (** We say that the arrival sequence is valid iff it is a set and arrival times
-     are consistent *)
-  Definition valid_arrival_sequence :=
-    consistent_arrival_times /\ arrival_sequence_uniq.
-
 End ValidArrivalSequence.
 
+(** We say that the arrival sequence is valid iff arrival times
+    are consistent *)
+Notation valid_arrival_sequence := consistent_arrival_times.
+
 (** * Arrival Time Predicates *)
 
 (** Next, we define properties of job arrival times. *)
@@ -111,7 +102,7 @@ Section ArrivalSequencePrefix.
   (** By concatenation, we construct the list of jobs that arrived in the
      interval <<[t1, t2)>>. *)
   Definition arrivals_between (t1 t2 : instant) :=
-    \cat_(t1 <= t < t2) arrivals_at arr_seq t.
+    \cat_(t1 <= t < t2) arr_seq t.
 
   (** Based on that, we define the list of jobs that arrived up to time t, ...*)
   Definition arrivals_up_to (t : instant) := arrivals_between 0 t.+1.
@@ -119,9 +110,9 @@ Section ArrivalSequencePrefix.
   (** ... the list of jobs that arrived strictly before time t, ... *)
   Definition arrivals_before (t : instant) := arrivals_between 0 t.
 
-  (** ... and the list of jobs that arrive in the interval <<[t1, t2)>> and 
+  (** ... and the list of jobs that arrive in the interval <<[t1, t2)>> and
    satisfy a certain predicate [P]. *)
   Definition arrivals_between_P (P : Job -> bool) (t1 t2 : instant) :=
-    [seq j <- arrivals_between t1 t2 | P j].  
-  
+    [seq j <- arrivals_between t1 t2 | P j].
+
 End ArrivalSequencePrefix.
diff --git a/behavior/service.v b/behavior/service.v
index b4ff0fa7e745df08ed404dd3d26f19c2f6682005..5273809ac281776747f503de641d6fd759788e04 100644
--- a/behavior/service.v
+++ b/behavior/service.v
@@ -60,7 +60,8 @@ Section Service.
   (** * Pending or Incomplete Jobs *)
 
   (** Job [j] is pending at time [t] iff it has arrived but has not yet completed. *)
-  Definition pending (j : Job) (t : instant) := has_arrived j t && ~~ completed_by j t.
+  Definition pending (j : Job) (t : instant) :=
+    has_arrived j t && ~~ completed_by j t.
 
   (** Job [j] is pending earlier and at time [t] iff it has arrived before time [t]
       and has not been completed yet. *)
diff --git a/model/task/arrivals.v b/model/task/arrivals.v
index 8c10fd472c2d552332cb1a96bf530abc51034328..d8e64709b0417e2cadb660b6c38c23957620cbc0 100644
--- a/model/task/arrivals.v
+++ b/model/task/arrivals.v
@@ -35,7 +35,7 @@ Section TaskArrivals.
 
   (** ... the list of jobs of task [tsk] that arrive exactly at an instant [t], ... *)
   Definition task_arrivals_at (tsk : Task) (t : instant) :=
-    [seq j <- arrivals_at arr_seq t | job_task j == tsk].
+    [seq j <- arr_seq t | job_task j == tsk].
   
   (** ... and finally count the number of job arrivals. *)
   Definition number_of_task_arrivals (t1 t2 : instant) :=
diff --git a/results/edf/rta/bounded_nps.v b/results/edf/rta/bounded_nps.v
index f58e54c46be849f2dfea96b39e8f79a22679a5f8..97e98f8609649a04c3f303b944ad22eaa2f74634 100644
--- a/results/edf/rta/bounded_nps.v
+++ b/results/edf/rta/bounded_nps.v
@@ -52,8 +52,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
   (** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-  Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
-  
+
   (** Next, consider any valid ideal uni-processor schedule of this arrival sequence ... *)
   Variable sched : schedule (ideal.processor_state Job).
   Hypothesis H_sched_valid : valid_schedule sched arr_seq.
diff --git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index bf82c7bf621befe8f445e1507670d27913ca0419..466977ce536abbcc816d39e251e0e23bc9724ea3 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -61,7 +61,6 @@ Section AbstractRTAforEDFwithArrivalCurves.
   (** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-  Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
 
   (** Next, consider any valid ideal uni-processor schedule of this arrival sequence ... *)
   Variable sched : schedule (ideal.processor_state Job).
diff --git a/results/edf/rta/floating_nonpreemptive.v b/results/edf/rta/floating_nonpreemptive.v
index c6f3cde84b486a84680d69a3ecd76500e5788591..99291185534abbfc331763afa5df252c319bc6ec 100644
--- a/results/edf/rta/floating_nonpreemptive.v
+++ b/results/edf/rta/floating_nonpreemptive.v
@@ -35,7 +35,6 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
   (** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-  Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
 
   (** Assume we have the model with floating non-preemptive regions.
       I.e., for each task only the length of the maximal non-preemptive
diff --git a/results/edf/rta/fully_nonpreemptive.v b/results/edf/rta/fully_nonpreemptive.v
index 4034a3e6e1c68e34331b9afaceb532694811a0e9..5cf6d2414a3516fadd85ef41b93d6c6c0d1a9bc9 100644
--- a/results/edf/rta/fully_nonpreemptive.v
+++ b/results/edf/rta/fully_nonpreemptive.v
@@ -36,7 +36,6 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
   (** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-  Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
 
   (** Consider an arbitrary task set ts, ... *)
   Variable ts : list Task.
diff --git a/results/edf/rta/fully_preemptive.v b/results/edf/rta/fully_preemptive.v
index 5ca06a9c032eece661467b2e9934df0b2fdab92b..3b01b653d9981f4305f65e49efabab4795c07734 100644
--- a/results/edf/rta/fully_preemptive.v
+++ b/results/edf/rta/fully_preemptive.v
@@ -35,7 +35,6 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
   (** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-  Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
 
   (** Consider an arbitrary task set ts, ... *)
   Variable ts : list Task.
@@ -139,4 +138,3 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
   Qed.
     
 End RTAforFullyPreemptiveEDFModelwithArrivalCurves.
-
diff --git a/results/edf/rta/limited_preemptive.v b/results/edf/rta/limited_preemptive.v
index cbfced66a1da95def3810fe172b6b9809cecd964..63e6db920b0c250d6c647bd6cb28a10c29ac21c8 100644
--- a/results/edf/rta/limited_preemptive.v
+++ b/results/edf/rta/limited_preemptive.v
@@ -37,7 +37,6 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
   (** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-  Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
 
   (** Consider an arbitrary task set ts, ... *)
   Variable ts : list Task.
diff --git a/results/fifo/rta.v b/results/fifo/rta.v
index 1a2f653be75c669644226b60b2b68d8ee4260813..0830ce3fa62565cf49998cbf654a2e1764ac4b6d 100644
--- a/results/fifo/rta.v
+++ b/results/fifo/rta.v
@@ -44,7 +44,6 @@ Section AbstractRTAforFIFOwithArrivalCurves.
   (** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-  Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
 
   (** Next, consider any valid ideal uni-processor schedule of this arrival sequence. *)
   Variable sched : schedule (ideal.processor_state Job).
@@ -286,7 +285,7 @@ Section AbstractRTAforFIFOwithArrivalCurves.
       rewrite (instantiated_cumulative_interference_of_hep_jobs_equal_total_interference_of_hep_jobs arr_seq) //=; 
               try by (try rewrite instantiated_quiet_time_equivalent_quiet_time); eauto 2 with basic_facts.
       eapply leq_trans; first by apply service_of_jobs_le_workload; eauto 2 with basic_facts.
-      rewrite (leqRW (workload_equal_subset _ _ _ _ _ _  _)); eauto 2 with basic_facts.
+      rewrite (leqRW (workload_equal_subset _ _ _ _ _  _)); eauto 2 with basic_facts.
       specialize (workload_minus_job_cost j) => ->.
       { rewrite /workload_of_jobs /IBF (big_rem tsk) //= (addnC (rbf tsk (job_arrival j - t1 + ε))).
         rewrite -addnBA; last first.
@@ -421,7 +420,4 @@ Section AbstractRTAforFIFOwithArrivalCurves.
       by eapply H_valid_job_cost.
   Qed.
   
-End AbstractRTAforFIFOwithArrivalCurves. 
-
-
-
+End AbstractRTAforFIFOwithArrivalCurves.
diff --git a/results/fixed_priority/rta/bounded_nps.v b/results/fixed_priority/rta/bounded_nps.v
index 92b197be70d863476fe08c96a90ea048b29d4526..aaebf83ce49a0db6bf5a3594b117934ee0e72cff 100644
--- a/results/fixed_priority/rta/bounded_nps.v
+++ b/results/fixed_priority/rta/bounded_nps.v
@@ -43,7 +43,6 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
   (** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-  Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
 
   (** Next, consider any ideal uni-processor schedule of this arrival sequence, ... *)
   Variable sched : schedule (ideal.processor_state Job).
diff --git a/results/fixed_priority/rta/bounded_pi.v b/results/fixed_priority/rta/bounded_pi.v
index e9182e7f9ad257e066ff3a07c3918ef093688178..d47c811c6346598d4a2e637373f51cd2f0397cb2 100644
--- a/results/fixed_priority/rta/bounded_pi.v
+++ b/results/fixed_priority/rta/bounded_pi.v
@@ -48,7 +48,6 @@ Section AbstractRTAforFPwithArrivalCurves.
   (** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-  Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
 
   (** Next, consider any ideal uni-processor schedule of this arrival sequence, ... *)
   Variable sched : schedule (ideal.processor_state Job).
diff --git a/results/fixed_priority/rta/floating_nonpreemptive.v b/results/fixed_priority/rta/floating_nonpreemptive.v
index f7d9c99f0d10a163447b9e4856f5e998ab849ba2..0ac4259f4f3f2f16192b4c956202897cb36e74f9 100644
--- a/results/fixed_priority/rta/floating_nonpreemptive.v
+++ b/results/fixed_priority/rta/floating_nonpreemptive.v
@@ -34,7 +34,6 @@ Section RTAforFloatingModelwithArrivalCurves.
   (** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-  Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
 
   (** Assume we have the model with floating non-preemptive regions. 
       I.e., for each task only the length of the maximal non-preemptive 
diff --git a/results/fixed_priority/rta/fully_nonpreemptive.v b/results/fixed_priority/rta/fully_nonpreemptive.v
index 5de85eaf48524cd10d95a89aebe406274309a6e4..bff07f037cc46e82dc35847010be23097f3415ff 100644
--- a/results/fixed_priority/rta/fully_nonpreemptive.v
+++ b/results/fixed_priority/rta/fully_nonpreemptive.v
@@ -34,7 +34,6 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
   (** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-  Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
 
   (** Consider an arbitrary task set ts, ... *)
   Variable ts : list Task.
diff --git a/results/fixed_priority/rta/fully_preemptive.v b/results/fixed_priority/rta/fully_preemptive.v
index 7e2b4800aacc8a90ecdb2f5e203c93c665ba1321..c7ce53599d9467b7ad76e0840957c3989cdb07f5 100644
--- a/results/fixed_priority/rta/fully_preemptive.v
+++ b/results/fixed_priority/rta/fully_preemptive.v
@@ -34,7 +34,6 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
   (** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-  Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
 
   (** Consider an arbitrary task set ts, ... *)
   Variable ts : list Task.
diff --git a/results/fixed_priority/rta/limited_preemptive.v b/results/fixed_priority/rta/limited_preemptive.v
index 14de81fb1117f3196536fdc9df42dca0ae68249f..fdcd208ac3d9354c5997c555ace4dd4ca505fa64 100644
--- a/results/fixed_priority/rta/limited_preemptive.v
+++ b/results/fixed_priority/rta/limited_preemptive.v
@@ -35,7 +35,6 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
   (** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-  Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
 
   (** Consider an arbitrary task set ts, ... *)
   Variable ts : list Task.