diff --git a/analysis/abstract/abstract_rta.v b/analysis/abstract/abstract_rta.v
index bfbeb31c08cacf6e8c2f497d786fb441cd9b8127..438b9c0b260531000b481ab36202c82871d9aa6f 100644
--- a/analysis/abstract/abstract_rta.v
+++ b/analysis/abstract/abstract_rta.v
@@ -439,7 +439,7 @@ Section Abstract_RTA.
           specialize (L1 H0).
           feed_n 2 L1; try done.
           { move: (H_busy_interval_exists j H_j_arrives H_job_of_tsk H_job_cost_positive)
-            => [t1' [t2' [_ [BOUND BUSY]]]].
+            => [t1' [t2' [BOUND BUSY]]].
             have EQ:= busy_interval_is_unique _ _ _ _ _ _ _ _ H_busy_interval BUSY.
             destruct EQ as [EQ1 EQ2].
             subst t1' t2'; clear BUSY.
@@ -467,7 +467,7 @@ Section Abstract_RTA.
         Lemma relative_arrival_is_bounded: A < L.
         Proof.
           rewrite /A.
-          move: (H_busy_interval_exists j H_j_arrives H_job_of_tsk H_job_cost_positive) => [t1' [t2' [_ [BOUND BUSY]]]].
+          move: (H_busy_interval_exists j H_j_arrives H_job_of_tsk H_job_cost_positive) => [t1' [t2' [BOUND BUSY]]].
           have EQ:= busy_interval_is_unique _ _ _ _ _ _ _ _ H_busy_interval BUSY. destruct EQ as [EQ1 EQ2].
           subst t1' t2'; clear BUSY.
           apply leq_trans with (t2 - t1); last by rewrite leq_subLR.
@@ -535,8 +535,8 @@ Section Abstract_RTA.
     intros j ARR JOBtsk. unfold job_response_time_bound.
     move: (posnP (@job_cost _ H3 j)) => [ZERO|POS].
     { by rewrite /completed_by ZERO. } 
-    move: (H_busy_interval_exists j ARR JOBtsk POS) => [t1 [t2 [NEQ [T2 BUSY]]]].
-    move: (NEQ) (BUSY)=> /andP [GE LT] [_ QTt2].
+    move: (H_busy_interval_exists j ARR JOBtsk POS) => [t1 [t2 [T2 BUSY]]].
+    move: (BUSY) => [[/andP [GE LT] _] QTt2].
     have A2LTL := relative_arrival_is_bounded _ ARR JOBtsk POS _ _ BUSY.
     set (A2 := job_arrival j - t1) in *.
     move: (representative_exists tsk _ interference_bound_function _ A2LTL) => [A1 [ALEA2 [EQΦ INSP]]].
diff --git a/analysis/abstract/definitions.v b/analysis/abstract/definitions.v
index 0755c902905791571644c71802f2fd6d69dd77a9..1b579b9d63680e6aebeb94523f3209827d1c554f 100644
--- a/analysis/abstract/definitions.v
+++ b/analysis/abstract/definitions.v
@@ -175,7 +175,6 @@ Section AbstractRTADefinitions.
           job_of_task tsk j ->
           job_cost j > 0 ->
           exists t1 t2,
-            t1 <= job_arrival j < t2 /\
             t2 <= t1 + L /\
             busy_interval j t1 t2.
 
diff --git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index 9a1fb488daffa38906c546a557a828edb2e8618f..1554639b79aaa4ac39c9b8e85f01edad4ba402b3 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -292,7 +292,6 @@ Section AbstractRTAforEDFwithArrivalCurves.
         with (Δ := L) as [t1 [t2 [T1 [T2 GGG]]]]; rt_eauto.
       { by intros; rewrite {2}H_fixed_point; apply total_workload_le_total_rbf. }
       exists t1, t2; split; first by done.
-      split; first by done.
       by eapply instantiated_busy_interval_equivalent_busy_interval; rt_eauto.
     Qed.
     
diff --git a/results/fifo/rta.v b/results/fifo/rta.v
index 2b8b0f5ebbedb9b38b40f50673aa067e2090c76e..416afe07cf2736014a72ac197c9f0020817a157b 100644
--- a/results/fifo/rta.v
+++ b/results/fifo/rta.v
@@ -199,7 +199,6 @@ Section AbstractRTAforFIFOwithArrivalCurves.
         with (Δ := L) as [t1 [t2 [T1 [T2 GGG]]]]; rt_eauto.
       { by intros; rewrite {2}H_fixed_point; apply total_workload_le_total_rbf. }
       { exists t1, t2; split; first by done.
-        split; first by done.
         by eapply instantiated_busy_interval_equivalent_busy_interval; rt_eauto. }
     Qed.
 
diff --git a/results/fixed_priority/rta/bounded_pi.v b/results/fixed_priority/rta/bounded_pi.v
index ac0830a0ff44cf58ae5b2561fde99b940a00e326..2efb27187546ecd0d2c26921d87adc06f979bfe6 100644
--- a/results/fixed_priority/rta/bounded_pi.v
+++ b/results/fixed_priority/rta/bounded_pi.v
@@ -242,7 +242,6 @@ Section AbstractRTAforFPwithArrivalCurves.
         rt_eauto.
       { by intros; rewrite {2}H_fixed_point leq_add //; apply total_workload_le_total_hep_rbf. }
       exists t1, t2; split; first by done.
-      split; first by done.
       by eapply instantiated_busy_interval_equivalent_busy_interval; rt_eauto.
     Qed.