diff --git a/implementation/facts/maximal_arrival_sequence.v b/implementation/facts/maximal_arrival_sequence.v
index ba77aee36f8ad75fef58580dd242205acba0468a..efba3fcba3a87166f807cd6a8198494cfde1cd97 100644
--- a/implementation/facts/maximal_arrival_sequence.v
+++ b/implementation/facts/maximal_arrival_sequence.v
@@ -253,31 +253,6 @@ Section MaximalArrivalSequence.
         apply map_f.
         by rewrite mem_iota; lia. }
     Qed.
-
-    (** Lastly, we prove that the concrete arrival sequence respects the arrival curve
-        at each time instant [t].  *) 
-    Lemma concrete_respects_at :
-      forall t,
-        respects_max_arrivals_at (concrete_arrival_sequence generate_jobs_at ts) tsk
-                                 (max_arrivals tsk) t.
-    Proof.
-      induction t; move => Δ LEQ.
-      { rewrite sub0n.
-        rewrite number_of_task_arrivals_eq //.
-        by vm_compute; rewrite unlock. }
-      { rewrite /respects_max_arrivals_at in IHt.
-        rewrite number_of_task_arrivals_eq //.
-        destruct Δ; first by rewrite /index_iota subnn; vm_compute; rewrite unlock.
-        rewrite subSS.
-        specialize (IHt Δ).
-        feed IHt; first by lia.
-        rewrite number_of_task_arrivals_eq // in IHt.
-        rewrite big_nat_recr //=; last by lia.
-        rewrite -leq_subRL; first apply n_arrivals_at_leq; try lia.
-        move: (H_valid_arrival_curve tsk H_tsk_in_ts) => [ZERO MONO].
-        apply (leq_trans IHt).
-        by apply MONO. }
-    Qed.
     
   End Facts.
   
@@ -286,9 +261,26 @@ Section MaximalArrivalSequence.
   Lemma concrete_is_arrival_curve :
     taskset_respects_max_arrivals (concrete_arrival_sequence generate_jobs_at ts) ts.
   Proof.
-    move=> tsk IN.
-    apply respects_max_arrivals_at_respects_max_arrivals_eq.
-    by apply concrete_respects_at.
-  Qed. 
+    move=> tsk IN t1 t LEQ.
+    set Δ := t - t1.
+    replace t1 with (t-Δ); last by lia.
+    have LEQd: Δ <= t by lia.
+    generalize Δ LEQd; clear LEQ Δ LEQd.
+    induction t; move => Δ LEQ.
+    { rewrite sub0n.
+      rewrite number_of_task_arrivals_eq //.
+      by vm_compute; rewrite unlock. }
+    { rewrite number_of_task_arrivals_eq //.
+      destruct Δ; first by rewrite /index_iota subnn; vm_compute; rewrite unlock.
+      rewrite subSS.
+      specialize (IHt Δ).
+      feed IHt; first by lia.
+      rewrite number_of_task_arrivals_eq // in IHt.
+      rewrite big_nat_recr //=; last by lia.
+      rewrite -leq_subRL; first apply n_arrivals_at_leq; try lia.
+      move: (H_valid_arrival_curve tsk IN) => [ZERO MONO].
+      apply (leq_trans IHt).
+      by apply MONO. }
+  Qed.    
 
 End MaximalArrivalSequence.
diff --git a/model/task/arrival/curves.v b/model/task/arrival/curves.v
index 6a3c21bd53ef8de8509f2f7808a3ee600f175db8..09ac4b0364c8c643d56055cb7d9a7be07bf40a72 100644
--- a/model/task/arrival/curves.v
+++ b/model/task/arrival/curves.v
@@ -104,46 +104,6 @@ Section ArrivalCurves.
 
   End SeparationBound.
 
-  (** In this section we give an alternative, point-wise notion of respecting an upper 
-      arrival bound, and then show that, if valid for any instant [t], it is equivalent 
-      to the standard definition. This notion is used to prove the correctness of the 
-      maximal arrival sequence implementation. *)
-  Section PointWiseRespectingMaxArrivals.
-
-    (** Consider a task [tsk]... *)
-    Variable (tsk : Task).
-
-    (** ... and an arrival bound function [max_arrivals]. *)
-    Variable (max_arrivals : duration -> nat).
-
-    (** We say that [max_arrivals] is an upper arrival bound for task
-    [tsk] at time [t] iff, for any interval <<[t - Δ, t)>>,
-    [max_arrivals Δ] bounds the number of jobs of [tsk] that
-    arrive in that interval. *)
-    Definition respects_max_arrivals_at (t : instant) :=
-      forall Δ,
-        Δ <= t -> 
-        number_of_task_arrivals arr_seq tsk (t-Δ) t <= max_arrivals Δ.
-
-    (** Next, we prove that, if [respects_max_arrivals_at] holds for
-        any time instant [t], then the standard definition holds as well. *)
-    Lemma respects_max_arrivals_at_respects_max_arrivals_eq:
-      (forall t, respects_max_arrivals_at t) <->
-      respects_max_arrivals tsk max_arrivals.
-    Proof.
-      split.
-      { move=> RESP t1 t2 LEQ.
-        move: (RESP t2 (t2-t1)) => Rat.
-        rewrite subKn // in Rat.
-        by apply Rat; lia. }
-      { move=> RESP t Δ LEQ.
-        move: (RESP (t-Δ) t) => Rat.
-        rewrite subKn // in Rat.
-        by apply Rat; lia. }
-    Qed.
-    
-  End PointWiseRespectingMaxArrivals.
-
 End ArrivalCurves.