diff --git a/restructuring/analysis/basic_facts/arrivals.v b/restructuring/analysis/basic_facts/arrivals.v
index 3b0c19700c3f8037bb53fc2cdd94866b3d25f9c0..c225c2660d9afe347cc5c017915bc4cb79920f2c 100644
--- a/restructuring/analysis/basic_facts/arrivals.v
+++ b/restructuring/analysis/basic_facts/arrivals.v
@@ -14,14 +14,28 @@ Section Arrived.
      readiness. *)
   Context `{JobCost Job}.
   Context `{JobArrival Job}.
-  Context `{JobReady Job PState}.
+  (* We give the readiness typeclass instance a name here because we rely on it
+     explicitly in proofs. *)
+  Context {ReadyParam : JobReady Job PState}.
+
+  (** First, we note that readiness models are by definition consistent
+      w.r.t. [pending]. *)
+  Lemma any_ready_job_is_pending:
+    forall j t,
+      job_ready sched j t -> pending sched j t.
+  Proof.
+    move: ReadyParam => [is_ready CONSISTENT].
+    move=> j t READY.
+    apply CONSISTENT.
+    by exact READY.
+  Qed.
 
-  (** We observe that a given job must have arrived to be ready... *)
+  (** Next, we observe that a given job must have arrived to be ready... *)
   Lemma ready_implies_arrived:
     forall j t, job_ready sched j t -> has_arrived j t.
   Proof.
     move=> j t READY.
-    move: (any_ready_job_is_pending sched j t READY).
+    move: (any_ready_job_is_pending j t READY).
     by rewrite /pending => /andP [ARR _].
   Qed.
 
diff --git a/restructuring/analysis/basic_facts/completion.v b/restructuring/analysis/basic_facts/completion.v
index bb9ed0f1f2eead62c4eeb6c0c955d91ede6c2a18..7a5eab4e7de8da9974779176b76b42b84fcf7ad9 100644
--- a/restructuring/analysis/basic_facts/completion.v
+++ b/restructuring/analysis/basic_facts/completion.v
@@ -1,5 +1,5 @@
 From rt.restructuring.behavior Require Export all.
-From rt.restructuring.analysis.basic_facts Require Export service.
+From rt.restructuring.analysis.basic_facts Require Export service arrivals.
 
 From rt.util Require Import nat.
 
diff --git a/restructuring/behavior/ready.v b/restructuring/behavior/ready.v
index ea7133f2a9881830d5e9393785296eae613e052c..a2a5d2ee337b836e87c494b481a206994fd91766 100644
--- a/restructuring/behavior/ready.v
+++ b/restructuring/behavior/ready.v
@@ -3,15 +3,20 @@ From rt.restructuring.behavior Require Export service.
 
 
 (** We define a general notion of readiness of a job: a job can be
-   scheduled only when it is ready. This notion of readiness is a general
-   concept that is used to model jitter, self-suspensions, etc.  Crucially, we
-   require that any sensible notion of readiness is a refinement of the notion
+   scheduled only when it is ready, as determined by the predicate
+   [job_ready]. This notion of readiness is a general concept that is
+   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} :=
   {
     job_ready : schedule PState -> Job -> instant -> bool;
-    any_ready_job_is_pending : forall sched j t, job_ready sched j t -> pending sched j t;
+
+    (** What follows is the consistency requirement: We require any
+        reasonable readiness model to consider only pending jobs to be
+        ready. *)
+    _ : forall sched j t, job_ready sched j t -> pending sched j t;
   }.
 
 (** Based on the general notion of readiness, we define what it means to be